[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n
[PROOFSTEP]
simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
cases fintypeOrInfinite α
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Fintype α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
simpa only [card_eq_fintype_card] using Fintype.equivFin α
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Infinite α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
simp only [card_eq_zero_of_infinite, ne_eq] at h
[GOAL]
α : Type u_1
β : Type u_2
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1
[PROOFSTEP]
letI := Fintype.ofSubsingleton a
[GOAL]
α : Type u_1
β : Type u_2
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1
[PROOFSTEP]
rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : IsEmpty α
⊢ Nat.card α = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
have := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
have := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
⊢ Nat.card (α × β) = Nat.card α * Nat.card β
[PROOFSTEP]
simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]
[GOAL]
α : Type u_1
β✝ : Type u_2
β : α → Type u_3
inst✝ : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)
[PROOFSTEP]
simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, toNat_finset_prod]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
[PROOFSTEP]
rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
⊢ Nat.card (ZMod n) = n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
⊢ Nat.card (ZMod zero) = zero
[PROOFSTEP]
exact @Nat.card_eq_zero_of_infinite _ Int.infinite
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ : ℕ
⊢ Nat.card (ZMod (succ n✝)) = succ n✝
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, ZMod.card]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
⊢ card (α ⊕ β) = card α + card β
[PROOFSTEP]
simp only [PartENat.card, Cardinal.mk_sum, map_add, Cardinal.toPartENat_lift]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ ↑toPartENat c ↔ ↑n ≤ c
[PROOFSTEP]
rw [← toPartENat_cast n, toPartENat_le_iff_of_le_aleph0 (le_of_lt (nat_lt_aleph0 n))]
[GOAL]
α : Type u_1
β : Type u_2
c : Cardinal.{u_3}
n : ℕ
⊢ ↑toPartENat c ≤ ↑n ↔ c ≤ ↑n
[PROOFSTEP]
rw [← toPartENat_cast n, toPartENat_le_iff_of_lt_aleph0 (nat_lt_aleph0 n)]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n = ↑toPartENat c ↔ ↑n = c
[PROOFSTEP]
rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toPartENat_le_natCast_iff, Cardinal.natCast_le_toPartENat_iff]
[GOAL]
α : Type u_1
β : Type u_2
c : Cardinal.{u_3}
n : ℕ
⊢ ↑toPartENat c = ↑n ↔ c = ↑n
[PROOFSTEP]
rw [eq_comm, Cardinal.natCast_eq_toPartENat_iff, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n < ↑toPartENat c ↔ ↑n < c
[PROOFSTEP]
simp only [← not_le, Cardinal.toPartENat_le_natCast_iff]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑toPartENat c < ↑n ↔ c < ↑n
[PROOFSTEP]
simp only [← not_le, Cardinal.natCast_le_toPartENat_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ IsEmpty α
[PROOFSTEP]
rw [← Cardinal.mk_eq_zero_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ #α = 0
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α = 0
[PROOFSTEP]
rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α = 0
[PROOFSTEP]
rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α = 0
[PROOFSTEP]
rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ #α = ↑0
[PROOFSTEP]
simp only [← Cardinal.toPartENat_eq_natCast_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ ↑toPartENat #α = ↑0
[PROOFSTEP]
simp only [PartENat.card, Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ Subsingleton α
[PROOFSTEP]
rw [← le_one_iff_subsingleton]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α ≤ 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α ≤ 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α ≤ 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ ↑1
[PROOFSTEP]
rw [← Cardinal.toPartENat_le_natCast_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ ↑toPartENat #α ≤ ↑1
[PROOFSTEP]
simp only [PartENat.card, Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ Nontrivial α
[PROOFSTEP]
rw [← Cardinal.one_lt_iff_nontrivial]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ 1 < #α
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| 1 < #α
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| 1 < #α
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| 1 < #α
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α
[PROOFSTEP]
rw [← natCast_lt_toPartENat_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ ↑1 < ↑toPartENat #α
[PROOFSTEP]
simp only [PartENat.card, Nat.cast_one]


[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∃ h, Bijective h
[PROOFSTEP]
cases' isEmpty_or_nonempty β with hβ hβ
[GOAL]
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
⊢ ∃ h, Bijective h
[PROOFSTEP]
have : IsEmpty α := Function.isEmpty f
[GOAL]
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
this : IsEmpty α
⊢ ∃ h, Bijective h
[PROOFSTEP]
exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective⟩
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
⊢ ∃ h, Bijective h
[PROOFSTEP]
set F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
    monotone' := fun s t hst =>
      compl_subset_compl.mpr <| image_subset _ <| compl_subset_compl.mpr <| image_subset _ hst }
    -- Porting note: dot notation `F.lfp` doesn't work here
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
⊢ ∃ h, Bijective h
[PROOFSTEP]
set s : Set α := OrderHom.lfp F
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
⊢ ∃ h, Bijective h
[PROOFSTEP]
have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ ∃ h, Bijective h
[PROOFSTEP]
have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ (g '' (f '' s)ᶜ)ᶜ = sᶜᶜ
[PROOFSTEP]
simp [hs]
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
⊢ ∃ h, Bijective h
[PROOFSTEP]
set g' := invFun g
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
⊢ ∃ h, Bijective h
[PROOFSTEP]
have g'g : LeftInverse g' g := leftInverse_invFun hg
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ ∃ h, Bijective h
[PROOFSTEP]
have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ g' '' sᶜ = (f '' s)ᶜ
[PROOFSTEP]
rw [← hns, g'g.image_image]
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
⊢ ∃ h, Bijective h
[PROOFSTEP]
set h : α → β := s.piecewise f g'
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
⊢ ∃ h, Bijective h
[PROOFSTEP]
have : Surjective h := by rw [← range_iff_surjective, range_piecewise, hg'ns, union_compl_self]
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
⊢ Surjective h
[PROOFSTEP]
rw [← range_iff_surjective, range_piecewise, hg'ns, union_compl_self]
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
⊢ ∃ h, Bijective h
[PROOFSTEP]
have : Injective h := by
  refine' (injective_piecewise_iff _).2 ⟨hf.injOn _, _, _⟩
  · intro x hx y hy hxy
    obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
    obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
    rw [g'g _, g'g _] at hxy
    rw [hxy]
  · intro x hx y hy hxy
    obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
    rw [g'g _] at hxy
    exact hy' ⟨x, hx, hxy⟩
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
⊢ Injective h
[PROOFSTEP]
refine' (injective_piecewise_iff _).2 ⟨hf.injOn _, _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
⊢ InjOn g' sᶜ
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case refine'_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x = y
[PROOFSTEP]
obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ g '' (f '' s)ᶜ
[PROOFSTEP]
rwa [hns]
[GOAL]
case refine'_1.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ g x' = y
[PROOFSTEP]
obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ y ∈ g '' (f '' s)ᶜ
[PROOFSTEP]
rwa [hns]
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : g' (g x') = g' (g y')
⊢ g x' = g y'
[PROOFSTEP]
rw [g'g _, g'g _] at hxy
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'
[PROOFSTEP]
rw [hxy]
[GOAL]
case refine'_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g' y
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case refine'_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : ¬y ∈ s
hxy : f x = g' y
⊢ False
[PROOFSTEP]
obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : ¬y ∈ s
hxy : f x = g' y
⊢ y ∈ g '' (f '' s)ᶜ
[PROOFSTEP]
rwa [hns]
[GOAL]
case refine'_2.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y' : β
hy' : y' ∈ (f '' s)ᶜ
hy : ¬g y' ∈ s
hxy : f x = g' (g y')
⊢ False
[PROOFSTEP]
rw [g'g _] at hxy
[GOAL]
case refine'_2.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y' : β
hy' : y' ∈ (f '' s)ᶜ
hy : ¬g y' ∈ s
hxy : f x = y'
⊢ False
[PROOFSTEP]
exact hy' ⟨x, hx, hxy⟩
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ,
    monotone' := (_ : ∀ (s t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := piecewise s f g'
this✝ : Surjective h
this : Injective h
⊢ ∃ h, Bijective h
[PROOFSTEP]
exact ⟨h, ‹Injective h›, ‹Surjective h›⟩
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
⊢ ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
[PROOFSTEP]
simpa only [ne_eq, not_exists, not_forall, not_and] using h
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
cases' hy with hy hy
[GOAL]
case inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
cases' hy with hy hy
[GOAL]
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
subst x
[GOAL]
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
y : (i : ι) → β i
hy : y ∈ s
⊢ ∀ (i : ι), f i = y i → f = y
[PROOFSTEP]
exact fun i e => (hf i y hy e.symm).elim
[GOAL]
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
subst y
[GOAL]
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ s
⊢ ∀ (i : ι), x i = f i → x = f
[PROOFSTEP]
exact fun i e => (hf i x hx e).elim
[GOAL]
case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
exact hs x hx y hy
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
⊢ a = b
[PROOFSTEP]
let ⟨sa, ea⟩ := hf a
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
⊢ a = b
[PROOFSTEP]
let ⟨sb, eb⟩ := hf b
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
sb : f b ∈ s
eb : f b i = b
⊢ a = b
[PROOFSTEP]
rw [← ea, ← eb, hs _ sa _ sb _ e']


[GOAL]
x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∩ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∩ y
[PROOFSTEP]
rw [mem_inter] at hz ⊢
[GOAL]
x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∧ z ∈ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y
[PROOFSTEP]
exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩
[GOAL]
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
[GOAL]
case intro.intro
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
w : ZFSet
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)
[GOAL]
x y✝ z✝ : ZFSet
H : ∀ (y : ZFSet), y ∈ x → IsTransitive y
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
[GOAL]
case intro.intro
x y✝ z✝ : ZFSet
H : ∀ (y : ZFSet), y ∈ x → IsTransitive y
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
w : ZFSet
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (x ∪ y)
[PROOFSTEP]
rw [← sUnion_pair]
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (⋃₀ {x, y})
[PROOFSTEP]
apply IsTransitive.sUnion' fun z => _
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ ∀ (z : ZFSet), z ∈ {x, y} → IsTransitive z
[PROOFSTEP]
intro
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ ∈ {x, y} → IsTransitive z✝
[PROOFSTEP]
rw [mem_pair]
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ = x ∨ z✝ = y → IsTransitive z✝
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
y z : ZFSet
hy : IsTransitive y
z✝ : ZFSet
hx : IsTransitive z✝
⊢ IsTransitive z✝
case inr x z : ZFSet hx : IsTransitive x z✝ : ZFSet hy : IsTransitive z✝ ⊢ IsTransitive z✝
[PROOFSTEP]
assumption'
[GOAL]
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ powerset x
z : ZFSet
hz : z ∈ y
⊢ z ∈ powerset x
[PROOFSTEP]
rw [mem_powerset] at hy ⊢
[GOAL]
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ⊆ x
z : ZFSet
hz : z ∈ y
⊢ z ⊆ x
[PROOFSTEP]
exact h.subset_of_mem (hy hz)
[GOAL]
x y✝ z : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
⊢ y ∈ x
[PROOFSTEP]
rcases mem_sUnion.1 hy with ⟨z, hz, hz'⟩
[GOAL]
case intro.intro
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x
[PROOFSTEP]
exact h.mem_trans hz' hz


[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a
[PROOFSTEP]
rcases lt_or_le a ℵ₀ with ha | ha
[GOAL]
case inl
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : a < ℵ₀
⊢ #↑t ≤ a
[PROOFSTEP]
obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
[GOAL]
case inl.intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
⊢ #↑t ≤ ↑n
[PROOFSTEP]
apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
⊢ Finset.card s ≤ n
[PROOFSTEP]
have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
⊢ Finset.card s ≤ n
[PROOFSTEP]
have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
⊢ Finset.card s ≤ n
[PROOFSTEP]
rcases B.exists with ⟨i, hi⟩
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
⊢ Finset.card s ≤ n
[PROOFSTEP]
have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
⊢ Finset.card s ≤ n
[PROOFSTEP]
let u : Finset α := (f i).toFinset
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
⊢ Finset.card s ≤ n
[PROOFSTEP]
have I1 : s.card ≤ u.card :=
  by
  have : s ⊆ u := fun x hx ↦ by simpa only [Set.mem_toFinset] using hi x hx
  exact Finset.card_le_of_subset this
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
⊢ Finset.card s ≤ Finset.card u
[PROOFSTEP]
have : s ⊆ u := fun x hx ↦ by simpa only [Set.mem_toFinset] using hi x hx
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
x : α
hx : x ∈ s
⊢ x ∈ u
[PROOFSTEP]
simpa only [Set.mem_toFinset] using hi x hx
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this✝ : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
this : s ⊆ u
⊢ Finset.card s ≤ Finset.card u
[PROOFSTEP]
exact Finset.card_le_of_subset this
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
⊢ Finset.card s ≤ n
[PROOFSTEP]
have I2 : (u.card : Cardinal) ≤ n := by convert h'f i; simp only [Set.toFinset_card, mk_fintype]
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
⊢ ↑(Finset.card u) ≤ ↑n
[PROOFSTEP]
convert h'f i
[GOAL]
case h.e'_3
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
⊢ ↑(Finset.card u) = #↑(f i)
[PROOFSTEP]
simp only [Set.toFinset_card, mk_fintype]
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
I2 : ↑(Finset.card u) ≤ ↑n
⊢ Finset.card s ≤ n
[PROOFSTEP]
exact
  I1.trans
    (Nat.cast_le.1 I2)
      -- case `a` infinite:
[GOAL]
case inr
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
⊢ #↑t ≤ a
[PROOFSTEP]
have : t ⊆ ⋃ i, f i := by
  intro x hx
  obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
  exact mem_iUnion_of_mem i hi
[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
⊢ t ⊆ ⋃ (i : ι), f i
[PROOFSTEP]
intro x hx
[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
⊢ x ∈ ⋃ (i : ι), f i
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
[GOAL]
case intro
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ (i : ι), f i
[PROOFSTEP]
exact mem_iUnion_of_mem i hi
[GOAL]
case inr
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ #↑t ≤ a
[PROOFSTEP]
calc
  #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
  _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
  _ ≤ sum (fun _ ↦ a) := (sum_le_sum _ _ h'f)
  _ = #ι * a := by simp
  _ ≤ ℵ₀ * a := (mul_le_mul_right' mk_le_aleph0 a)
  _ = a := aleph0_mul_eq ha
[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ (sum fun x => a) = #ι * a
[PROOFSTEP]
simp
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a
[PROOFSTEP]
let g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (ULift.down ⁻¹' ·) ∘ f ∘ ULift.down
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
⊢ #↑t ≤ a
[PROOFSTEP]
suffices #(ULift.down.{v} ⁻¹' t) ≤ Cardinal.lift.{v, u} a by simpa
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
this : #↑(ULift.down ⁻¹' t) ≤ lift a
⊢ #↑t ≤ a
[PROOFSTEP]
simpa
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
⊢ #↑(ULift.down ⁻¹' t) ≤ lift a
[PROOFSTEP]
let l' : Filter (ULift.{u} ι) := Filter.map ULift.up l
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
⊢ #↑(ULift.down ⁻¹' t) ≤ lift a
[PROOFSTEP]
have : NeBot l' := map_neBot
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
⊢ #↑(ULift.down ⁻¹' t) ≤ lift a
[PROOFSTEP]
apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
[GOAL]
case ht
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
⊢ ∀ (x : ULift α), x ∈ ULift.down ⁻¹' t → ∀ᶠ (i : ULift ι) in l', x ∈ g i
[PROOFSTEP]
intro x hx
[GOAL]
case ht
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
x : ULift α
hx : x ∈ ULift.down ⁻¹' t
⊢ ∀ᶠ (i : ULift ι) in l', x ∈ g i
[PROOFSTEP]
simpa only [Function.comp_apply, mem_preimage, eventually_map] using ht _ hx
[GOAL]
case h'f
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
⊢ ∀ (i : ULift ι), #↑(g i) ≤ lift a
[PROOFSTEP]
intro i
[GOAL]
case h'f
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
i : ULift ι
⊢ #↑(g i) ≤ lift a
[PROOFSTEP]
simpa using h'f i.down
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #α ≤ a
[PROOFSTEP]
rw [← mk_univ]
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑Set.univ ≤ a
[PROOFSTEP]
exact mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α = a
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α ≤ a
[PROOFSTEP]
apply mk_le_of_countable_eventually_mem ht (fun i ↦ (h'f i).le)
[GOAL]
case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ a ≤ #α
[PROOFSTEP]
obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l
[GOAL]
case a.intro
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
i : ι
⊢ a ≤ #α
[PROOFSTEP]
rw [← (h'f i)]
[GOAL]
case a.intro
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
i : ι
⊢ #↑(f i) ≤ #α
[PROOFSTEP]
exact mk_set_le (f i)


[GOAL]
⊢ lift 𝔠 = 𝔠
[PROOFSTEP]
rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]
[GOAL]
c : Cardinal.{u}
⊢ 𝔠 ≤ lift c ↔ 𝔠 ≤ c
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_le]
[GOAL]
c : Cardinal.{u}
⊢ lift c ≤ 𝔠 ↔ c ≤ 𝔠
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_le]
[GOAL]
c : Cardinal.{u}
⊢ 𝔠 < lift c ↔ 𝔠 < c
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_lt]
[GOAL]
c : Cardinal.{u}
⊢ lift c < 𝔠 ↔ c < 𝔠
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_lt]
[GOAL]
⊢ beth 1 = 𝔠
[PROOFSTEP]
simpa using beth_succ 0
[GOAL]
⊢ #(Set ℕ) = 𝔠
[PROOFSTEP]
simp
[GOAL]
⊢ aleph 1 ≤ 𝔠
[PROOFSTEP]
rw [← succ_aleph0]
[GOAL]
⊢ Order.succ ℵ₀ ≤ 𝔠
[PROOFSTEP]
exact Order.succ_le_of_lt aleph0_lt_continuum
[GOAL]
⊢ 𝔠 ^ ℵ₀ = 𝔠
[PROOFSTEP]
rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]


[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
suffices mkAlgHom R L (ιₜ ⁅x, y⁆ + ιₜ y * ιₜ x) = mkAlgHom R L (ιₜ x * ιₜ y) by rw [AlgHom.map_mul] at this ;
  simp [LieRing.of_associative_ring_bracket, ← this]
[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
this : ↑(mkAlgHom R L) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(mkAlgHom R L) (↑ιₜ x * ↑ιₜ y)
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
rw [AlgHom.map_mul] at this
[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
this : ↑(mkAlgHom R L) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(mkAlgHom R L) (↑ιₜ x) * ↑(mkAlgHom R L) (↑ιₜ y)
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
simp [LieRing.of_associative_ring_bracket, ← this]
[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
⊢ ↑(mkAlgHom R L) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(mkAlgHom R L) (↑ιₜ x * ↑ιₜ y)
[PROOFSTEP]
exact RingQuot.mkAlgHom_rel _ (Rel.lie_compat x y)
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
⊢ ∀ ⦃x y : TensorAlgebra R L⦄, Rel R L x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
h : Rel R L a b
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b
[PROOFSTEP]
induction' h with x y
[GOAL]
case lie_compat
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
x y : L
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(↑(TensorAlgebra.lift R) ↑f) (↑ιₜ x * ↑ιₜ y)
[PROOFSTEP]
simp only [LieRing.of_associative_ring_bracket, map_add, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
  LieHom.map_lie, map_mul, sub_add_cancel]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
⊢ (fun F => LieHom.comp (AlgHom.toLieHom F) (ι R))
      ((fun f =>
          ↑(RingQuot.liftAlgHom R)
            { val := ↑(TensorAlgebra.lift R) ↑f,
              property :=
                (_ :
                  ∀ ⦃a b : TensorAlgebra R L⦄,
                    Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
        f) =
    f
[PROOFSTEP]
ext
  -- Porting note: was
      -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
      --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_toLieHom,
      --   LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
      --   RingQuot.liftAlgHom_mkAlgHom_apply]
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ↑((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R))
          ((fun f =>
              ↑(RingQuot.liftAlgHom R)
                { val := ↑(TensorAlgebra.lift R) ↑f,
                  property :=
                    (_ :
                      ∀ ⦃a b : TensorAlgebra R L⦄,
                        Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom, UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ↑(↑(RingQuot.liftAlgHom R)
          { val := ↑(TensorAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ ⦃a b : TensorAlgebra R L⦄,
                  Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
      (↑(RingQuot.mkAlgHom R (Rel R L)) (↑ιₜ x✝)) =
    ↑f x✝
[PROOFSTEP]
rw [RingQuot.liftAlgHom_mkAlgHom_apply]
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) (↑ιₜ x✝) = ↑f x✝
[PROOFSTEP]
simp only [TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ (fun f =>
        ↑(RingQuot.liftAlgHom R)
          { val := ↑(TensorAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ ⦃a b : TensorAlgebra R L⦄,
                  Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
      ((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R)) F) =
    F
[PROOFSTEP]
apply RingQuot.ringQuot_ext'
[GOAL]
case w
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ AlgHom.comp
      ((fun f =>
          ↑(RingQuot.liftAlgHom R)
            { val := ↑(TensorAlgebra.lift R) ↑f,
              property :=
                (_ :
                  ∀ ⦃a b : TensorAlgebra R L⦄,
                    Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
        ((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R)) F))
      (RingQuot.mkAlgHom R (Rel R L)) =
    AlgHom.comp F (RingQuot.mkAlgHom R (Rel R L))
[PROOFSTEP]
ext
  -- Porting note: was
      -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
      --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_linearMap_comp,
      --   AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply,
      --   RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_toLieHom, LieHom.coe_mk]
[GOAL]
case w.w.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
x✝ : L
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp
              ((fun f =>
                  ↑(RingQuot.liftAlgHom R)
                    { val := ↑(TensorAlgebra.lift R) ↑f,
                      property :=
                        (_ :
                          ∀ ⦃a b : TensorAlgebra R L⦄,
                            Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
                ((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R)) F))
              (RingQuot.mkAlgHom R (Rel R L))))
          ιₜ)
      x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp F (RingQuot.mkAlgHom R (Rel R L)))) ιₜ) x✝
[PROOFSTEP]
simp [mkAlgHom]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ↑(↑(lift R) f) (↑(ι R) x) = ↑f x
[PROOFSTEP]
rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ↑(↑(lift R) f) (↑(mkAlgHom R L) (↑ιₜ x)) = ↑f x
[PROOFSTEP]
simpa using lift_ι_apply R f x
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f ↔ g = ↑(lift R) f
[PROOFSTEP]
refine' Iff.trans _ (lift R).symm_apply_eq
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f ↔ ↑(lift R).symm g = f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f → ↑(lift R).symm g = f
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑g ∘ ↑(ι R) = ↑f
⊢ ↑(lift R).symm g = f
[PROOFSTEP]
ext
[GOAL]
case mp.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑g ∘ ↑(ι R) = ↑f
x✝ : L
⊢ ↑(↑(lift R).symm g) x✝ = ↑f x✝
[PROOFSTEP]
simp [← h]
[GOAL]
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑(lift R).symm g = f → ↑g ∘ ↑(ι R) = ↑f
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
⊢ ↑g ∘ ↑(ι R) = ↑f
[PROOFSTEP]
ext
[GOAL]
case mpr.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
x✝ : L
⊢ (↑g ∘ ↑(ι R)) x✝ = ↑f x✝
[PROOFSTEP]
simp [← h]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
⊢ ↑(lift R).symm g₁ = ↑(lift R).symm g₂
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
x✝ : L
⊢ ↑(↑(lift R).symm g₁) x✝ = ↑(↑(lift R).symm g₂) x✝
[PROOFSTEP]
simp [h]


[GOAL]
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
⊢ C o
[PROOFSTEP]
by_cases h : o = 0
[GOAL]
case pos
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
h : o = 0
⊢ C o
[PROOFSTEP]
rw [h]
[GOAL]
case pos
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
h : o = 0
⊢ C 0
[PROOFSTEP]
exact H0
[GOAL]
case neg
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
h : ¬o = 0
⊢ C o
[PROOFSTEP]
exact H o h (CNFRec _ H0 H (o % b ^ log b o))
[GOAL]
b o : Ordinal.{u_2}
h : ¬o = 0
⊢ (invImage (fun a => a) wellFoundedRelation).1 (o % b ^ log b o) o
[PROOFSTEP]
exact mod_opow_log_lt_self b h
[GOAL]
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNFRec b H0 H 0 = H0
[PROOFSTEP]
rw [CNFRec, dif_pos rfl]
[GOAL]
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ Eq.mpr (_ : C 0 = C 0) H0 = H0
[PROOFSTEP]
rfl
[GOAL]
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNFRec b H0 H o = H o ho (CNFRec b H0 H (o % b ^ log b o))
[PROOFSTEP]
rw [CNFRec, dif_neg ho]
[GOAL]
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 0 o = [(0, o)]
[PROOFSTEP]
simp [CNF_ne_zero ho]
[GOAL]
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 1 o = [(0, o)]
[PROOFSTEP]
simp [CNF_ne_zero ho]
[GOAL]
b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]
[PROOFSTEP]
rcases le_one_iff.1 hb with (rfl | rfl)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]
[PROOFSTEP]
exact zero_CNF ho
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]
[PROOFSTEP]
exact one_CNF ho
[GOAL]
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]
[PROOFSTEP]
simp only [CNF_ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, CNF_zero]
[GOAL]
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.fst * p.snd + r) 0 (CNF b 0) = 0
[PROOFSTEP]
rw [CNF_zero]
[GOAL]
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.fst * p.snd + r) 0 [] = 0
[PROOFSTEP]
rfl
[GOAL]
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r => b ^ p.fst * p.snd + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r => b ^ p.fst * p.snd + r) 0 (CNF b o) = o
[PROOFSTEP]
rw [CNF_ne_zero ho, foldr_cons, IH, div_add_mod]
[GOAL]
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.fst ≤ log b o
[PROOFSTEP]
refine' CNFRec b _ (fun o ho H ↦ _) o
[GOAL]
case refine'_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.fst ≤ log b 0
[PROOFSTEP]
rw [CNF_zero]
[GOAL]
case refine'_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ [] → x.fst ≤ log b 0
[PROOFSTEP]
intro contra
[GOAL]
case refine'_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
contra : x ∈ []
⊢ x.fst ≤ log b 0
[PROOFSTEP]
contradiction
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.fst ≤ log b o
[PROOFSTEP]
rw [CNF_ne_zero ho, mem_cons]
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
⊢ x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b o
[PROOFSTEP]
rintro (rfl | h)
[GOAL]
case refine'_2.inl
b o✝ o : Ordinal.{u}
ho : o ≠ 0
H : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).fst ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst ≤ log b o
[PROOFSTEP]
exact le_rfl
[GOAL]
case refine'_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.fst ≤ log b o
[PROOFSTEP]
exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)
[GOAL]
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → 0 < x.snd
[PROOFSTEP]
refine' CNFRec b (by simp) (fun o ho IH ↦ _) o
[GOAL]
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → 0 < x.snd
[PROOFSTEP]
simp
[GOAL]
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ CNF b o → 0 < x.snd
[PROOFSTEP]
rw [CNF_ne_zero ho]
[GOAL]
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.snd
[PROOFSTEP]
rintro (h | ⟨_, h⟩)
[GOAL]
case head
b o✝ o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).snd
⊢ 0 < (log b o, o / b ^ log b o).snd
[PROOFSTEP]
exact div_opow_log_pos b ho
[GOAL]
case tail
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.snd
[PROOFSTEP]
exact IH h
[GOAL]
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.snd < b
[PROOFSTEP]
refine' CNFRec b _ (fun o ho IH ↦ _) o
[GOAL]
case refine'_1
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.snd < b
[PROOFSTEP]
simp only [CNF_zero, not_mem_nil, IsEmpty.forall_iff]
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
⊢ x ∈ CNF b o → x.snd < b
[PROOFSTEP]
rw [CNF_ne_zero ho]
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.snd < b
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.snd < b
[PROOFSTEP]
cases' (mem_cons.mp h) with h h
[GOAL]
case refine'_2.inl
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x = (log b o, o / b ^ log b o)
⊢ x.snd < b
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_2.inl
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x = (log b o, o / b ^ log b o)
⊢ (log b o, o / b ^ log b o).snd < b
[PROOFSTEP]
simpa only using div_opow_log_lt o hb
[GOAL]
case refine'_2.inr
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.snd < b
[PROOFSTEP]
exact IH h
[GOAL]
b o : Ordinal.{u_1}
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
refine' CNFRec b _ (fun o ho IH ↦ _) o
[GOAL]
case refine'_1
b o : Ordinal.{u_1}
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b 0))
[PROOFSTEP]
simp only [CNF_zero]
[GOAL]
case refine'_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case refine'_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
simp only [CNF_of_le_one hb ho, map]
[GOAL]
case refine'_2.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
cases' lt_or_le o b with hob hbo
[GOAL]
case refine'_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
simp only [CNF_of_lt ho hob, map]
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
rw [CNF_ne_zero ho, map_cons, sorted_cons]
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 ∈ map Prod.fst (CNF b (o % b ^ log b o)) → (log b o, o / b ^ log b o).fst > b_1) ∧
    Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
[PROOFSTEP]
refine' ⟨fun a H ↦ _, IH⟩
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).fst > a
[PROOFSTEP]
rw [mem_map] at H
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : ∃ a_1, a_1 ∈ CNF b (o % b ^ log b o) ∧ a_1.fst = a
⊢ (log b o, o / b ^ log b o).fst > a
[PROOFSTEP]
rcases H with ⟨⟨a, a'⟩, H, rfl⟩
[GOAL]
case refine'_2.inr.inr.intro.mk.intro
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a a' : Ordinal.{u_1}
H : (a, a') ∈ CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst > (a, a').fst
[PROOFSTEP]
exact (CNF_fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb ho hbo)