-- 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 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⟩

Tactic:
refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩

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
⊢ fQ (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

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
⊢ (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 M' := M.comap (algebraMap P.Ring S)

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
⊢ (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 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
⊢ (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 P : Extension R S := (Generators.self R S).toExtension

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
⊢ (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:
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
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩

Result:
no goals

Proof state:
case intro.intro.mk
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 : S
hs : s ∈ M
⊢ ∃ a, fQ a = IsLocalization.mk' T x ⟨s, hs⟩

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

Result:
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⟩

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
⊢ fQ (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]

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
⊢ (IsLocalization.lift ⋯) (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩