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
x : A
⊢ (fun (x : A) ↦ (single ((algebraMap A B : (a : A) → B) x) 1 : B →₀ B)) x ∈
    (↑(Submodule.comap (M₂ := Ω[B⁄R]) (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R]))
          (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))) :
      Set (B →₀ B))
have h : Eq (α := Ω[B⁄R]) ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) x) : Ω[B⁄R])
  ((linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R]) : (a : B →₀ B) → Ω[B⁄R])
      ((fun (x : A) ↦ (single ((algebraMap A B : (a : A) → B) x) 1 : B →₀ B)) x) :
    Ω[B⁄R])
Tactic: use 1 ⊗ₜ D _ _ x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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)
have 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))
Tactic: rw [Submodule.smul_eq_map₂]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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))
have 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))
Tactic: apply iSup_le_iff.mpr
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ ∀ (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))
have 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)))
Tactic: simp only [Submodule.map_le_iff_le_comap, Subtype.forall]
-- 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)
⊢ 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)))
have 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
Tactic: ext x
-- 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 : 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
have 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
Tactic: constructor
-- 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 : 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
⊢ 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
have 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
Tactic: constructor
-- 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 : Ideal.Cotangent (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]) x : B ⊗[A] Ω[A⁄R])
have 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])
Tactic: obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
Cleared hypotheses: x
-- 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 : 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
⊢ Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B)) x
have 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])
Tactic: obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x
Cleared hypotheses: x, hx
-- 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] Ω[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])
have 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])
Tactic: obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
Cleared hypotheses: x, hx
-- 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⁄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])
have hx₁ : 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
Cleared hypotheses: hx
-- 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⁄R]
hx : Membership.mem (γ := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄R]) (map R R A B)) x
⊢ 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])
have 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
Tactic: rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx
Cleared hypotheses: hx
-- 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⁄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
⊢ 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])
have 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])
Tactic: obtain ⟨x, hx, rfl⟩ := hx
Cleared hypotheses: x, hx
-- 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))
⊢ 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])
have 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])
Tactic: simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
      Algebra.linearMap_apply, map_one]
-- 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))
⊢ 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])
have 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)))
Tactic: rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]
-- 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))
⊢ 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)))
have 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)))
Tactic: simp only [map_sum (s := x.support.image (algebraMap A B)),
      TensorProduct.tmul_sum]
-- 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))
⊢ 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)))
have 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)))
Tactic: apply sum_mem
-- 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
⊢ ∃ (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])
have 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])
Tactic: simp only [map_sum, Finsupp.linearCombination_single]
-- 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
⊢ ∃ (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 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)
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