awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ ∃ (x : K), eval x p = 0
have this : K ⊨ genericMonicPolyHasRoot p.natDegree
Tactic: have := h _ p.natDegree (natDegree_pos_iff_degree_pos.2
    (degree_pos_of_irreducible hpi)) rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∃ (x : K), eval x p = 0
have this₁ : ∀ (p_2 : { p_2 : K[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }), ∃ (x : K), eval x (↑p_2 : K[X]) = 0
Tactic: rw [realize_genericMonicPolyHasRoot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
⊢ (Theory.ACF p).IsSatisfiable
have this : Fact (Nat.Prime p)
Tactic: have : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : p = 0
⊢ (Theory.ACF p).IsSatisfiable
have inr : (Theory.ACF 0).IsSatisfiable
Tactic: subst hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable
have inl : ∀ (hp : Nat.Prime p), (Theory.ACF p).IsSatisfiable
Tactic: cases hp with
  | inl hp =>
    have : Fact p.Prime := ⟨hp⟩
    let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
    exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
  | inr hp =>
    subst hp
    let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
    exact ⟨⟨AlgebraicClosure ℚ⟩⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
inl : ∀ (hp : Nat.Prime p), (Theory.ACF p).IsSatisfiable
⊢ (Theory.ACF p).IsSatisfiable
have inr : ∀ (hp : p = 0), (Theory.ACF p).IsSatisfiable
Tactic: cases hp with
  | inl hp =>
    have : Fact p.Prime := ⟨hp⟩
    let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
    exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
  | inr hp =>
    subst hp
    let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
    exact ⟨⟨AlgebraicClosure ℚ⟩⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have this : M ⊨ Theory.field
Tactic: have := modelField_of_modelACF p M
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have this₁ : IsAlgClosed M
Tactic: have := isAlgClosed_of_model_ACF p M
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this : IsAlgClosed M
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have this₁ : CharP M p
Tactic: have := charP_of_model_fieldOfChar p M
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this : CharP M p
x_2 : Field N := fieldOfModelACF p N
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have this₁ : N ⊨ Theory.field
Tactic: have := modelField_of_modelACF p N
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have this₁ : IsAlgClosed N
Tactic: have := isAlgClosed_of_model_ACF p N
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this : IsAlgClosed N
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have this₁ : CharP N p
Tactic: have := charP_of_model_fieldOfChar p N
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have val : (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
  (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
have val : (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+* (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
Tactic: refine languageEquivEquivRingEquiv.symm ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
have val : Nonempty.{u_2 + 1}
  ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
Tactic: apply Classical.choice
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have val : ℵ₀ < #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2)
Tactic: refine IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val : ℵ₀ < #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2)
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have val₁ : Nonempty.{u_2 + 1}
  ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
Tactic: refine IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have val : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
Tactic: rw [← Cardinal.eq, hM, hN]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val :
  #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) =
    #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have val₁ : κ = #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
Tactic: rw [← Cardinal.eq, hM, hN]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
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_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val :
  #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) =
    #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
val₁ : κ = #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
have val₂ : κ = κ
Tactic: rw [← Cardinal.eq, hM, hN]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsComplete
have h2 : Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)
Tactic: apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _
    (ACF_categorical _ (Order.lt_succ _))
    (Order.le_succ ℵ₀)
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
h2 : Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)
⊢ (Theory.ACF p).IsComplete
have hS : (Theory.ACF p).IsSatisfiable
Tactic: apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _
    (ACF_categorical _ (Order.lt_succ _))
    (Order.le_succ ℵ₀)
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
h2 : Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)
hS : (Theory.ACF p).IsSatisfiable
⊢ (Theory.ACF p).IsComplete
have hT : ∀ (M : (Theory.ACF p).ModelType), Infinite (↑M : Type)
Tactic: apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _
    (ACF_categorical _ (Order.lt_succ _))
    (Order.le_succ ℵ₀)
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)
have h2 : 5 ≤ Order.succ ℵ₀
Tactic: simp only [card_ring, lift_id']
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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 (T := Theory.ACF p) M) : Type)
have this : M ⊨ Theory.field
Tactic: have := modelField_of_modelACF p M
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
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_1 : CompatibleRing M := compatibleRingOfModelField M
⊢ Infinite (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type)
have this₁ : IsAlgClosed M
Tactic: have := isAlgClosed_of_model_ACF p M
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
h : Theory.ACF 0 ⊨ᵇ φ
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
have h₁ : ∃ (T0 : Finset Language.ring.Sentence),
  (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0 ∧ (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
Tactic: rw [Theory.models_iff_finset_models] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
h :
  ∃ (T0 : Finset Language.ring.Sentence),
    (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0 ∧ (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
have rcases : ∀ (T0 : Finset Language.ring.Sentence) (hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0)
  (h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ),
  Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
Tactic: rcases h with ⟨T0, hT0, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.ACF 0
⊢ { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
have hψ₁ : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
  ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ
Tactic: rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ
Cleared hypotheses: hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
    ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ
⊢ { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
have a : Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
Tactic: apply Classical.choice
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
    ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
have a : ∀ (h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}),
  Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
Tactic: rcases hψ with h | ⟨p, hp, rfl⟩
Cleared hypotheses: hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
    ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ
a :
  ∀ (h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}),
    Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
have a₁ : ∀ (p : ℕ) (hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p),
  Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p) }
Tactic: rcases hψ with h | ⟨p, hp, rfl⟩
Cleared hypotheses: ψ, hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
have a : ∀ q ∉ ∅, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ
Tactic: refine ⟨⟨∅, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
q : Nat.Primes
h_2 : q ∉ ∅
⊢ ψ ∈ Theory.ACF (↑q : ℕ)
have rw : ψ ∈
  Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∪
    if (↑q : ℕ) = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
    else if Nat.Prime (↑q : ℕ) then {eqZero (↑q : ℕ)} else {⊥}
Tactic: rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm]