awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (hypothesis)
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)
⊢ IsUnit P.jacobian
have 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 sorry) : (a : P.toExtension.Cotangent) → σ →₀ S)
      (⇑b : (a : σ) → P.toExtension.Cotangent)))
Tactic: have heq : (fun j i ↦ (aeval P.val) (pderiv (P.map i) (P.relation j))) =
      Finsupp.linearEquivFunOnFinite S S _ ∘ P.cotangentRestrict P.map_inj ∘ ⇑b := by
    ext i j
    simp only [Function.comp_apply, hb, Finsupp.linearEquivFunOnFinite_apply, cotangentRestrict_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
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)))
⊢ IsUnit P.jacobian
have hli : LinearIndependent S (M := (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)
Tactic: apply P.isUnit_jacobian_of_linearIndependent_of_span_eq_top
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
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)))
hli :
  LinearIndependent S (M := (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)
⊢ IsUnit P.jacobian
have hsp : Eq (α := Submodule S ((i : σ) → S))
  (Submodule.span S
    (Set.range fun (j i : σ) ↦
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
  ⊤
Tactic: apply P.isUnit_jacobian_of_linearIndependent_of_span_eq_top
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
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) fun (j i : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)
have hli : LinearIndependent (ι := σ) S (M := (i : σ) → S)
  (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
    (Function.comp (β := P.toExtension.Cotangent) (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → σ →₀ S)
      (⇑b : (a : σ) → P.toExtension.Cotangent)))
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
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)))
⊢ Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
have hsp : Eq (α := Submodule S ((i : σ) → S))
  (Submodule.span S
    (Set.range (ι := σ)
      (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Function.comp (β := P.toExtension.Cotangent)
          (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → σ →₀ S)
          (⇑b : (a : σ) → P.toExtension.Cotangent)))))
  ⊤
Tactic: rw [heq, Set.range_comp, Set.range_comp, Submodule.span_image_linearEquiv, ← Submodule.map_span,
      b.span_eq, Submodule.map_top, LinearMap.range_eq_top_of_surjective _ h.surjective,
      Submodule.map_top, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
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)))
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range (ι := σ)
        (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)))))
    ⊤
⊢ Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
have hsp₁ : Eq (α := Submodule S ((i : σ) → S))
  (Submodule.span S
    (Set.image (α := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Set.range (ι := σ)
        (Function.comp (β := P.toExtension.Cotangent)
          (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → σ →₀ S)
          (⇑b : (a : σ) → P.toExtension.Cotangent)))))
  ⊤
Tactic: rw [heq, Set.range_comp, Set.range_comp, Submodule.span_image_linearEquiv, ← Submodule.map_span,
      b.span_eq, Submodule.map_top, LinearMap.range_eq_top_of_surjective _ h.surjective,
      Submodule.map_top, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
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)))
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range (ι := σ)
        (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)))))
    ⊤
hsp₁ :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.image (α := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Set.range (ι := σ)
          (Function.comp (β := P.toExtension.Cotangent)
            (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
            (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ⊤
⊢ Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
have hsp₂ : Eq (α := Submodule S ((i : σ) → S))
  (Submodule.span S
    (Set.image (α := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Set.image (α := P.toExtension.Cotangent) (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → σ →₀ S)
        (Set.range (ι := σ) (⇑b : (a : σ) → P.toExtension.Cotangent)))))
  ⊤
Tactic: rw [heq, Set.range_comp, Set.range_comp, Submodule.span_image_linearEquiv, ← Submodule.map_span,
      b.span_eq, Submodule.map_top, LinearMap.range_eq_top_of_surjective _ h.surjective,
      Submodule.map_top, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
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}))
have rw : Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
  (Ideal.span
    (Set.image (α := Generators.Ring (comp (localizationAway T g) P))
      (⇑(Hom.toAlgHom (ofComp (localizationAway T g) P)) :
        (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
      {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: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
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
rw :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.span
      (Set.image (α := Generators.Ring (comp (localizationAway T g) P))
        (⇑(Hom.toAlgHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
        {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 (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}))
have rw₁ : Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
  (Ideal.span
    (singleton (α := Generators.Ring (localizationAway T g))
      ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
            (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
          (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) :
        Generators.Ring (localizationAway T g))))
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (hypothesis)
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 (comp (localizationAway T g) P))) (ker (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.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})
have 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}))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
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))) (ker (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.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})
have rw : 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: rw [ker_comp_eq_sup, Algebra.Generators.map_toComp_ker, this,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective _ P), ← RingHom.ker_eq_comap_bot,
    ← sup_assoc]