-- Mathlib/RingTheory/Etale/Kaehler.lean
lemma tensorH1CotangentOfIsLocalization_toLinearMap
    (M : Submonoid S) [IsLocalization M T] :
    (tensorH1CotangentOfIsLocalization R T M).toLinearMap =
      (Algebra.H1Cotangent.map R R S T).liftBaseChange T

Proof state:
case hf
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
i : T
⊢ ((IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ)) (MvPolynomial.X i) =
    (IsScalarTower.toAlgHom R (Generators.self R T).toExtension.Ring T) (MvPolynomial.X i)

Tactic:
show _ = algebraMap (Generators.self R T).Ring _ (.X i)

Result:
case hf
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
i : T
⊢ ((IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ)) (MvPolynomial.X i) =
    (algebraMap (Generators.self R T).Ring T) (MvPolynomial.X i)

Proof state:
case a.h.h
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)
        (Generators.self R T).toExtension)
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x

Tactic:
rw [← Extension.H1Cotangent.equivOfFormallySmooth_symm, LinearEquiv.symm_apply_eq,
  @Extension.H1Cotangent.equivOfFormallySmooth_apply (f := f),
  Algebra.H1Cotangent.map, ← (Extension.H1Cotangent.map f).coe_restrictScalars S,
  ← LinearMap.comp_apply, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq]

Result:
no goals

Proof state:
case intro.intro.mk.intro.intro
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) x =
    ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨s, ⋯⟩ *
      IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
simp

Result:
no goals

Proof state:
case a.h.h
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)
        (Generators.self R T).toExtension)
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x

Tactic:
letI Q : Extension R T := .ofSurjective fQ (by
  intro x
  obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective M x
  obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
  obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
  refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
  simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
  rw [IsLocalization.lift_mk'_spec]
  simp)

Result:
case a.h.h
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)
        (Generators.self R T).toExtension)
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x

Proof state:
case intro.intro.mk.intro
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
s : S
hs : s ∈ M
x : P.Ring
⊢ ∃ a, fQ a = IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨s, hs⟩

Tactic:
obtain ⟨s, rfl⟩ := P.algebraMap_surjective s

Result:
case intro.intro.mk.intro.intro
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ∃ a, fQ a = IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩