-- Mathlib/RingTheory/Kaehler/Basic.lean
lemma KaehlerDifferential.range_mapBaseChange :
    LinearMap.range (mapBaseChange R A B) = LinearMap.ker (map R A B B)

Proof state:
case h.e'_3.e_p
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
⊢ Submodule.comap (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B))
      (Submodule.restrictScalars B (kerTotal A B)) =
    kerTotal A B

Tactic:
convert Submodule.comap_id _

Result:
case h.e'_2.h.e'_15
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
⊢ mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B) = LinearMap.id

Proof state:
case a.intro.tmul.intro
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
r : B
x : A →₀ A
⊢ (mapBaseChange R A B) (r ⊗ₜ[A] (linearCombination A ⇑(D R A)) x) ∈ LinearMap.ker (map R A B B)

Tactic:
simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]

Result:
case a.intro.tmul.intro
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
r : B
x : A →₀ A
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) x)) = 0

Proof state:
case 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
x : A
⊢ (mapBaseChange R A B) (1 ⊗ₜ[A] (D R A) x) =
    (linearCombination B ⇑(D R B)) ((fun x => single ((algebraMap A B) x) 1) x)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.e'_15.h.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
a✝¹ a✝ : B
⊢ (((mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B)) ∘ₗ lsingle a✝¹) 1) a✝ =
    ((LinearMap.id ∘ₗ lsingle a✝¹) 1) a✝

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
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
⊢ Submodule.map (linearCombination B ⇑(D R B))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B))
        (Submodule.restrictScalars B (kerTotal A B))) =
    Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)

Tactic:
congr 1

Result:
case h.e'_3.e_p
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
⊢ Submodule.comap (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B))
      (Submodule.restrictScalars B (kerTotal A B)) =
    kerTotal A B

Proof state:
case a
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
⊢ LinearMap.ker (map R A B B) ≤ LinearMap.range (mapBaseChange R A B)

Tactic:
convert_to (kerTotal A B).map (Finsupp.linearCombination B (D R B)) ≤ _

Result:
case h.e'_3
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
⊢ LinearMap.ker (map R A B B) = Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)

case a.convert_2
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
⊢ Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B) ≤ LinearMap.range (mapBaseChange R A B)