awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
this :
  Function.Injective (α := P.toExtension.Cotangent) (β := σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace))))
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)

Tactic:
exact Function.Injective.of_comp (Function.Injective.of_comp <| Function.Injective.of_comp this)

Premises used: Function.Injective.of_comp
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
rw :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
⊢ Subsingleton P.toExtension.H1Cotangent

Tactic:
rw [Algebra.Extension.subsingleton_h1Cotangent]

Premises used: Algebra.Extension.subsingleton_h1Cotangent
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)

Tactic:
cotangentComplex_injective P

Premises used: Algebra.SubmersivePresentation.cotangentComplex_injective
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)

Tactic:
exact cotangentComplex_injective P

Premises used: Algebra.SubmersivePresentation.cotangentComplex_injective
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
r : σ
symm :
  Eq (α := P.toExtension.Cotangent)
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
      P.toExtension.Cotangent)
    ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)
⊢ Eq (α := P.toExtension.Cotangent) ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
      P.toExtension.Cotangent)

Tactic:
symm
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
r : σ
a :
  Eq (α := σ → S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
          P.toExtension.Cotangent) :
      σ → S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent) :
      σ → S)
⊢ Eq (α := P.toExtension.Cotangent)
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
      P.toExtension.Cotangent)
    ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)

Tactic:
apply P.cotangentEquiv.injective

Premises used: Algebra.SubmersivePresentation.cotangentEquiv, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
r : σ
a :
  ∀ (x : σ),
    Eq.{u_2 + 1} (α := S)
      ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
          ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
            P.toExtension.Cotangent)
          x :
        S)
      ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
          ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent) x :
        S)
⊢ Eq (α := σ → S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
          P.toExtension.Cotangent) :
      σ → S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent) :
      σ → S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
r x : σ
a :
  Eq.{u_2 + 1} (α := S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
          P.toExtension.Cotangent)
        x :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map x) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation r) : MvPolynomial ι R) :
      S)
⊢ Eq.{u_2 + 1} (α := S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
          P.toExtension.Cotangent)
        x :
      S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent) x :
      S)

Tactic:
simp_rw [basisCotangent, Basis.map_apply, LinearEquiv.apply_symm_apply, basisDeriv_apply]

Premises used: Algebra.SubmersivePresentation.basisCotangent, Module.Basis.map_apply, LinearEquiv.apply_symm_apply, Algebra.SubmersivePresentation.basisDeriv_apply
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
r x : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
          P.toExtension.Cotangent)
        x :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map x) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation r) : MvPolynomial ι R) :
      S)

Tactic:
apply P.toPreSubmersivePresentation.cotangentComplexAux_apply _ _

Premises used: Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Algebra.SubmersivePresentation.toPreSubmersivePresentation
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Free S P.toExtension.Cotangent

Tactic:
Module.Free.of_basis P.basisCotangent

Premises used: Algebra.SubmersivePresentation.basisCotangent, Module.Free.of_basis
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
simp :
  (P.cotangentEquiv.symm : (a : σ → S) → P.toExtension.Cotangent)
        ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
          ((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S)
              ((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x) :
            σ →₀ S)) =
      y ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x : ι →₀ S) : (a : ι) → S)
            (P.map i) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) y i : S)
⊢ (P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent) x = y ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x : ι →₀ S) : (a : ι) → S)
            (P.map i) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) y i : S)

Tactic:
simp only [sectionCotangent, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]

Premises used: LinearMap.coe_comp, Function.comp_apply, Algebra.SubmersivePresentation.sectionCotangent, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
rw :
  (∀ (x_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
            ((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S)
                ((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x) :
              σ →₀ S)
            x_1 :
          S)
        ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S) y x_1 : S)) ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x : ι →₀ S) : (a : ι) → S)
            (P.map i) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) y i : S)
⊢ (P.cotangentEquiv.symm : (a : σ → S) → P.toExtension.Cotangent)
        ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
          ((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S)
              ((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x) :
            σ →₀ S)) =
      y ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x : ι →₀ S) : (a : ι) → S)
            (P.map i) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) y i : S)

Tactic:
rw [← (cotangentEquiv P).injective.eq_iff, funext_iff, LinearEquiv.apply_symm_apply]

Premises used: Algebra.SubmersivePresentation.cotangentEquiv, Function.Injective.eq_iff, funext_iff, LinearEquiv.apply_symm_apply, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
            ((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S)
                ((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x) :
              σ →₀ S)
            x_1 :
          S)
        ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S) y x_1 : S)) ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S) x : ι →₀ S) : (a : ι) → S)
            (P.map i) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) y i : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
h :
  ∀ (x : P.toExtension.Cotangent),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
          x :
        P.toExtension.Cotangent)
      ((LinearMap.id : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)
⊢ P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex = LinearMap.id

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.Cotangent
h :
  (P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
      ((P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace) x) =
    x
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
        x :
      P.toExtension.Cotangent)
    ((LinearMap.id : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]

Premises used: LinearMap.id_coe, LinearMap.coe_comp, Function.comp_apply, id_eq
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.Cotangent
h :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
                ((P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace) x) :
              ι →₀ S) :
            (a : ι) → S)
          (P.map i) :
        S)
      ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) x i : S)
⊢ (P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
      ((P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace) x) =
    x

Tactic:
rw [sectionCotangent_eq_iff]

Premises used: Algebra.SubmersivePresentation.sectionCotangent_eq_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.Cotangent
i : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              ((P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace) x) :
            ι →₀ S) :
          (a : ι) → S)
        (P.map i) :
      S)
    ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) x i : S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi : i ∉ Set.range P.map
contrapose :
  ∀
    (hi :
      ¬Eq (α := P.toExtension.Cotangent)
          ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
              ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
            P.toExtension.Cotangent)
          (0 : P.toExtension.Cotangent)),
    i ∈ Set.range P.map
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)

Tactic:
contrapose hi
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi :
  ¬Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
⊢ ¬∀ (i_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
                  ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
                ι →₀ S) :
              (a : ι) → S)
            (P.map i_1) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) 0 i_1 : S)

Tactic:
rw [sectionCotangent_eq_iff] at hi

Premises used: Algebra.SubmersivePresentation.sectionCotangent_eq_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi :
  ¬∀ (i_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
                  ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
                ι →₀ S) :
              (a : ι) → S)
            (P.map i_1) :
          S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) 0 i_1 : S)
⊢ ¬∀ (i_1 : σ), Eq.{u_2 + 1} (α := S) (if i = P.map i_1 then 1 else 0) 0

Tactic:
simp only [Basis.repr_self, map_zero, Pi.zero_apply, Finsupp.single_apply] at hi

Premises used: Pi.zero_apply, map_zero, Finsupp.single_apply, Module.Basis.repr_self
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi : ¬∀ (i_1 : σ), Eq.{u_2 + 1} (α := S) (if i = P.map i_1 then 1 else 0) 0
⊢ i ∈ Set.range P.map

Tactic:
grind
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
i : ι
hi : i ∉ Set.range P.map
contrapose contrapose₁ :
  ∀ (hi : i ∉ Set.range P.map),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
contrapose₂ contrapose₃ contrapose₄ :
  ∀
    (hi :
      ¬Eq (α := P.toExtension.Cotangent)
          ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
              ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
            P.toExtension.Cotangent)
          (0 : P.toExtension.Cotangent)),
    i ∈ Set.range P.map
contrapose₅ :
  ∀
    (hi :
      ¬∀ (i_1 : σ),
          Eq.{u_2 + 1} (α := S)
            ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
                      ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
                    ι →₀ S) :
                  (a : ι) → S)
                (P.map i_1) :
              S)
            ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) 0 i_1 : S)),
    i ∈ Set.range P.map
contrapose₆ : ∀ (hi : ¬∀ (i_1 : σ), Eq.{u_2 + 1} (α := S) (if i = P.map i_1 then 1 else 0) 0), i ∈ Set.range P.map
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)

Tactic:
classical
  contrapose hi
  rw [sectionCotangent_eq_iff] at hi
  simp only [Basis.repr_self, map_zero, Pi.zero_apply, Finsupp.single_apply] at hi
  grind

Premises used: Pi.zero_apply, map_zero, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Finsupp.single_apply, Module.Basis.repr_self
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
hsa :
  ∀ (i : κ),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (f i)) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
hlib :
  LinearIndependent S (M := P.toExtension.Cotangent)
    (Function.comp (β := P.toExtension.CotangentSpace)
      (⇑P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
      ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))
hab : Codisjoint (Set.range f) (Set.range P.map)
⊢ Basis κ S Ω[S⁄R]

Tactic:
apply P.cotangentSpaceBasis.ofSplitExact (sectionCotangent_comp P)
    Extension.exact_cotangentComplex_toKaehler Extension.toKaehler_surjective hf (b := P.map)

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Generators.cotangentSpaceBasis, Algebra.Extension.toKaehler_surjective, Module.Basis.ofSplitExact, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.Extension.exact_cotangentComplex_toKaehler, Algebra.Presentation.toGenerators
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
i : κ
hsa : f i ∉ Set.range P.map
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (f i)) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)

Tactic:
apply sectionCotangent_zero_of_notMem_range _ _

Premises used: Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range