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)
⊢ Eq (α := Submodule A (B →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (kerTotal R A ⊔ Submodule.span A (Set.range fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    (Submodule.restrictScalars A (kerTotal R B))
have rw : Eq (α := Submodule A (B →₀ B))
  (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (kerTotal R A) ⊔
    Submodule.span A
      (Set.range.{u_3, u + 1} (ι := R)
        (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
            (a : A →₀ A) → B →₀ B)
          fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
  (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (kerTotal R A) ⊔
    Submodule.span A (Set.range fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1))
Tactic: rw [Submodule.map_sup, ← kerTotal_map R R A B h, Submodule.map_span, ← Set.range_comp]
-- 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 →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A
        (Set.range.{u_3, u + 1} (ι := R)
          (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
              (a : A →₀ A) → B →₀ B)
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A (Set.range fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1))
have e_a : Eq (α := R → B →₀ B)
  (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
    (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
      (a : A →₀ A) → B →₀ B)
    fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)
  fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1
Tactic: congr
-- 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 (α := R → B →₀ B)
    (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
      (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
        (a : A →₀ A) → B →₀ B)
      fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)
    fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1
have e_a : ∀ (x : R) (a : B),
  Eq (α := B)
    ((Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
              (a : A →₀ A) → B →₀ B)
            (fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1) x :
          (a : B) → B)
        a :
      B)
    (((single ((algebraMap R B : (a : R) → B) x) 1 : B →₀ B) : (a : B) → B) a : B)
Tactic: ext
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
⊢ Eq (α := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B))))
have rw : Eq (α := Submodule A Ω[A⁄R])
  (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
    (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B))))
  (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
    (Submodule.comap (M₂ := B →₀ B)
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (Submodule.restrictScalars A (kerTotal S B))))
Tactic: rw [← Submodule.map_comap_eq_of_surjective (linearCombination_surjective R A) (LinearMap.ker _)]
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
⊢ Eq (α := Submodule A Ω[A⁄R])
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B))))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B))))
have e_p : Eq (α := Submodule A (A →₀ A))
  (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
    (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
  (Submodule.comap (M₂ := B →₀ B)
    (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
    (Submodule.restrictScalars A (kerTotal S B)))
Tactic: congr 1
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
⊢ Eq (α := Submodule A (A →₀ A))
    (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
    (Submodule.comap (M₂ := B →₀ B)
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (Submodule.restrictScalars A (kerTotal S B)))
have e_p : ∀ (x : A →₀ A),
  Membership.mem (γ := Submodule A (A →₀ A))
      (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
      x ↔
    Membership.mem (γ := Submodule A (A →₀ A))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B)))
      x
Tactic: ext 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ Membership.mem (γ := Submodule A (A →₀ A))
      (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
      x ↔
    Membership.mem (γ := Submodule A (A →₀ A))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B)))
      x
have e_p : Eq.{u_3 + 1} (α := Ω[B⁄S])
    ((linearCombination A
            (Function.comp (β := Ω[A⁄R]) (⇑(map R S A B) : (a : Ω[A⁄R]) → Ω[B⁄S]) (⇑(D R A) : (a : A) → Ω[A⁄R])) :
          (a : A →₀ A) → Ω[B⁄S])
        x :
      Ω[B⁄S])
    (0 : Ω[B⁄S]) ↔
  Eq (α := Ω[B⁄S])
    ((linearCombination B (⇑(D S B) : (a : B) → Ω[B⁄S]) : (a : B →₀ B) → Ω[B⁄S])
        (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
              LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
            (a : A →₀ A) → B →₀ B)
          x) :
      Ω[B⁄S])
    (0 : Ω[B⁄S])
Tactic: simp only [Submodule.mem_comap, LinearMap.mem_ker, Finsupp.apply_linearCombination, ← kerTotal_eq,
    Submodule.restrictScalars_mem]
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      ((linearCombination A
              (Function.comp (β := Ω[A⁄R]) (⇑(map R S A B) : (a : Ω[A⁄R]) → Ω[B⁄S]) (⇑(D R A) : (a : A) → Ω[A⁄R])) :
            (a : A →₀ A) → Ω[B⁄S])
          x :
        Ω[B⁄S])
      (0 : Ω[B⁄S]) ↔
    Eq (α := Ω[B⁄S])
      ((linearCombination B (⇑(D S B) : (a : B) → Ω[B⁄S]) : (a : B →₀ B) → Ω[B⁄S])
          (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
              (a : A →₀ A) → B →₀ B)
            x) :
        Ω[B⁄S])
      (0 : Ω[B⁄S])
have e_p : Eq.{u_3 + 1} (α := Ω[B⁄S])
    (x.sum fun (i a : A) ↦
      HSMul.hSMul (β := Ω[B⁄S]) a
        (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
            ((D R A : (a : A) → Ω[A⁄R]) i) :
          Ω[B⁄S]))
    0 ↔
  Eq (α := Ω[B⁄S])
    (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) sorry (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
      fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
    0
Tactic: simp only [linearCombination_apply, Function.comp_apply, LinearMap.coe_comp, lmapDomain_apply,
    Finsupp.mapRange.linearMap_apply]
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq (α := Ω[B⁄S])
      (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) ⋯ (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
        fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
      0
have e_p : Eq.{u_3 + 1} (α := Ω[B⁄S])
    (x.sum fun (i a : A) ↦
      HSMul.hSMul (β := Ω[B⁄S]) a
        (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
            ((D R A : (a : A) → Ω[A⁄R]) i) :
          Ω[B⁄S]))
    0 ↔
  Eq.{u_3 + 1} (α := Ω[B⁄S])
    (x.sum fun (a m : A) ↦
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m : B)
        ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a) : Ω[B⁄S]))
    0
Tactic: rw [Finsupp.sum_mapRange_index, Finsupp.sum_mapDomain_index]
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
e_p :
  Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (a m : A) ↦
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m : B)
          ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a) : Ω[B⁄S]))
      0
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq (α := Ω[B⁄S])
      (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) ⋯ (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
        fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
      0
have e_p₁ : ∀ (b : B),
  HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) 0 : B)
      ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
    0
Tactic: rw [Finsupp.sum_mapRange_index, Finsupp.sum_mapDomain_index]
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
e_p :
  Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (a m : A) ↦
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m : B)
          ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a) : Ω[B⁄S]))
      0
e_p₁ :
  ∀ (b : B),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) 0 : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      0
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq (α := Ω[B⁄S])
      (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) ⋯ (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
        fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
      0
have e_p₂ : ∀ (b : B) (m₁ m₂ : A),
  HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) (m₁ + m₂) : B)
      ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₁ : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) +
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₂ : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S])
Tactic: rw [Finsupp.sum_mapRange_index, Finsupp.sum_mapDomain_index]
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
e_p :
  Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (a m : A) ↦
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m : B)
          ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a) : Ω[B⁄S]))
      0
e_p₁ :
  ∀ (b : B),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) 0 : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      0
e_p₂ :
  ∀ (b : B) (m₁ m₂ : A),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) (m₁ + m₂) : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₁ : B)
          ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) +
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₂ : B)
          ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S])
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq (α := Ω[B⁄S])
      (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) ⋯ (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
        fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
      0
have e_p₃ : ∀ (a : B), HSMul.hSMul (α := B) (β := Ω[B⁄S]) 0 ((D S B : (a : B) → Ω[B⁄S]) a : Ω[B⁄S]) = 0
Tactic: rw [Finsupp.sum_mapRange_index, Finsupp.sum_mapDomain_index]
-- 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 Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄R]) (map R R A B))
    (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))))
have rw : Eq (α := Submodule A Ω[A⁄R])
  (Submodule.span A
      (Set.range.{u_2, u + 1} (ι := R)
        (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
          fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
    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))))
  (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))))
Tactic: rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup,
    Submodule.map_sup, ← kerTotal_eq, ← Submodule.comap_bot,
    Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _),
    bot_sup_eq, Submodule.map_span, ← Set.range_comp]
-- 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 Ω[A⁄R])
    (Submodule.span A
        (Set.range.{u_2, u + 1} (ι := R)
          (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
      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))))
    (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))))
have h₁ : Eq (α := Submodule A Ω[A⁄R])
  (Submodule.span A
    (Set.range.{u_2, u + 1} (ι := R)
      (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
        fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
  ⊥
Tactic: convert! bot_sup_eq _
-- 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)
h₁ :
  Eq (α := Submodule A Ω[A⁄R])
    (Submodule.span A
      (Set.range.{u_2, u + 1} (ι := R)
        (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
          fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    ⊥
⊢ Eq (α := Submodule A Ω[A⁄R])
    (Submodule.span A
        (Set.range.{u_2, u + 1} (ι := R)
          (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
      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))))
    (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))))
have convert_3 : OrderBot (Submodule A Ω[A⁄R])
Tactic: convert! bot_sup_eq _
-- 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := Ω[A⁄R]) (β := Ω[B⁄S]) (⇑(map R S A B) : (a : Ω[A⁄R]) → Ω[B⁄S])
have rw : Set.range (ι := B) (⇑(D S B) : (a : B) → Ω[B⁄S]) ⊆ (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
Tactic: rw [← LinearMap.range_eq_top, _root_.eq_top_iff,
    ← @Submodule.restrictScalars_top A B, ← span_range_derivation,
    Submodule.restrictScalars_span _ _ h, Submodule.span_le]