awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type (max u v)
inst : Small.{v, max u v} α
rw : lift.{max v u, v} #(Shrink.{v, max u v} α) = #α
rw₁ : lift.{v, max u v} #α = #α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α
have rw₂ : lift.{max u v, max u v} #α = #α
Tactic: rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type (max u v)
inst : Small.{v, max u v} α
rw : lift.{max v u, v} #(Shrink.{v, max u v} α) = #α
rw₁ : lift.{v, max u v} #α = #α
rw₂ : lift.{max u v, max u v} #α = #α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α
have rw₃ : #α = #α
Tactic: rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
f : α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : α, f i)
have revert : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
Tactic: revert f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
have refine_1 : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
  (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
    ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)
Tactic: refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
refine_1 :
  ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
have refine_2 : ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
Tactic: refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
refine_1 :
  ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)
refine_2 : ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
have refine_3 : ∀ (α : Type u) [inst : Fintype α],
  (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
    ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : Option α, f i)
Tactic: refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α_1 : Type u
h_1 : Fintype α_1
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i : β, f i)
have refine_1 : prod f = prod.{u, v} fun (i : α) ↦ f ((e : (a : α) → β) i)
Tactic: rw [← e.prod_comp f, ← h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
have refine_2 : prod f = lift.{u, v} (∏ i ∈ ∅, f i)
Tactic: rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
refine_2 : prod f = lift.{u, v} (∏ i ∈ ∅, f i)
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
have refine_2₁ : prod f = lift.{u, v} 1
Tactic: rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
refine_2 : prod f = lift.{u, v} (∏ i ∈ ∅, f i)
refine_2₁ : prod f = lift.{u, v} 1
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
have refine_2₂ : prod f = 1
Tactic: rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
refine_2 : prod f = lift.{u, v} (∏ i ∈ ∅, f i)
refine_2₁ : prod f = lift.{u, v} 1
refine_2₂ : prod f = 1
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
have refine_2₃ : #((i : PEmpty.{u + 1}) → Quotient.out (f i)) = 1
Tactic: rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
refine_2 : prod f = lift.{u, v} (∏ i ∈ ∅, f i)
refine_2₁ : prod f = lift.{u, v} 1
refine_2₂ : prod f = 1
refine_2₃ : #((i : PEmpty.{u + 1}) → Quotient.out (f i)) = 1
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
have refine_2₄ : Eq (α := Cardinal.{max u v}) 1 1
Tactic: rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α_1 : Type u
h_1 : Fintype α_1
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : Option α, f i)
have refine_3 : (lift.{u, v} (f none) * prod.{u, v} fun (i : α) ↦ lift.{v, v} (f (some i))) =
  lift.{u, v} (f none) * prod.{u, v} fun (a : α) ↦ f (some a)
Tactic: rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax.{v, u}, mk_out, ←
        Cardinal.prod, lift_prod, Fintype.prod_option, lift_mul, ← h fun a => f (some a)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ 1 < #α ↔ Nontrivial α
have rw : ¬#α ≤ 1 ↔ Nontrivial α
Tactic: rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : ¬#α ≤ 1 ↔ Nontrivial α
⊢ 1 < #α ↔ Nontrivial α
have rw₁ : ¬Subsingleton α ↔ Nontrivial α
Tactic: rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : ¬#α ≤ 1 ↔ Nontrivial α
rw₁ : ¬Subsingleton α ↔ Nontrivial α
⊢ 1 < #α ↔ Nontrivial α
have rw₂ : ¬¬Nontrivial α ↔ Nontrivial α
Tactic: rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : ¬#α ≤ 1 ↔ Nontrivial α
rw₁ : ¬Subsingleton α ↔ Nontrivial α
rw₂ : ¬¬Nontrivial α ↔ Nontrivial α
⊢ 1 < #α ↔ Nontrivial α
have rw₃ : Nontrivial α ↔ Nontrivial α
Tactic: rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0
have refine_1 : ∀ (h : sInf s = 0), s = ∅ ∨ ∃ a ∈ s, a = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
refine_1 : ∀ (h : sInf s = 0), s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0
have refine_2 : ∀ (h : s = ∅ ∨ ∃ a ∈ s, a = 0), sInf s = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
h : sInf s = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
have refine_1 : ∀ (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0),
  Eq.{u_1 + 2} (α := Set Cardinal.{u_1}) ∅ ∅ ∨
    ∃ (a : Cardinal.{u_1}), Membership.mem (γ := Set Cardinal.{u_1}) ∅ a ∧ a = 0
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
h : sInf s = 0
refine_1 :
  ∀ (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0),
    Eq.{u_1 + 2} (α := Set Cardinal.{u_1}) ∅ ∅ ∨
      ∃ (a : Cardinal.{u_1}), Membership.mem (γ := Set Cardinal.{u_1}) ∅ a ∧ a = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
have refine_1₁ : ∀ (hne : s.Nonempty), s = ∅ ∨ ∃ a ∈ s, a = 0
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0
have refine_2 : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0
Tactic: rcases h with rfl | ⟨a, ha, rfl⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
refine_2 : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0
⊢ sInf s = 0
have refine_2₁ : ∀ (ha : 0 ∈ s), sInf s = 0
Tactic: rcases h with rfl | ⟨a, ha, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{v}
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
have inl : lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{v}
inl : lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
have inr : ∀ (hs : s.Nonempty), lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (sInf (range f)) = sInf (range fun (i : ι) ↦ lift.{u, v} (f i))
have h : (range fun (i : ι) ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f
Tactic: convert! lift_sInf (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun (i : ι) ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f
have h : (range fun (i : ι) ↦ (lift.{u, v} ∘ f) i) = lift.{u, v} '' range f
Tactic: simp_rw [← comp_apply (f := lift), range_comp]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Iic a) : Type (u + 1))
have rw : Small.{u, u + 1} (↑(Iic #(Quotient.out a)) : Type (u + 1))
Tactic: rw [← mk_out a]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Iic #(Quotient.out a)) : Type (u + 1))
have apply : Surjective (β := (↑(Iic #(Quotient.out a)) : Type (u + 1))) fun (x : Set (Quotient.out a)) ↦
  Subtype.mk (p := fun (x : Cardinal.{u}) ↦ x ∈ Iic #(Quotient.out a)) #(↑x : Type u) sorry
Tactic: apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u}
ι : Type u
e : (↑s : Type (u + 1)) ≃ ι
⊢ BddAbove s
have h : (sum fun (x : ι) ↦ (↑((e.symm : (a : ι) → (↑s : Type (u + 1))) x) : Cardinal.{u})) ∈ upperBounds s
Tactic: use sum.{u, u} fun x ↦ e.symm x
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
⊢ BddAbove (f '' s)
have rw : ∀ (hs : Small.{u, u + 1} (↑s : Type (u + 1))), Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))
Tactic: rw [bddAbove_iff_small] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (range (g ∘ f))
have rw : BddAbove (g '' range f)
Tactic: rw [range_comp]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False
have this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
Tactic: have := small_lift.{_, v} Cardinal.{max u v}
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False
have this₁ : BddAbove (α := Cardinal.{max u v}) univ
Tactic: rw [← small_univ_iff, ← bddAbove_iff_small] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)
have rw : (sum fun (i : ι) ↦ lift.{max u v, v} (f i)) ≤ sum fun (x : ι) ↦ ⨆ (i : ι), lift.{u, v} (f i)
Tactic: rw [← (sum f).lift_id, lift_sum, ← lift_umax.{u, v}, ← (⨆ i, lift (f i)).lift_id,
    lift_umax.{max v u, u}, ← sum_const]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
⊢ (sum fun (i : ι) ↦ lift.{max u v, v} (f i)) ≤ sum fun (x : ι) ↦ ⨆ (i : ι), lift.{u, v} (f i)
have refine : ∀ (i : ι), lift.{max u v, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)
Tactic: refine sum_le_sum _ _ fun i => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{max u v, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)
have rw : lift.{u, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)
Tactic: rw [lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)
have apply : ∀ (c : Cardinal.{max u_1 u}) (hc : c ∈ upperBounds (lift.{u, u_1} '' s)), lift.{u, u_1} (sSup s) ≤ c
Tactic: apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
apply : ∀ (c : Cardinal.{max u_1 u}) (hc : c ∈ upperBounds (lift.{u, u_1} '' s)), lift.{u, u_1} (sSup s) ≤ c
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)
have apply₁ : lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)
Tactic: apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
⊢ lift.{u, u_1} (sSup s) ≤ c
have by_contra : ∀ (h : ¬lift.{u, u_1} (sSup s) ≤ c), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ c
⊢ False
have obtain : ∀ (d : Cardinal.{u_1}) (hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s))
  (h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d), False
Tactic: obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d
⊢ False
have h₁ : ¬sSup s ≤ d
Tactic: simp_rw [lift_le] at h hc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ False
have h₁ : ¬∀ x ∈ s, x ≤ d
Tactic: rw [csSup_le_iff' hs] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (iSup f) = ⨆ (i : ι), lift.{u, w} (f i)
have rw : sSup (range (lift.{u, w} ∘ f)) = sSup (range fun (i : ι) ↦ lift.{u, w} (f i))
Tactic: rw [iSup, iSup, lift_sSup hf, ← range_comp]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t
have rw : ⨆ (i : ι), lift.{u, w} (f i) ≤ t
Tactic: rw [lift_iSup hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
have rw : ⨆ (i : ι), lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
Tactic: rw [lift_iSup hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')
have rw : LE.le (α := Cardinal.{max w w'}) (⨆ (i : ι), lift.{w', w} (f i)) (⨆ (i : ι'), lift.{w, w'} (f' i))
Tactic: rw [lift_iSup hf, lift_iSup hf']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ lift.{u, v} (⨆ (i : ι), f i) ≤ sum f
have rw : ⨆ (i : ι), lift.{u, v} (f i) ≤ sum f
Tactic: rw [lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
⊢ succ (↑n : Cardinal.{u_1}) = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
have refine : (↑n : Cardinal.{u_1}) < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
Tactic: refine (succ_le_of_lt ?_).antisymm (add_one_le_of_lt <| lt_succ _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u_1}) < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
have rw : LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑n.succ : Cardinal.{u_1})
Tactic: rw [← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
c : Cardinal.{u_1}
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔ (↑n : Cardinal.{u_1}) < c
have rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔ succ (↑n : Cardinal.{u_1}) ≤ c
Tactic: rw [← Order.succ_le_iff, succ_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
c : Cardinal.{u_1}
rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔ succ (↑n : Cardinal.{u_1}) ≤ c
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔ (↑n : Cardinal.{u_1}) < c
have rw₁ : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c
Tactic: rw [← Order.succ_le_iff, succ_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
c : Cardinal.{u_1}
⊢ c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ c ≤ (↑n : Cardinal.{u_1})
have rw : c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ c < succ (↑n : Cardinal.{u_1})
Tactic: rw [← Order.lt_succ_iff, succ_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
c : Cardinal.{u_1}
rw : c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ c < succ (↑n : Cardinal.{u_1})
⊢ c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ c ≤ (↑n : Cardinal.{u_1})
have rw₁ : c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔
  c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
Tactic: rw [← Order.lt_succ_iff, succ_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
⊢ 2 ≤ c ↔ 1 < c
have h : 2 = HAdd.hAdd (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) 1
Tactic: convert! natCast_add_one_le_iff
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
⊢ 2 = HAdd.hAdd (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) 1
have h : 2 = HAdd.hAdd (α := ℕ) 1 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (succ 0) 1
have norm_cast : HAdd.hAdd (α := ℕ) 0 1 = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
⊢ LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) 1 2
have norm_cast : LT.lt (α := ℕ) 1 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
⊢ ∃ (s : Finset α), n = s.card
have inl : ∀ (hα : Finite α), ∃ (s : Finset α), n = s.card
Tactic: obtain hα | hα := finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
inl : ∀ (hα : Finite α), ∃ (s : Finset α), n = s.card
⊢ ∃ (s : Finset α), n = s.card
have inr : ∀ (hα : Infinite α), ∃ (s : Finset α), n = s.card
Tactic: obtain hα | hα := finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα_1 : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ ∃ (s : Finset α), n = s.card
have inl : ∀ (t : Finset α) (h : (↑t.card : Cardinal.{u_1}) ≤ #α), ∃ (s : Finset α), t.card = s.card
Tactic: obtain ⟨t, -, rfl⟩ := @Finset.exists_subset_card_eq α .univ n <| by simpa using h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα : Infinite α
⊢ ∃ (s : Finset α), n = s.card
have inr : ∀ (s : Finset α) (hs : s.card = n), ∃ (s : Finset α), n = s.card
Tactic: obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
H : ∀ (s : Finset α), s.card ≤ n
⊢ #α ≤ (↑n : Cardinal.{u})
have contrapose! : ∀ (H : (↑n : Cardinal.{u}) < #α), ∃ (s : Finset α), n < s.card
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
H : (↑n : Cardinal.{u}) < #α
⊢ ∃ (s : Finset α), n < s.card
have apply : (↑(n + 1) : Cardinal.{u}) ≤ #α
Tactic: apply exists_finset_le_card α (n + 1)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
hb : succ 1 ≤ b
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (succ 1) 2
have norm_cast : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
a b : Cardinal.{u_1}
hb : 1 < b
⊢ a < b ^ a
have hb₁ : 2 ≤ b
Tactic: rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ 0 < c
have rw : succ 0 ≤ c ↔ 0 < c
Tactic: rw [← succ_zero, succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
rw : succ 0 ≤ c ↔ 0 < c
⊢ 1 ≤ c ↔ 0 < c
have rw₁ : 0 < c ↔ 0 < c
Tactic: rw [← succ_zero, succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ c ≠ 0
have rw : 0 < c ↔ c ≠ 0
Tactic: rw [Cardinal.one_le_iff_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
rw : 0 < c ↔ c ≠ 0
⊢ 1 ≤ c ↔ c ≠ 0
have rw₁ : c ≠ 0 ↔ c ≠ 0
Tactic: rw [Cardinal.one_le_iff_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u}) < ℵ₀
have rw : Nonempty (Fin (n + 1) ↪ ℕ)
Tactic: rw [← natCast_add_one_le_iff, ← Nat.cast_add_one, ← lift_mk_fin, aleph0, lift_mk_le.{u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
have rcases : ∀ (c : Cardinal.{0}) (h' : c < #ℕ) (h : lift.{u_1, 0} c < ℵ₀), ∃ (n : ℕ), lift.{u_1, 0} c = (↑n : Cardinal.{u_1})
Tactic: rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{0}
h' : c < #ℕ
h : lift.{u_1, 0} c < ℵ₀
⊢ ∃ (n : ℕ), lift.{u_1, 0} c = (↑n : Cardinal.{u_1})
have rcases : ∀ (S : Set ℕ) (h' : #(↑S : Type) < #ℕ) (h : lift.{u_1, 0} #(↑S : Type) < ℵ₀),
  ∃ (n : ℕ), lift.{u_1, 0} #(↑S : Type) = (↑n : Cardinal.{u_1})
Tactic: rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩
Cleared hypotheses: c, h', h