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

Tactic:
constructor

Result:
case h.mp
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))

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)

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

Tactic:
obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x

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

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

Tactic:
simp only [Function.comp_apply, map_sum (s := x.support.image (algebraMap A B)),
  TensorProduct.tmul_sum]

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

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]
hx : x ∈ Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B))
⊢ x ∈ LinearMap.range (kerCotangentToTensor R A B)

Tactic:
obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective (Ω[A⁄R]) (g := Algebra.linearMap A B) h x

Result:
case h.mpr.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] Ω[A⁄R]
hx :
  (LinearMap.rTensor (Ω[A⁄R]) (Algebra.linearMap A B)) x ∈
    Submodule.restrictScalars A (LinearMap.ker (mapBaseChange R A B))
⊢ (LinearMap.rTensor (Ω[A⁄R]) (Algebra.linearMap A B)) 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
this : (Finset.filter (fun x => (algebraMap A B) x = c) x.support).sum ⇑x ∈ RingHom.ker (algebraMap A B)
⊢ ∃ 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

Tactic:
obtain ⟨a, ha⟩ := h c

Result:
case h.mpr.intro.intro.intro.intro.h.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)))
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
⊢ ∃ 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 ∈
    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)

Tactic:
obtain ⟨x, hx, rfl⟩ := hx

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