awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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 σ
P' : Generators R S σ'
x : ↥Q.toExtension.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
h :
  Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : 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) x) hx) :
      T ⊗[S] Ω[S⁄R])
h₁ h₂ :
  Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
⊢ Eq (α := 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) 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)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])

Tactic:
rw [δ_eq_δAux, δ_eq_δAux]

Premises used: Algebra.Generators.H1Cotangent.δ_eq_δAux
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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₂
Q : Generators S T ι
P : Generators R S σ
hF :
  ∀ (x : Extension.H1Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.ker.Cotangent)
      (Extension.Cotangent.val
        ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ Extension.h1Cotangentι :
            (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.Cotangent)
          x))
      (Extension.Cotangent.val
        ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.Cotangent)
          x))
⊢ Eq (α := Extension.H1Cotangent (toExtension (Q.comp P)) →ₗ[T] Q.toExtension.Cotangent)
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ Extension.h1Cotangentι)
    (Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P)))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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₂
Q : Generators S T ι
P : Generators R S σ
x : Extension.H1Cotangent (toExtension (Q.comp P))
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ Extension.h1Cotangentι :
          (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.Cotangent)
        x))
    (Extension.Cotangent.val
      ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.Cotangent)
        x))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Injective (α := Q.toExtension.H1Cotangent) (β := Q.toExtension.Cotangent)
    (⇑Extension.h1Cotangentι : (a : Q.toExtension.H1Cotangent) → Q.toExtension.Cotangent)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective, Algebra.Extension.H1Cotangent
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Injective (α := Q.toExtension.H1Cotangent) (β := Q.toExtension.Cotangent)
    (⇑Extension.h1Cotangentι : (a : Q.toExtension.H1Cotangent) → Q.toExtension.Cotangent)

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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
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])
⊢ 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])

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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
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])
⊢ 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 ⟨⟨y, hy⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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)
⊢ 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:
simpa only [LinearMap.mem_ker, Extension.cotangentComplex_mk, ker, RingHom.mem_ker] using hx

Premises used: Algebra.Generators.ker, RingHom.mem_ker, LinearMap.mem_ker, Algebra.Extension.cotangentComplex_mk
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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)
⊢ 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
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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])
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])
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [LinearMap.domRestrict_apply, Extension.Cotangent.map_mk, δ_eq_δAux]

Premises used: Algebra.Generators.H1Cotangent.δ_eq_δAux, Algebra.Extension.Cotangent.map_mk, LinearMap.domRestrict_apply
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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])

Tactic:
(δAux_toAlgHom f _).trans ?_

Premises used: Algebra.Generators.H1Cotangent.δAux_toAlgHom, Eq.trans
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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])
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
⊢ 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:
refine (δAux_toAlgHom f _).trans ?_

Premises used: Algebra.Generators.H1Cotangent.δAux_toAlgHom, Eq.trans
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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
rw₃ 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])
⊢ 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:
rw [hx, map_zero, map_zero, add_zero]

Premises used: map_zero, add_zero
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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 σ'
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])
⊢ δ Q P ∘ₗ (↑(equiv Q' Q) : Q'.toExtension.H1Cotangent →ₗ[T] Q.toExtension.H1Cotangent) = δ Q' P'

Tactic:
ext x
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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 σ'
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:
δ_map Q P Q' P' _ _

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Algebra.Generators.H1Cotangent.δ_map
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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 σ'
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:
exact δ_map Q P Q' P' _ _

Premises used: Algebra.Generators.H1Cotangent.δ_map
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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])

Tactic:
(H1Cotangent.equiv (Q.comp P) W).surjective.comp_exact_iff_exact.mp ?_

Premises used: Algebra.Generators.H1Cotangent.equiv, Algebra.Generators.comp, LinearEquiv.surjective, Function.Surjective.comp_exact_iff_exact, Iff.mp
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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
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])
⊢ 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])

Tactic:
refine (H1Cotangent.equiv (Q.comp P) W).surjective.comp_exact_iff_exact.mp ?_

Premises used: Algebra.Generators.H1Cotangent.equiv, Algebra.Generators.comp, LinearEquiv.surjective, Function.Surjective.comp_exact_iff_exact, Iff.mp