awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb :
  ∀ (r : σ),
    Eq (α := P.toExtension.Cotangent) ((b : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)
      ((Extension.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)
h :
  Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
heq :
  Eq (α := (j i : σ) → S)
    (fun (j i : σ) ↦
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R))
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := P.toExtension.Cotangent) (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
        (⇑b : (a : σ) → P.toExtension.Cotangent)))
⊢ LinearIndependent (ι := σ) S (M := (i : σ) → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := P.toExtension.Cotangent) (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
        (⇑b : (a : σ) → P.toExtension.Cotangent)))

Tactic:
exact (b.linearIndependent.map' _ (LinearMap.ker_eq_bot_of_injective h.injective)).map' _
      (Finsupp.linearEquivFunOnFinite S S σ).ker

Premises used: Finsupp.linearEquivFunOnFinite, LinearIndependent.map', Function.Bijective.injective, Module.Basis.linearIndependent, LinearMap.ker_eq_bot_of_injective, LinearEquiv.ker
-- 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 ι
f : P.Ring
h : (algebraMap P.Ring S : (a : P.Ring) → S) f = g
⊢ Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.map (R := Generators.Ring (comp (localizationAway T g) P)) (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
      (Hom.toAlgHom (ofComp (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) f :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1}))

Tactic:
have : (localizationAway T g).ker = Ideal.map ((localizationAway T g).ofComp P).toAlgHom
      (Ideal.span {MvPolynomial.rename Sum.inr f * MvPolynomial.X (Sum.inl ()) - 1}) := by
    rw [Ideal.map_span, Set.image_singleton, map_sub, map_mul, map_one, ker_localizationAway,
      Hom.toAlgHom_X, toAlgHom_ofComp_rename, h, ofComp_val, Sum.elim_inl]
-- 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 ι
f : P.Ring
h : (algebraMap P.Ring S : (a : P.Ring) → S) f = g
this :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.map (R := Generators.Ring (comp (localizationAway T g) P)) (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
      (Hom.toAlgHom (ofComp (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) f :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1}))
⊢ Eq (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (RingHom.ker (F := Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
          (Hom.toAlgHom (ofComp (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) f :
                  MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                (X (Sum.inl ())) -
              1} ⊔
      RingHom.ker (F := Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
        (Hom.toAlgHom (ofComp (localizationAway T g) P)))
    (RingHom.ker (F := Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
        (Hom.toAlgHom (ofComp (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) f :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1})

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 ι
x : P.Ring
⊢ 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)))
        ((Hom.toAlgHom (toComp (localizationAway T g) P) : (a : P.Ring) → ((localizationAway T g).comp P).Ring) 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))
    ((algebraMap P.Ring
            (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)) :
          (a : 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))

Tactic:
simp only [toComp_toAlgHom, compLocalizationAwayAlgHom, comp,
    localizationAway, AlgHom.toRingHom_eq_coe, aeval_rename,
    Sum.elim_comp_inr, ← IsScalarTower.toAlgHom_apply (R := R), ← comp_aeval_apply,
    aeval_X_left_apply]

Premises used: MvPolynomial.aeval_X_left_apply, Sum.elim_comp_inr, Algebra.Generators.comp, Algebra.Generators.toComp_toAlgHom, AlgHom.toRingHom_eq_coe, MvPolynomial.comp_aeval_apply, Algebra.Generators.compLocalizationAwayAlgHom, MvPolynomial.aeval_rename, Algebra.Generators.localizationAway, IsScalarTower.toAlgHom_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 ι
⊢ 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 (Sum.inl ())) :
      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))
    (IsLocalization.Away.invSelf (R := 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) :
      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))

Tactic:
simp [compLocalizationAwayAlgHom]

Premises used: Algebra.Generators.compLocalizationAwayAlgHom
-- 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 ι
⊢ HMul.hMul (α :=
        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))
        (β :=
        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))
        ((algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
                (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)) :
              (a : P.Ring ⧸ P.ker ^ 2) →
                Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
            ((algebraMap P.Ring (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)) :
          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))
        (IsLocalization.Away.invSelf (R := 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) :
          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)) -
      1 =
    0

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 ι
⊢ ∀ {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))

Tactic:
have hsple {x} (hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) :
        (compLocalizationAwayAlgHom T g P) x = 0 := by
    obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton.mp hx
    rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]
-- 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))
⊢ (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ g) = 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 ι
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))
a :
  HPow.hPow (β := ℕ) P.ker 2 ≤
    Ideal.comap (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
      (Hom.toAlgHom (toComp (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))
⊢ HMul.hMul (α := 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)
      (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
        (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker) ≤
    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)

Tactic:
rw [← Ideal.map_mul, Ideal.map_le_iff_le_comap, ← sq]

Premises used: Ideal.map_mul, sq, Ideal.map_le_iff_le_comap
-- 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.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
      (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker)
    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 hy]