case a
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ Nonempty (K ≃+* L)
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
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
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
case a
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ Nonempty (K ≃+* L)
cases' exists_isTranscendenceBasis (ZMod p)
  (show Function.Injective (algebraMap (ZMod p) K) from RingHom.injective _) with s hs
case a.intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
case a.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
cases' exists_isTranscendenceBasis (ZMod p)
  (show Function.Injective (algebraMap (ZMod p) L) from RingHom.injective _) with t ht
case a.intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) 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
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
have : (#s) = (#t) := by
  rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs
    (lt_aleph0_of_finite (ZMod p)).le hK,
    ← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht
      (lt_aleph0_of_finite (ZMod p)).le, hKL]
  rwa [← hKL]
case a.intro.intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) 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
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) 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
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) 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
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < (#L)
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ (#↑s) = (#↑t)
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs
  (lt_aleph0_of_finite (ZMod p)).le hK,
  ← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht
    (lt_aleph0_of_finite (ZMod p)).le, hKL]
no goals
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < (#L)
rwa [← hKL]