-- 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 a
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 }
⊢ x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c ↔ ↑i ∈ Finset.filter (fun x => (algebraMap A B) x = c) x.support

Tactic:
simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]

Result:
no goals

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⁄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))
⊢ x ∈ LinearMap.ker (map R R A B)

Tactic:
simpa using hx

Result:
no goals

Proof state:
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)

Tactic:
obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x

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

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

Tactic:
intro c _

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

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
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 }
⊢ x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c

Tactic:
convert i.prop

Result:
case a
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 }
⊢ x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c ↔ ↑i ∈ Finset.filter (fun x => (algebraMap A B) x = c) x.support

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

Tactic:
simp only [Finset.filter_congr_decidable, TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
  AlgHom.toLinearMap_apply, map_one, LinearMap.mem_range]

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]
        (linearCombination A ⇑(D R A)) (∑ i ∈ Finset.filter (fun i => (algebraMap A B) i = c) x.support, single i (x i))

Proof state:
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))

Tactic:
rintro ⟨x, rfl⟩

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