case a
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
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✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ K ≃+* L
apply Classical.choice
case a.inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)

case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
hp : p = 0
⊢ Nonempty (K ≃+* L)
case a
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
⊢ Nonempty (K ≃+* L)
rcases CharP.char_is_prime_or_zero K p with (hp | hp)
case a.inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ Nonempty (K ≃+* L)
case a.inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)
haveI : Fact p.Prime := ⟨hp⟩
no goals
case a.inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ Nonempty (K ≃+* L)
exact ⟨ringEquivOfCardinalEqOfCharP p hK hKL⟩
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
⊢ Nonempty (K ≃+* L)
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
hp : p = 0
⊢ Nonempty (K ≃+* L)
simp only [hp] at *
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this : CharZero K := CharP.charP_to_charZero K
⊢ Nonempty (K ≃+* L)
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
⊢ Nonempty (K ≃+* L)
letI : CharZero K := CharP.charP_to_charZero K
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this✝ : CharZero K := CharP.charP_to_charZero K
this : CharZero L := CharP.charP_to_charZero L
⊢ Nonempty (K ≃+* L)
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this : CharZero K := CharP.charP_to_charZero K
⊢ Nonempty (K ≃+* L)
letI : CharZero L := CharP.charP_to_charZero L
no goals
case a.inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < (#K)
hKL : (#K) = (#L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this✝ : CharZero K := CharP.charP_to_charZero K
this : CharZero L := CharP.charP_to_charZero L
⊢ Nonempty (K ≃+* L)
exact ⟨ringEquivOfCardinalEqOfCharZero hK hKL⟩