awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
A : Type u_2
B : Type u_3
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra A B
inst_11 : Algebra S B
rw :
  LE.le (α := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
    (Submodule.map₂ (LinearMap.lsmul A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
      (RingHom.ker (F := A →+* B) (algebraMap A B)) ⊤)
    (LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B))
⊢ HSMul.hSMul (α := Ideal A) (β := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
      (RingHom.ker (F := A →+* B) (algebraMap A B)) ⊤ ≤
    LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B)

Tactic:
rw [Submodule.smul_eq_map₂]

Premises used: Submodule.smul_eq_map₂
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
A : Type u_2
B : Type u_3
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra A B
inst_11 : Algebra S B
apply :
  ∀ (i : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))),
    LE.le (α := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
      (Submodule.map (R := A) (M := ↥(RingHom.ker (F := A →+* B) (algebraMap A B))) (σ₁₂ := RingHom.id A)
        ((LinearMap.lsmul A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)) :
            (a : A) → ↥(RingHom.ker (algebraMap A B)) →ₗ[A] ↥(RingHom.ker (algebraMap A B)))
          (↑i : A))
        ⊤)
      (LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B))
⊢ LE.le (α := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
    (Submodule.map₂ (LinearMap.lsmul A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
      (RingHom.ker (F := A →+* B) (algebraMap A B)) ⊤)
    (LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B))

Tactic:
apply iSup_le_iff.mpr

Premises used: Iff.mpr, iSup_le_iff
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
A : Type u_2
B : Type u_3
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra A B
inst_11 : Algebra S B
simp :
  ∀ (a : A) (b : Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* B) (algebraMap A B)) a),
    LE.le (α := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B))) ⊤
      (Submodule.comap (M₂ := ↥(RingHom.ker (F := A →+* B) (algebraMap A B))) (σ₁₂ := RingHom.id A)
        ((LinearMap.lsmul A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)) :
            (a : A) → ↥(RingHom.ker (algebraMap A B)) →ₗ[A] ↥(RingHom.ker (algebraMap A B)))
          a)
        (LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B)))
⊢ ∀ (i : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))),
    LE.le (α := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
      (Submodule.map (R := A) (M := ↥(RingHom.ker (F := A →+* B) (algebraMap A B))) (σ₁₂ := RingHom.id A)
        ((LinearMap.lsmul A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)) :
            (a : A) → ↥(RingHom.ker (algebraMap A B)) →ₗ[A] ↥(RingHom.ker (algebraMap A B)))
          (↑i : A))
        ⊤)
      (LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B))

Tactic:
simp only [Submodule.map_le_iff_le_comap, Subtype.forall]

Premises used: Subtype.forall, Submodule.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
A : Type u_2
B : Type u_3
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra A B
inst_11 : Algebra S B
x : A
hx : Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* B) (algebraMap A B)) x
y : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))
⊢ Membership.mem (γ := Submodule A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)))
    (Submodule.comap (M₂ := ↥(RingHom.ker (F := A →+* B) (algebraMap A B))) (σ₁₂ := RingHom.id A)
      ((LinearMap.lsmul A ↥(RingHom.ker (F := A →+* B) (algebraMap A B)) :
          (a : A) → ↥(RingHom.ker (algebraMap A B)) →ₗ[A] ↥(RingHom.ker (algebraMap A B)))
        x)
      (LinearMap.ker (M₂ := B ⊗[A] Ω[A⁄R]) (kerToTensor R A B)))
    y

Tactic:
simp only [Submodule.mem_comap, LinearMap.lsmul_apply, LinearMap.mem_ker, map_smul,
      kerToTensor_apply, TensorProduct.smul_tmul', ← algebraMap_eq_smul_one,
      RingHom.mem_ker.mp hx, TensorProduct.zero_tmul]

Premises used: KaehlerDifferential.kerToTensor_apply, Submodule.mem_comap, RingHom.mem_ker, TensorProduct.zero_tmul, Algebra.algebraMap_eq_smul_one, LinearMap.mem_ker, LinearMap.lsmul_apply, TensorProduct.smul_tmul', Iff.mp, map_smul
-- 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
x : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))
⊢ Eq (α := B ⊗[A] Ω[A⁄R])
    ((kerCotangentToTensor R A B : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := A →+* B) (algebraMap A B)) :
            (a : ↥(RingHom.ker (algebraMap A B))) → (RingHom.ker (algebraMap A B)).Cotangent)
          x) :
      B ⊗[A] Ω[A⁄R])
    (1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) (↑x : A) : B ⊗[A] Ω[A⁄R])

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul, AddCon.toQuotient, rfl
-- 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
⊢ 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:
ext x
-- 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)
x : B ⊗[A] Ω[A⁄R]
h₁ :
  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₂ :
  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
⊢ 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

Tactic:
constructor
-- 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)
x : Ideal.Cotangent (RingHom.ker (F := A →+* B) (algebraMap A B))
h₁ :
  ∀ (x : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))),
    Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
      (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
      ((kerCotangentToTensor R A B : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R])
          ((Ideal.toCotangent (RingHom.ker (F := A →+* B) (algebraMap A B)) :
              (a : ↥(RingHom.ker (algebraMap A B))) → (RingHom.ker (algebraMap A B)).Cotangent)
            x) :
        B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
    ((kerCotangentToTensor R A B : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])

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

Premises used: Ideal.toCotangent_surjective, rfl
-- 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)
x : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))
⊢ Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
    ((kerCotangentToTensor R A B : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := A →+* B) (algebraMap A B)) :
            (a : ↥(RingHom.ker (algebraMap A B))) → (RingHom.ker (algebraMap A B)).Cotangent)
          x) :
      B ⊗[A] Ω[A⁄R])

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]

Premises used: KaehlerDifferential.kerCotangentToTensor_toCotangent, KaehlerDifferential.mapBaseChange_tmul, RingHom.mem_ker, smul_zero, map_zero, LinearMap.mem_ker, Submodule.restrictScalars_mem, Iff.mp, KaehlerDifferential.map_D, Subtype.property
-- 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)
x : B ⊗[A] Ω[A⁄R]
hx :
  Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B))) x
h₁ :
  ∀ (x : A ⊗[A] Ω[A⁄R])
    (hx :
      Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
        (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
        ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])),
    Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
      (LinearMap.range (kerCotangentToTensor R A B))
      ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B)) x

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

Premises used: LinearMap.rTensor_surjective, KaehlerDifferential, rfl
-- 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)
x : A ⊗[A] Ω[A⁄R]
hx :
  Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
    ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])
h₁ :
  ∀ (x : Ω[A⁄R])
    (hx :
      Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
        (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
        ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
            ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R]) x) :
          B ⊗[A] Ω[A⁄R])),
    Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
      (LinearMap.range (kerCotangentToTensor R A B))
      ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
          ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R]) x) :
        B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])

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

Premises used: LinearEquiv.symm, LinearEquiv.surjective, TensorProduct.lid, rfl
-- 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)
x : Ω[A⁄R]
hx :
  Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
    ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
        ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R]) x) :
      B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (γ := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄R]) (map R R A B)) x

Tactic:
simpa using hx
-- 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)
x : Ω[A⁄R]
hx :
  Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
    ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
        ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R]) x) :
      B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (γ := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄R]) (map R R A B)) x

Tactic:
replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using hx
-- 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)
x : Ω[A⁄R]
hx : Membership.mem (γ := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄R]) (map R R A B)) x
⊢ Membership.mem (γ := Submodule A Ω[A⁄R])
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))
    x

Tactic:
rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx

Premises used: KaehlerDifferential.ker_map_of_surjective
-- 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)
x : Ω[A⁄R]
hx :
  Membership.mem (γ := Submodule A Ω[A⁄R])
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))
    x
h₁ :
  ∀ (x : A →₀ A)
    (hx :
      x ∈
        (↑(LinearMap.ker (M₂ := B →₀ B)
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))) :
          Set (A →₀ A))),
    Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
      (LinearMap.range (kerCotangentToTensor R A B))
      ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
          ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x)) :
        B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
        ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R]) x) :
      B ⊗[A] Ω[A⁄R])

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

Premises used: rfl
-- 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)
x : A →₀ A
hx :
  x ∈
    (↑(LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))) :
      Set (A →₀ A))
h₁ :
  Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (1 ⊗ₜ[A] (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])
⊢ Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    ((LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B) : (a : A ⊗[A] Ω[A⁄R]) → B ⊗[A] Ω[A⁄R])
        ((LinearEquiv.symm (TensorProduct.lid A Ω[A⁄R]) : (a : Ω[A⁄R]) → A ⊗[A] Ω[A⁄R])
          ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x)) :
      B ⊗[A] Ω[A⁄R])

Tactic:
simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
      Algebra.linearMap_apply, map_one]

Premises used: LinearMap.rTensor_tmul, Algebra.linearMap_apply, TensorProduct.lid_symm_apply, map_one
-- 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)
x : A →₀ A
hx :
  x ∈
    (↑(LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))) :
      Set (A →₀ A))
h₁ :
  Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (1 ⊗ₜ[A]
      (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R])
        (∑ j ∈ Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support,
          ∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = j, single i ((x : (a : A) → A) i)))
⊢ Membership.mem (α := B ⊗[A] Ω[A⁄R]) (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (1 ⊗ₜ[A] (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x : B ⊗[A] Ω[A⁄R])

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

Premises used: Algebra.algebraMap, Finset.sum_fiberwise_of_maps_to, Finsupp.sum, Finset.mem_image_of_mem, DFunLike.coe, Finsupp.sum_single
-- 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)
x : A →₀ A
hx :
  x ∈
    (↑(LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))) :
      Set (A →₀ A))
h₁ :
  Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (∑ a ∈ Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support,
      1 ⊗ₜ[A]
        (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R])
          (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = a, single i ((x : (a : A) → A) i)))
⊢ Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (1 ⊗ₜ[A]
      (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R])
        (∑ j ∈ Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support,
          ∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = j, single i ((x : (a : A) → A) i)))

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

Premises used: Algebra.algebraMap, Finsupp.support, map_sum, TensorProduct.tmul_sum, DFunLike.coe, Finset.image
-- 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)
x : A →₀ A
hx :
  x ∈
    (↑(LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))) :
      Set (A →₀ A))
h₁ :
  ∀ (c : B),
    Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c →
      Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
        (1 ⊗ₜ[A]
          (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R])
            (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, single i ((x : (a : A) → A) i)))
⊢ Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (∑ a ∈ Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support,
      1 ⊗ₜ[A]
        (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R])
          (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = a, single i ((x : (a : A) → A) i)))

Tactic:
apply sum_mem

Premises used: sum_mem