awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
h : x = 0
subst :
  Eq (α :=
    HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ((Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      0)
    0
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      0 =
    x

Tactic:
subst h
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq (α :=
    HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ((Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      0)
    0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
h_1 : ¬x = 0
h : x = -1
subst :
  ¬Eq (α :=
        HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
        (-1) 0 →
    Eq (α :=
      HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
        (Ideal.span
          (Set.range (ι := σ)
            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
      ((Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
          (a : MvPolynomial ι R) →
            MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
        (-1))
      (-1)
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (-1) =
    x

Tactic:
subst h
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
h :
  ¬Eq (α :=
      HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
        (Ideal.span
          (Set.range (ι := σ)
            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
      (-1) 0
⊢ Eq (α :=
    HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ((Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (-1))
    (-1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
h : ¬x = 0
h_1 : ¬x = -1
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (Function.surjInv (f :=
        (⇑(Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
          (a : MvPolynomial ι R) →
            MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
        ⋯ x) =
    x

Tactic:
simp [Function.surjInv_eq]

Premises used: Function.surjInv_eq
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : ι
⊢ Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (X i) : S)
    ((algebraMap D.T S : (a : D.T) → S) (D.presLeft.val i) : S)

Tactic:
simp [RingHom.algebraMap_toAlgebra, presLeft, hom, T]

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T, RingHom.algebraMap_toAlgebra, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hom
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
hf :
  ∀ (i : ι),
    Eq (α := P.Ring) ((D.fhom.toAlgHom : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
      ((AlgHom.id R P.Ring : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
⊢ D.fhom.toAlgHom = AlgHom.id R P.Ring

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : ι
⊢ Eq (α := P.Ring) ((D.fhom.toAlgHom : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
    ((AlgHom.id R P.Ring : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)

Tactic:
simp [fhom]

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.fhom
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : D.presLeft.Ring
hx : x ∈ D.presLeft.ker
⊢ x ∈ P.ker

Tactic:
simpa only [toExtension_commRing, toExtension_Ring, RingHom.mem_ker,
    toExtension_algebra₂, algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    map_zero] using (algebraMap D.T S).congr_arg hx

Premises used: Algebra.algebraMap, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T, Ideal.Quotient.algebraMap_eq, Algebra.Generators.toExtension_algebra₂, Algebra.Generators.algebraMap_apply, RingHom.mem_ker, map_zero, Algebra.Generators.toExtension_Ring, RingHom.congr_arg, Algebra.Generators.toExtension_commRing
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : σ
⊢ Eq (α := S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    ((D.tensorCotangentInv : (a : P.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
        ((b : (a : σ) → P.toExtension.Cotangent) i) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    (1 ⊗ₜ[D.T]
        (Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)

Tactic:
Module.Basis.constr_basis _ _ _ _

Premises used: Set.Mem, Module.Basis.constr_basis
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq (α := Submodule D.T D.presLeft.toExtension.Cotangent)
    (Submodule.span D.T
      (Set.range fun (i : σ) ↦
        (Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)))
    ⊤

Tactic:
Extension.Cotangent.span_eq_top_of_span_eq_ker _ ?_

Premises used: Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, Set.Mem, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine :
  Ideal.span (Set.range fun (i : σ) ↦ (↑(D.f ((b : (a : σ) → P.toExtension.Cotangent) i)) : P.toExtension.Ring)) =
    D.presLeft.toExtension.ker
⊢ Eq (α := Submodule D.T D.presLeft.toExtension.Cotangent)
    (Submodule.span D.T
      (Set.range fun (i : σ) ↦
        (Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)))
    ⊤

Tactic:
refine Extension.Cotangent.span_eq_top_of_span_eq_ker _ ?_

Premises used: Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Ideal.span (Set.range fun (i : σ) ↦ (↑(D.f ((b : (a : σ) → P.toExtension.Cotangent) i)) : P.toExtension.Ring)) =
    (naive
          (fun
              (x :
                HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) ↦
            if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
          ⋯).toExtension.ker

Tactic:
(Generators.ker_naive _ _).symm

Premises used: AddMonoidAlgebra.singleZeroRingHom, Quotient, AddMonoidAlgebra, Eq.symm, Algebra.Generators.ker_naive, Algebra.Generators.naive, Finsupp.single
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Ideal.span (Set.range fun (i : σ) ↦ (↑(D.f ((b : (a : σ) → P.toExtension.Cotangent) i)) : P.toExtension.Ring)) =
    (naive
          (fun
              (x :
                HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) ↦
            if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
          ⋯).toExtension.ker

Tactic:
exact (Generators.ker_naive _ _).symm

Premises used: Eq.symm, Algebra.Generators.ker_naive
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_1 : D.tensorCotangentHom ∘ₗ D.tensorCotangentInv = LinearMap.id
refine_2 : D.tensorCotangentInv ∘ₗ D.tensorCotangentHom = LinearMap.id
⊢ S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent

Tactic:
refine LinearEquiv.ofLinear D.tensorCotangentHom D.tensorCotangentInv ?_ ?_

Premises used: LinearEquiv.ofLinear, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentInv, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.tensorCotangentHom ∘ₗ D.tensorCotangentInv = LinearMap.id

Tactic:
b.ext fun i ↦ ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_1 :
  ∀ (i : σ),
    Eq (α := P.toExtension.Cotangent)
      ((D.tensorCotangentHom ∘ₗ D.tensorCotangentInv : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
          ((b : (a : σ) → P.toExtension.Cotangent) i) :
        P.toExtension.Cotangent)
      ((LinearMap.id : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
          ((b : (a : σ) → P.toExtension.Cotangent) i) :
        P.toExtension.Cotangent)
⊢ D.tensorCotangentHom ∘ₗ D.tensorCotangentInv = LinearMap.id

Tactic:
refine b.ext fun i ↦ ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : σ
⊢ Eq (α := P.toExtension.Cotangent)
    ((D.tensorCotangentHom ∘ₗ D.tensorCotangentInv : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
        ((b : (a : σ) → P.toExtension.Cotangent) i) :
      P.toExtension.Cotangent)
    ((LinearMap.id : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
        ((b : (a : σ) → P.toExtension.Cotangent) i) :
      P.toExtension.Cotangent)

Tactic:
simpa only [LinearMap.coe_comp, Function.comp_apply, tensorCotangentInv_apply,
      tensorCotangentHom_tmul] using D.hf (b i)

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hf, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentInv_apply, LinearMap.coe_comp, Function.comp_apply, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom_tmul, DFunLike.coe
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_2 :
  Eq (α :=
    LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent (S ⊗[D.T] D.presLeft.toExtension.Cotangent))
    (((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)
    (((AlgebraTensorModule.curry LinearMap.id :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)
⊢ D.tensorCotangentInv ∘ₗ D.tensorCotangentHom = LinearMap.id

Tactic:
ext : 2
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq (α :=
    LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent (S ⊗[D.T] D.presLeft.toExtension.Cotangent))
    (((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)
    (((AlgebraTensorModule.curry LinearMap.id :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)

Tactic:
LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_

Premises used: LinearMap.ext_on_range, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.span_range_mk_kerGen
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_2 :
  ∀ (i : σ),
    Eq (α := S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      ((((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
                  S →ₗ[S]
                    LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
                      (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
                (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
              1 :
            (a : D.presLeft.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent)
            (D.kerGen i)) :
        S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      ((((AlgebraTensorModule.curry LinearMap.id :
                  S →ₗ[S]
                    LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
                      (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
                (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
              1 :
            (a : D.presLeft.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent)
            (D.kerGen i)) :
        S ⊗[D.T] D.presLeft.toExtension.Cotangent)
⊢ Eq (α :=
    LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent (S ⊗[D.T] D.presLeft.toExtension.Cotangent))
    (((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)
    (((AlgebraTensorModule.curry LinearMap.id :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)

Tactic:
refine LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_

Premises used: LinearMap.ext_on_range, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.span_range_mk_kerGen