-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem ringEquiv_of_equiv_of_charZero [CharZero K] [CharZero L] (hK : ℵ₀ < #K)
    (hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L)

Proof state:
case intro.intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)

Tactic:
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩

Result:
no goals

Proof state:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨s, hs⟩ := exists_isTranscendenceBasis ℤ
  (show Function.Injective (algebraMap ℤ K) from Int.cast_injective)

Result:
case intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)

Proof state:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < #L

Tactic:
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]

Result:
no goals

Proof state:
case intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)

Tactic:
have hL : ℵ₀ < #L := by
  rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]

Result:
case intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Nonempty (K ≃+* L)

Proof state:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t

Tactic:
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
    hs (le_of_eq mk_int) hK),
  ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
    ht (le_of_eq mk_int) hL)]

Result:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Proof state:
case intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Nonempty (K ≃+* L)

Tactic:
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
  rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
      hs (le_of_eq mk_int) hK),
    ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
      ht (le_of_eq mk_int) hL)]
  exact Cardinal.lift_mk_eq'.2 hKL

Result:
case intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
⊢ Nonempty (K ≃+* L)

Proof state:
case intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨t, ht⟩ := exists_isTranscendenceBasis ℤ
  (show Function.Injective (algebraMap ℤ L) from Int.cast_injective)

Result:
case intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)

Proof state:
case intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this

Result:
case intro.intro.intro
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)

Proof state:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Tactic:
exact Cardinal.lift_mk_eq'.2 hKL

Result:
no goals