-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma cotangentComplexAux_injective : Function.Injective P.cotangentComplexAux

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : P.rels
this : LinearIndependent S fun i j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))
⊢ (aeval P.val) (c i) = 0

Tactic:
rw [linearIndependent_iff''] at this

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : P.rels
this :
  ∀ (s : Finset P.rels) (g : P.rels → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : P.rels), g i = 0
⊢ (aeval P.val) (c i) = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i✝ : P.rels
this :
  ∀ (s : Finset P.rels) (g : P.rels → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : P.rels), g i = 0
i : P.rels
⊢ i ∉ c.support → (fun i => (aeval P.val) (c i)) i = 0

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

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i✝ : P.rels
this :
  ∀ (s : Finset P.rels) (g : P.rels → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : P.rels), g i = 0
i : P.rels
⊢ c i = 0 → (aeval P.val) (c i) = 0

Proof state:
case intro.intro.a.hr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : P.rels), (aeval P.val) (c i) = 0
i : P.rels
hi : i ∈ c.support
⊢ c i ∈ P.ker

Tactic:
rw [P.ker_eq_ker_aeval_val]

Result:
case intro.intro.a.hr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : P.rels), (aeval P.val) (c i) = 0
i : P.rels
hi : i ∈ c.support
⊢ c i ∈ RingHom.ker (aeval P.val)

Proof state:
case intro.intro.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : P.rels), (aeval P.val) (c i) = 0
i : P.rels
hi : i ∈ c.support
⊢ (fun i a => a * P.relation i) i (c i) ∈ P.ker ^ 2

Tactic:
rw [pow_two]

Result:
case intro.intro.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : P.rels), (aeval P.val) (c i) = 0
i : P.rels
hi : i ∈ c.support
⊢ (fun i a => a * P.relation i) i (c i) ∈ P.ker * P.ker

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : P.rels
this :
  ∀ (s : Finset P.rels) (g : P.rels → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : P.rels), g i = 0
⊢ ∀ i ∉ c.support, (fun i => (aeval P.val) (c i)) i = 0

Tactic:
intro i

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : ↥P.ker
hx : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : P.rels →₀ P.Ring
hc : (c.sum fun i a => a * P.relation i) = ↑x
heq : ∀ (i : P.rels), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i✝ : P.rels
this :
  ∀ (s : Finset P.rels) (g : P.rels → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : P.rels), g i = 0
i : P.rels
⊢ i ∉ c.support → (fun i => (aeval P.val) (c i)) i = 0