awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
inr inr₁ : ∀ (α_emp : Nonempty α), card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α
have inr₂ : ∀ (α_emp : Nonempty α), Finite α → card (α → β) = card β ^ card α
Tactic: classical
  rcases isEmpty_or_nonempty α with α_emp | α_emp
  · simp [(card_eq_zero_iff_empty α).2 α_emp]
  rcases finite_or_infinite α
  · rcases finite_or_infinite β
    · letI := Fintype.ofFinite α
      letI := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm
  · rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · letI := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · letI := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
inr inr₁ : ∀ (α_emp : Nonempty α), card (α → β) = card β ^ card α
inr₂ : ∀ (α_emp : Nonempty α), Finite α → card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α
have inr₃ : ∀ (α_emp : Nonempty α), Infinite α → card (α → β) = card β ^ card α
Tactic: classical
  rcases isEmpty_or_nonempty α with α_emp | α_emp
  · simp [(card_eq_zero_iff_empty α).2 α_emp]
  rcases finite_or_infinite α
  · rcases finite_or_infinite β
    · letI := Fintype.ofFinite α
      letI := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm
  · rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · letI := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · letI := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have a : #(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : #(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have a₁ : max (lift.{v, u} #α) (lift.{u, v} #β) ≤ #(α →₀ β)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have h : ℵ₀ ≤ lift.{v, u} #α
Tactic: rw [mk_prod, mul_eq_max_of_aleph0_le_left]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
h : ℵ₀ ≤ lift.{v, u} #α
⊢ #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have h' : lift.{u, v} #β ≠ 0
Tactic: rw [mk_prod, mul_eq_max_of_aleph0_le_left]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ #(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)
have mk_le_of_injective : #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)
Tactic: calc
      #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
      _ = #(α × β) := mk_finset_of_infinite _
      _ = max (lift.{v} #α) (lift.{u} #β) := by
        rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ max (lift.{v, u} #α) (lift.{u, v} #β) ≤ #(α →₀ β)
have a : lift.{v, u} #α ≤ #(α →₀ β)
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : lift.{v, u} #α ≤ #(α →₀ β)
⊢ max (lift.{v, u} #α) (lift.{u, v} #β) ≤ #(α →₀ β)
have a₁ : lift.{u, v} #β ≤ #(α →₀ β)
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ lift.{v, u} #α ≤ #(α →₀ β)
have a : lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
Tactic: rw [← lift_id #(α →₀ β), ← lift_umax]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ lift.{u, v} #β ≤ #(α →₀ β)
have a : lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
Tactic: rw [← lift_id #(α →₀ β), ← lift_umax]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
have a : ∀ (b : β) (hb : b ≠ 0), lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
Tactic: obtain ⟨b, hb⟩ := exists_ne (0 : β)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
have a : ∀ (inhabited_h : Inhabited α), lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have inl : ∀ (val : Fintype α), #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
inl : ∀ (val : Fintype α), #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have inr : Infinite α → #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
have inl : lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
Tactic: rw [mk_finsupp_lift_of_fintype]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (hypothesis)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
have this : ℵ₀ ≤ lift.{u, v} #β
Tactic: have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
have inl : 1 ≤ Fintype.card α
Tactic: rw [max_eq_right (le_trans _ this), power_nat_eq this]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finsupp (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
inl : 1 ≤ Fintype.card α
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
have rw : lift.{v, u} #α ≤ ℵ₀
Tactic: rw [max_eq_right (le_trans _ this), power_nat_eq this]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(FreeGroup α) = max #α ℵ₀
have a : #(FreeGroup α) ≤ max #α ℵ₀
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
a : #(FreeGroup α) ≤ max #α ℵ₀
⊢ #(FreeGroup α) = max #α ℵ₀
have a₁ : max #α ℵ₀ ≤ #(FreeGroup α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(FreeGroup α) ≤ max #α ℵ₀
have a : #(List (α × Bool)) = max #α ℵ₀
Tactic: apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(List (α × Bool)) = max #α ℵ₀
have a : max (#α * 2) ℵ₀ = max #α ℵ₀
Tactic: simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀
have a : ∀ (hα : #α < ℵ₀), max (#α * 2) ℵ₀ = max #α ℵ₀
Tactic: obtain hα | hα := lt_or_ge #α ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
a : ∀ (hα : #α < ℵ₀), max (#α * 2) ℵ₀ = max #α ℵ₀
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀
have a₁ : ∀ (hα : ℵ₀ ≤ #α), max (#α * 2) ℵ₀ = max #α ℵ₀
Tactic: obtain hα | hα := lt_or_ge #α ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
hα : #α < ℵ₀
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀
have a : #α * 2 ≤ ℵ₀
Tactic: simp only [hα.le, max_eq_right, max_eq_right_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
hα : ℵ₀ ≤ #α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀
have rw : 2 ≤ #α
Tactic: rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ max #α ℵ₀ ≤ #(FreeGroup α)
have a : #α ≤ #(FreeGroup α)
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
a : #α ≤ #(FreeGroup α)
⊢ max #α ℵ₀ ≤ #(FreeGroup α)
have a₁ : ℵ₀ ≤ #(FreeGroup α)
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(FreeGroup α) = max #α ℵ₀
have a : #(FreeGroup α) ≤ max #α ℵ₀
Tactic: classical
  apply le_antisymm
  · apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
    simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
    obtain hα | hα := lt_or_ge #α ℵ₀
    · simp only [hα.le, max_eq_right, max_eq_right_iff]
      exact (mul_lt_aleph0 hα natCast_lt_aleph0).le
    · rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα
  · apply max_le
    · exact mk_le_of_injective FreeGroup.of_injective
    · simp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
a : #(FreeGroup α) ≤ max #α ℵ₀
⊢ #(FreeGroup α) = max #α ℵ₀
have a₁ : max #α ℵ₀ ≤ #(FreeGroup α)
Tactic: classical
  apply le_antisymm
  · apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
    simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
    obtain hα | hα := lt_or_ge #α ℵ₀
    · simp only [hα.le, max_eq_right, max_eq_right_iff]
      exact (mul_lt_aleph0 hα natCast_lt_aleph0).le
    · rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα
  · apply max_le
    · exact mk_le_of_injective FreeGroup.of_injective
    · simp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(FreeAbelianGroup α) = max #α ℵ₀
have rw : #(α →₀ ℤ) = max #α ℵ₀
Tactic: rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
⊢ #(FreeRing α) = max #α ℵ₀
have inl : IsEmpty α → #(FreeRing α) = max #α ℵ₀
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inl : IsEmpty α → #(FreeRing α) = max #α ℵ₀
⊢ #(FreeRing α) = max #α ℵ₀
have inr : Nonempty α → #(FreeRing α) = max #α ℵ₀
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
⊢ #(FreeCommRing α) = max #α ℵ₀
have inl : IsEmpty α → #(FreeCommRing α) = max #α ℵ₀
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inl : IsEmpty α → #(FreeCommRing α) = max #α ℵ₀
⊢ #(FreeCommRing α) = max #α ℵ₀
have inr : Nonempty α → #(FreeCommRing α) = max #α ℵ₀
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ Nonempty.{u + 1} (CommRing α)
have inl : ∀ (hR : Finite α), Nonempty.{u + 1} (CommRing α)
Tactic: obtain hR | hR := finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
inl : ∀ (hR : Finite α), Nonempty.{u + 1} (CommRing α)
⊢ Nonempty.{u + 1} (CommRing α)
have inr : ∀ (hR : Infinite α), Nonempty.{u + 1} (CommRing α)
Tactic: obtain hR | hR := finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
⊢ Nonempty.{u + 1} (CommRing α)
have inl : ∀ (x : Fintype α), Nonempty.{u + 1} (CommRing α)
Tactic: obtain ⟨x⟩ := nonempty_fintype α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (hypothesis)
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
⊢ Nonempty.{u + 1} (CommRing α)
have this : NeZero (Fintype.card α)
Tactic: have : NeZero (Fintype.card α) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
⊢ Nonempty.{u + 1} (CommRing α)
have inl : ∀ (x_1 : Trunc (α ≃ Fin (Fintype.card α))) (e : α ≃ Fin (Fintype.card α)), Nonempty.{u + 1} (CommRing α)
Tactic: obtain ⟨e⟩ := Fintype.truncEquivFin α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
⊢ Nonempty.{u + 1} (CommRing α)
have inl : ∀ (x_1 : Trunc (α ≃ Fin (Fintype.card α))) (e : α ≃ Fin (Fintype.card α)), Nonempty.{u + 1} (CommRing α)
Tactic: classical
    obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in e.commRing⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Free (goal)
Goal:
α : Type u
inst : Nonempty α
hR : Infinite α
⊢ Nonempty.{u + 1} (CommRing α)
have inr : ∀ (e : α ≃ FreeCommRing α), Nonempty.{u + 1} (CommRing α)
Tactic: have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
⊢ Small.{v, u} X
have h₁ : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
Tactic: rw [← Cardinal.lift_lt.{_, v + 1}, Cardinal.lift_lift, Cardinal.lift_lift] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ
have rw : Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Tactic: rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
have rw : ∀ (h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ) {Y : Type u'} (f : Y → X)
  (hf : Function.Injective f), Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Tactic: rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h
Cleared hypotheses: h, Y, f, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ
have rw : Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Tactic: rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
have rw : ∀ (h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ) {Y : Type u'} (f : X → Y)
  (hf : Function.Surjective f), Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Tactic: rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h
Cleared hypotheses: h, Y, f, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ
have mp : HasCardinalLT (X ⊕ Y) κ → HasCardinalLT X κ ∧ HasCardinalLT Y κ
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
mp : HasCardinalLT (X ⊕ Y) κ → HasCardinalLT X κ ∧ HasCardinalLT Y κ
⊢ HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ
have mpr : HasCardinalLT X κ ∧ HasCardinalLT Y κ → HasCardinalLT (X ⊕ Y) κ
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{w, u} (Cardinal.mk X) < Cardinal.lift.{u, w} κ
hY : Cardinal.lift.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ
have hX₁ : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
Tactic: rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at hX
Cleared hypotheses: hX, hY
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ
have hY₁ : Cardinal.lift.{max w u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, w} κ
Tactic: rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift] at hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{max w u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ
have mpr : Cardinal.lift.{max u' w, u} (Cardinal.mk X) + Cardinal.lift.{max u w, u'} (Cardinal.mk Y) <
  Cardinal.lift.{max u' u, w} κ
Tactic: simp only [Cardinal.mk_sum, Cardinal.lift_add, Cardinal.lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT.{w, u} (Option X) κ ↔ HasCardinalLT X κ
have rw : HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ
Tactic: rw [hasCardinalLT_iff_of_equiv (Equiv.optionEquivSumPUnit.{0} X),
    hasCardinalLT_sum_iff _ _ _ hκ, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ
have refine : HasCardinalLT X κ → HasCardinalLT PUnit.{1} Cardinal.aleph0
Tactic: refine fun _ ↦ HasCardinalLT.of_le ?_ hκ
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT X κ
⊢ HasCardinalLT PUnit.{1} Cardinal.aleph0
have rw : Finite PUnit.{1}
Tactic: rw [hasCardinalLT_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
have rw : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ ∧ HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
Tactic: rw [hasCardinalLT_sum_iff _ _ _ hκ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype (P₁ ⊔ P₂)) κ
have this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
Tactic: have : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ := by
    rw [hasCardinalLT_sum_iff _ _ _ hκ]
    exact ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype (P₁ ⊔ P₂)) κ
have refine : Function.Surjective.{u_1 + 1, u_1 + 1} (α := Subtype P₁ ⊕ Subtype P₂) (β := Subtype (P₁ ⊔ P₂))
  (Sum.elim (fun (x : Subtype P₁) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) sorry) fun (x : Subtype P₂) ↦
    Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) sorry)
Tactic: refine this.of_surjective (Sum.elim (fun x ↦ ⟨x.1, Or.inl x.2⟩)
    (fun x ↦ ⟨x.1, Or.inr x.2⟩)) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ
have simp : ∀ (hι : Cardinal.mk ι < κ) (hα : ∀ (i : ι), Cardinal.mk (α i) < κ), Cardinal.mk ((i : ι) × α i) < κ
Tactic: simp only [hasCardinalLT_iff_cardinal_mk_lt] at hι hα ⊢
Cleared hypotheses: hι, hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
⊢ Cardinal.mk ((i : ι) × α i) < κ
have rw : (Cardinal.sum fun (i : ι) ↦ Cardinal.mk (α i)) < κ
Tactic: rw [Cardinal.mk_sigma]