-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δ_map
    (Q : Generators.{u₁} S T) (P : Generators.{u₂} R S)
    (Q' : Generators.{u₃} S T) (P' : Generators.{u₄} R S) (f : Hom Q' Q) (x) :
    δ Q P (Extension.H1Cotangent.map f.toExtensionHom x) = δ Q' P' x

Proof state:
case mk.intro.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δAux R Q') y +
      (Finsupp.linearCombination T (⇑(δAux R Q) ∘ f.val))
        (Q'.cotangentSpaceBasis.repr (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y)) =
    (δAux R Q') y

Tactic:
rw [hx, map_zero, map_zero, add_zero]

Result:
no goals

Proof state:
case mk.intro.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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 : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩) =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩

Tactic:
show δ _ _ ⟨_, _⟩ = δ _ _ _

Result:
case mk.intro.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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 : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ (δ Q P)
      ⟨((Extension.Cotangent.map f.toExtensionHom).domRestrict (LinearMap.ker Q'.toExtension.cotangentComplex))
          ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩,
        ⋯⟩ =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
Q' : Generators S T
P' : Generators R S
f : Q'.Hom Q
x : Q'.toExtension.H1Cotangent
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) x) = (δ Q' P') x

Tactic:
letI : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) x) = (δ Q' P') x

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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 : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0

Tactic:
simpa only [LinearMap.mem_ker, Extension.cotangentComplex_mk, ker, RingHom.mem_ker] using hx

Result:
no goals

Proof state:
case mk.intro.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δAux R Q) (f.toExtensionHom.toAlgHom y) = (δAux R Q') y

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

Result:
case mk.intro.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δAux R Q') y +
      (Finsupp.linearCombination T (⇑(δAux R Q) ∘ f.val))
        (Q'.cotangentSpaceBasis.repr (1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y)) =
    (δAux R Q') y

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) x) = (δ Q' P') x

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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 ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨x, hx⟩) = (δ Q' P') ⟨x, hx⟩

Proof state:
case mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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 ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨x, hx⟩) = (δ Q' P') ⟨x, hx⟩

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Result:
case mk.intro.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
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 : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩) =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩