awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
x : Q'.toExtension.H1Cotangent
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        ((Extension.H1Cotangent.map f.toExtensionHom : (a : Q'.toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
          x) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q' P' : (a : Q'.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R]) x : T ⊗[S] Ω[S⁄R])
have obtain : ∀ (x : Q'.toExtension.Cotangent) (hx : x ∈ Q'.toExtension.cotangentComplex.ker),
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        ((Extension.H1Cotangent.map f.toExtensionHom : (a : Q'.toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
          (Subtype.mk (p := fun (x : Q'.toExtension.Cotangent) ↦ x ∈ Q'.toExtension.cotangentComplex.ker) x hx)) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q' P' : (a : Q'.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q'.toExtension.Cotangent) ↦ x ∈ Q'.toExtension.cotangentComplex.ker) x hx) :
      T ⊗[S] Ω[S⁄R])
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
x : Q'.toExtension.Cotangent
hx : x ∈ Q'.toExtension.cotangentComplex.ker
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        ((Extension.H1Cotangent.map f.toExtensionHom : (a : Q'.toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
          (Subtype.mk (p := fun (x : Q'.toExtension.Cotangent) ↦ x ∈ Q'.toExtension.cotangentComplex.ker) x hx)) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q' P' : (a : Q'.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q'.toExtension.Cotangent) ↦ x ∈ Q'.toExtension.cotangentComplex.ker) x hx) :
      T ⊗[S] Ω[S⁄R])
have obtain : ∀ (y : Q'.toExtension.Ring) (hy : y ∈ Q'.toExtension.ker)
  (hx :
    Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
      ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
        Q'.toExtension.Cotangent)),
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        ((Extension.H1Cotangent.map f.toExtensionHom : (a : Q'.toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
          (Subtype.mk (p := fun (x : Q'.toExtension.Cotangent) ↦ x ∈ Q'.toExtension.cotangentComplex.ker)
            ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy))
            hx)) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q' P' : (a : Q'.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q'.toExtension.Cotangent) ↦ x ∈ Q'.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy))
          hx) :
      T ⊗[S] Ω[S⁄R])
Tactic: obtain ⟨⟨y, hy⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (hypothesis)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hx₁ : Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
  (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
  (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
Tactic: replace hx : (1 : T) ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0 := by
    simpa only [LinearMap.mem_ker, Extension.cotangentComplex_mk, ker, RingHom.mem_ker] using hx
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx_1 :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
hx :
  Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : Eq (α := T ⊗[S] Ω[S⁄R])
  ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
      ((Extension.Hom.toAlgHom f.toExtensionHom : (a : Q'.toExtension.Ring) → Q.toExtension.Ring) y) :
    T ⊗[S] Ω[S⁄R])
  ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
Tactic: simp only [LinearMap.domRestrict_apply, Extension.Cotangent.map_mk, δ_eq_δAux]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx_1 :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
hx :
  Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
        ((Extension.Hom.toAlgHom f.toExtensionHom : (a : Q'.toExtension.Ring) → Q.toExtension.Ring) y) :
      T ⊗[S] Ω[S⁄R])
    ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
have refine : HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
    ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
          (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
        ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T)
          (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y)) :
      T ⊗[S] Ω[S⁄R]) =
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
Tactic: refine (δAux_toAlgHom f _).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx_1 :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
hx :
  Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
⊢ HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T)
            (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y)) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
have rw : HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
    ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
          (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
        ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T) 0) :
      T ⊗[S] Ω[S⁄R]) =
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
Tactic: rw [hx, map_zero, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx_1 :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
hx :
  Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
rw :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T) 0) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
⊢ HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T)
            (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y)) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
have rw₁ : HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
    ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
          (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
        0 :
      T ⊗[S] Ω[S⁄R]) =
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
Tactic: rw [hx, map_zero, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx_1 :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
hx :
  Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
rw :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T) 0) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
rw₁ :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          0 :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
⊢ HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T)
            (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y)) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
have rw₂ : HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
    (0 : T ⊗[S] Ω[S⁄R]) =
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
Tactic: rw [hx, map_zero, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx_1 :
  Membership.mem (α := Q'.toExtension.Cotangent) Q'.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q'.toExtension.ker) → Q'.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q'.toExtension.Ring) ↦ x ∈ Q'.toExtension.ker) y hy) :
      Q'.toExtension.Cotangent)
hx :
  Eq (α := T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
    (0 : T ⊗[Q'.Ring] Ω[Q'.Ring⁄S])
rw :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T) 0) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
rw₁ :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          0 :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
rw₂ :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      (0 : T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
⊢ HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q) : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι' →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q'.cotangentSpaceBasis.repr : (a : Q'.toExtension.CotangentSpace) → ι' →₀ T)
            (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring : (a : Q'.Ring) → Ω[Q'.Ring⁄S]) y)) :
        T ⊗[S] Ω[S⁄R]) =
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y
have rw₃ : Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
  ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R])
Tactic: rw [hx, map_zero, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
⊢ δ Q P ∘ₗ (↑(equiv Q' Q) : Q'.toExtension.H1Cotangent →ₗ[T] Q.toExtension.H1Cotangent) = δ Q' P'
have h : ∀ (x : Q'.toExtension.H1Cotangent),
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P ∘ₗ (↑(equiv Q' Q) : Q'.toExtension.H1Cotangent →ₗ[T] Q.toExtension.H1Cotangent) :
          (a : Q'.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        x :
      T ⊗[S] Ω[S⁄R])
    ((δ Q' P' : (a : Q'.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R]) x : T ⊗[S] Ω[S⁄R])
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact (M := W.toExtension.H1Cotangent) (N := Q.toExtension.H1Cotangent) (P := T ⊗[S] Ω[S⁄R])
    (⇑(Extension.H1Cotangent.map f.toExtensionHom) : (a : W.toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
have refine : Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
  T ⊗[S] Ω[S⁄R])
  (⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ
        (↑(equiv (Q.comp P) W) : (Q.comp P).toExtension.H1Cotangent →ₗ[T] W.toExtension.H1Cotangent)) :
    (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
  (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
Tactic: refine (H1Cotangent.equiv (Q.comp P) W).surjective.comp_exact_iff_exact.mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ
          (↑(equiv (Q.comp P) W) : (Q.comp P).toExtension.H1Cotangent →ₗ[T] W.toExtension.H1Cotangent)) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
have change : Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
  T ⊗[S] Ω[S⁄R])
  (⇑((↑T :
            {S : Type u₃} →
              {M : Type (max u₁ w₅)} →
                {M₂ : Type (max u₂ w₁)} →
                  [inst : Semiring T] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module T M] →
                            [inst_11 : Module T M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ T S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[T] M₂)
          (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map (Hom.toExtensionHom (defaultHom (Q.comp P) W))) :
    (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
  (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
Tactic: change Function.Exact ((Extension.H1Cotangent.map f.toExtensionHom).restrictScalars T ∘ₗ
    (Extension.H1Cotangent.map _)) (δ Q P)
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑((↑T :
              {S : Type u₃} →
                {M : Type (max u₁ w₅)} →
                  {M₂ : Type (max u₂ w₁)} →
                    [inst : Semiring T] →
                      [inst_7 : Semiring S] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module T M] →
                              [inst_11 : Module T M₂] →
                                [inst_12 : Module S M] →
                                  [inst_13 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ T S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[T] M₂)
            (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
          Extension.H1Cotangent.map (Hom.toExtensionHom (defaultHom (Q.comp P) W))) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
have rw : Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
  T ⊗[S] Ω[S⁄R])
  (⇑(Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
    (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
  (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
Tactic: rw [← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq _ (Q.ofComp P).toExtensionHom]