-- 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:
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
⊢ (Finset.filter (fun x => (algebraMap A B) x = c) x.support).sum ⇑x ∈ RingHom.ker (algebraMap A B)

Tactic:
simpa [Finsupp.mapDomain, Finsupp.sum, Finsupp.finset_sum_apply, RingHom.mem_ker,
  Finsupp.single_apply, ← Finset.sum_filter] using DFunLike.congr_fun hx c

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
⊢ (kerCotangentToTensor R A B)
      (∑ i ∈ (Finset.filter (fun x => (algebraMap A B) x = c) x.support).attach,
        x ↑i • (RingHom.ker (algebraMap A B)).toCotangent ⟨↑i - a, ⋯⟩) =
    1 ⊗ₜ[A] ∑ x_1 ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, x x_1 • (D R A) x_1

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

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 }
⊢ ↑i - a ∈ RingHom.ker (algebraMap A B)

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
⊢ (kerCotangentToTensor R A B)
      (∑ i ∈ (Finset.filter (fun x => (algebraMap A B) x = c) x.support).attach,
        x ↑i • (RingHom.ker (algebraMap A B)).toCotangent ⟨↑i - 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
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
⊢ (kerCotangentToTensor R A B)
      (∑ i ∈ (Finset.filter (fun x => (algebraMap A B) x = c) x.support).attach,
        x ↑i • (RingHom.ker (algebraMap A B)).toCotangent ⟨↑i - 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 [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]

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

Proof state:
case h.mpr
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 ∈ Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B)) →
    x ∈ LinearMap.range (kerCotangentToTensor R A B)

Tactic:
intro hx

Result:
case h.mpr
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]
hx : x ∈ Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B))
⊢ 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)))
⊢ ∑ a ∈ Finset.image (⇑(algebraMap A B)) x.support,
      1 ⊗ₜ[A]
        (linearCombination A ⇑(D R A))
          (∑ i ∈ Finset.filter (fun i => (algebraMap A B) i = a) x.support, single i (x i)) ∈
    LinearMap.range (kerCotangentToTensor R A B)

Tactic:
apply sum_mem

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 ∈ Finset.image (⇑(algebraMap A B)) x.support,
    1 ⊗ₜ[A]
        (linearCombination A ⇑(D R A))
          (∑ i ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, single i (x i)) ∈
      LinearMap.range (kerCotangentToTensor R A B)