-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_map [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B]
    (h : Function.Surjective (algebraMap A B)) :
    (KaehlerDifferential.kerTotal R A).map finsupp_map ⊔
        Submodule.span A (Set.range fun x : S => .single (algebraMap S B x) (1 : B)) =
      (KaehlerDifferential.kerTotal S B).restrictScalars _

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (Set.range fun x =>
          single ((algebraMap A B) x.1) 1 + single ((algebraMap A B) x.2) 1 -
            single ((algebraMap A B) x.1 + (algebraMap A B) x.2) 1) ⊔
      (Submodule.span A
          (Set.range fun x =>
            single ((algebraMap A B) x.2) ((algebraMap A B) x.1) +
                single ((algebraMap A B) x.1) ((algebraMap A B) x.2) -
              single ((algebraMap A B) x.1 * (algebraMap A B) x.2) 1) ⊔
        (Submodule.span A (Set.range fun x => single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔
          Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1))) =
    Submodule.span A
        (Set.range
          ((fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∘
            Prod.map ⇑(algebraMap A B) ⇑(algebraMap A B))) ⊔
      (Submodule.span A
          (Set.range
            ((fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∘
              Prod.map ⇑(algebraMap A B) ⇑(algebraMap A B))) ⊔
        Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1))

Tactic:
congr!

Result:
case h.e'_4.h.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x => single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔
      Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1) =
    Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1)

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1) =
    Submodule.restrictScalars A (kerTotal S B)

Tactic:
rw [KaehlerDifferential.kerTotal, Submodule.map_span, KaehlerDifferential.kerTotal,
  Submodule.restrictScalars_span _ _ h]

Result:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
          (((Set.range fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
              Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
            Set.range fun x => single ((algebraMap R A) x) 1)) ⊔
      Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1) =
    Submodule.span A
      (((Set.range fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
          Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
        Set.range fun x => single ((algebraMap S B) x) 1)

Proof state:
case h.e'_4.h.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x => single ((algebraMap R B) x) 1) ⊔
      Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1) =
    Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1)

Tactic:
rw [sup_eq_right]

Result:
case h.e'_4.h.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x => single ((algebraMap R B) x) 1) ≤
    Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1)