-- 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 =>
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.1 1) +
                  (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.2 1) -
                (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
                  (single (x.1 + x.2) 1)) ⊔
          Submodule.span A
            (Set.range fun x =>
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.2 x.1) +
                  (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.1 x.2) -
                (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
                  (single (x.1 * x.2) 1)) ⊔
        Submodule.span A
          (Set.range fun x =>
            (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
              (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) ⊔
        Submodule.span A (Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
      Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1)

Tactic:
simp only [LinearMap.comp_apply, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single,
  Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply,
  map_one, map_add, map_mul]

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
            (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) ⊔
        Submodule.span A (Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
      Submodule.span A (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)

Tactic:
apply Submodule.span_mono

Result:
case h.e'_4.h.e'_4.h
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)
⊢ (Set.range fun x => single ((algebraMap R B) x) 1) ⊆ 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.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)

Tactic:
simp_rw [Set.image_union, Submodule.span_union, ← Set.image_univ, Set.image_image, Set.image_univ,
  map_sub, map_add]

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
            (Set.range fun x =>
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.1 1) +
                  (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.2 1) -
                (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
                  (single (x.1 + x.2) 1)) ⊔
          Submodule.span A
            (Set.range fun x =>
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.2 x.1) +
                  (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.1 x.2) -
                (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
                  (single (x.1 * x.2) 1)) ⊔
        Submodule.span A
          (Set.range fun x =>
            (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
              (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) ⊔
        Submodule.span A (Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
      Submodule.span A (Set.range fun x => single ((algebraMap S B) x) 1)