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

Tactic:
simp [RingHom.mem_ker, ha, this.2]

Result:
no goals

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 :
  (LinearMap.rTensor (Ω[A⁄R]) (Algebra.linearMap A B)) ((TensorProduct.lid A (Ω[A⁄R])).symm x) ∈
    Submodule.restrictScalars A (LinearMap.ker (mapBaseChange 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:
replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using 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 ∈ 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)

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)))
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) x ∈ LinearMap.range (kerCotangentToTensor R A B)

Tactic:
rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
  (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]

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))
        (∑ j ∈ Finset.image (⇑(algebraMap A B)) x.support,
          ∑ i ∈ Finset.filter (fun i => (algebraMap A B) i = j) x.support, single i (x i)) ∈
    LinearMap.range (kerCotangentToTensor R A B)

Proof state:
case h.mp.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 : ↥(RingHom.ker (algebraMap A B))
⊢ (kerCotangentToTensor R A B) ((RingHom.ker (algebraMap A B)).toCotangent x) ∈
    Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B))

Tactic:
simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
  mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]

Result:
no goals

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
⊢ 1 ⊗ₜ[A] ((∑ x_1 ∈ Finset.filter (fun x => (algebraMap A B) x = c) x.support, x x_1) • (D R A) a) = 0

Tactic:
rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
  TensorProduct.zero_tmul]

Result:
no goals

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

Tactic:
simp only [smul_sub, TensorProduct.tmul_sub, Finset.sum_sub_distrib, ← TensorProduct.tmul_sum,
  ← Finset.sum_smul, Finset.sum_attach, sub_eq_self,
  Finset.sum_attach (f := fun i ↦ x i • KaehlerDifferential.D R A i)]

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
⊢ 1 ⊗ₜ[A] ((∑ x_1 ∈ Finset.filter (fun x => (algebraMap A B) x = c) x.support, x x_1) • (D R A) a) = 0