awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
i : σ
hi : i ∈ c.support
a : Membership.mem (α := P.Ring) P.ker ((c : (a : σ) → P.Ring) i : P.Ring)
⊢ (fun (i : σ) (a : P.Ring) ↦ a * P.relation i) i ((c : (a : σ) → P.Ring) i) ∈ P.ker * P.ker
have a₁ : P.relation i ∈ P.ker
Tactic: apply Ideal.mul_mem_mul
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this_1 : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      (∑ x ∈ c.support,
        HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
              ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
            S))
      0
heq2 :
  Eq (α := (j : σ) → S)
    (∑ i ∈ c.support,
      HSMul.hSMul (α := S) (β := (j : σ) → S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) fun (j : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R))
    0
this :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) i : P.Ring) : S) (0 : S)
i : σ
hi : i ∈ c.support
⊢ Membership.mem (α := P.Ring) P.ker ((c : (a : σ) → P.Ring) i : P.Ring)
have a : Membership.mem (α := P.Ring) (γ := Ideal P.Ring) (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))
  ((c : (a : σ) → P.Ring) i : P.Ring)
Tactic: rw [P.ker_eq_ker_aeval_val]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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.Surjective (α := P.toExtension.Cotangent) (β := σ → S)
    (⇑P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
have rw : Set.range (ι := σ) (⇑P.basisDeriv : (a : σ) → σ → S) ⊆ (↑P.cotangentComplexAux.range : Set (σ → S))
Tactic: rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← P.basisDeriv.span_eq, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : σ
⊢ Membership.mem (α := σ → S) (↑P.cotangentComplexAux.range : Set (σ → S)) ((P.basisDeriv : (a : σ) → σ → S) i : σ → S)
have h : Eq (α := σ → S)
  ((P.cotangentComplexAux : (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 i) sorry) :
        P.toExtension.Cotangent) :
    σ → S)
  ((P.basisDeriv : (a : σ) → σ → S) i : σ → S)
Tactic: use Cotangent.mk ⟨P.relation i, P.relation_mem_ker i⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : σ
⊢ Eq (α := σ → S)
    ((P.cotangentComplexAux : (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 i) ⋯) :
          P.toExtension.Cotangent) :
      σ → S)
    ((P.basisDeriv : (a : σ) → σ → S) i : σ → S)
have h : ∀ (j : σ),
  Eq.{u_2 + 1} (α := S)
    ((P.cotangentComplexAux : (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 i) sorry) :
          P.toExtension.Cotangent)
        j :
      S)
    ((P.basisDeriv : (a : σ) → σ → S) i j : S)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 j : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((P.cotangentComplexAux : (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 i) ⋯) :
          P.toExtension.Cotangent)
        j :
      S)
    ((P.basisDeriv : (a : σ) → σ → S) i j : S)
have h : Eq.{u_2 + 1} (α := S)
  ((aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R)
          (↑(Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation i) sorry) : P.Ring) :
        MvPolynomial ι R) :
    S)
  ((P.basisDeriv : (a : σ) → σ → S) i j : S)
Tactic: rw [P.cotangentComplexAux_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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)
have this : Function.Injective (α := P.toExtension.Cotangent) (β := σ → S)
  (⇑P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
Tactic: have := P.cotangentComplexAux_injective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 ι σ
⊢ Subsingleton P.toExtension.H1Cotangent
have rw : Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
  (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
Tactic: rw [Algebra.Extension.subsingleton_h1Cotangent]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : σ
⊢ 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)
have 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) sorry) :
    P.toExtension.Cotangent)
  ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : σ
⊢ 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)
have 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) sorry) :
        P.toExtension.Cotangent) :
    σ → S)
  ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
      ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent) :
    σ → S)
Tactic: apply P.cotangentEquiv.injective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : σ
⊢ 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)
have 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) sorry) :
          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: ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
    ((P.cotangentEquiv : (a : P.toExtension.Cotangent) → σ → S)
        ((P.basisCotangent : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent) x :
      S)
have 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) sorry) :
        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: simp_rw [basisCotangent, Basis.map_apply, LinearEquiv.apply_symm_apply, basisDeriv_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ (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)
have simp : (P.cotangentEquiv.symm : (a : σ → S) → P.toExtension.Cotangent)
      ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
        ((Finsupp.lcomapDomain P.map sorry : (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: simp only [sectionCotangent, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ (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)
have rw : (∀ (x_1 : σ),
    Eq.{u_2 + 1} (α := S)
      ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
          ((Finsupp.lcomapDomain P.map sorry : (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: rw [← (cotangentEquiv P).injective.eq_iff, funext_iff, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 ι σ
⊢ P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ 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)
have h : (P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
    ((P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace) x) =
  x
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ (P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
      ((P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace) x) =
    x
have 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)
Tactic: rw [sectionCotangent_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ 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)
have 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
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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 ∈ Set.range P.map
have 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)
Tactic: rw [sectionCotangent_eq_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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 ∈ Set.range P.map
have hi₁ : ¬∀ (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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ 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)
have 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)
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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
⊢ 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)
have contrapose₂ : ¬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
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
Cleared hypotheses: hi