-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma exact_δ_map :
    Function.Exact (δ Q P) (mapBaseChange R S T)

Proof state:
case hF
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
⊢ ∀ (i : P.vars),
    (mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler)
        ((Basis.baseChange T P.cotangentSpaceBasis) i) =
      ((Q.comp P).toExtension.toKaehler ∘ₗ
          LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)

Tactic:
intro i

Result:
case hF
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
i : P.vars
⊢ (mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler)
      ((Basis.baseChange T P.cotangentSpaceBasis) i) =
    ((Q.comp P).toExtension.toKaehler ∘ₗ
        LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
      ((Basis.baseChange T P.cotangentSpaceBasis) i)

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
⊢ Function.Exact ⇑(δ Q P) ⇑(mapBaseChange R S T)

Tactic:
simp only [δ]

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
⊢ Function.Exact
    ⇑(SnakeLemma.δ' (LinearMap.baseChange T P.toExtension.cotangentComplex) (Q.comp P).toExtension.cotangentComplex
        Q.toExtension.cotangentComplex
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ⋯
        (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ⋯ ⋯ ⋯ Extension.h1Cotangentι ⋯
        (LinearMap.baseChange T P.toExtension.toKaehler) ⋯ ⋯ ⋯)
    ⇑(mapBaseChange R S T)

Proof state:
case hF
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
i : P.vars
⊢ (mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler)
      ((Basis.baseChange T P.cotangentSpaceBasis) i) =
    ((Q.comp P).toExtension.toKaehler ∘ₗ
        LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
      ((Basis.baseChange T P.cotangentSpaceBasis) i)

Tactic:
simp only [Basis.baseChange_apply, LinearMap.coe_comp, Function.comp_apply,
  LinearMap.baseChange_tmul, toKaehler_cotangentSpaceBasis, mapBaseChange_tmul, map_D,
  one_smul, comp_vars, LinearMap.liftBaseChange_tmul]

Result:
case hF
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
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (P.cotangentSpaceBasis i))

Proof state:
case h
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
⊢ Function.Surjective ⇑(LinearMap.baseChange T P.toExtension.toKaehler)

Tactic:
exact LinearMap.lTensor_surjective T P.toExtension.toKaehler_surjective

Result:
no goals

Proof state:
case hF
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
⊢ mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler =
    (Q.comp P).toExtension.toKaehler ∘ₗ
      LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

Tactic:
apply (P.cotangentSpaceBasis.baseChange T).ext

Result:
case hF
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
⊢ ∀ (i : P.vars),
    (mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler)
        ((Basis.baseChange T P.cotangentSpaceBasis) i) =
      ((Q.comp P).toExtension.toKaehler ∘ₗ
          LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)

Proof state:
case hF
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
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))

Tactic:
conv_rhs => enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..

Result:
case hF
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
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((algebraMap S T) 1 ⊗ₜ[(Q.comp P).toExtension.Ring]
        (D R (Q.comp P).toExtension.Ring) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))

Proof state:
case hF
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
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((algebraMap S T) 1 ⊗ₜ[(Q.comp P).toExtension.Ring]
        (D R (Q.comp P).toExtension.Ring) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))

Tactic:
simp only [map_one, mapBaseChange_tmul, map_D, one_smul]

Result:
case hF
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
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (D R T) ((algebraMap (Q.comp P).toExtension.Ring T) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))

Proof state:
case hF
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
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (D R T) ((algebraMap (Q.comp P).toExtension.Ring T) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))

Tactic:
simp [Extension.Hom.toAlgHom]

Result:
no goals