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

Proof state:
case intro.intro
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
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
have (i : P.rels) : 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

Result:
case intro.intro
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
⊢ ↑x ∈ P.toExtension.ker ^ 2

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
⊢ (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0

Tactic:
ext j

Result:
case h
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
j : P.rels
⊢ (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) j = 0 j

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ Function.Injective ⇑P.cotangentComplexAux

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ LinearMap.ker P.cotangentComplexAux ≤ ⊥

Proof state:
case intro.intro
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
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
have heq (i : P.rels) :
    aeval P.val (pderiv (P.map i) <| c.sum fun i a ↦ a * P.relation i) = 0 := by
  rw [hc]
  apply hx

Result:
case intro.intro
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), (aeval P.val) ((pderiv (P.map i)) (c.sum fun i a => a * P.relation i)) = 0
⊢ ↑x ∈ P.toExtension.ker ^ 2

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 ∈ RingHom.ker (aeval P.val)

Tactic:
simpa using this i

Result:
no goals

Proof state:
case h
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
j : P.rels
⊢ (∑ i ∈ c.support, (aeval P.val) (c i) • fun j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))) j = 0 j

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

Result:
case h
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
j : P.rels
⊢ ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map j)) (P.relation x)) = 0