-- Mathlib/SetTheory/Cardinal/Subfield.lean
lemma cardinalMk_closure_le_max : #(closure s) ≤ max #s ℵ₀ :=
  (Cardinal.mk_le_of_surjective <| surjective_ofWType s).trans <| by
    convert WType.cardinalMk_le_max_aleph0_of_finite' using 1
    · rw [lift_uzero, mk_sum, lift_uzero]
      have : lift.{u,0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)
      obtain h|h := lt_or_le #s ℵ₀
      · rw [max_eq_right h.le, max_eq_right]
        exact (add_lt_aleph0 this h).le
      · rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
    rintro (n|_)
    · fin_cases n <;> (dsimp only [id_eq]; infer_instance)
    infer_instance

Proof state:
case h.e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #↑s ≤ ℵ₀

Tactic:
exact (add_lt_aleph0 this h).le

Result:
no goals

Proof state:
case convert_3
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ (a : Fin 6 ⊕ ↑s), Finite (Subfield.Operands s a)

Tactic:
rintro (n|_)

Result:
case convert_3.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
n : Fin 6
⊢ Finite (Subfield.Operands s (Sum.inl n))

case convert_3.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
val✝ : ↑s
⊢ Finite (Subfield.Operands s (Sum.inr val✝))

Proof state:
case convert_3.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
n : Fin 6
⊢ Finite (Subfield.Operands s (Sum.inl n))

Tactic:
fin_cases n <;> (dsimp only [id_eq]; infer_instance)

Result:
no goals

Proof state:
case h.e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #↑s ⊔ ℵ₀ = lift.{0, u} #(Fin 6 ⊕ ↑s) ⊔ ℵ₀

Tactic:
rw [lift_uzero, mk_sum, lift_uzero]

Result:
case h.e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

Proof state:
case convert_3.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
val✝ : ↑s
⊢ Finite (Subfield.Operands s (Sum.inr val✝))

Tactic:
infer_instance

Result:
no goals

Proof state:
case h.e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

Tactic:
rw [max_eq_right h.le, max_eq_right]

Result:
case h.e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #↑s ≤ ℵ₀

Proof state:
case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Subfield.Operands s (Sum.inl ((fun i => i) ⟨5, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Result:
case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Subfield.Operands s (Sum.inl ⟨5, ⋯⟩))

Proof state:
case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Subfield.Operands s (Sum.inl ⟨5, ⋯⟩))

Tactic:
infer_instance

Result:
no goals

Proof state:
case h.e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

Tactic:
have : lift.{u,0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)

Result:
case h.e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #(WType (Subfield.Operands s)) ≤ #↑s ⊔ ℵ₀

Tactic:
convert WType.cardinalMk_le_max_aleph0_of_finite' using 1

Result:
case h.e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #↑s ⊔ ℵ₀ = lift.{0, u} #(Fin 6 ⊕ ↑s) ⊔ ℵ₀

case convert_3
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ (a : Fin 6 ⊕ ↑s), Finite (Subfield.Operands s a)

Proof state:
case h.e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

Tactic:
rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]

Result:
no goals

Proof state:
case h.e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

Tactic:
obtain h|h := lt_or_le #s ℵ₀

Result:
case h.e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀

case h.e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ #↑s ⊔ ℵ₀ = (lift.{u, 0} #(Fin 6) + #↑s) ⊔ ℵ₀