awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x : R
y : M
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x • y) - x • f_inv y) : M) (0 : M)

Tactic:
simp [hf _]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
this : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv 1 - 1) : A) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M)
    (({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → M)
        1 :
      M)
    (0 : M)

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
suffices : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv 1 - 1) : A) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M)
    (({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → M)
        1 :
      M)
    (0 : M)

Tactic:
suffices f (d (f_inv 1 - 1)) = 0 by simpa [sub_eq_zero]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv 1 - 1) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv 1 - 1) : A) : M) (0 : M)

Tactic:
apply hd
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv 1 - 1) : M) (0 : M)

Tactic:
simp [hf _]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x y : M
this : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv (x * y) - f_inv x * f_inv y) : A) : M) (0 : M)
⊢ ({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ } :
        (a : M) → M)
      (x * y) =
    HSMul.hSMul (β := M) x
        (({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ :
                M →ₗ[R] M } :
              (a : M) → M)
            y :
          M) +
      HSMul.hSMul (β := M) y
        (({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ :
                M →ₗ[R] M } :
              (a : M) → M)
            x :
          M)

Tactic:
simpa [sub_eq_zero, hf _]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x y : M
suffices :
  Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv (x * y) - f_inv x * f_inv y) : A) : M) (0 : M)
⊢ ({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ } :
        (a : M) → M)
      (x * y) =
    HSMul.hSMul (β := M) x
        (({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ :
                M →ₗ[R] M } :
              (a : M) → M)
            y :
          M) +
      HSMul.hSMul (β := M) y
        (({ toFun := fun (x : M) ↦ (f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A), map_add' := ⋯, map_smul' := ⋯ :
                M →ₗ[R] M } :
              (a : M) → M)
            x :
          M)

Tactic:
suffices f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0 by simpa [sub_eq_zero, hf _]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x y : M
a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x * y) - f_inv x * f_inv y) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv (x * y) - f_inv x * f_inv y) : A) : M) (0 : M)

Tactic:
apply hd
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x y : M
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x * y) - f_inv x * f_inv y) : M) (0 : M)

Tactic:
simp [hf _]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x : A
this : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv ((f : (a : A) → M) x) - x) : A) : M) (0 : M)
⊢ Eq (α := M) ((liftOfRightInverse hf hd : (a : M) → M) ((f : (a : A) → M) x : M) : M)
    ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M)

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x : A
suffices :
  Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv ((f : (a : A) → M) x) - x) : A) : M) (0 : M)
⊢ Eq (α := M) ((liftOfRightInverse hf hd : (a : M) → M) ((f : (a : A) → M) x : M) : M)
    ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M)

Tactic:
suffices f (d (f_inv (f x) - x)) = 0 by simpa [sub_eq_zero]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x : A
a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv ((f : (a : A) → M) x) - x) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv ((f : (a : A) → M) x) - x) : A) : M) (0 : M)

Tactic:
apply hd
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x : A
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv ((f : (a : A) → M) x) - x) : M) (0 : M)

Tactic:
simp [hf _]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ (⇑f : (a : A) → M)
hf₂ : Function.RightInverse f_inv₂ (⇑f : (a : A) → M)
h :
  ∀ (x : Derivation R A A)
    (x_1 :
      ∀ (x_1 : A),
        Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x_1 : M) (0 : M) →
          Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((x : (a : A) → A) x_1 : A) : M) (0 : M))
    (x_2 : M),
    Eq (α := M) ((liftOfRightInverse hf₁ x_1 : (a : M) → M) x_2 : M)
      ((liftOfRightInverse hf₂ x_1 : (a : M) → M) x_2 : M)
⊢ Eq (α :=
    ⦃d : Derivation R A A⦄ →
      (hd :
          ∀ (x : A),
            Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
              Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)) →
        Derivation R M M)
    (liftOfRightInverse hf₁) (liftOfRightInverse hf₂)

Tactic:
ext _ _ x
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ (⇑f : (a : A) → M)
hf₂ : Function.RightInverse f_inv₂ (⇑f : (a : A) → M)
x_1 : Derivation R A A
h_1 :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((x_1 : (a : A) → A) x : A) : M) (0 : M)
x : M
h :
  ∀ (x : A),
    Eq (α := M) ((liftOfRightInverse hf₁ h_1 : (a : M) → M) ((f : (a : A) → M) x : M) : M)
      ((liftOfRightInverse hf₂ h_1 : (a : M) → M) ((f : (a : A) → M) x : M) : M)
⊢ Eq (α := M) ((liftOfRightInverse hf₁ h_1 : (a : M) → M) x : M) ((liftOfRightInverse hf₂ h_1 : (a : M) → M) x : M)

Tactic:
obtain ⟨x, rfl⟩ := hf₁.surjective x

Premises used: Function.RightInverse.surjective, rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ (⇑f : (a : A) → M)
hf₂ : Function.RightInverse f_inv₂ (⇑f : (a : A) → M)
x_1 : Derivation R A A
h :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((x_1 : (a : A) → A) x : A) : M) (0 : M)
x : A
⊢ Eq (α := M) ((liftOfRightInverse hf₁ h : (a : M) → M) ((f : (a : A) → M) x : M) : M)
    ((liftOfRightInverse hf₂ h : (a : M) → M) ((f : (a : A) → M) x : M) : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing M
inst_3 : Algebra R A
inst_4 : Algebra R M
F : Type u_4
inst_5 : FunLike F A M
inst_6 : AlgHomClass F R A M
f : F
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := M) (⇑f : (a : A) → M)
d : Derivation R A A
hd :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) (0 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M) (0 : M)
x : A
⊢ Eq (α := M) ((liftOfSurjective hf hd : (a : M) → M) ((f : (a : A) → M) x : M) : M)
    ((f : (a : A) → M) ((d : (a : A) → A) x : A) : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCancelCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
D : A →ₗ[R] M
h :
  ∀ (a b : A),
    (D : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
⊢ HAdd.hAdd (α := M) (β := M) ((D : (a : A) → M) 1 : M) ((D : (a : A) → M) 1 : M) = (D : (a : A) → M) 1

Tactic:
simpa only [one_smul, one_mul] using (h 1 1).symm

Premises used: one_smul, OfNat.ofNat, Eq.symm, one_mul
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCancelCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
D : A →ₗ[R] M
h :
  ∀ (a b : A),
    (D : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
⊢ Eq (α := (a : A) → M) (⇑(mk' D h) : (a : A) → M) (⇑D : (a : A) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCancelCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
D : A →ₗ[R] M
h :
  ∀ (a b : A),
    (D : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
⊢ (↑(mk' D h) : A →ₗ[R] M) = D

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (-a) : M) (-(D : (a : A) → M) a : M)

Tactic:
map_neg D a

Premises used: map_neg
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
⊢ (D : (a : A) → M) (a - b) = HSub.hSub (α := M) (β := M) ((D : (a : A) → M) a : M) ((D : (a : A) → M) b : M)

Tactic:
map_sub D a b

Premises used: map_sub
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
n : ℤ
rw : Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) n 1) : M) (0 : M)
rw₁ : HSMul.hSMul (β := M) n ((D : (a : A) → M) 1 : M) = 0
rw₂ : HSMul.hSMul (β := M) n 0 = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)

Tactic:
rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]

Premises used: Derivation.map_one_eq_zero, smul_zero, Derivation.map_smul_of_tower, zsmul_one
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
rw : (D : (a : A) → M) a = -HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)
⊢ (D : (a : A) → M) a = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)

Tactic:
rw [neg_smul]

Premises used: neg_smul
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ (D : (a : A) → M) a = -HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)

Tactic:
eq_neg_of_add_eq_zero_left ?_

Premises used: eq_neg_of_add_eq_zero_left
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
refine :
  HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    0
⊢ (D : (a : A) → M) a = -HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)

Tactic:
refine eq_neg_of_add_eq_zero_left ?_

Premises used: eq_neg_of_add_eq_zero_left
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M)

Tactic:
simp only [smul_smul, h, one_smul, sq]

Premises used: smul_smul, sq, one_smul
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
rw :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    a • (HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M))
rw₁ :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
rw₂ rw₃ :
  a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) =
    a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
⊢ a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M)

Tactic:
rw [leibniz, smul_add, add_comm]

Premises used: add_comm, Derivation.leibniz, smul_add
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
rw : HSMul.hSMul (β := M) a ((D : (a : A) → M) 1 : M) = 0
rw₁ : HSMul.hSMul (β := M) a 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M) = 0

Tactic:
rw [h, map_one_eq_zero, smul_zero]

Premises used: Derivation.map_one_eq_zero, smul_zero
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
D₁ :
  HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M)
D₂ :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M)
D₃ : HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M) = 0
⊢ HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    0

Tactic:
calc
    D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
    _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
    _ = 0 := by rw [h, map_one_eq_zero, smul_zero]

Premises used: HMul.hMul, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
inst_6 : Invertible a
⊢ (D : (a : A) → M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) =
    HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) 2)
      ((D : (a : A) → M) a : M)

Tactic:
D.leibniz_of_mul_eq_one <| invOf_mul_self a

Premises used: invOf_mul_self, Derivation.leibniz_of_mul_eq_one
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
inl : (D : (a : K) → M) 0⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (α := K) (β := ℕ) 0⁻¹ 2) ((D : (a : K) → M) 0 : M)
inr : ∀ (ha : a ≠ 0), (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
⊢ (D : (a : K) → M) 0⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (α := K) (β := ℕ) 0⁻¹ 2) ((D : (a : K) → M) 0 : M)

Tactic:
simp