-- Mathlib/RingTheory/Kaehler/Basic.lean
lemma KaehlerDifferential.ker_map_of_surjective (h : Function.Surjective (algebraMap A B)) :
    LinearMap.ker (map R R A B) =
      (LinearMap.ker finsupp_map).map (Finsupp.linearCombination A (D R 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.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x => single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))) =
    Submodule.map (linearCombination A ⇑(D R A))
      (LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))

Tactic:
convert bot_sup_eq _

Result:
case h.e'_2.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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x => single ((algebraMap R A) x) 1)) = ⊥

case convert_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
h : Function.Surjective ⇑(algebraMap A B)
⊢ OrderBot (Submodule A (Ω[A⁄R]))

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)
⊢ LinearMap.ker (map R R A B) =
    Submodule.map (linearCombination A ⇑(D R A))
      (LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))

Tactic:
rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup,
  Submodule.map_sup, ← kerTotal_eq, ← Submodule.comap_bot,
  Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _),
  bot_sup_eq, 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.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x => single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))) =
    Submodule.map (linearCombination A ⇑(D R A))
      (LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))

Proof state:
case h.e'_2.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
h : Function.Surjective ⇑(algebraMap A B)
⊢ ∀ x ∈ Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x => single ((algebraMap R A) x) 1), x = 0

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x => single ((algebraMap R A) x) 1)) = ⊥

case convert_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
h : Function.Surjective ⇑(algebraMap A B)
⊢ OrderBot (Submodule A (Ω[A⁄R]))

Tactic:
rw [Submodule.span_eq_bot]

Result:
case h.e'_2.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
h : Function.Surjective ⇑(algebraMap A B)
⊢ ∀ x ∈ Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x => single ((algebraMap R A) x) 1), x = 0