-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem ACF_isComplete {p : ℕ} (hp : p.Prime ∨ p = 0) :
    (Theory.ACF p).IsComplete

Proof state:
case hS
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
exact ACF_isSatisfiable hp

Result:
no goals

Proof state:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
⊢ Infinite ↑(Theory.ModelType.mk M)

Tactic:
let _ := fieldOfModelACF p M

Result:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝ : Field M := fieldOfModelACF p M
⊢ Infinite ↑(Theory.ModelType.mk M)

Proof state:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsComplete

Tactic:
apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _
  (ACF_categorical _ (Order.lt_succ _))
  (Order.le_succ ℵ₀)

Result:
case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)

case hS
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ ∀ (M : (Theory.ACF p).ModelType), Infinite ↑M

Proof state:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝¹ : Field M := fieldOfModelACF p M
this✝ : M ⊨ Theory.field
x✝ : CompatibleRing M := compatibleRingOfModelField M
this : IsAlgClosed M
⊢ Infinite ↑(Theory.ModelType.mk M)

Tactic:
infer_instance

Result:
no goals

Proof state:
case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ 5 ≤ Order.succ ℵ₀

Tactic:
exact le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)

Result:
no goals

Proof state:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝ : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
⊢ Infinite ↑(Theory.ModelType.mk M)

Tactic:
let _ := compatibleRingOfModelField M

Result:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝¹ : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
x✝ : CompatibleRing M := compatibleRingOfModelField M
⊢ Infinite ↑(Theory.ModelType.mk M)

Proof state:
case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ ∀ (M : (Theory.ACF p).ModelType), Infinite ↑M

Tactic:
rintro ⟨M⟩

Result:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
⊢ Infinite ↑(Theory.ModelType.mk M)

Proof state:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝ : Field M := fieldOfModelACF p M
⊢ Infinite ↑(Theory.ModelType.mk M)

Tactic:
have := modelField_of_modelACF p M

Result:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝ : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
⊢ Infinite ↑(Theory.ModelType.mk M)

Proof state:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝¹ : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
x✝ : CompatibleRing M := compatibleRingOfModelField M
⊢ Infinite ↑(Theory.ModelType.mk M)

Tactic:
have := isAlgClosed_of_model_ACF p M

Result:
case hT.mk
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝¹ : Field M := fieldOfModelACF p M
this✝ : M ⊨ Theory.field
x✝ : CompatibleRing M := compatibleRingOfModelField M
this : IsAlgClosed M
⊢ Infinite ↑(Theory.ModelType.mk M)

Proof state:
case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)

Tactic:
simp only [card_ring, lift_id']

Result:
case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ 5 ≤ Order.succ ℵ₀