awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ 𝔠
have rw : Order.succ ℵ₀ ≤ 𝔠
Tactic: rw [← succ_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
⊢ 𝔠 ^ ℵ₀ = 𝔠
have rw : HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ ^ ℵ₀ = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
Tactic: rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
rw : HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ ^ ℵ₀ = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
⊢ 𝔠 ^ ℵ₀ = 𝔠
have rw₁ : HPow.hPow (α := Cardinal.{u_1}) 2 (ℵ₀ * ℵ₀) = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
Tactic: rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
rw : HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ ^ ℵ₀ = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
rw₁ : HPow.hPow (α := Cardinal.{u_1}) 2 (ℵ₀ * ℵ₀) = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
⊢ 𝔠 ^ ℵ₀ = 𝔠
have rw₂ : HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
Tactic: rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ = 𝔠
have a : x ^ ℵ₀ ≤ 𝔠
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
a : x ^ ℵ₀ ≤ 𝔠
⊢ x ^ ℵ₀ = 𝔠
have a₁ : 𝔠 ≤ x ^ ℵ₀
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠
have a : x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
Tactic: rw [← continuum_power_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
⊢ #(↑t : Type u) ≤ a
have inl : ∀ (ha : a < ℵ₀), #(↑t : Type u) ≤ a
Tactic: rcases lt_or_ge a ℵ₀ with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
inl : ∀ (ha : a < ℵ₀), #(↑t : Type u) ≤ a
⊢ #(↑t : Type u) ≤ a
have inr : ∀ (ha : ℵ₀ ≤ a), #(↑t : Type u) ≤ a
Tactic: rcases lt_or_ge a ℵ₀ with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : a < ℵ₀
⊢ #(↑t : Type u) ≤ a
have inl : ∀ (n : ℕ) (h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})) (ha : (↑n : Cardinal.{u}) < ℵ₀),
  #(↑t : Type u) ≤ (↑n : Cardinal.{u})
Tactic: obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
Cleared hypotheses: a, h'f, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
⊢ #(↑t : Type u) ≤ (↑n : Cardinal.{u})
have apply : ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ t), s.card ≤ n
Tactic: apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (hypothesis)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
⊢ s.card ≤ n
have A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
Tactic: have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (hypothesis)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
⊢ s.card ≤ n
have B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
Tactic: have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
⊢ s.card ≤ n
have rcases : ∀ (i : ι) (hi : ∀ x ∈ s, x ∈ f i), s.card ≤ n
Tactic: rcases B.exists with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
⊢ s.card ≤ n
have have : ∀ (this : (i : ι) → Fintype (↑(f i) : Type u)), s.card ≤ n
Tactic: have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (hypothesis)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
⊢ s.card ≤ u.card
have this₁ : s ⊆ u
Tactic: have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (hypothesis)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
⊢ s.card ≤ n
have I1 : s.card ≤ u.card
Tactic: have I1 : s.card ≤ u.card := by
      have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
      exact Finset.card_le_card this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ LE.le.{u + 1} (α := Cardinal.{u}) (↑u.card : Cardinal.{u}) (↑n : Cardinal.{u})
have h : (↑u.card : Cardinal.{u}) = #(↑(f i) : Type u)
Tactic: convert! h'f i
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (hypothesis)
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ s.card ≤ n
have I2 : LE.le.{u + 1} (α := Cardinal.{u}) (↑u.card : Cardinal.{u}) (↑n : Cardinal.{u})
Tactic: have I2 : (u.card : Cardinal) ≤ n := by
      convert! h'f i; simp only [u, Set.toFinset_card, mk_fintype]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), f i) x
have obtain : ∀ (i : ι) (hi : x ∈ f i), Membership.mem (γ := Set α) (⋃ (i : ι), f i) x
Tactic: obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (hypothesis)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
⊢ #(↑t : Type u) ≤ a
have this : t ⊆ ⋃ (i : ι), f i
Tactic: 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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ #ι * a ≤ ℵ₀ * a
have grw : ℵ₀ * a ≤ ℵ₀ * a
Tactic: grw [mk_le_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ #(↑t : Type u) ≤ a
have calc : (sum fun (x : ι) ↦ a) = #ι * a
Tactic: 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 := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
calc : (sum fun (x : ι) ↦ a) = #ι * a
⊢ #(↑t : Type u) ≤ a
have calc₁ : #ι * a ≤ ℵ₀ * a
Tactic: 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 := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
⊢ #(↑t : Type u) ≤ a
have suffices : #(↑(ULift.down ⁻¹' t) : Type (max u v)) ≤ lift.{v, u} a
Tactic: suffices #(ULift.down.{v} ⁻¹' t) ≤ Cardinal.lift.{v, u} a by simpa
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
⊢ #(↑(ULift.down ⁻¹' t) : Type (max u v)) ≤ lift.{v, u} a
have ht₁ : ∀ x ∈ ULift.down ⁻¹' t, ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i
Tactic: apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
ht₁ : ∀ x ∈ ULift.down ⁻¹' t, ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i
⊢ #(↑(ULift.down ⁻¹' t) : Type (max u v)) ≤ lift.{v, u} a
have h'f₁ : ∀ (i : ULift.{u, v} ι), #(↑(g i) : Type (max u v)) ≤ lift.{v, u} a
Tactic: apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
⊢ #α ≤ a
have rw : #(↑Set.univ : Type u) ≤ a
Tactic: rw [← mk_univ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
⊢ #α = a
have a₁ : #α ≤ a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
a₁ : #α ≤ a
⊢ #α = a
have a₂ : a ≤ #α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
⊢ a ≤ #α
have a₁ : ∀ (i : ι), a ≤ #α
Tactic: obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.CountableCover (goal)
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
i : ι
⊢ a ≤ #α
have a₁ : #(↑(f i) : Type u) ≤ #α
Tactic: rw [← (h'f i)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)
have rw : Nonempty (Quotient.out #(ULift.{v, u} (Quotient.out a)) ≃ Quotient.out a)
Tactic: rw [← mk_out a, ← mk_uLift, mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
⊢ Nonempty.{u_1 + 1} (Quotient.out x)
have rwa : #(Quotient.out x) ≠ 0
Tactic: rwa [← mk_ne_zero_iff, mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
α : Type u
⊢ #(Option α) = #α + 1
have rw : #(α ⊕ PUnit) = #α + 1
Tactic: rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
α : Type u
rw : #(α ⊕ PUnit) = #α + 1
⊢ #(Option α) = #α + 1
have rw₁ : lift.{u, u} #α + lift.{u, u} #PUnit = #α + 1
Tactic: rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
α : Type u
rw : #(α ⊕ PUnit) = #α + 1
rw₁ : lift.{u, u} #α + lift.{u, u} #PUnit = #α + 1
⊢ #(Option α) = #α + 1
have rw₂ : lift.{u, u} #α + lift.{u, u} 1 = #α + 1
Tactic: rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
α : Type u
rw : #(α ⊕ PUnit) = #α + 1
rw₁ : lift.{u, u} #α + lift.{u, u} #PUnit = #α + 1
rw₂ : lift.{u, u} #α + lift.{u, u} 1 = #α + 1
⊢ #(Option α) = #α + 1
have rw₃ : #α + lift.{u, u} 1 = #α + 1
Tactic: rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
α : Type u
rw : #(α ⊕ PUnit) = #α + 1
rw₁ : lift.{u, u} #α + lift.{u, u} #PUnit = #α + 1
rw₂ : lift.{u, u} #α + lift.{u, u} 1 = #α + 1
rw₃ : #α + lift.{u, u} 1 = #α + 1
⊢ #(Option α) = #α + 1
have rw₄ : #α + 1 = #α + 1
Tactic: rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
have rw : lift.{max v w, v} #(Quotient.out (f a)) =
  lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
Tactic: rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
a : ι
rw :
  lift.{max v w, v} #(Quotient.out (f a)) =
    lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
have rw₁ : lift.{max v w, v} (f a) = lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
Tactic: rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
a : ι
rw :
  lift.{max v w, v} #(Quotient.out (f a)) =
    lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
rw₁ :
  lift.{max v w, v} (f a) = lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
have rw₂ : lift.{max v w, v} (f a) = lift.{v, max v w} ((fun (i : ι) ↦ lift.{w, v} (f i)) a)
Tactic: rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
a : ι
rw :
  lift.{max v w, v} #(Quotient.out (f a)) =
    lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
rw₁ :
  lift.{max v w, v} (f a) = lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
rw₂ : lift.{max v w, v} (f a) = lift.{v, max v w} ((fun (i : ι) ↦ lift.{w, v} (f i)) a)
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
have rw₃ : lift.{max v w, v} (f a) = lift.{max w v, v} (f a)
Tactic: rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun (i : ℕ) ↦ f (i + 1)
have refine : #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun (i : ℕ) ↦ f (i + 1)
Tactic: refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ (i : ι), f i = 0
have lift : ∀ (f : (i : ι) → Type u),
  (prod.{u_1, u} fun (i : ι) ↦ #(f i)) = 0 ↔
    ∃ (i : ι), Eq.{u + 2} (α := Cardinal.{u}) ((fun (i : ι) ↦ mk.{u} (f i)) i) 0
Tactic: lift f to ι → Type u using fun _ => trivial
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
α : Type v
f : ι → Type v
⊢ #((i : ι) × Quotient.out #(f i) → ULift.{u, v} α) = #((i : ι) → Quotient.out #(f i → α))
have mk : ((i : ι) × Quotient.out #(f i) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))
Tactic: apply mk_congr
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
α : Type v
f : ι → Type v
⊢ ((i : ι) × Quotient.out #(f i) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))
have mk : ((a : ι) → (b : Quotient.out #(f a)) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))
Tactic: refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
α : Type v
f : ι → Type v
⊢ ((a : ι) → (b : Quotient.out #(f a)) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))
have mk : (b : ι) → ((b : Quotient.out #(f b)) → ULift.{u, v} α) ≃ Quotient.out #(f b → α)
Tactic: refine Equiv.piCongrRight fun b => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
α : Type v
f : ι → Type v
b : ι
⊢ ((b : Quotient.out #(f b)) → ULift.{u, v} α) ≃ Quotient.out #(f b → α)
have mk : (f b → α) ≃ Quotient.out #(f b → α)
Tactic: refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
α : Type v
⊢ lift.{u, v} #α ^ sum f = prod.{u, v} fun (i : ι) ↦ #α ^ f i
have mk : ∀ (f : ι → Type v),
  (lift.{u, v} #α ^ sum.{u, v} fun (i : ι) ↦ #(f i)) =
    prod.{u, v} fun (i : ι) ↦ HPow.hPow (β := Cardinal.{v}) (#α) ((fun (i : ι) ↦ mk.{v} (f i)) i)
Tactic: induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
a : Cardinal.{v}
f : ι → Cardinal.{v}
⊢ lift.{u, v} a ^ sum f = prod.{u, v} fun (i : ι) ↦ a ^ f i
have mk : ∀ (α : Type v), lift.{u, v} #α ^ sum f = prod.{u, v} fun (i : ι) ↦ #α ^ f i
Tactic: induction a using Cardinal.inductionOn with | _ α =>
  induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
c : ι → Cardinal.{v}
⊢ lift.{w, max v u} (prod c) = prod fun (i : ι) ↦ lift.{w, v} (c i)
have lift : ∀ (c : (i : ι) → Type v),
  lift.{w, max v u} (prod.{u, v} fun (i : ι) ↦ #(c i)) = prod fun (i : ι) ↦ lift.{w, v} ((fun (i : ι) ↦ mk.{v} (c i)) i)
Tactic: lift c to ι → Type v using fun _ => trivial
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Defs (goal)
Goal:
ι : Type u
c : (i : ι) → Type v
⊢ lift.{w, max v u} (prod.{u, v} fun (i : ι) ↦ #(c i)) = prod fun (i : ι) ↦ lift.{w, v} ((fun (i : ι) ↦ mk.{v} (c i)) i)
have simp : #(ULift ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))
Tactic: simp only [← mk_pi, ← mk_uLift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
⊢ IsUnit a ↔ a = 1
have h : ∀ (h : IsUnit a), a = 1
Tactic: refine
    ⟨fun h => ?_, by
      rintro rfl
      exact isUnit_one⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : IsUnit a
⊢ a = 1
have inl : ∀ (h : IsUnit.{u + 1} (M := Cardinal.{u}) 0), Eq.{u + 2} (α := Cardinal.{u}) 0 1
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : IsUnit a
inl : ∀ (h : IsUnit.{u + 1} (M := Cardinal.{u}) 0), Eq.{u + 2} (α := Cardinal.{u}) 0 1
⊢ a = 1
have inr : ∀ (ha : a ≠ 0), a = 1
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1
have h₁ : ∀ (y : Cardinal.{u}), a ∣ y
Tactic: rw [isUnit_iff_forall_dvd] at h
Cleared hypotheses: h, ha