awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
⊢ Multiset.Nodup (α := (l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)
    (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
          Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
          Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
          Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
          Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
      Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l))

Tactic:
decide
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
x : ring.Symbols
inl :
  ∀ (fst : ℕ) (f : ring.Functions fst),
    Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) fst f) ∈
      {
        val :=
          (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
            Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
        nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
inr :
  ∀ (fst : ℕ) (f : ring.Relations fst),
    Sum.inr (Sigma.mk (β := fun (l : ℕ) ↦ ring.Relations l) fst f) ∈
      {
        val :=
          (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
            Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
        nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
⊢ x ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
rcases x with ⟨_, f⟩ | ⟨_, f⟩
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
decide
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
decide
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
decide
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
decide
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
decide
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
fst : ℕ
f : ring.Relations fst
⊢ Sum.inr (Sigma.mk (β := fun (l : ℕ) ↦ ring.Relations l) fst f) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }

Tactic:
cases f
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
⊢ Fintype.card ring.Symbols = 5

Tactic:
have : Fintype.card Language.ring.Symbols = 5 := rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
this : Fintype.card ring.Symbols = 5
⊢ ring.card = 5

Tactic:
simp [Language.card, this]

Premises used: FirstOrder.Language.card
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : One R
inst_4 : Zero R
inst_5 : CompatibleRing R
x y : ring.Term α
v : α → R
⊢ Term.realize v (x + y) = Term.realize v x + Term.realize v y

Tactic:
simp [add_def, funMap_add]

Premises used: FirstOrder.Ring.CompatibleRing.funMap_add, FirstOrder.Ring.add_def
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : One R
inst_4 : Zero R
inst_5 : CompatibleRing R
x y : ring.Term α
v : α → R
⊢ Term.realize v (x * y) = Term.realize v x * Term.realize v y

Tactic:
simp [mul_def, funMap_mul]

Premises used: FirstOrder.Ring.mul_def, FirstOrder.Ring.CompatibleRing.funMap_mul
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : One R
inst_4 : Zero R
inst_5 : CompatibleRing R
x : ring.Term α
v : α → R
⊢ Term.realize v (-x) = -Term.realize v x

Tactic:
simp [neg_def, funMap_neg]

Premises used: FirstOrder.Ring.neg_def, FirstOrder.Ring.CompatibleRing.funMap_neg
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : One R
inst_4 : Zero R
inst_5 : CompatibleRing R
v : α → R
⊢ Term.realize (L := ring) v 0 = 0

Tactic:
simp [zero_def, funMap_zero, constantMap]

Premises used: FirstOrder.Language.constantMap, FirstOrder.Ring.CompatibleRing.funMap_zero, FirstOrder.Ring.zero_def
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : One R
inst_4 : Zero R
inst_5 : CompatibleRing R
v : α → R
⊢ Term.realize (L := ring) v 1 = 1

Tactic:
simp [one_def, funMap_one, constantMap]

Premises used: FirstOrder.Ring.CompatibleRing.funMap_one, FirstOrder.Language.constantMap, FirstOrder.Ring.one_def
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃[ring] S
x y : R
⊢ f.toFun (x * y) = f.toFun x * f.toFun y

Tactic:
simpa using f.map_fun mulFunc ![x, y]

Premises used: FirstOrder.Ring.mulFunc, FirstOrder.Language.Equiv.map_fun, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃[ring] S
x y : R
⊢ f.toFun (x + y) = f.toFun x + f.toFun y

Tactic:
simpa using f.map_fun addFunc ![x, y]

Premises used: FirstOrder.Language.Equiv.map_fun, Matrix.vecEmpty, Matrix.vecCons, FirstOrder.Ring.addFunc
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Functions n
add : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.add x) = funMap (L := ring) ringFunc.add (f_1.toFun ∘ x)
mul : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.mul x) = funMap (L := ring) ringFunc.mul (f_1.toFun ∘ x)
neg : ∀ (x : Fin 1 → R), f_1.toFun (funMap (L := ring) ringFunc.neg x) = funMap (L := ring) ringFunc.neg (f_1.toFun ∘ x)
zero :
  ∀ (x : Fin 0 → R), f_1.toFun (funMap (L := ring) ringFunc.zero x) = funMap (L := ring) ringFunc.zero (f_1.toFun ∘ x)
one : ∀ (x : Fin 0 → R), f_1.toFun (funMap (L := ring) ringFunc.one x) = funMap (L := ring) ringFunc.one (f_1.toFun ∘ x)
⊢ ∀ (x : Fin n → R), f_1.toFun (funMap f x) = funMap f (f_1.toFun ∘ x)

Tactic:
cases f
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap (L := ring) add x) = funMap (L := ring) add (f.toFun ∘ x)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap (L := ring) mul x) = funMap (L := ring) mul (f.toFun ∘ x)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 1 → R), f.toFun (funMap (L := ring) neg x) = funMap (L := ring) neg (f.toFun ∘ x)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap (L := ring) zero x) = funMap (L := ring) zero (f.toFun ∘ x)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap (L := ring) one x) = funMap (L := ring) one (f.toFun ∘ x)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Relations n
⊢ ∀ (x : Fin n → R), RelMap f (f_1.toFun ∘ x) ↔ RelMap f x

Tactic:
cases f
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
simp :
  ∀ (a a_1 : R),
    funMap addFunc
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))) =
      HAdd.hAdd (β := R) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))
            1 :
          R)
⊢ ∀ (x : Fin 2 → R), funMap addFunc x = x 0 + x 1

Tactic:
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]

Premises used: Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, Fin.cons_zero
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
a a_1 : R
⊢ funMap addFunc
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))) =
    HAdd.hAdd (β := R) a
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1 :
        R)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
simp :
  ∀ (a a_1 : R),
    funMap mulFunc
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))) =
      HMul.hMul (β := R) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))
            1 :
          R)
⊢ ∀ (x : Fin 2 → R), funMap mulFunc x = x 0 * x 1

Tactic:
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]

Premises used: Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, Fin.cons_zero
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
a a_1 : R
⊢ funMap mulFunc
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))) =
    HMul.hMul (β := R) a
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1 :
        R)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
simp :
  ∀ (a : R),
    funMap negFunc
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a (finZeroElim (α := fun (i : Fin 0) ↦ R))) =
      -a
⊢ ∀ (x : Fin 1 → R), funMap negFunc x = -x 0

Tactic:
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]

Premises used: Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, Fin.cons_zero
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
a : R
⊢ funMap negFunc
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a (finZeroElim (α := fun (i : Fin 0) ↦ R))) =
    -a

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
simp : Eq.{u_2 + 1} (α := R) (funMap zeroFunc (finZeroElim (α := fun (i : Fin 0) ↦ R))) 0
⊢ ∀ (x : Fin 0 → R), funMap zeroFunc x = 0

Tactic:
simp only [Fin.forall_fin_zero_pi]

Premises used: Fin.forall_fin_zero_pi
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ Eq.{u_2 + 1} (α := R) (funMap zeroFunc (finZeroElim (α := fun (i : Fin 0) ↦ R))) 0

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
simp : Eq.{u_2 + 1} (α := R) (funMap oneFunc (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1
⊢ ∀ (x : Fin 0 → R), funMap oneFunc x = 1

Tactic:
simp only [Fin.forall_fin_zero_pi]

Premises used: Fin.forall_fin_zero_pi
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ Eq.{u_2 + 1} (α := R) (funMap oneFunc (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
rw :
  ∃ (φ :
    ring.Formula
      (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
    zeroLocus K (Ideal.span (↑S : Set (MvPolynomial ι K))) =
      {v : ι → K |
        φ.Realize
          (Sum.elim
            (Subtype.val (p := fun (x : K) ↦
              Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
            v)}
⊢ Set.Definable (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) ring
    (zeroLocus K (Ideal.span (↑S : Set (MvPolynomial ι K))))

Tactic:
rw [Set.definable_iff_exists_formula_sum]

Premises used: Set.definable_iff_exists_formula_sum
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
rw :
  ∃ (φ :
    ring.Formula
      (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
    Eq (α := Set (ι → K))
      {x : ι → K |
        ∀ p ∈ (↑S : Set (MvPolynomial ι K)),
          Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
      {v : ι → K |
        φ.Realize
          (Sum.elim
            (Subtype.val (p := fun (x : K) ↦
              Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
            v)}
⊢ ∃ (φ :
    ring.Formula
      (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
    zeroLocus K (Ideal.span (↑S : Set (MvPolynomial ι K))) =
      {v : ι → K |
        φ.Realize
          (Sum.elim
            (Subtype.val (p := fun (x : K) ↦
              Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
            v)}

Tactic:
rw [MvPolynomial.zeroLocus_span]

Premises used: MvPolynomial.zeroLocus_span
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : ↥S
p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support
simp :
  ∃ (i : MvPolynomial ι K) (_ : i ∈ S),
    Membership.mem (γ := Set K) ((fun (m : ι →₀ ℕ) ↦ coeff m i) '' (↑i.support : Set (ι →₀ ℕ)))
      (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
        (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))
⊢ Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ)))
    (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
      (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))

Tactic:
simp only [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : ↥S
p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support
⊢ ∃ (i : MvPolynomial ι K) (_ : i ∈ S),
    Membership.mem (γ := Set K) ((fun (m : ι →₀ ℕ) ↦ coeff m i) '' (↑i.support : Set (ι →₀ ℕ)))
      (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
        (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))

Tactic:
⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩

Premises used: Sigma.fst, Set.mem_image_of_mem, Exists.intro, Sigma.snd, Subtype.val, Subtype.property
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : ↥S
p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support
⊢ ∃ (i : MvPolynomial ι K) (_ : i ∈ S),
    Membership.mem (γ := Set K) ((fun (m : ι →₀ ℕ) ↦ coeff m i) '' (↑i.support : Set (ι →₀ ℕ)))
      (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
        (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))

Tactic:
exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩