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

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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Tactic:
have := modelField_of_modelACF 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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Tactic:
let _ := compatibleRingOfModelField M

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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Tactic:
let _ := fieldOfModelACF 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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

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
⊢ ℵ₀ < #↑(Theory.ModelType.mk M)

Tactic:
rw [hM]

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
⊢ ℵ₀ < κ

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
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Tactic:
have := isAlgClosed_of_model_ACF p M

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
⊢ 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) ≃[Language.ring] ↑(Theory.ModelType.mk N)

Tactic:
refine languageEquivEquivRingEquiv.symm ?_

Result:
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)