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

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 * P.ker

Tactic:
apply Ideal.mul_mem_mul

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 ∈ P.ker

case intro.intro.a.hs
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
⊢ P.relation i ∈ P.ker

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
this : ∀ (i : P.rels), (aeval P.val) (c i) = 0
⊢ ↑x ∈ P.ker ^ 2

Tactic:
rw [← hc]

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
⊢ (c.sum fun i a => a * P.relation i) ∈ P.ker ^ 2

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
this : ∀ (i : P.rels), (aeval P.val) (c i) = 0
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
show _ ∈ P.ker ^ 2

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.ker ^ 2

Proof state:
case 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 : Cotangent.mk x ∈ LinearMap.ker P.cotangentComplexAux
⊢ Cotangent.mk x ∈ ⊥

Tactic:
rw [Submodule.mem_bot, Cotangent.mk_eq_zero_iff]

Result:
case 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 : Cotangent.mk x ∈ LinearMap.ker P.cotangentComplexAux
⊢ ↑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
⊢ ↑x ∈ Ideal.span (Set.range P.relation)

Tactic:
rw [P.span_range_relation_eq_ker]

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
⊢ ↑x ∈ 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
⊢ LinearMap.ker P.cotangentComplexAux ≤ ⊥

Tactic:
intro x hx

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.toExtension.Cotangent
hx : x ∈ LinearMap.ker P.cotangentComplexAux
⊢ x ∈ ⊥

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
⊢ (aeval P.val) (c 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

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
this : ∀ (i : P.rels), (fun i => (aeval P.val) (c i)) i = 0
⊢ (aeval P.val) (c i) = 0