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_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:
exact this i
-- 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 : σ),
    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
-- 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
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
rw : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) ∈ HPow.hPow (β := ℕ) P.ker 2
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2

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_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)
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
⊢ (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) ∈ HPow.hPow (β := ℕ) P.ker 2

Tactic:
apply Ideal.sum_mem

Premises used: Ideal.sum_mem
-- 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
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
a : (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ P.ker * P.ker
⊢ (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ HPow.hPow (β := ℕ) P.ker 2

Tactic:
rw [pow_two]

Premises used: pow_two
-- 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
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
a : Membership.mem (α := P.Ring) P.ker ((c : (a : σ) → P.Ring) i : P.Ring)
a₁ : P.relation i ∈ P.ker
⊢ (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ P.ker * P.ker

Tactic:
apply Ideal.mul_mem_mul

Premises used: Ideal.mul_mem_mul
-- 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
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
a :
  Membership.mem (α := P.Ring) (γ := Ideal P.Ring) (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))
    ((c : (a : σ) → P.Ring) i : P.Ring)
⊢ Membership.mem (α := P.Ring) P.ker ((c : (a : σ) → P.Ring) i : P.Ring)

Tactic:
rw [P.ker_eq_ker_aeval_val]

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Presentation.toGenerators
-- 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
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
⊢ Membership.mem (α := P.Ring) (γ := Ideal P.Ring) (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))
    ((c : (a : σ) → P.Ring) i : P.Ring)

Tactic:
simpa using this i
-- 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
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
⊢ P.relation i ∈ P.ker

Tactic:
P.relation_mem_ker i

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.relation_mem_ker
-- 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
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
⊢ P.relation i ∈ P.ker

Tactic:
exact P.relation_mem_ker i

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.relation_mem_ker
-- 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 ι σ
rw : Set.range (ι := σ) (⇑P.basisDeriv : (a : σ) → σ → S) ⊆ (↑P.cotangentComplexAux.range : Set (σ → S))
⊢ Function.Surjective (α := P.toExtension.Cotangent) (β := σ → S)
    (⇑P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)

Tactic:
rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← P.basisDeriv.span_eq, Submodule.span_le]

Premises used: Algebra.SubmersivePresentation.basisDeriv, eq_top_iff, LinearMap.range_eq_top, Module.Basis.span_eq, Submodule.span_le
-- 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 ι σ
i : σ
h :
  Eq (α := σ → S)
    ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) ⋯) :
          P.toExtension.Cotangent) :
      σ → S)
    ((P.basisDeriv : (a : σ) → σ → S) i : σ → S)
⊢ Membership.mem (α := σ → S) (↑P.cotangentComplexAux.range : Set (σ → S)) ((P.basisDeriv : (a : σ) → σ → S) i : σ → S)

Tactic:
use Cotangent.mk ⟨P.relation i, P.relation_mem_ker i⟩

Premises used: Subtype.mk, Algebra.Extension.Cotangent.mk, DFunLike.coe
-- 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 ι σ
i : σ
h :
  ∀ (j : σ),
    Eq.{u_2 + 1} (α := S)
      ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
          ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) ⋯) :
            P.toExtension.Cotangent)
          j :
        S)
      ((P.basisDeriv : (a : σ) → σ → S) i j : S)
⊢ Eq (α := σ → S)
    ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) ⋯) :
          P.toExtension.Cotangent) :
      σ → S)
    ((P.basisDeriv : (a : σ) → σ → S) i : σ → S)

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 ι σ
i j : σ
h :
  Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R)
            (↑(Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) ⋯) : P.Ring) :
          MvPolynomial ι R) :
      S)
    ((P.basisDeriv : (a : σ) → σ → S) i j : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) ⋯) :
          P.toExtension.Cotangent)
        j :
      S)
    ((P.basisDeriv : (a : σ) → σ → S) i j : S)

Tactic:
rw [P.cotangentComplexAux_apply]

Premises used: Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Algebra.SubmersivePresentation.toPreSubmersivePresentation
-- 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 ι σ
i j : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R)
            (↑(Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) ⋯) : P.Ring) :
          MvPolynomial ι R) :
      S)
    ((P.basisDeriv : (a : σ) → σ → S) i j : S)

Tactic:
simp
-- 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 ι σ
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := σ → S)
    (⇑P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)

Tactic:
have := P.cotangentComplexAux_injective
-- 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 ι σ
this :
  Function.Injective (α := P.toExtension.Cotangent) (β := σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace))))
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)

Tactic:
Function.Injective.of_comp (Function.Injective.of_comp <| Function.Injective.of_comp this)

Premises used: Function.Injective.of_comp