-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.range_kerCotangentToTensor
    (h : Function.Surjective (algebraMap A B)) :
    LinearMap.range (kerCotangentToTensor R A B) =
      (LinearMap.ker (KaehlerDifferential.mapBaseChange R A B)).restrictScalars A

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
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : (Finset.filter (fun x => (algebraMap A B) x = c) x.support).sum ⇑x ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ ∑ x_1 ∈ (Finset.filter (fun x => (algebraMap A B) x = c) x.support).attach,
      x ↑x_1 • 1 ⊗ₜ[A] ((D R A) ↑x_1 - (D R A) a) =
    1 ⊗ₜ[A] ∑ x_1 ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, x x_1 • (D R A) x_1

Tactic:
simp_rw [← TensorProduct.tmul_smul]

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
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : (Finset.filter (fun x => (algebraMap A B) x = c) x.support).sum ⇑x ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ ∑ x_1 ∈ (Finset.filter (fun x => (algebraMap A B) x = c) x.support).attach,
      1 ⊗ₜ[A] (x ↑x_1 • ((D R A) ↑x_1 - (D R A) a)) =
    1 ⊗ₜ[A] ∑ x_1 ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, x x_1 • (D R A) x_1

Proof state:
case h.mpr.intro.intro.intro.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
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
⊢ (LinearMap.rTensor (Ω[A⁄R]) (Algebra.linearMap A B))
      ((TensorProduct.lid A (Ω[A⁄R])).symm ((linearCombination A ⇑(D R A)) x)) ∈
    LinearMap.range (kerCotangentToTensor R A B)

Tactic:
simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
  Algebra.linearMap_apply, map_one]

Result:
case h.mpr.intro.intro.intro.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
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) x ∈ LinearMap.range (kerCotangentToTensor R A B)

Proof state:
case h.mpr.intro.intro.intro.intro.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 : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
⊢ ∃ y,
    (kerCotangentToTensor R A B) y =
      1 ⊗ₜ[A]
        (linearCombination A ⇑(D R A)) (∑ i ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, single i (x i))

Tactic:
simp only [map_sum, Finsupp.linearCombination_single]

Result:
case h.mpr.intro.intro.intro.intro.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 : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
⊢ ∃ y,
    (kerCotangentToTensor R A B) y =
      1 ⊗ₜ[A] ∑ x_1 ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, x x_1 • (D R A) x_1

Proof state:
case h.mpr.intro.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
h : Function.Surjective ⇑(algebraMap A B)
x : Ω[A⁄R]
hx : x ∈ LinearMap.ker (map R R A B)
⊢ (LinearMap.rTensor (Ω[A⁄R]) (Algebra.linearMap A B)) ((TensorProduct.lid A (Ω[A⁄R])).symm x) ∈
    LinearMap.range (kerCotangentToTensor R A B)

Tactic:
rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx

Result:
case h.mpr.intro.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
h : Function.Surjective ⇑(algebraMap A B)
x : Ω[A⁄R]
hx :
  x ∈
    Submodule.map (linearCombination A ⇑(D R A))
      (LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
⊢ (LinearMap.rTensor (Ω[A⁄R]) (Algebra.linearMap A B)) ((TensorProduct.lid A (Ω[A⁄R])).symm x) ∈
    LinearMap.range (kerCotangentToTensor R A B)

Proof state:
case w
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 : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : (Finset.filter (fun x => (algebraMap A B) x = c) x.support).sum ⇑x ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
i : { x_1 // x_1 ∈ Finset.filter (fun x => (algebraMap A B) x = c) x.support }
⊢ ↑i - a ∈ RingHom.ker (algebraMap A B)

Tactic:
have : x i ≠ 0 ∧ algebraMap A B i = c := by
  convert i.prop
  simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]

Result:
case w
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 : A →₀ A
hx : x ∈ ↑(LinearMap.ker (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)))
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this✝ : (Finset.filter (fun x => (algebraMap A B) x = c) x.support).sum ⇑x ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
i : { x_1 // x_1 ∈ Finset.filter (fun x => (algebraMap A B) x = c) x.support }
this : x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c
⊢ ↑i - a ∈ RingHom.ker (algebraMap A 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
h : Function.Surjective ⇑(algebraMap A B)
⊢ LinearMap.range (kerCotangentToTensor R A B) = Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B))

Tactic:
ext 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
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ LinearMap.range (kerCotangentToTensor R A B) ↔
    x ∈ Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B))