awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : Generators.Ring (comp (localizationAway T g) P)}
    (hx :
      Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                  MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                (X (Sum.inl ())) -
              1})
        x),
    Eq (α :=
      Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      ((compLocalizationAwayAlgHom T g P :
            (a : ((localizationAway T g).comp P).Ring) →
              Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
          x :
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (0 :
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
x : Generators.Ring (comp (localizationAway T g) P)
hx :
  Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
              MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
            (X (Sum.inl ())) -
          1})
    x
y : Generators.Ring (comp (localizationAway T g) P)
hy :
  Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
      (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker)
    y
⊢ Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (RingHom.ker (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (compLocalizationAwayAlgHom T g P))
    (x * y)

Tactic:
simp [hsple hx]
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : Generators.Ring (comp (localizationAway T g) P)}
    (hx :
      Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                  MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                (X (Sum.inl ())) -
              1})
        x),
    Eq (α :=
      Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      ((compLocalizationAwayAlgHom T g P :
            (a : ((localizationAway T g).comp P).Ring) →
              Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
          x :
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (0 :
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
x : Generators.Ring (comp (localizationAway T g) P)
hx :
  Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
              MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
            (X (Sum.inl ())) -
          1})
    x
y : Generators.Ring (comp (localizationAway T g) P)
hy :
  Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
              MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
            (X (Sum.inl ())) -
          1})
    y
⊢ Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (RingHom.ker (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (compLocalizationAwayAlgHom T g P))
    (x * y)

Tactic:
simp [hsple hx]
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
set :
  let Q : Generators S T Unit := localizationAway T g;
  Function.Injective (α := T ⊗[S] P.toExtension.Cotangent) (β := Extension.Cotangent (toExtension (Q.comp P)))
    (⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
      (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
⊢ Function.Injective (α := T ⊗[S] P.toExtension.Cotangent) (β :=
    Extension.Cotangent (toExtension (comp (localizationAway T g) P)))
    (⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (toComp (localizationAway T g) P)))) :
      (a : T ⊗[S] P.toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)

Tactic:
set Q := Generators.localizationAway T g

Premises used: Algebra.Generators.localizationAway
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst : Algebra P.Ring (Generators.Ring (comp (localizationAway T g) P)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Hom.toAlgHom (toComp (localizationAway T g) P)))
f : P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2 :=
  (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)
π : Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
  Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) :=
  compLocalizationAwayAlgHom T g P
⊢ Function.Injective (α := T ⊗[S] P.toExtension.Cotangent) (β := Extension.Cotangent (toExtension (Q.comp P)))
    (⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
      (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)

Tactic:
IsLocalizedModule.injective_of_map_zero (Submonoid.powers g)
    (TensorProduct.mk S T P.toExtension.Cotangent 1) (fun x hx ↦ ?_)

Premises used: Submonoid.powers, Algebra.Generators.toExtension, IsLocalizedModule.injective_of_map_zero, OfNat.ofNat, DFunLike.coe, TensorProduct.mk, Algebra.Extension.Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst : Algebra P.Ring (Generators.Ring (comp (localizationAway T g) P)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Hom.toAlgHom (toComp (localizationAway T g) P)))
f : P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2 :=
  (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)
π : Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
  Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((lift
            ((↑S :
                {S_1 M : Type u_3} →
                  {M₂ : Type (max u_1 u_4)} →
                    [inst : Semiring S] →
                      [inst_8 : Semiring S_1] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [inst_13 : Module S_1 M] →
                                  [inst_14 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (S := T)
              (((↑(LinearEquiv.symm
                        (LinearMap.ringLmapEquivSelf T T
                          (P.toExtension.Cotangent →ₗ[S] Extension.Cotangent (toExtension (Q.comp P))))) :
                    (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →ₗ[T]
                      T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) :
                  (a : P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →
                    T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)
                (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))) :
          (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
        (((TensorProduct.mk S T P.toExtension.Cotangent :
                (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
              1 :
            (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x)) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (0 : Extension.Cotangent (toExtension (Q.comp P)))
n : ℕ
hm : P.σ g ^ n * (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2
⊢ g = (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ g)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst : Algebra P.Ring (Generators.Ring (comp (localizationAway T g) P)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Hom.toAlgHom (toComp (localizationAway T g) P)))
f : P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2 :=
  (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)
π : Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
  Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((lift
            ((↑S :
                {S_1 M : Type u_3} →
                  {M₂ : Type (max u_1 u_4)} →
                    [inst : Semiring S] →
                      [inst_8 : Semiring S_1] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [inst_13 : Module S_1 M] →
                                  [inst_14 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (S := T)
              (((↑(LinearEquiv.symm
                        (LinearMap.ringLmapEquivSelf T T
                          (P.toExtension.Cotangent →ₗ[S] Extension.Cotangent (toExtension (Q.comp P))))) :
                    (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →ₗ[T]
                      T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) :
                  (a : P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →
                    T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)
                (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))) :
          (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
        (((TensorProduct.mk S T P.toExtension.Cotangent :
                (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
              1 :
            (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x)) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (0 : Extension.Cotangent (toExtension (Q.comp P)))
n : ℕ
hm : P.σ g ^ n * (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2
⊢ (↑(P.σ g ^ n • x) : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2

Tactic:
simpa using hm
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
rw :
  (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
    x
rw₁ :
  ((Module.Basis.constr (basisCotangentAway T g) T :
            (a : Unit → ((localizationAway T g).comp P).toExtension.Cotangent) →
              (localizationAway T g).toExtension.Cotangent →ₗ[T] ((localizationAway T g).comp P).toExtension.Cotangent)
          fun (x_1 : Unit) ↦ x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
    x
rw₂ rw₃ : x = x
⊢ (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      (cMulXSubOneCotangent T g) =
    x

Tactic:
rw [← basisCotangentAway_apply _ (), cotangentCompAwaySec, Module.Basis.constr_basis]

Premises used: Algebra.Generators.cotangentCompAwaySec, Unit.unit, Module.Basis.constr_basis, Algebra.Generators.basisCotangentAway_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
hx :
  Eq.{u_2 + 1} (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        x :
      Extension.Cotangent (toExtension (localizationAway T g)))
    (cMulXSubOneCotangent T g : Extension.Cotangent (toExtension (localizationAway T g)))
⊢ Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) ∘ₗ cotangentCompAwaySec g P x =
    LinearMap.id

Tactic:
(basisCotangentAway T g).ext fun r ↦ ?_

Premises used: Algebra.Generators.basisCotangentAway, Module.Basis.ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
hx :
  Eq.{u_2 + 1} (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        x :
      Extension.Cotangent (toExtension (localizationAway T g)))
    (cMulXSubOneCotangent T g : Extension.Cotangent (toExtension (localizationAway T g)))
refine :
  ∀ (r : Unit),
    Eq (α := Extension.Cotangent (toExtension (localizationAway T g)))
      ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) ∘ₗ cotangentCompAwaySec g P x :
            (a : (localizationAway T g).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
          ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) r) :
        Extension.Cotangent (toExtension (localizationAway T g)))
      ((LinearMap.id :
            (a : (localizationAway T g).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
          ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) r) :
        Extension.Cotangent (toExtension (localizationAway T g)))
⊢ Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) ∘ₗ cotangentCompAwaySec g P x =
    LinearMap.id

Tactic:
refine (basisCotangentAway T g).ext fun r ↦ ?_

Premises used: Algebra.Generators.basisCotangentAway, Module.Basis.ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
hx :
  Eq.{u_2 + 1} (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        x :
      Extension.Cotangent (toExtension (localizationAway T g)))
    (cMulXSubOneCotangent T g : Extension.Cotangent (toExtension (localizationAway T g)))
r : Unit
⊢ Eq (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) ∘ₗ cotangentCompAwaySec g P x :
          (a : (localizationAway T g).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) r) :
      Extension.Cotangent (toExtension (localizationAway T g)))
    ((LinearMap.id : (a : (localizationAway T g).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) r) :
      Extension.Cotangent (toExtension (localizationAway T g)))

Tactic:
simpa only [LinearMap.coe_comp, Function.comp_apply, basisCotangentAway_apply,
    cotangentCompAwaySec_apply]

Premises used: Algebra.Generators.cotangentCompAwaySec_apply, LinearMap.coe_comp, Function.comp_apply, Algebra.Generators.basisCotangentAway_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
hx :
  Eq.{u_2 + 1} (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        x :
      Extension.Cotangent (toExtension (localizationAway T g)))
    (cMulXSubOneCotangent T g : Extension.Cotangent (toExtension (localizationAway T g)))
⊢ ((cotangentCompLocalizationAwayEquiv g P hx).symm :
        (a : T ⊗[S] P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent) →
          ((localizationAway T g).comp P).toExtension.Cotangent)
      (0, cMulXSubOneCotangent T g) =
    x

Tactic:
simpa [cotangentCompLocalizationAwayEquiv, Function.Exact.splitSurjectiveEquiv] using
    cotangentCompAwaySec_apply g P x

Premises used: Algebra.Generators.cotangentCompLocalizationAwayEquiv, Algebra.Generators.cotangentCompAwaySec_apply, Function.Exact.splitSurjectiveEquiv