awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
i : σ
rw :
  Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)
    (0 : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R)
          (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i)) :
      S)
    (0 : S)

Tactic:
rw [hc]
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
i : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)
    (0 : S)

Tactic:
apply hx
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
⊢ ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R)
            (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i)) :
        S)
      (0 : S)

Tactic:
have heq (i : σ) :
      aeval P.val (pderiv (P.map i) <| c.sum fun i a ↦ a * P.relation i) = 0 := by
    rw [hc]
    apply hx
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R)
            (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i)) :
        S)
      (0 : S)
⊢ ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0

Tactic:
simp only [Finsupp.sum, map_sum, Derivation.leibniz, smul_eq_mul, map_add, map_mul,
    Presentation.aeval_val_relation, zero_mul, add_zero] at heq

Premises used: MulZeroClass.zero_mul, Finsupp.sum, map_add, Algebra.Presentation.aeval_val_relation, map_sum, Derivation.leibniz, map_mul, smul_eq_mul, add_zero
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
h :
  ∀ (j : σ),
    Eq.{u_2 + 1} (α := S)
      ((∑ i ∈ c.support,
          HSMul.hSMul (α := S) (β := (j : σ) → S)
            ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
            (aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
        j)
      (0 j)
⊢ Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0

Tactic:
ext j
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
j : σ
h :
  Eq.{u_2 + 1} (α := S)
    (∑ x ∈ c.support,
      HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
          S))
    0
⊢ Eq.{u_2 + 1} (α := S)
    ((∑ i ∈ c.support,
        HSMul.hSMul (α := S) (β := (j : σ) → S)
          ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
          (aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
      j)
    (0 j)

Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]

Premises used: Finset.sum_apply, Pi.zero_apply, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
j : σ
⊢ Eq.{u_2 + 1} (α := S)
    (∑ x ∈ c.support,
      HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
          S))
    0

Tactic:
apply heq
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
⊢ Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0

Tactic:
have heq2 : ∑ i ∈ c.support,
      aeval P.val (c i) • (fun j ↦ aeval P.val (pderiv (P.map j) (P.relation i))) = 0 := by
    ext j
    simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
    apply heq
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
i : σ
⊢ LinearIndependent S (M := (j : σ) → S) fun (i j : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R)

Tactic:
have := P.linearIndependent_aeval_val_pderiv_relation
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
i : σ
this :
  LinearIndependent S (M := (j : σ) → S) fun (i j : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R)
⊢ ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      Eq (α := (j : σ) → S)
          (∑ i ∈ s,
            HSMul.hSMul (β := (j : σ) → S) (g i) fun (j : σ) ↦
              (aeval P.val : (a : MvPolynomial ι R) → S)
                ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
          0 →
        ∀ (i : σ), g i = 0

Tactic:
rw [linearIndependent_iff''] at this

Premises used: linearIndependent_iff''
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
i_1 : σ
this :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      Eq (α := (j : σ) → S)
          (∑ i ∈ s,
            HSMul.hSMul (β := (j : σ) → S) (g i) fun (j : σ) ↦
              (aeval P.val : (a : MvPolynomial ι R) → S)
                ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
          0 →
        ∀ (i : σ), g i = 0
i : σ
simp :
  Eq (α := P.Ring) ((c : (a : σ) → P.Ring) i : P.Ring) (0 : P.Ring) →
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
⊢ i ∉ c.support →
    Eq.{u_2 + 1} (α := S)
      ((fun (i : σ) ↦ ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S)) i) 0

Tactic:
simp only [Finsupp.mem_support_iff, ne_eq, not_not]

Premises used: Finsupp.mem_support_iff, Classical.not_not, ne_eq
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
i_1 : σ
this :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      Eq (α := (j : σ) → S)
          (∑ i ∈ s,
            HSMul.hSMul (β := (j : σ) → S) (g i) fun (j : σ) ↦
              (aeval P.val : (a : MvPolynomial ι R) → S)
                ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
          0 →
        ∀ (i : σ), g i = 0
i : σ
h : Eq (α := P.Ring) ((c : (a : σ) → P.Ring) i : P.Ring) (0 : P.Ring)
⊢ Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
i : σ
this :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      Eq (α := (j : σ) → S)
          (∑ i ∈ s,
            HSMul.hSMul (β := (j : σ) → S) (g i) fun (j : σ) ↦
              (aeval P.val : (a : MvPolynomial ι R) → S)
                ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
          0 →
        ∀ (i : σ), g i = 0
⊢ ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((fun (i : σ) ↦ ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S)) i) 0

Tactic:
have := this c.support (fun i ↦ aeval P.val (c i))
      (by intro i; simp only [Finsupp.mem_support_iff, ne_eq, not_not]; intro h; simp [h]) heq2
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
i : σ
this_2 :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      Eq (α := (j : σ) → S)
          (∑ i ∈ s,
            HSMul.hSMul (β := (j : σ) → S) (g i) fun (j : σ) ↦
              (aeval P.val : (a : MvPolynomial ι R) → S)
                ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
          0 →
        ∀ (i : σ), g i = 0
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((fun (i : σ) ↦ ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S)) i) 0
⊢ Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)

Tactic:
this i