awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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]) x)) :
        Ω[B⁄A]) =
    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])
        (r ⊗ₜ[A] (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x) :
      Ω[B⁄R])

Tactic:
simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]

Premises used: KaehlerDifferential.mapBaseChange_tmul, LinearMap.mem_ker, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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
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
⊢ 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:
induction x using Finsupp.induction_linear
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
r : B
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
r : B
f g : A →₀ A
h :
  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
h_1 :
  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:
simp [smul_add, *]

Premises used: smul_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
r : B
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:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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])
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]))
⊢ 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:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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 (γ := 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:
add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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 (γ := 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:
exact add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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])
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])
⊢ 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])

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 ‹_› ‹_›

Premises used: KaehlerDifferential.mapBaseChange_tmul, map_add, LinearMap.mem_ker, AddMemClass.add_mem, smul_add, rfl, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h :
  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))
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))
⊢ 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:
convert_to (kerTotal A B).map (Finsupp.linearCombination B (D R B)) ≤ _

Premises used: KaehlerDifferential.D, Submodule.map, Finsupp.linearCombination, DFunLike.coe, KaehlerDifferential.kerTotal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h :
  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))
⊢ 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:
rw [KaehlerDifferential.ker_map]

Premises used: KaehlerDifferential.ker_map
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h :
  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
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
⊢ Eq (α := Submodule B (B →₀ B)) (Submodule.comap LinearMap.id (Submodule.restrictScalars B (kerTotal A B)))
    (Submodule.restrictScalars B (kerTotal A B))

Tactic:
Submodule.comap_id _

Premises used: Submodule.comap_id
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h :
  Eq (α := (B →₀ B) →ₗ[B] B →₀ B)
    (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B)) LinearMap.id
⊢ 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:
convert! Submodule.comap_id _

Premises used: Submodule.comap_id
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h :
  ∀ (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)
⊢ Eq (α := (B →₀ B) →ₗ[B] B →₀ B)
    (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B (⇑(algebraMap B B) : (a : B) → B)) LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
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))
⊢ 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:
rw [Submodule.map_le_iff_le_comap, kerTotal, Submodule.span_le]

Premises used: Submodule.map_le_iff_le_comap, Submodule.span_le, KaehlerDifferential.kerTotal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x y : B
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)))
⊢ (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))

Tactic:
use 0
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x y : B
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x y : B
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)))
⊢ (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))

Tactic:
use 0
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x y : B
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
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])
⊢ (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))

Tactic:
use 1 ⊗ₜ D _ _ x

Premises used: KaehlerDifferential.D, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
⊢ Function.Exact (M := B ⊗[A] Ω[A⁄R]) (N := Ω[B⁄R]) (P := Ω[B⁄A])
    (⇑(mapBaseChange R A B) : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (⇑(map R A B B) : (a : Ω[B⁄R]) → Ω[B⁄A])

Tactic:
SetLike.ext_iff.mp (range_mapBaseChange R A B).symm

Premises used: Function.Exact, Set.Mem, setOf, KaehlerDifferential.range_mapBaseChange, SetLike.ext_iff, Set.preimage, Set.singleton, Iff.mp, Set.range, Eq.symm
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
x y : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))
⊢ 1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) (↑(x + y) : A) =
    HAdd.hAdd (α := B ⊗[A] Ω[A⁄R]) (β := B ⊗[A] Ω[A⁄R]) (1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) (↑x : A) : B ⊗[A] Ω[A⁄R])
      (1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) (↑y : A) : B ⊗[A] Ω[A⁄R])

Tactic:
simp only [Submodule.coe_add, map_add, TensorProduct.tmul_add]

Premises used: Submodule.coe_add, map_add, TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
r : A
x : ↥(RingHom.ker (F := A →+* B) (algebraMap A B))
⊢ 1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) (↑(r • x) : A) =
    HSMul.hSMul (α := A) (β := B ⊗[A] Ω[A⁄R]) ((RingHom.id A : (a : A) → A) r : A)
      (1 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) (↑x : A) : B ⊗[A] Ω[A⁄R])

Tactic:
simp only [SetLike.val_smul, smul_eq_mul, Derivation.leibniz,
    TensorProduct.tmul_add, TensorProduct.tmul_smul, TensorProduct.smul_tmul', ←
    algebraMap_eq_smul_one, RingHom.mem_ker.mp x.prop, TensorProduct.zero_tmul, add_zero,
    RingHom.id_apply]

Premises used: RingHom.id_apply, TensorProduct.tmul_smul, RingHom.mem_ker, TensorProduct.zero_tmul, Derivation.leibniz, Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul', SetLike.val_smul, Subtype.prop, Iff.mp, TensorProduct.tmul_add, smul_eq_mul, add_zero