-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem ACF_categorical {p : ℕ} (κ : Cardinal) (hκ : ℵ₀ < κ) :
    Categorical κ (Theory.ACF p)

Proof state:
case mk.mk.val.a.refine_1
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ ℵ₀ < κ

Tactic:
exact hκ

Result:
no goals

Proof state:
case mk.mk.val.a.refine_2
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃ ↑(Theory.ModelType.mk N))

Tactic:
rw [← Cardinal.eq, hM, hN]

Result:
no goals

Proof state:
case mk.mk
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝² : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝¹ : IsAlgClosed M
this✝ : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Tactic:
have := isAlgClosed_of_model_ACF p N

Result:
case mk.mk
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝³ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝² : IsAlgClosed M
this✝¹ : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this : IsAlgClosed N
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Proof state:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
⊢ κ.Categorical (Theory.ACF p)

Tactic:
rintro ⟨M⟩ ⟨N⟩ hM hN

Result:
case mk.mk
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Proof state:
case mk.mk.val
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ ↑(Theory.ModelType.mk M) ≃+* ↑(Theory.ModelType.mk N)

Tactic:
apply Classical.choice

Result:
case mk.mk.val.a
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃+* ↑(Theory.ModelType.mk N))

Proof state:
case mk.mk.val.a
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃+* ↑(Theory.ModelType.mk N))

Tactic:
refine IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_

Result:
case mk.mk.val.a.refine_1
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ ℵ₀ < #↑(Theory.ModelType.mk M)

case mk.mk.val.a.refine_2
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑(Theory.ModelType.mk M) = κ
hN : #↑(Theory.ModelType.mk N) = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃ ↑(Theory.ModelType.mk N))