-- Mathlib/RingTheory/Etale/Kaehler.lean
lemma KaehlerDifferential.isBaseChange_of_formallyEtale [Algebra.FormallyEtale S T] :
    IsBaseChange T (map R R S T)

Proof state:
case h.e'_3
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
inst✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T))

Tactic:
congr!

Result:
case h.e'_3.h.e'_5
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
inst✝ : Algebra.FormallyEtale S T
⊢ lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T))) =
    ↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T)

Proof state:
case h.e'_3.h.e'_5
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
inst✝ : Algebra.FormallyEtale S T
⊢ lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T))) =
    ↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T)

Tactic:
ext

Result:
case h.e'_3.h.e'_5.a.h.hf.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
inst✝ : Algebra.FormallyEtale S T
x✝ : T
a✝ : S
⊢ (((AlgebraTensorModule.curry
              (lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))))
            x✝).compDer
        (D R S))
      a✝ =
    (((AlgebraTensorModule.curry (↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T))) x✝).compDer (D R S)) a✝

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
inst✝ : Algebra.FormallyEtale S T
⊢ IsBaseChange T (map R R S T)

Tactic:
show Function.Bijective _

Result:
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
inst✝ : Algebra.FormallyEtale S T
⊢ Function.Bijective ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T))))

Proof state:
case h.e'_3.h.e'_5.a.h.hf.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
inst✝ : Algebra.FormallyEtale S T
x✝ : T
a✝ : S
⊢ (((AlgebraTensorModule.curry
              (lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))))
            x✝).compDer
        (D R S))
      a✝ =
    (((AlgebraTensorModule.curry (↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T))) x✝).compDer (D R S)) a✝

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
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
inst✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(tensorKaehlerEquivOfFormallyEtale R S T)

Tactic:
show _ = ((tensorKaehlerEquivOfFormallyEtale
  R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)

Result:
case h.e'_3
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
inst✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T))

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
inst✝ : Algebra.FormallyEtale S T
⊢ Function.Bijective ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T))))

Tactic:
convert (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1

Result:
case h.e'_3
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
inst✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(tensorKaehlerEquivOfFormallyEtale R S T)