awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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)
⊢ ∃ (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])
have 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])
Tactic: obtain ⟨a, ha⟩ := h c
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ ∃ (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])
have 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) sorry) :
          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: use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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]))
⊢ ∃ (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])
have 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)
Tactic: use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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]))
have 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]))
Tactic: simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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]))
have 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]))
Tactic: simp_rw [← TensorProduct.tmul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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]))
have 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
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)]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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
have 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])
Tactic: rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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])
⊢ 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
have 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])
Tactic: rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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])
⊢ 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
have 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])
Tactic: rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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])
⊢ 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
have h₄ : Eq (α := B ⊗[A] Ω[A⁄R]) 0 0
Tactic: rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
have 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}
Tactic: convert! i.prop
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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 ↔
    (↑i : A) ∈ {i ∈ x.support | (algebraMap A B : (a : A) → B) i = c}
have 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
Tactic: simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
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})
⊢ Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* B) (algebraMap A B)) ((↑i : A) - a)
have this₁ : 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]