awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
    ((∑ 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)
have 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
Tactic: simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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 : σ
⊢ Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
have 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)
Tactic: have := P.linearIndependent_aeval_val_pderiv_relation
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
have 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
Tactic: rw [linearIndependent_iff''] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : σ
⊢ 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
have 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)
Tactic: simp only [Finsupp.mem_support_iff, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
have this₁ : ∀ (i : σ),
  Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
Tactic: have (i : σ) : aeval P.val (c i) = 0 := by
    have := P.linearIndependent_aeval_val_pderiv_relation
    rw [linearIndependent_iff''] at this
    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
    exact this i
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2
have rw : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) ∈ HPow.hPow (β := ℕ) P.ker 2
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
⊢ (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) ∈ HPow.hPow (β := ℕ) P.ker 2
have a : ∀ c_1 ∈ c.support,
  (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) c_1 ((c : (a : σ) → P.Ring) c_1) ∈ HPow.hPow (β := ℕ) P.ker 2
Tactic: apply Ideal.sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
i : σ
hi : i ∈ c.support
⊢ (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ HPow.hPow (β := ℕ) P.ker 2
have a : (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ P.ker * P.ker
Tactic: rw [pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
i : σ
hi : i ∈ c.support
⊢ (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ P.ker * P.ker
have a : Membership.mem (α := P.Ring) P.ker ((c : (a : σ) → P.Ring) i : P.Ring)
Tactic: apply Ideal.mul_mem_mul