-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma sectionCotangent_zero_of_not_mem_range (i : P.vars) (hi : i ∉ Set.range P.map) :
    (sectionCotangent P) (P.cotangentSpaceBasis i) = 0

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
i : P.vars
j : P.rels
hij : i = P.map j
h✝ : ¬1 = 0
⊢ P.map j = i

Tactic:
exact hij.symm

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
i : P.vars
hi : i ∉ Set.range P.map
⊢ P.sectionCotangent (P.cotangentSpaceBasis i) = 0

Tactic:
classical
contrapose hi
rw [sectionCotangent_eq_iff] at hi
simp only [Basis.repr_self, map_zero, Pi.zero_apply, not_forall,
  Finsupp.single_apply, ite_eq_right_iff, Classical.not_imp, exists_and_right] at hi
obtain ⟨j, hij, _⟩ := hi
simp only [Set.mem_range, not_exists, not_forall, not_not]
use j
exact hij.symm

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
i : P.vars
hi : ¬P.sectionCotangent (P.cotangentSpaceBasis i) = 0
⊢ ¬i ∉ Set.range P.map

Tactic:
rw [sectionCotangent_eq_iff] at hi

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.vars
hi : ¬∀ (i_1 : P.rels), (P.cotangentSpaceBasis.repr (P.cotangentSpaceBasis i)) (P.map i_1) = P.cotangentComplexAux 0 i_1
⊢ ¬i ∉ Set.range P.map

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.vars
hi : ∃ x, ∃ (_ : i = P.map x), ¬1 = 0
⊢ ¬i ∉ Set.range P.map

Tactic:
obtain ⟨j, hij, _⟩ := hi

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
i : P.vars
j : P.rels
hij : i = P.map j
h✝ : ¬1 = 0
⊢ ¬i ∉ Set.range P.map

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
i : P.vars
j : P.rels
hij : i = P.map j
h✝ : ¬1 = 0
⊢ ¬i ∉ Set.range P.map

Tactic:
simp only [Set.mem_range, not_exists, not_forall, not_not]

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
i : P.vars
j : P.rels
hij : i = P.map j
h✝ : ¬1 = 0
⊢ ∃ x, P.map x = i

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
i : P.vars
j : P.rels
hij : i = P.map j
h✝ : ¬1 = 0
⊢ ∃ x, P.map x = i

Tactic:
use 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
i : P.vars
j : P.rels
hij : i = P.map j
h✝ : ¬1 = 0
⊢ P.map j = i

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.vars
hi : i ∉ Set.range P.map
⊢ P.sectionCotangent (P.cotangentSpaceBasis i) = 0

Tactic:
contrapose hi

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.vars
hi : ¬P.sectionCotangent (P.cotangentSpaceBasis i) = 0
⊢ ¬i ∉ Set.range P.map

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.vars
hi : ¬∀ (i_1 : P.rels), (P.cotangentSpaceBasis.repr (P.cotangentSpaceBasis i)) (P.map i_1) = P.cotangentComplexAux 0 i_1
⊢ ¬i ∉ Set.range P.map

Tactic:
simp only [Basis.repr_self, map_zero, Pi.zero_apply, not_forall,
  Finsupp.single_apply, ite_eq_right_iff, Classical.not_imp, exists_and_right] at hi

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.vars
hi : ∃ x, ∃ (_ : i = P.map x), ¬1 = 0
⊢ ¬i ∉ Set.range P.map