awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
inst : Nonempty α
⊢ #(Multiset α) = max #α ℵ₀

Tactic:
Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

Premises used: Cardinal.mk_finsupp_nat, Multiset.toFinsupp, AddEquiv.toEquiv, Eq.trans, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
inst : Nonempty α
⊢ #(Multiset α) = max #α ℵ₀

Tactic:
exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

Premises used: Cardinal.mk_finsupp_nat, Multiset.toFinsupp, AddEquiv.toEquiv, Eq.trans, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
inst : Nonempty α
⊢ #(Multiset α) = max #α ℵ₀

Tactic:
classical
  exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

Premises used: Cardinal.mk_finsupp_nat, Multiset.toFinsupp, AddEquiv.toEquiv, Eq.trans, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
inst : Infinite α
⊢ #(Multiset α) = #α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ Infinite.{u + 1} (FreeMonoid α)

Tactic:
inferInstanceAs <| Infinite (List α)

Premises used: _private.0.instInfiniteFreeMonoidOfNonempty._proof_1
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ Infinite.{u + 1} (FreeGroup α)

Tactic:
Infinite.of_surjective FreeGroup.norm FreeGroup.norm_surjective

Premises used: FreeGroup.norm_surjective, FreeGroup.norm, Infinite.of_surjective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ Infinite.{u + 1} (FreeGroup α)

Tactic:
exact Infinite.of_surjective FreeGroup.norm FreeGroup.norm_surjective

Premises used: FreeGroup.norm_surjective, FreeGroup.norm, Infinite.of_surjective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ Infinite.{u + 1} (FreeGroup α)

Tactic:
classical
  exact Infinite.of_surjective FreeGroup.norm FreeGroup.norm_surjective

Premises used: FreeGroup.norm_surjective, FreeGroup.norm, Infinite.of_surjective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ Infinite.{u + 1} (FreeAbelianGroup α)

Tactic:
(FreeAbelianGroup.equivFinsupp α).toEquiv.infinite_iff.2 inferInstance

Premises used: Iff.mpr, inferInstance, FreeAbelianGroup.equivFinsupp, Equiv.infinite_iff, AddEquiv.toEquiv
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Countable α
⊢ Countable.{u + 1} (FreeMonoid α)

Tactic:
inferInstanceAs <| Countable (List α)

Premises used: _private.0.instCountableFreeMonoid._proof_1
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Countable α
⊢ Countable.{u + 1} (FreeGroup α)

Tactic:
inferInstanceAs <| Countable (Quot _)

Premises used: _private.0.instCountableFreeGroup._proof_1
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Countable α
⊢ Countable.{u + 1} (FreeAbelianGroup α)

Tactic:
inferInstanceAs <| Countable (Quot _)

Premises used: _private.0.instCountableFreeAbelianGroup._proof_1
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Countable α
⊢ Countable.{u + 1} (FreeRing α)

Tactic:
inferInstanceAs <| Countable (Quot _)

Premises used: _private.0.instCountableFreeRing._proof_1
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Countable α
⊢ Countable.{u + 1} (FreeCommRing α)

Tactic:
inferInstanceAs <| Countable (FreeAbelianGroup (Multiset α))

Premises used: _private.0.instCountableFreeCommRing._proof_1
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
G : Type u
inst : Group G
⊢ #(Abelianization G) ≤ #G

Tactic:
Cardinal.mk_le_of_surjective Quotient.mk_surjective

Premises used: Cardinal.mk_le_of_surjective, Quotient.mk_surjective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ #(FreeMonoid α) = max #α ℵ₀

Tactic:
Cardinal.mk_list_eq_max_mk_aleph0 _

Premises used: Cardinal.mk_list_eq_max_mk_aleph0, FreeMonoid
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
a : #(FreeGroup α) ≤ max #α ℵ₀
a₁ : max #α ℵ₀ ≤ #(FreeGroup α)
⊢ #(FreeGroup α) = max #α ℵ₀

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
a : #(List (α × Bool)) = max #α ℵ₀
⊢ #(FreeGroup α) ≤ max #α ℵ₀

Tactic:
apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq

Premises used: LE.le.trans_eq, FreeGroup.toWord_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
a : max (#α * 2) ℵ₀ = max #α ℵ₀
⊢ #(List (α × Bool)) = max #α ℵ₀

Tactic:
simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]

Premises used: Nat.cast_ofNat, Cardinal.mk_list_eq_max_mk_aleph0, Cardinal.mk_fintype, Cardinal.lift_uzero, Cardinal.lift_ofNat, Cardinal.mk_prod, Fintype.card_bool
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
a : ∀ (hα : #α < ℵ₀), max (#α * 2) ℵ₀ = max #α ℵ₀
a₁ : ∀ (hα : ℵ₀ ≤ #α), max (#α * 2) ℵ₀ = max #α ℵ₀
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀

Tactic:
obtain hα | hα := lt_or_ge #α ℵ₀

Premises used: Cardinal.mk, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : #α < ℵ₀
a : #α * 2 ≤ ℵ₀
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀

Tactic:
simp only [hα.le, max_eq_right, max_eq_right_iff]

Premises used: LT.lt.le, max_eq_right, max_eq_right_iff
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : #α < ℵ₀
⊢ #α * 2 ≤ ℵ₀

Tactic:
(mul_lt_aleph0 hα natCast_lt_aleph0).le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, Cardinal.mul_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : #α < ℵ₀
⊢ #α * 2 ≤ ℵ₀

Tactic:
exact (mul_lt_aleph0 hα natCast_lt_aleph0).le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, Cardinal.mul_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : ℵ₀ ≤ #α
⊢ Ne.{u + 2} (α := Cardinal.{u}) 2 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : ℵ₀ ≤ #α
rw : 2 ≤ #α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀

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)]

Premises used: Cardinal.mul_eq_left, max_eq_left, two_ne_zero, Cardinal.le_mul_right, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α

Tactic:
natCast_le_aleph0.trans hα

Premises used: LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α

Tactic:
exact natCast_le_aleph0.trans hα

Premises used: LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
a : #α ≤ #(FreeGroup α)
a₁ : ℵ₀ ≤ #(FreeGroup α)
⊢ max #α ℵ₀ ≤ #(FreeGroup α)

Tactic:
apply max_le

Premises used: max_le
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ #α ≤ #(FreeGroup α)

Tactic:
mk_le_of_injective FreeGroup.of_injective

Premises used: FreeGroup.of_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ #α ≤ #(FreeGroup α)

Tactic:
exact mk_le_of_injective FreeGroup.of_injective

Premises used: FreeGroup.of_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ ℵ₀ ≤ #(FreeGroup α)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
a : #(FreeGroup α) ≤ max #α ℵ₀
a₁ a₂ : max #α ℵ₀ ≤ #(FreeGroup α)
⊢ #(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

Premises used: Nat.cast_ofNat, Cardinal.mk_list_eq_max_mk_aleph0, Cardinal.mk, Cardinal.aleph0, Cardinal.mk_fintype, max_eq_right, le_antisymm, Cardinal.lift_uzero, max_eq_right_iff, max_le, Cardinal.lift_ofNat, FreeGroup.of_injective, Cardinal.mk_le_of_injective, lt_or_ge, Cardinal.mk_prod, Fintype.card_bool
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
rw : #(α →₀ ℤ) = max #α ℵ₀
⊢ #(FreeAbelianGroup α) = max #α ℵ₀

Tactic:
rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]

Premises used: FreeAbelianGroup.equivFinsupp, AddEquiv.toEquiv, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
⊢ #(α →₀ ℤ) = max #α ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inl : IsEmpty α → #(FreeRing α) = max #α ℵ₀
inr : Nonempty α → #(FreeRing α) = max #α ℵ₀
⊢ #(FreeRing α) = max #α ℵ₀

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
h : IsEmpty α
⊢ #(FreeRing α) = max #α ℵ₀

Tactic:
simp [FreeRing]

Premises used: FreeRing
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
h : Nonempty α
⊢ #(FreeRing α) = max #α ℵ₀

Tactic:
simp [FreeRing]

Premises used: FreeRing
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inl : IsEmpty α → #(FreeCommRing α) = max #α ℵ₀
inr : Nonempty α → #(FreeCommRing α) = max #α ℵ₀
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
h : IsEmpty α
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
simp [FreeCommRing]

Premises used: FreeCommRing
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
h : Nonempty α
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
simp [FreeCommRing]

Premises used: FreeCommRing
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
inl : ∀ (hR : Finite α), Nonempty.{u + 1} (CommRing α)
inr : ∀ (hR : Infinite α), Nonempty.{u + 1} (CommRing α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
obtain hR | hR := finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
inl : ∀ (x : Fintype α), Nonempty.{u + 1} (CommRing α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
obtain ⟨x⟩ := nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
⊢ Fintype.card α ≠ 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
⊢ NeZero (Fintype.card α)

Tactic:
have : NeZero (Fintype.card α) := ⟨by simp⟩
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
inl : ∀ (x_1 : Trunc (α ≃ Fin (Fintype.card α))) (e : α ≃ Fin (Fintype.card α)), Nonempty.{u + 1} (CommRing α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
obtain ⟨e⟩ := Fintype.truncEquivFin α

Premises used: Fintype.truncEquivFin
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
x_1 : Trunc (α ≃ Fin (Fintype.card α))
e : α ≃ Fin (Fintype.card α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
⟨open scoped Fin.CommRing in e.commRing⟩

Premises used: Equiv.commRing, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
x_1 : Trunc (α ≃ Fin (Fintype.card α))
e : α ≃ Fin (Fintype.card α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
exact ⟨open scoped Fin.CommRing in e.commRing⟩
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
inl : ∀ (x_1 : Trunc (α ≃ Fin (Fintype.card α))) (e : α ≃ Fin (Fintype.card α)), Nonempty.{u + 1} (CommRing α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
classical
    obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in e.commRing⟩
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Infinite α
⊢ Nonempty.{max 1 (u + 1)} (α ≃ FreeCommRing α)

Tactic:
simp [← Cardinal.eq]

Premises used: Cardinal.eq
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Infinite α
inr : ∀ (e : α ≃ FreeCommRing α), Nonempty.{u + 1} (CommRing α)
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Infinite α
e : α ≃ FreeCommRing α
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
⟨e.commRing⟩

Premises used: Equiv.commRing, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
inst : Nonempty α
hR : Infinite α
e : α ≃ FreeCommRing α
⊢ Nonempty.{u + 1} (CommRing α)

Tactic:
exact ⟨e.commRing⟩
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
⊢ Nonempty.{u + 1} (CommRing α) ↔ Nonempty α

Tactic:
⟨Nonempty.map (·.zero), fun _ => nonempty_commRing _⟩

Premises used: Zero.zero, Iff.intro, nonempty_commRing, Nonempty.map
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
⊢ Nonempty.{u + 1} (Ring α) ↔ Nonempty α

Tactic:
⟨Nonempty.map (·.zero), fun _ => (nonempty_commRing _).map (·.toRing)⟩

Premises used: Zero.zero, Iff.intro, nonempty_commRing, Nonempty.map
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
⊢ Nonempty.{u + 1} (CommSemiring α) ↔ Nonempty α

Tactic:
⟨Nonempty.map (·.zero), fun _ => (nonempty_commRing _).map (·.toCommSemiring)⟩

Premises used: Zero.zero, Iff.intro, nonempty_commRing, Nonempty.map
-- Module: Mathlib.SetTheory.Cardinal.Free
Goal:
α : Type u
⊢ Nonempty.{u + 1} (Semiring α) ↔ Nonempty α

Tactic:
⟨Nonempty.map (·.zero), fun _ => (nonempty_commRing _).map (·.toSemiring)⟩

Premises used: Zero.zero, Iff.intro, nonempty_commRing, Nonempty.map
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{u}
⊢ HasCardinalLT X κ ↔ Cardinal.mk X < κ

Tactic:
simp [HasCardinalLT]

Premises used: HasCardinalLT
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
⊢ 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

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
⊢ Small.{v, u} X

Tactic:
simpa only [Cardinal.small_iff_lift_mk_lt_univ] using h.trans (Cardinal.lift_lt_univ' κ)

Premises used: Cardinal.lift_lt_univ', Cardinal.small_iff_lift_mk_lt_univ, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
κ' : Cardinal.{v}
hκ' : κ ≤ κ'
⊢ Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ'

Tactic:
simpa only [Cardinal.lift_le] using hκ'

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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
rw : Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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
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} κ
⊢ 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

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
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:
lt_of_le_of_lt (Cardinal.mk_le_of_injective
    (Function.Injective.comp ULift.up_injective
      (Function.Injective.comp hf ULift.down_injective))) h

Premises used: lt_of_le_of_lt, ULift.up_injective, Function.Injective.comp, ULift.down_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
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:
exact lt_of_le_of_lt (Cardinal.mk_le_of_injective
    (Function.Injective.comp ULift.up_injective
      (Function.Injective.comp hf ULift.down_injective))) h

Premises used: lt_of_le_of_lt, ULift.up_injective, Function.Injective.comp, ULift.down_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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
rw : Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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
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} κ
⊢ 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

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
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:
lt_of_le_of_lt (Cardinal.mk_le_of_surjective
    (Function.Surjective.comp ULift.up_surjective (Function.Surjective.comp hf
      ULift.down_surjective))) h

Premises used: Cardinal.mk_le_of_surjective, lt_of_le_of_lt, ULift.down_surjective, ULift.up_surjective, Function.Surjective.comp
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{v}
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:
exact lt_of_le_of_lt (Cardinal.mk_le_of_surjective
    (Function.Surjective.comp ULift.up_surjective (Function.Surjective.comp hf
      ULift.down_surjective))) h

Premises used: Cardinal.mk_le_of_surjective, lt_of_le_of_lt, ULift.down_surjective, ULift.up_surjective, Function.Surjective.comp
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
e : X ≃ Y
κ : Cardinal.{v}
⊢ HasCardinalLT X κ ↔ HasCardinalLT Y κ

Tactic:
⟨fun h ↦ h.of_injective _ e.symm.injective,
    fun h ↦ h.of_injective _ e.injective⟩

Premises used: HasCardinalLT.of_injective, Iff.intro, Equiv.injective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
⊢ HasCardinalLT X Cardinal.aleph0 ↔ Finite X

Tactic:
simpa [HasCardinalLT] using Cardinal.mk_lt_aleph0_iff

Premises used: HasCardinalLT, Cardinal.mk_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
inst : Finite X
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
rwa rwa₁ rwa₂ rwa₃ : Finite X
⊢ HasCardinalLT X Cardinal.aleph0

Tactic:
rwa [hasCardinalLT_aleph0_iff]

Premises used: hasCardinalLT_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type v
κ : Cardinal.{w}
⊢ HasCardinalLT X (Cardinal.lift.{u, w} κ) ↔ HasCardinalLT X κ

Tactic:
simp [HasCardinalLT, ← (Cardinal.lift_strictMono.{max v w, max u}).lt_iff_lt]

Premises used: HasCardinalLT
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type v
κ : Cardinal.{w}
⊢ HasCardinalLT (ULift.{u, v} X) κ ↔ HasCardinalLT X κ

Tactic:
hasCardinalLT_iff_of_equiv Equiv.ulift κ

Premises used: hasCardinalLT_iff_of_equiv, Equiv.ulift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
mp : HasCardinalLT (X ⊕ Y) κ → HasCardinalLT X κ ∧ HasCardinalLT Y κ
mpr : HasCardinalLT X κ ∧ HasCardinalLT Y κ → HasCardinalLT (X ⊕ Y) κ
⊢ HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT (X ⊕ Y) κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
⟨h.of_injective _ Sum.inl_injective,
      h.of_injective _ Sum.inr_injective⟩

Premises used: Sum.inr_injective, Sum.inl_injective, HasCardinalLT.of_injective, And.intro
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT (X ⊕ Y) κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
exact ⟨h.of_injective _ Sum.inl_injective,
      h.of_injective _ Sum.inr_injective⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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.{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

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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} κ
hX₁ : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
⊢ Cardinal.lift.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at hX

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
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.{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

Premises used: Cardinal.lift_lift