awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
c : B
h₁ :
  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 (γ := 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)))

Tactic:
_
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
h₁ :
  ∃ (y : Ideal.Cotangent (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]) y : B ⊗[A] Ω[A⁄R])
      (1 ⊗ₜ[A]
          ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
            HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R])
⊢ ∃ (y : Ideal.Cotangent (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]) y : B ⊗[A] Ω[A⁄R])
      (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)) :
        B ⊗[A] Ω[A⁄R])

Tactic:
simp only [map_sum, Finsupp.linearCombination_single]

Premises used: map_sum, Finsupp.linearCombination_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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
⊢ Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)

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

Premises used: DFunLike.congr_fun, Finsupp.mapDomain, Finsupp.sum, RingHom.mem_ker, Finsupp.single_apply, Finsupp.finsetSum_apply, Finset.sum_filter
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
⊢ Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)

Tactic:
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
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
h₁ :
  ∀ (a : A) (ha : (algebraMap A B : (a : A) → B) a = c),
    ∃ (y : Ideal.Cotangent (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]) y :
          B ⊗[A] Ω[A⁄R])
        (1 ⊗ₜ[A]
            ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
              HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]) :
          B ⊗[A] Ω[A⁄R])
⊢ ∃ (y : Ideal.Cotangent (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]) y : B ⊗[A] Ω[A⁄R])
      (1 ⊗ₜ[A]
          ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
            HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R])

Tactic:
obtain ⟨a, ha⟩ := h c
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
h₁ :
  Eq (α := B ⊗[A] Ω[A⁄R])
    ((kerCotangentToTensor R A B : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R])
      (∑ i ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}.attach,
        HSMul.hSMul (α := A) (β := Ideal.Cotangent (RingHom.ker (F := A →+* B) (algebraMap A B)))
          ((x : (a : A) → A) (↑i : A) : A)
          ((Ideal.toCotangent (RingHom.ker (F := A →+* B) (algebraMap A B)) :
                (a : ↥(RingHom.ker (algebraMap A B))) → (RingHom.ker (algebraMap A B)).Cotangent)
              (Subtype.mk (p := fun (x : A) ↦
                Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B)) x) ((↑i : A) - a) ⋯) :
            Ideal.Cotangent (RingHom.ker (F := A →+* B) (algebraMap A B)))))
    (1 ⊗ₜ[A]
      ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
        HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]))
w :
  ∀ (i : ↥({i ∈ x.support | (algebraMap A B : (a : A) → B) i = c})),
    Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B)) ((↑i : A) - a)
⊢ ∃ (y : Ideal.Cotangent (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]) y : B ⊗[A] Ω[A⁄R])
      (1 ⊗ₜ[A]
          ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
            HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R])

Tactic:
use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩

Premises used: Algebra.algebraMap, Finsupp.support, Finset.attach, Finset.filter, Eq, DFunLike.coe
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
h₁ :
  Eq (α := B ⊗[A] Ω[A⁄R])
    (∑ x_1 ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}.attach,
      HSMul.hSMul (α := A) (β := B ⊗[A] Ω[A⁄R]) ((x : (a : A) → A) (↑x_1 : A) : A)
        (1 ⊗ₜ[A]
          HSub.hSub (α := Ω[A⁄R]) (β := Ω[A⁄R]) ((D R A : (a : A) → Ω[A⁄R]) (↑x_1 : A) : Ω[A⁄R])
            ((D R A : (a : A) → Ω[A⁄R]) a : Ω[A⁄R])))
    (1 ⊗ₜ[A]
      ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
        HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]))
⊢ Eq (α := B ⊗[A] Ω[A⁄R])
    ((kerCotangentToTensor R A B : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R])
      (∑ i ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}.attach,
        HSMul.hSMul (α := A) (β := Ideal.Cotangent (RingHom.ker (F := A →+* B) (algebraMap A B)))
          ((x : (a : A) → A) (↑i : A) : A)
          ((Ideal.toCotangent (RingHom.ker (F := A →+* B) (algebraMap A B)) :
                (a : ↥(RingHom.ker (algebraMap A B))) → (RingHom.ker (algebraMap A B)).Cotangent)
              (Subtype.mk (p := fun (x : A) ↦
                Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B)) x) ((↑i : A) - a) ⋯) :
            Ideal.Cotangent (RingHom.ker (F := A →+* B) (algebraMap A B)))))
    (1 ⊗ₜ[A]
      ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
        HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]))

Tactic:
simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]

Premises used: KaehlerDifferential.kerCotangentToTensor_toCotangent, map_sub, map_sum, LinearMapClass.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
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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
h₁ :
  Eq (α := B ⊗[A] Ω[A⁄R])
    (∑ x_1 ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}.attach,
      1 ⊗ₜ[A]
        HSMul.hSMul (α := A) ((x : (a : A) → A) (↑x_1 : A) : A)
          (HSub.hSub (α := Ω[A⁄R]) (β := Ω[A⁄R]) ((D R A : (a : A) → Ω[A⁄R]) (↑x_1 : A) : Ω[A⁄R])
            ((D R A : (a : A) → Ω[A⁄R]) a : Ω[A⁄R])))
    (1 ⊗ₜ[A]
      ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
        HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]))
⊢ Eq (α := B ⊗[A] Ω[A⁄R])
    (∑ x_1 ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}.attach,
      HSMul.hSMul (α := A) (β := B ⊗[A] Ω[A⁄R]) ((x : (a : A) → A) (↑x_1 : A) : A)
        (1 ⊗ₜ[A]
          HSub.hSub (α := Ω[A⁄R]) (β := Ω[A⁄R]) ((D R A : (a : A) → Ω[A⁄R]) (↑x_1 : A) : Ω[A⁄R])
            ((D R A : (a : A) → Ω[A⁄R]) a : Ω[A⁄R])))
    (1 ⊗ₜ[A]
      ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
        HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]))

Tactic:
simp_rw [← TensorProduct.tmul_smul]

Premises used: TensorProduct.tmul_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
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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
h₁ :
  Eq (α := B ⊗[A] Ω[A⁄R])
    (1 ⊗ₜ[A]
      HSMul.hSMul (α := A) (β := Ω[A⁄R])
        (∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c, (x : (a : A) → A) x_1)
        ((D R A : (a : A) → Ω[A⁄R]) a : Ω[A⁄R]))
    0
⊢ Eq (α := B ⊗[A] Ω[A⁄R])
    (∑ x_1 ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}.attach,
      1 ⊗ₜ[A]
        HSMul.hSMul (α := A) ((x : (a : A) → A) (↑x_1 : A) : A)
          (HSub.hSub (α := Ω[A⁄R]) (β := Ω[A⁄R]) ((D R A : (a : A) → Ω[A⁄R]) (↑x_1 : A) : Ω[A⁄R])
            ((D R A : (a : A) → Ω[A⁄R]) a : Ω[A⁄R])))
    (1 ⊗ₜ[A]
      ∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c,
        HSMul.hSMul (α := A) (β := Ω[A⁄R]) ((x : (a : A) → A) x_1 : A) ((D R A : (a : A) → Ω[A⁄R]) x_1 : Ω[A⁄R]))

Tactic:
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)]

Premises used: Finset.sum_smul, TensorProduct.tmul_sub, Finset.sum_attach, sub_eq_self, TensorProduct.tmul_sum, smul_sub, KaehlerDifferential.D, Finset.sum_sub_distrib, HSMul.hSMul, DFunLike.coe
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
h₁ :
  Eq (α := B ⊗[A] Ω[A⁄R])
    (HSMul.hSMul (α := A) (β := B)
          (∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c, (x : (a : A) → A) x_1) 1 ⊗ₜ[A]
        (D R A : (a : A) → Ω[A⁄R]) a :
      B ⊗[A] Ω[A⁄R])
    (0 : B ⊗[A] Ω[A⁄R])
h₂ :
  Eq (α := B ⊗[A] Ω[A⁄R])
    ((algebraMap A B : (a : A) → B)
          (∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c, (x : (a : A) → A) x_1) ⊗ₜ[A]
        (D R A : (a : A) → Ω[A⁄R]) a :
      B ⊗[A] Ω[A⁄R])
    (0 : B ⊗[A] Ω[A⁄R])
h₃ : Eq (α := B ⊗[A] Ω[A⁄R]) (0 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a : B ⊗[A] Ω[A⁄R]) (0 : B ⊗[A] Ω[A⁄R])
h₄ h₅ : Eq (α := B ⊗[A] Ω[A⁄R]) 0 0
⊢ Eq (α := B ⊗[A] Ω[A⁄R])
    (1 ⊗ₜ[A]
      HSMul.hSMul (α := A) (β := Ω[A⁄R])
        (∑ x_1 ∈ x.support with (algebraMap A B : (a : A) → B) x_1 = c, (x : (a : A) → A) x_1)
        ((D R A : (a : A) → Ω[A⁄R]) a : Ω[A⁄R]))
    0

Tactic:
rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]

Premises used: TensorProduct.smul_tmul, RingHom.mem_ker, TensorProduct.zero_tmul, Algebra.algebraMap_eq_smul_one, Iff.mp
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
i : ↥({i ∈ x.support | (algebraMap A B : (a : A) → B) i = c})
⊢ (↑i : A) ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}

Tactic:
i.prop

Premises used: Subtype.prop
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
i : ↥({i ∈ x.support | (algebraMap A B : (a : A) → B) i = c})
a₁ :
  Ne (α := A) ((x : (a : A) → A) (↑i : A) : A) (0 : A) ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c ↔
    (↑i : A) ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}
⊢ Ne (α := A) ((x : (a : A) → A) (↑i : A) : A) (0 : A) ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c

Tactic:
convert! i.prop

Premises used: Subtype.prop
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
i : ↥({i ∈ x.support | (algebraMap A B : (a : A) → B) i = c})
a₁ :
  Ne (α := A) ((x : (a : A) → A) (↑i : A) : A) (0 : A) ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c ↔
    (↑i : A) ∈ x.support ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c
⊢ Ne (α := A) ((x : (a : A) → A) (↑i : A) : A) (0 : A) ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c ↔
    (↑i : A) ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}

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

Premises used: Finsupp.mem_support_iff, Finset.mem_filter
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
i : ↥({i ∈ x.support | (algebraMap A B : (a : A) → B) i = c})
⊢ Ne (α := A) ((x : (a : A) → A) (↑i : A) : A) (0 : A) ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c

Tactic:
have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
-- 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))
c : B
h_1 : Membership.mem (γ := Finset B) (Finset.image (⇑(algebraMap A B) : (a : A) → B) x.support) c
this_1 :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B))
    (∑ i ∈ x.support with (algebraMap A B : (a : A) → B) i = c, (x : (a : A) → A) i)
a : A
ha : (algebraMap A B : (a : A) → B) a = c
i : ↥({i ∈ x.support | (algebraMap A B : (a : A) → B) i = c})
this : Ne (α := A) ((x : (a : A) → A) (↑i : A) : A) (0 : A) ∧ (algebraMap A B : (a : A) → B) (↑i : A) = c
⊢ Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B)) ((↑i : A) - a)

Tactic:
simp [RingHom.mem_ker, ha, this.2]

Premises used: RingHom.mem_ker, And.right