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

Tactic:
exact x.property

Result:
no goals

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

Tactic:
apply Ideal.sum_mem

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
⊢ ∀ c_1 ∈ c.support, (fun i a => a * P.relation i) c_1 (c c_1) ∈ P.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
i : P.rels
⊢ (aeval P.val) ((pderiv (P.map i)) (c.sum fun i a => a * P.relation i)) = 0

Tactic:
rw [hc]

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
i : P.rels
⊢ (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

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 : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
obtain ⟨c, hc⟩ := Finsupp.mem_ideal_span_range_iff_exists_finsupp.mp this

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
⊢ ↑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
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

Tactic:
exact this i

Result:
no goals

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

Tactic:
intro i hi

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

Tactic:
rw [LinearMap.mem_ker, P.cotangentComplexAux_zero_iff] at hx

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

Tactic:
have : x.val ∈ Ideal.span (Set.range P.relation) := by
  rw [P.span_range_relation_eq_ker]
  exact x.property

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 : ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
⊢ ↑x ∈ P.toExtension.ker ^ 2

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

Tactic:
apply heq

Result:
no goals