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

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

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

Tactic:
constructor

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

Tactic:
have := charP_of_model_fieldOfChar 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
this : CharP M p
⊢ 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
x✝ : Field N := fieldOfModelACF p N
this : N ⊨ Theory.field
⊢ Nonempty (↑(Theory.ModelType.mk M) ≃[Language.ring] ↑(Theory.ModelType.mk N))

Tactic:
let _ := compatibleRingOfModelField 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
⊢ 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
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))

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