-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
/-- A variant of `exact_map_δ` that takes in an arbitrary map between generators. -/
lemma exact_map_δ'
    (Q : Generators.{u₁} S T) (P : Generators.{u₂} R S) (P' : Generators.{u₃} R T) (f : Hom P' Q) :
    Function.Exact (Extension.H1Cotangent.map f.toExtensionHom) (δ Q P)

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map f.toExtensionHom) ⇑(δ Q P)

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

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv (Q.comp P) P')) ⇑(δ Q P)

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv (Q.comp P) P')) ⇑(δ Q P)

Tactic:
show Function.Exact ((Extension.H1Cotangent.map f.toExtensionHom).restrictScalars T ∘ₗ
  (Extension.H1Cotangent.map _)) (δ Q P)

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact
    ⇑(↑T (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map ((Q.comp P).defaultHom P').toExtensionHom)
    ⇑(δ Q P)

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(δ Q P)

Tactic:
exact exact_map_δ Q P

Result:
no goals

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact
    ⇑(↑T (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map ((Q.comp P).defaultHom P').toExtensionHom)
    ⇑(δ Q P)

Tactic:
rw [← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq _ (Q.ofComp P).toExtensionHom]

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
P' : Generators R T
f : P'.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(δ Q P)