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

Proof state:
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

Tactic:
exact P.relation_mem_ker i

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

Tactic:
simp only [Finsupp.sum, map_sum, Derivation.leibniz, smul_eq_mul, map_add, map_mul,
  Presentation.aeval_val_relation, zero_mul, add_zero] at heq

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

Tactic:
intro h

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
h : c 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
h : c i = 0
⊢ (aeval P.val) (c i) = 0

Tactic:
simp [h]

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

Tactic:
have heq2 : ∑ i ∈ c.support,
    aeval P.val (c i) • (fun j ↦ aeval P.val (pderiv (P.map j) (P.relation i))) = 0 := by
  ext j
  simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
  apply heq

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

Tactic:
obtain ⟨(x : P.ker), rfl⟩ := Cotangent.mk_surjective x

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

Tactic:
apply hx

Result:
no goals

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

Tactic:
have := P.linearIndependent_aeval_val_pderiv_relation

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 : LinearIndependent S fun i j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))
⊢ (aeval P.val) (c i) = 0