awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ leftDistrib.toSentence ↔ toProp K leftDistrib

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ existsPairNE.toSentence ↔ toProp K existsPairNE

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
inst_6 : K ⊨ Theory.field
ax : FieldAxiom
⊢ toProp K ax

Tactic:
(FieldAxiom.realize_toSentence_iff_toProp ax).1
    (Theory.realize_sentence_of_mem Theory.field
      (Set.mem_range_self ax))

Premises used: Set.mem_range_self, FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp, Iff.mp, FirstOrder.Language.Theory.field, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
simp : ∀ (φ : ring.Sentence) (x : FieldAxiom), x.toSentence = φ → K ⊨ φ
⊢ ∀ φ ∈ Theory.field, K ⊨ φ

Tactic:
simp only [Theory.field, Set.mem_range, exists_imp]

Premises used: Set.mem_range, exists_imp, FirstOrder.Language.Theory.field
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
a : FieldAxiom
rw : toProp K a
⊢ K ⊨ a.toSentence

Tactic:
rw [a.realize_toSentence_iff_toProp (K := K)]

Premises used: FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K existsPairNE

Tactic:
exists_pair_ne K

Premises used: FirstOrder.Field.FieldAxiom.toProp, exists_pair_ne
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K existsPairNE

Tactic:
exact exists_pair_ne K

Premises used: exists_pair_ne
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K existsInv

Tactic:
fun x hx0 => ⟨x⁻¹, mul_inv_cancel₀ hx0⟩

Premises used: mul_inv_cancel₀, FirstOrder.Field.FieldAxiom.toProp, Inv.inv, Exists.intro
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K existsInv

Tactic:
exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel₀ hx0⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K addAssoc

Tactic:
add_assoc

Premises used: add_assoc, FirstOrder.Field.FieldAxiom.toProp
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K addAssoc

Tactic:
exact add_assoc

Premises used: add_assoc
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K zeroAdd

Tactic:
zero_add

Premises used: zero_add, FirstOrder.Field.FieldAxiom.toProp
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K zeroAdd

Tactic:
exact zero_add

Premises used: zero_add
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K negAddCancel

Tactic:
neg_add_cancel

Premises used: FirstOrder.Field.FieldAxiom.toProp, neg_add_cancel
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K negAddCancel

Tactic:
exact neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K mulAssoc

Tactic:
mul_assoc

Premises used: mul_assoc, FirstOrder.Field.FieldAxiom.toProp
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K mulAssoc

Tactic:
exact mul_assoc

Premises used: mul_assoc
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K mulComm

Tactic:
mul_comm

Premises used: FirstOrder.Field.FieldAxiom.toProp, mul_comm
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K mulComm

Tactic:
exact mul_comm

Premises used: mul_comm
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K oneMul

Tactic:
one_mul

Premises used: FirstOrder.Field.FieldAxiom.toProp, one_mul
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K oneMul

Tactic:
exact one_mul

Premises used: one_mul
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K leftDistrib

Tactic:
mul_add

Premises used: FirstOrder.Field.FieldAxiom.toProp, mul_add
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ toProp K leftDistrib

Tactic:
exact mul_add

Premises used: mul_add
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
a : FieldAxiom
existsPairNE : toProp K FieldAxiom.existsPairNE
existsInv : toProp K FieldAxiom.existsInv
addAssoc : toProp K FieldAxiom.addAssoc
zeroAdd : toProp K FieldAxiom.zeroAdd
negAddCancel : toProp K FieldAxiom.negAddCancel
mulAssoc : toProp K FieldAxiom.mulAssoc
mulComm : toProp K FieldAxiom.mulComm
oneMul : toProp K FieldAxiom.oneMul
leftDistrib : toProp K FieldAxiom.leftDistrib
⊢ toProp K a

Tactic:
cases a with
      | existsPairNE => exact exists_pair_ne K
      | existsInv => exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel₀ hx0⟩
      | addAssoc => exact add_assoc
      | zeroAdd => exact zero_add
      | negAddCancel => exact neg_add_cancel
      | mulAssoc => exact mul_assoc
      | mulComm => exact mul_comm
      | oneMul => exact one_mul
      | leftDistrib => exact mul_add

Premises used: add_assoc, mul_assoc, FirstOrder.Field.FieldAxiom.leftDistrib, FirstOrder.Field.FieldAxiom.existsPairNE, FirstOrder.Field.FieldAxiom.oneMul, FirstOrder.Field.FieldAxiom.mulAssoc, zero_add, FirstOrder.Field.FieldAxiom.zeroAdd, neg_add_cancel, FirstOrder.Field.FieldAxiom.mulComm, FirstOrder.Field.FieldAxiom.addAssoc, mul_comm, mul_add, FirstOrder.Field.FieldAxiom.negAddCancel, FirstOrder.Field.FieldAxiom.existsInv, one_mul, exists_pair_ne
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : CommRing K
inst_1 : CompatibleRing K
n : ℕ
v : Empty → K
⊢ Formula.Realize (eqZero n) v ↔ Eq.{u_1 + 1} (α := K) (↑n : K) 0

Tactic:
simp [eqZero]

Premises used: FirstOrder.Field.eqZero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K p
⊢ K ⊨ Theory.fieldOfChar p

Tactic:
Language.Theory.model_union_iff.2 ⟨inferInstance, ?_⟩

Premises used: Iff.mpr, FirstOrder.Language.Theory.model_union_iff, inferInstance, FirstOrder.Language.Theory.fieldOfChar, And.intro
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K p
refine :
  Theory.Model (L := ring) K
    (if p = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥})
⊢ K ⊨ Theory.fieldOfChar p

Tactic:
refine Language.Theory.model_union_iff.2 ⟨inferInstance, ?_⟩

Premises used: Iff.mpr, FirstOrder.Language.Theory.model_union_iff, inferInstance, And.intro
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K p
hp : Nat.Prime p
⊢ Theory.Model (L := ring) K
    (if p = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥})

Tactic:
simp [hp.ne_zero, hp, Sentence.Realize]

Premises used: FirstOrder.Language.Sentence.Realize, Nat.Prime.ne_zero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K p
hp : p = 0
inr :
  ∀ [CharP K 0],
    Theory.Model (L := ring) K
      (if Eq (α := ℕ) 0 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
      else if Nat.Prime 0 then {eqZero 0} else {⊥})
⊢ Theory.Model (L := ring) K
    (if p = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥})

Tactic:
subst hp
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K 0
inr : CharZero K
⊢ Theory.Model (L := ring) K
    (if Eq (α := ℕ) 0 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
    else if Nat.Prime 0 then {eqZero 0} else {⊥})

Tactic:
simp only [ite_true, Theory.model_iff, Set.mem_image, Set.mem_setOf_eq,
      Sentence.Realize, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
      Formula.realize_not, realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Field.realize_eqZero, and_imp, FirstOrder.Language.Theory.model_iff, Set.mem_image, forall_exists_index, CharZero.charZero_iff_forall_prime_ne_zero, Set.mem_setOf_eq, ite_true, FirstOrder.Language.Formula.realize_not, forall_apply_eq_imp_iff₂
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K 0
⊢ CharZero K

Tactic:
CharP.charP_to_charZero K

Premises used: CharP.charP_to_charZero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K 0
⊢ CharZero K

Tactic:
exact CharP.charP_to_charZero K

Premises used: CharP.charP_to_charZero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K p
⊢ Nat.Prime p ∨ p = 0

Tactic:
cases CharP.char_is_prime_or_zero K p with
  | inl hp =>
    simp [hp.ne_zero, hp, Sentence.Realize]
  | inr hp =>
    subst hp
    simp only [ite_true, Theory.model_iff, Set.mem_image, Set.mem_setOf_eq,
      Sentence.Realize, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
      Formula.realize_not, realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]
    exact CharP.charP_to_charZero K

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Field.realize_eqZero, and_imp, FirstOrder.Language.Theory.model_iff, Set.mem_image, forall_exists_index, CharZero.charZero_iff_forall_prime_ne_zero, Set.mem_setOf_eq, ite_true, CharP.char_is_prime_or_zero, FirstOrder.Language.Formula.realize_not, forall_apply_eq_imp_iff₂
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ K ⊨ Theory.field

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
simp :
  Theory.Model (L := ring) K
      (if p = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
      else if Nat.Prime p then {eqZero p} else {⊥}) ↔
    CharP K p
⊢ K ⊨ Theory.fieldOfChar p ↔ CharP K p

Tactic:
simp only [Theory.fieldOfChar, Theory.model_union_iff,
    (show (Theory.field.Model K) by infer_instance), true_and]

Premises used: FirstOrder.Language.Theory.model_union_iff, FirstOrder.Language.Theory.fieldOfChar, true_and
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
pos : ∀ (hp0 : p = 0), Theory.Model (L := ring) K ((fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}) ↔ CharP K p
pos₁ : ∀ (hp0 : ¬p = 0) (hp : Nat.Prime p), Theory.Model (L := ring) K {eqZero p} ↔ CharP K p
neg : ∀ (hp0 : ¬p = 0) (hp : ¬Nat.Prime p), Theory.Model (L := ring) K {⊥} ↔ CharP K p
⊢ Theory.Model (L := ring) K
      (if p = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
      else if Nat.Prime p then {eqZero p} else {⊥}) ↔
    CharP K p

Tactic:
split_ifs with hp0 hp
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
hp0 : p = 0
pos : Theory.Model (L := ring) K ((fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}) ↔ CharP K 0
⊢ Theory.Model (L := ring) K ((fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}) ↔ CharP K p

Tactic:
subst hp0
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
pos : CharZero K ↔ CharP K 0
⊢ Theory.Model (L := ring) K ((fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}) ↔ CharP K 0

Tactic:
simp only [Theory.model_iff, Set.mem_image, Set.mem_setOf_eq, Sentence.Realize,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Formula.realize_not,
      realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Field.realize_eqZero, and_imp, FirstOrder.Language.Theory.model_iff, Set.mem_image, forall_exists_index, CharZero.charZero_iff_forall_prime_ne_zero, Set.mem_setOf_eq, FirstOrder.Language.Formula.realize_not, forall_apply_eq_imp_iff₂
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ CharZero K ↔ CharP K 0

Tactic:
⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩

Premises used: CharP.charP_to_charZero, Iff.intro, CharP.ofCharZero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
⊢ CharZero K ↔ CharP K 0

Tactic:
exact ⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
hp0 : ¬p = 0
hp : Nat.Prime p
⊢ Theory.Model (L := ring) K {eqZero p} ↔ CharP K p

Tactic:
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize, forall_eq,
      realize_eqZero, ← CharP.charP_iff_prime_eq_zero hp]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Field.realize_eqZero, FirstOrder.Language.Theory.model_iff, forall_eq, Set.mem_singleton_iff, CharP.charP_iff_prime_eq_zero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
neg : ¬CharP K p
⊢ Theory.Model (L := ring) K {⊥} ↔ CharP K p

Tactic:
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize,
      forall_eq, Formula.realize_bot, false_iff]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.Formula.realize_bot, FirstOrder.Language.Theory.model_iff, forall_eq, false_iff, Set.mem_singleton_iff
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
neg : Nat.Prime p → False
neg₁ : p = 0 → False
⊢ False

Tactic:
cases (CharP.char_is_prime_or_zero K p)

Premises used: CharP.char_is_prime_or_zero
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
h : Nat.Prime p
⊢ False

Tactic:
simp_all
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
h : p = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
inst_2 : CharP K p
⊢ K ⊨ Theory.fieldOfChar p

Tactic:
charP_iff_model_fieldOfChar.2 inferInstance

Premises used: Iff.mpr, inferInstance, FirstOrder.Field.charP_iff_model_fieldOfChar
-- Module: Mathlib.ModelTheory.Algebra.Field.CharP
Goal:
p : ℕ
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
h : K ⊨ Theory.fieldOfChar p
⊢ CharP K p

Tactic:
charP_iff_model_fieldOfChar.1 h

Premises used: Iff.mp, FirstOrder.Field.charP_iff_model_fieldOfChar
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : CommRing K
inst_1 : Nontrivial K
n : ℕ
v : Fin (n + 1) → K
⊢ (((lift : (a : Fin (n + 1) → K) → FreeCommRing (Fin (n + 1)) →+* K) v : FreeCommRing (Fin (n + 1)) →+* K) :
        (a : FreeCommRing (Fin (n + 1))) → K)
      (genericMonicPoly n) =
    eval (v (Fin.last n))
      (↑(((Equiv.trans (monicEquivDegreeLT n) (LinearEquiv.toEquiv (degreeLTEquiv K n))).symm :
              (a : Fin n → K) → { p : K[X] // p.Monic ∧ p.natDegree = n })
            (v ∘ Fin.castSucc)) :
        K[X])

Tactic:
simp [genericMonicPoly, monicEquivDegreeLT, degreeLTEquiv, eval_finsetSum]

Premises used: FirstOrder.Field.genericMonicPoly, Polynomial.degreeLTEquiv, Polynomial.eval_finsetSum, Polynomial.monicEquivDegreeLT
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
n : ℕ
rw :
  K ⊨ genericMonicPolyHasRoot n ↔
    ∀ (b : Fin n → K),
      ∃ (x : K),
        eval x
            (↑(((Equiv.trans (monicEquivDegreeLT n) (LinearEquiv.toEquiv (degreeLTEquiv K n))).symm :
                    (a : Fin n → K) → { p : K[X] // p.Monic ∧ p.natDegree = n })
                  b) :
              K[X]) =
          0
⊢ K ⊨ genericMonicPolyHasRoot n ↔ ∀ (p : { p : K[X] // p.Monic ∧ p.natDegree = n }), ∃ (x : K), eval x (↑p : K[X]) = 0

Tactic:
rw [Equiv.forall_congr_left ((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv)]

Premises used: Polynomial.degreeLTEquiv, Equiv.trans, Equiv.forall_congr_left, Polynomial.monicEquivDegreeLT, LinearEquiv.toEquiv
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
n : ℕ
⊢ K ⊨ genericMonicPolyHasRoot n ↔
    ∀ (b : Fin n → K),
      ∃ (x : K),
        eval x
            (↑(((Equiv.trans (monicEquivDegreeLT n) (LinearEquiv.toEquiv (degreeLTEquiv K n))).symm :
                    (a : Fin n → K) → { p : K[X] // p.Monic ∧ p.natDegree = n })
                  b) :
              K[X]) =
          0

Tactic:
simp [Sentence.Realize, genericMonicPolyHasRoot, lift_genericMonicPoly]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Field.lift_genericMonicPoly, FirstOrder.Field.genericMonicPolyHasRoot
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Language.ring.Structure K
p : ℕ
h : K ⊨ Theory.ACF p
⊢ K ⊨ Theory.fieldOfChar p

Tactic:
Theory.Model.mono h Set.subset_union_left

Premises used: Set.subset_union_left, FirstOrder.Language.Theory.Model.mono
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
p : ℕ
inst_2 : CharP K p
inst_3 : IsAlgClosed K
⊢ K ⊨ Theory.ACF p

Tactic:
Theory.model_union_iff.2 ⟨inferInstance, ?_⟩

Premises used: Iff.mpr, FirstOrder.Language.Theory.model_union_iff, FirstOrder.Language.Theory.ACF, inferInstance, And.intro
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
p : ℕ
inst_2 : CharP K p
inst_3 : IsAlgClosed K
refine : K ⊨ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
⊢ K ⊨ Theory.ACF p

Tactic:
refine Theory.model_union_iff.2 ⟨inferInstance, ?_⟩

Premises used: Iff.mpr, FirstOrder.Language.Theory.model_union_iff, inferInstance, And.intro
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
p : ℕ
inst_2 : CharP K p
inst_3 : IsAlgClosed K
simp :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ K ⊨ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}

Tactic:
simp only [Theory.model_iff, Set.mem_image,
    forall_exists_index, and_imp]

Premises used: and_imp, FirstOrder.Language.Theory.model_iff, Set.mem_image, forall_exists_index
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
p : ℕ
inst_2 : CharP K p
inst_3 : IsAlgClosed K
n : ℕ
hn0 : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} n
simp : ∀ (p : { p : K[X] // p.Monic ∧ p.natDegree = n }), ∃ (x : K), eval x (↑p : K[X]) = 0
⊢ K ⊨ genericMonicPolyHasRoot n

Tactic:
simp only [realize_genericMonicPolyHasRoot]

Premises used: FirstOrder.Field.realize_genericMonicPolyHasRoot
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
p_1 : ℕ
inst_2 : CharP K p_1
inst_3 : IsAlgClosed K
p : K[X]
left : p.Monic
hn0 : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} p.natDegree
⊢ ∃ (x : K), eval x (↑(Subtype.mk (p := fun (p_2 : K[X]) ↦ p_2.Monic ∧ p_2.natDegree = p.natDegree) p ⋯) : K[X]) = 0

Tactic:
IsAlgClosed.exists_root p (ne_of_gt
    (natDegree_pos_iff_degree_pos.1 hn0))

Premises used: Polynomial.IsRoot, ne_of_gt, IsAlgClosed.exists_root, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K : Type u_1
inst : Field K
inst_1 : CompatibleRing K
p_1 : ℕ
inst_2 : CharP K p_1
inst_3 : IsAlgClosed K
p : K[X]
left : p.Monic
hn0 : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} p.natDegree
⊢ ∃ (x : K), eval x (↑(Subtype.mk (p := fun (p_2 : K[X]) ↦ p_2.Monic ∧ p_2.natDegree = p.natDegree) p ⋯) : K[X]) = 0

Tactic:
exact IsAlgClosed.exists_root p (ne_of_gt
    (natDegree_pos_iff_degree_pos.1 hn0))

Premises used: ne_of_gt, IsAlgClosed.exists_root, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
K : Type u_2
inst : Language.ring.Structure K
h : K ⊨ Theory.ACF p
⊢ K ⊨ Theory.field

Tactic:
Theory.Model.mono h (Set.subset_union_of_subset_left Set.subset_union_left _)

Premises used: Set.subset_union_of_subset_left, Set.subset_union_left, FirstOrder.Language.Theory.Model.mono
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K_1 : Type u_1
p : ℕ
K : Type u_2
inst : Language.ring.Structure K
h : K ⊨ Theory.ACF p
⊢ K ⊨ Theory.field

Tactic:
have := modelField_of_modelACF p K
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
K_1 : Type u_1
p : ℕ
K : Type u_2
inst : Language.ring.Structure K
h : K ⊨ Theory.ACF p
this : K ⊨ Theory.field
⊢ Field K

Tactic:
exact fieldOfModelField K

Premises used: FirstOrder.Field.fieldOfModelField
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h : K ⊨ Theory.ACF p
⊢ IsAlgClosed K

Tactic:
IsAlgClosed.of_exists_root _ ?_

Premises used: IsAlgClosed.of_exists_root
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h : K ⊨ Theory.ACF p
refine : ∀ (p : K[X]), p.Monic → Irreducible p → ∃ (x : K), eval x p = 0
⊢ IsAlgClosed K

Tactic:
refine IsAlgClosed.of_exists_root _ ?_

Premises used: IsAlgClosed.of_exists_root
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ⊆ Theory.ACF p_1

Tactic:
simp [Theory.ACF]

Premises used: FirstOrder.Language.Theory.ACF
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ K ⊨ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}

Tactic:
have h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n} :=
    Theory.Model.mono h (by simp [Theory.ACF])