-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem lift_cardinalMk_adjoin_le {E : Type v} [Field E] [Algebra F E] (s : Set E) :
    Cardinal.lift.{u} #(adjoin F s) ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} #s ⊔ ℵ₀

Proof state:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↥(adjoin F s) ≤ Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
rw [show ↥(adjoin F s) = (adjoin F s).toSubfield from rfl, adjoin_toSubfield]

Result:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↥(Subfield.closure (Set.range ⇑(algebraMap F E) ∪ s)) ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Proof state:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} (#↑(Set.range ⇑(algebraMap F E) ∪ s) ⊔ ℵ₀) ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
rw [lift_max, sup_le_iff, lift_aleph0]

Result:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s) ≤ Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀ ∧
    ℵ₀ ≤ Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Proof state:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s) ≤ Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀ ∧
    ℵ₀ ≤ Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
refine ⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩

Result:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} (#↑(Set.range ⇑(algebraMap F E)) ⊔ #↑s ⊔ ℵ₀) ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Proof state:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} (#↑(Set.range ⇑(algebraMap F E)) ⊔ #↑s ⊔ ℵ₀) ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
simp_rw [lift_max, lift_aleph0, sup_assoc]

Result:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E)) ⊔ (Cardinal.lift.{u, v} #↑s ⊔ ℵ₀) ≤
    Cardinal.lift.{v, u} #F ⊔ (Cardinal.lift.{u, v} #↑s ⊔ ℵ₀)

Proof state:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E)) ⊔ (Cardinal.lift.{u, v} #↑s ⊔ ℵ₀) ≤
    Cardinal.lift.{v, u} #F ⊔ (Cardinal.lift.{u, v} #↑s ⊔ ℵ₀)

Tactic:
exact sup_le_sup_right mk_range_le_lift _

Result:
no goals

Proof state:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↥(Subfield.closure (Set.range ⇑(algebraMap F E) ∪ s)) ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
apply (Cardinal.lift_le.mpr (Subfield.cardinalMk_closure_le_max _)).trans

Result:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} (#↑(Set.range ⇑(algebraMap F E) ∪ s) ⊔ ℵ₀) ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑s ⊔ ℵ₀