-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt [Nontrivial R]
    (hv : IsTranscendenceBasis R v) (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K) :
    Cardinal.lift.{w} #K = Cardinal.lift.{v} #ι :=
  have : ℵ₀ ≤ Cardinal.lift.{max u v} #ι := le_of_not_lt fun h => not_le_of_gt
    (show ℵ₀ < Cardinal.lift.{max u w} #K by simpa) <|
    calc
      Cardinal.lift.{max u w, v} #K ≤ max (max (Cardinal.lift.{max v w, u} #R)
        (Cardinal.lift.{max u v, w} #ι)) ℵ₀ := cardinal_le_max_transcendence_basis v hv
      _ ≤ _ := max_le (max_le (by simpa) (by simpa using le_of_lt h)) le_rfl
  suffices Cardinal.lift.{max u w} #K = Cardinal.lift.{max u v} #ι
    from Cardinal.lift_injective.{u, max v w} (by simpa)
  le_antisymm
    (calc
      Cardinal.lift.{max u w} #K ≤ max (max
        (Cardinal.lift.{max v w} #R) (Cardinal.lift.{max u v} #ι)) ℵ₀ :=
        cardinal_le_max_transcendence_basis v hv
      _ = Cardinal.lift #ι

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max u v, w} #ι ≤ ℵ₀

Tactic:
simpa using le_of_lt h

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
simpa using hR

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι

Tactic:
exact le_trans (by simpa using hR) this

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ⊔ Cardinal.lift.{max u v, w} #ι ⊔ ℵ₀ = Cardinal.lift.{max u v, w} #ι

Tactic:
rw [max_eq_left, max_eq_right]

Result:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι

R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ Cardinal.lift.{max v w, u} #R ⊔ Cardinal.lift.{max u v, w} #ι

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ ℵ₀ < Cardinal.lift.{max u w, v} #K

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this✝ : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
this : Cardinal.lift.{max u w, v} #K = Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{u, max v w} (Cardinal.lift.{w, v} #K) = Cardinal.lift.{u, max v w} (Cardinal.lift.{v, w} #ι)

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ Cardinal.lift.{max v w, u} #R ⊔ Cardinal.lift.{max u v, w} #ι

Tactic:
exact le_max_of_le_right this

Result:
no goals