-- 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
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)

Tactic:
rw [KaehlerDifferential.ker_map]

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
⊢ 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)

Proof state:
case a.convert_2.inl.inl.intro.mk
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 y : B
⊢ (fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y) ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (LinearMap.range (mapBaseChange R A B)))

Tactic:
use 0

Result:
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 y : B
⊢ (mapBaseChange R A B) 0 =
    (linearCombination B ⇑(D R B)) ((fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y))

Proof state:
case a.intro.tmul.intro.hsingle
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
a✝ b✝ : A
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (single a✝ b✝))) = 0

Tactic:
simp

Result:
no goals

Proof state:
case a.intro.add
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✝ y✝ : B ⊗[A] Ω[A⁄R]
a✝¹ : (mapBaseChange R A B) x✝ ∈ LinearMap.ker (map R A B B)
a✝ : (mapBaseChange R A B) y✝ ∈ LinearMap.ker (map R A B B)
⊢ (mapBaseChange R A B) (x✝ + y✝) ∈ LinearMap.ker (map R A B B)

Tactic:
rw [map_add]

Result:
case a.intro.add
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✝ y✝ : B ⊗[A] Ω[A⁄R]
a✝¹ : (mapBaseChange R A B) x✝ ∈ LinearMap.ker (map R A B B)
a✝ : (mapBaseChange R A B) y✝ ∈ LinearMap.ker (map R A B B)
⊢ (mapBaseChange R A B) x✝ + (mapBaseChange R A B) y✝ ∈ LinearMap.ker (map R A B B)

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 y : B
⊢ (mapBaseChange R A B) 0 =
    (linearCombination B ⇑(D R B)) ((fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y))

Tactic:
simp

Result:
no goals

Proof state:
case a.intro.tmul
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
s : Ω[A⁄R]
⊢ (mapBaseChange R A B) (r ⊗ₜ[A] s) ∈ LinearMap.ker (map R A B B)

Tactic:
obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s

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
⊢ (mapBaseChange R A B) (r ⊗ₜ[A] (linearCombination A ⇑(D R A)) x) ∈ LinearMap.ker (map R A B 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.range (mapBaseChange R A B) ≤ LinearMap.ker (map R A B B)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case a.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
x : B ⊗[A] Ω[A⁄R]
⊢ (mapBaseChange R A B) x ∈ LinearMap.ker (map R A B B)

Proof state:
case a.convert_2.inl.inr.intro.mk
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 y : B
⊢ (fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y) ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (LinearMap.range (mapBaseChange R A B)))

Tactic:
use 0

Result:
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 y : B
⊢ (mapBaseChange R A B) 0 =
    (linearCombination B ⇑(D R B)) ((fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y))

Proof state:
case a.intro.tmul.intro.hadd
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
f✝ g✝ : A →₀ A
a✝¹ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) f✝)) = 0
a✝ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) g✝)) = 0
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (f✝ + g✝))) = 0

Tactic:
simp [smul_add, *]

Result:
no goals

Proof state:
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

Tactic:
ext

Result:
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✝

Proof state:
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)

Tactic:
rw [Submodule.map_le_iff_le_comap, kerTotal, Submodule.span_le]

Result:
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
⊢ (((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 A B) x) 1) ⊆
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (LinearMap.range (mapBaseChange R A B)))