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

Proof state:
case e_a.e_s
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Set.range
      (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
        single ((algebraMap R A) x) 1) =
    Set.range fun x => single ((algebraMap R B) x) 1

Tactic:
refine congr_arg Set.range ?_

Result:
case e_a.e_s
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
      single ((algebraMap R A) x) 1) =
    fun x => single ((algebraMap R B) x) 1

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A 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
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
            single ((algebraMap R A) x) 1)) =
    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 R B) x) 1)

Tactic:
congr

Result:
case e_a.e_s
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Set.range
      (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
        single ((algebraMap R A) x) 1) =
    Set.range fun x => single ((algebraMap R B) x) 1

Proof state:
case e_a.e_s.h.h
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x✝ : R
a✝ : B
⊢ ((⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
          single ((algebraMap R A) x) 1)
        x✝)
      a✝ =
    (single ((algebraMap R B) x✝) 1) a✝

Tactic:
simp [IsScalarTower.algebraMap_eq R A B]

Result:
no goals

Proof state:
case e_a.e_s
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
      single ((algebraMap R A) x) 1) =
    fun x => single ((algebraMap R B) x) 1

Tactic:
ext

Result:
case e_a.e_s.h.h
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x✝ : R
a✝ : B
⊢ ((⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
          single ((algebraMap R A) x) 1)
        x✝)
      a✝ =
    (single ((algebraMap R B) x✝) 1) a✝

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A 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 R A) x) 1)) =
    Submodule.restrictScalars A (kerTotal R B)

Tactic:
rw [Submodule.map_sup, ← kerTotal_map R R A B h, Submodule.map_span, ← Set.range_comp]

Result:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A 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
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x =>
            single ((algebraMap R A) x) 1)) =
    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 R B) x) 1)