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

Proof state:
case inr

⊢ (Theory.ACF 0).IsSatisfiable

Tactic:
let _ := compatibleRingOfRing (AlgebraicClosure ℚ)

Result:
case inr
x✝ : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
⊢ (Theory.ACF 0).IsSatisfiable

Proof state:
case inl
p : ℕ
hp : Nat.Prime p
this✝ : Fact (Nat.Prime p)
x✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩

Result:
no goals

Proof state:
case inr
x✝ : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
this : CharP (AlgebraicClosure ℚ) 0
⊢ (Theory.ACF 0).IsSatisfiable

Tactic:
exact ⟨⟨AlgebraicClosure ℚ⟩⟩

Result:
no goals

Proof state:
case inl
p : ℕ
hp : Nat.Prime p
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
have : Fact p.Prime := ⟨hp⟩

Result:
case inl
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ (Theory.ACF p).IsSatisfiable

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

Tactic:
cases hp with
| inl hp =>
  have : Fact p.Prime := ⟨hp⟩
  let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
  have : CharP (AlgebraicClosure (ZMod p)) p :=
    charP_of_injective_algebraMap
      (RingHom.injective (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) p
  exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
| inr hp =>
  subst hp
  let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
  have : CharP (AlgebraicClosure ℚ) 0 :=
    charP_of_injective_algebraMap
      (RingHom.injective (algebraMap ℚ (AlgebraicClosure ℚ))) 0
  exact ⟨⟨AlgebraicClosure ℚ⟩⟩

Result:
no goals

Proof state:
case inr
p : ℕ
hp : p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
subst hp

Result:
case inr

⊢ (Theory.ACF 0).IsSatisfiable

Proof state:
case inr
x✝ : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
⊢ (Theory.ACF 0).IsSatisfiable

Tactic:
have : CharP (AlgebraicClosure ℚ) 0 :=
  charP_of_injective_algebraMap
    (RingHom.injective (algebraMap ℚ (AlgebraicClosure ℚ))) 0

Result:
case inr
x✝ : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
this : CharP (AlgebraicClosure ℚ) 0
⊢ (Theory.ACF 0).IsSatisfiable

Proof state:
case inl
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))

Result:
case inl
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
x✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ (Theory.ACF p).IsSatisfiable

Proof state:
case inl
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
x✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
have : CharP (AlgebraicClosure (ZMod p)) p :=
  charP_of_injective_algebraMap
    (RingHom.injective (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) p

Result:
case inl
p : ℕ
hp : Nat.Prime p
this✝ : Fact (Nat.Prime p)
x✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
⊢ (Theory.ACF p).IsSatisfiable