awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
x : B
⊢ Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    ((D S B : (a : B) → Ω[B⁄S]) x : Ω[B⁄S])
have obtain : ∀ (y : A),
  Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) y) : Ω[B⁄S])
Tactic: obtain ⟨y, rfl⟩ := h x
Cleared hypotheses: 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
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
y : A
⊢ Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) y) : Ω[B⁄S])
have rw : Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
  (((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]) y) :
    Ω[B⁄S])
Tactic: rw [← KaehlerDifferential.map_D R S 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
x : B
y : Ω[A⁄R]
| (mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (x ⊗ₜ[A] y)
have rw : HSMul.hSMul (β := Ω[B⁄R]) x ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R])
Tactic: rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul', map_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
x : B
y : Ω[A⁄R]
⊢ HSMul.hSMul (β := Ω[B⁄R]) x ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R]) =
    HSMul.hSMul (β := Ω[B⁄R]) x
      (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])
have e_a : Eq.{u_3 + 1} (α := Ω[B⁄R]) ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R])
  (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])
Tactic: congr 1
-- 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
⊢ Eq (α := Submodule B Ω[B⁄R]) (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
    (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
have a : LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
  (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
Tactic: apply le_antisymm
-- 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
a :
  LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
    (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
⊢ Eq (α := Submodule B Ω[B⁄R]) (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
    (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
have a₁ : LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
  (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
Tactic: apply le_antisymm
-- 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
r : B
s : Ω[A⁄R]
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (r ⊗ₜ[A] s) : Ω[B⁄R])
have a : ∀ (x : A →₀ A),
  Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])
        (r ⊗ₜ[A] (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x) :
      Ω[B⁄R])
Tactic: obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
Cleared hypotheses: s
-- 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
r : B
x : A →₀ A
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])
        (r ⊗ₜ[A] (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x) :
      Ω[B⁄R])
have a : HSMul.hSMul (β := Ω[B⁄A]) r
    ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
        (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
          ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x)) :
      Ω[B⁄A]) =
  0
Tactic: simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_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
r : B
x : A →₀ A
⊢ HSMul.hSMul (β := Ω[B⁄A]) r
      ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
          (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x)) :
        Ω[B⁄A]) =
    0
have a : HSMul.hSMul (β := Ω[B⁄A]) r
    ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
        (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
          ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) 0)) :
      Ω[B⁄A]) =
  0
Tactic: induction x using Finsupp.induction_linear
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
r : B
x : A →₀ A
a :
  HSMul.hSMul (β := Ω[B⁄A]) r
      ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
          (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) 0)) :
        Ω[B⁄A]) =
    0
⊢ HSMul.hSMul (β := Ω[B⁄A]) r
      ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
          (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x)) :
        Ω[B⁄A]) =
    0
have a₁ : ∀ (f g : A →₀ A),
  HSMul.hSMul (β := Ω[B⁄A]) r
        ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
            (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
              ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) f)) :
          Ω[B⁄A]) =
      0 →
    HSMul.hSMul (β := Ω[B⁄A]) r
          ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
              (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
                ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) g)) :
            Ω[B⁄A]) =
        0 →
      HSMul.hSMul (β := Ω[B⁄A]) r
          ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
              (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
                ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) (f + g))) :
            Ω[B⁄A]) =
        0
Tactic: induction x using Finsupp.induction_linear
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
r : B
x : A →₀ A
a :
  HSMul.hSMul (β := Ω[B⁄A]) r
      ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
          (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) 0)) :
        Ω[B⁄A]) =
    0
a₁ :
  ∀ (f g : A →₀ A),
    HSMul.hSMul (β := Ω[B⁄A]) r
          ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
              (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
                ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) f)) :
            Ω[B⁄A]) =
        0 →
      HSMul.hSMul (β := Ω[B⁄A]) r
            ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
                (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
                  ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) g)) :
              Ω[B⁄A]) =
          0 →
        HSMul.hSMul (β := Ω[B⁄A]) r
            ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
                (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
                  ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) (f + g))) :
              Ω[B⁄A]) =
          0
⊢ HSMul.hSMul (β := Ω[B⁄A]) r
      ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
          (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x)) :
        Ω[B⁄A]) =
    0
have a₂ : ∀ (a b : A),
  HSMul.hSMul (β := Ω[B⁄A]) r
      ((map R A B B : (a : Ω[B⁄R]) → Ω[B⁄A])
          (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R])
            ((linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) (single a b))) :
        Ω[B⁄A]) =
    0
Tactic: induction x using Finsupp.induction_linear
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
x y : B ⊗[A] Ω[A⁄R]
h :
  Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) x : Ω[B⁄R])
h_1 :
  Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (x + y) : Ω[B⁄R])
have a : Membership.mem (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
  (HAdd.hAdd (α := Ω[B⁄R]) (β := Ω[B⁄R]) ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) x : Ω[B⁄R])
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R]))
Tactic: rw [map_add]
-- 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 : B ⊗[A] Ω[A⁄R]
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) x : Ω[B⁄R])
have a : Membership.mem (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
  ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) 0)
Tactic: induction x with
    | zero => simp
    | tmul r s =>
      obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
      induction x using Finsupp.induction_linear
      · simp
      · simp [smul_add, *]
      · simp
    | add => rw [map_add]; exact add_mem ‹_› ‹_›
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
x : B ⊗[A] Ω[A⁄R]
a :
  Membership.mem (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) 0)
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) x : Ω[B⁄R])
have a₁ : ∀ (r : B) (s : Ω[A⁄R]),
  Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (r ⊗ₜ[A] s) : Ω[B⁄R])
Tactic: induction x with
    | zero => simp
    | tmul r s =>
      obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
      induction x using Finsupp.induction_linear
      · simp
      · simp [smul_add, *]
      · simp
    | add => rw [map_add]; exact add_mem ‹_› ‹_›
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
x : B ⊗[A] Ω[A⁄R]
a :
  Membership.mem (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) 0)
a₁ :
  ∀ (r : B) (s : Ω[A⁄R]),
    Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
      ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (r ⊗ₜ[A] s) : Ω[B⁄R])
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) x : Ω[B⁄R])
have a₂ : ∀ (x y : B ⊗[A] Ω[A⁄R]),
  Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
      ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) x : Ω[B⁄R]) →
    Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
        ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R]) →
      Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
        ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (x + y) : Ω[B⁄R])
Tactic: induction x with
    | zero => simp
    | tmul r s =>
      obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
      induction x using Finsupp.induction_linear
      · simp
      · simp [smul_add, *]
      · simp
    | add => rw [map_add]; exact add_mem ‹_› ‹_›
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
⊢ LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
have h : Eq (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
  (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
Tactic: convert_to (kerTotal A B).map (Finsupp.linearCombination B (D R 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 :
  Eq (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
⊢ LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
have a : LE.le (α := Submodule B Ω[B⁄R]) (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
  (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
Tactic: convert_to (kerTotal A B).map (Finsupp.linearCombination B (D R 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
⊢ Eq (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
have h : Eq (α := Submodule B Ω[B⁄R])
  (Submodule.map (M := B →₀ B) (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R]))
    (Submodule.comap (M₂ := B →₀ B)
      (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B))
      (Submodule.restrictScalars B (kerTotal A B))))
  (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
Tactic: rw [KaehlerDifferential.ker_map]
-- 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
⊢ Eq (α := Submodule B Ω[B⁄R])
    (Submodule.map (M := B →₀ B) (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R]))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B))
        (Submodule.restrictScalars B (kerTotal A B))))
    (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
have h : Submodule.comap (M₂ := B →₀ B)
    (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B))
    (Submodule.restrictScalars B (kerTotal A B)) =
  kerTotal A B
Tactic: congr 1
-- 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
⊢ Submodule.comap (M₂ := B →₀ B)
      (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B))
      (Submodule.restrictScalars B (kerTotal A B)) =
    kerTotal A B
have h : Eq (α := (B →₀ B) →ₗ[B] B →₀ B)
  (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B)) LinearMap.id
Tactic: convert! Submodule.comap_id _
-- 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
⊢ Eq (α := (B →₀ B) →ₗ[B] B →₀ B)
    (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B)) LinearMap.id
have h : ∀ (a a_1 : B),
  Eq (α := B)
    ((((mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B)) ∘ₗ lsingle a :
              (a : B) → B →₀ B)
            1 :
          (a : B) → B)
        a_1 :
      B)
    (((LinearMap.id ∘ₗ lsingle a : (a : B) → B →₀ B) 1 : (a : B) → B) a_1 : B)
Tactic: ext
-- 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
⊢ LE.le (α := Submodule B Ω[B⁄R]) (Submodule.map (linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R])) (kerTotal A B))
    (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
have a : (((Set.range fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
      Set.range fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
    Set.range fun (x : A) ↦ single ((algebraMap A B : (a : A) → B) x) 1) ⊆
  (↑(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))
Tactic: rw [Submodule.map_le_iff_le_comap, kerTotal, Submodule.span_le]
-- 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 y : B
⊢ (fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) (x, y) ∈
    (↑(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]) 0)
  ((linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R]) : (a : B →₀ B) → Ω[B⁄R])
    ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) (x, y)))
Tactic: use 0
-- 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 y : B
⊢ (fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) (x, y) ∈
    (↑(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]) 0)
  ((linearCombination B (⇑(D R B) : (a : B) → Ω[B⁄R]) : (a : B →₀ B) → Ω[B⁄R])
    ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) (x, y)))
Tactic: use 0