-- 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 a.convert_2.inr.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 : A
⊢ (fun x => single ((algebraMap A B) x) 1) x ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (LinearMap.range (mapBaseChange R A B)))

Tactic:
use 1 ⊗ₜ D _ _ x

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

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.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y))

Tactic:
simp

Result:
no goals

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

Tactic:
induction' x with r s

Result:
case a.intro.zero
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
⊢ (mapBaseChange R A B) 0 ∈ LinearMap.ker (map R A B B)

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)

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)

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
⊢ LinearMap.range (mapBaseChange R A B) = LinearMap.ker (map R A B B)

Tactic:
apply le_antisymm

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

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)

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
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) x)) = 0

Tactic:
induction x using Finsupp.induction_linear

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

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

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

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✝ + (mapBaseChange R A B) y✝ ∈ LinearMap.ker (map R A B B)

Tactic:
exact add_mem ‹_› ‹_›

Result:
no goals

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

Tactic:
rintro f ((⟨⟨x, y⟩, rfl⟩|⟨⟨x, y⟩, rfl⟩)|⟨x, rfl⟩)

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

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

case a.convert_2.inr.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 : A
⊢ (fun x => single ((algebraMap A B) x) 1) x ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (LinearMap.range (mapBaseChange R A B)))

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals