-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h₁ :
  ∀ (x : B ⊗[A] Ω[A⁄R]),
    Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B)) x ↔
      Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
        (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B))) x
h₂ :
  ∀ (x : B ⊗[A] Ω[A⁄R]),
    Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B)) x →
      Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
        (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B))) x
h₃ h₄ :
  ∀ (x : B ⊗[A] Ω[A⁄R]),
    Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
        (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B))) x →
      Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B)) x
⊢ Eq (α := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))

Tactic:
classical
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
      mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]
  · intro hx
    obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x
    obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
    replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using hx
    rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx
    obtain ⟨x, hx, rfl⟩ := hx
    simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
      Algebra.linearMap_apply, map_one]
    rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]
    simp only [map_sum (s := x.support.image (algebraMap A B)),
      TensorProduct.tmul_sum]
    apply sum_mem
    intro c _
    simp only [LinearMap.mem_range]
    simp only [map_sum, Finsupp.linearCombination_single]
    have : ∑ i ∈ x.support with algebraMap A B i = c, x i ∈ RingHom.ker (algebraMap A B) := by
      simpa [Finsupp.mapDomain, Finsupp.sum, Finsupp.finsetSum_apply, RingHom.mem_ker,
        Finsupp.single_apply, ← Finset.sum_filter] using DFunLike.congr_fun hx c
    obtain ⟨a, ha⟩ := h c
    use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
    · simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]
      simp_rw [← TensorProduct.tmul_smul]
      -- TODO: was `simp [kerCotangentToTensor_toCotangent, RingHom.mem_ker.mp x.2]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      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)]
      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
    · have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
      simp [RingHom.mem_ker, ha, this.2]

Premises used: KaehlerDifferential.kerCotangentToTensor_toCotangent, Finset.sum_smul, TensorProduct.smul_tmul, map_sub, LinearMap.rTensor_tmul, KaehlerDifferential.mapBaseChange_tmul, TensorProduct.tmul_sub, Finsupp.sum, TensorProduct.tmul_smul, RingHom.mem_ker, smul_zero, map_zero, Finset.sum_attach, Algebra.linearMap_apply, TensorProduct.lid_symm_apply, sub_eq_self, map_sum, TensorProduct.zero_tmul, TensorProduct.tmul_sum, Finsupp.linearCombination_single, Algebra.algebraMap_eq_smul_one, LinearMap.mem_ker, smul_sub, Finset.sum_sub_distrib, map_one, LinearMap.mem_range, LinearMapClass.map_smul, Submodule.restrictScalars_mem, KaehlerDifferential.ker_map_of_surjective, KaehlerDifferential.map_D, sum_mem, rfl