case a
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ Nonempty (K ≃+* L)
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ K ≃+* L
apply Classical.choice
case a.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
case a
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ Nonempty (K ≃+* L)
cases' exists_isTranscendenceBasis ℤ
  (show Function.Injective (algebraMap ℤ K) from Int.cast_injective) with s hs
case a.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
case a.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
cases' exists_isTranscendenceBasis ℤ
  (show Function.Injective (algebraMap ℤ L) from Int.cast_injective) with t ht
case a.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : (#↑s) = (#↑t)
⊢ Nonempty (K ≃+* L)
case a.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
have : (#s) = (#t) := by
  rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
    cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
  rwa [← hKL]
case a.intro.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : (#↑s) = (#↑t)
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)
case a.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : (#↑s) = (#↑t)
⊢ Nonempty (K ≃+* L)
cases' Cardinal.eq.1 this with e
no goals
case a.intro.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : (#↑s) = (#↑t)
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < (#L)
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ (#↑s) = (#↑t)
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
  cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
no goals
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < (#L)
rwa [← hKL]