awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
N : Type u_5
inst_6 : AddCommMonoid N
inst_7 : Module A N
inst_8 : Module R N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
⊢ Eq (α := (a : A) → N)
    (⇑(((f.compDer : Derivation R A M →ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) D :
          Derivation R A N) :
      (a : A) → N)
    (⇑((↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f ∘ₗ
          (↑D : A →ₗ[R] M)) :
      (a : A) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
f₁ f₂ : M →ₗ[A] N
h :
  ∀ (x : Derivation R A M) (a : A),
    Eq.{u_5 + 1} (α := N)
      ((((((f₁ + f₂).compDer : Derivation R A M →ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) x :
              Derivation R A N) :
            (a : A) → N)
          a :
        N)
      ((((HAdd.hAdd (α := Derivation R A M →ₗ[A] Derivation R A N) (β := Derivation R A M →ₗ[A] Derivation R A N)
                    (f₁.compDer : Derivation R A M →ₗ[A] Derivation R A N)
                    (f₂.compDer : Derivation R A M →ₗ[A] Derivation R A N) :
                  (a : Derivation R A M) → Derivation R A N)
                x :
              Derivation R A N) :
            (a : A) → N)
          a :
        N)
⊢ (f₁ + f₂).compDer =
    HAdd.hAdd (α := Derivation R A M →ₗ[A] Derivation R A N) (β := Derivation R A M →ₗ[A] Derivation R A N)
      (f₁.compDer : Derivation R A M →ₗ[A] Derivation R A N) (f₂.compDer : Derivation R A M →ₗ[A] Derivation R A N)

Tactic:
ext
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
f₁ f₂ : M →ₗ[A] N
x : Derivation R A M
a_1 : A
⊢ Eq.{u_5 + 1} (α := N)
    ((((((f₁ + f₂).compDer : Derivation R A M →ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) x :
            Derivation R A N) :
          (a : A) → N)
        a_1 :
      N)
    ((((HAdd.hAdd (α := Derivation R A M →ₗ[A] Derivation R A N) (β := Derivation R A M →ₗ[A] Derivation R A N)
                  (f₁.compDer : Derivation R A M →ₗ[A] Derivation R A N)
                  (f₂.compDer : Derivation R A M →ₗ[A] Derivation R A N) :
                (a : Derivation R A M) → Derivation R A N)
              x :
            Derivation R A N) :
          (a : A) → N)
        a_1 :
      N)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r_1 : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
h :
  ∀ (x : Derivation R A M) (a : A),
    Eq.{u_5 + 1} (α := N)
      ((((((r • D).compDer : Derivation R A M →ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) x :
              Derivation R A N) :
            (a : A) → N)
          a :
        N)
      ((((HSMul.hSMul (α := A) (β := Derivation R A M →ₗ[A] Derivation R A N) ((RingHom.id A : (a : A) → A) r : A)
                    (D.compDer : Derivation R A M →ₗ[A] Derivation R A N) :
                  (a : Derivation R A M) → Derivation R A N)
                x :
              Derivation R A N) :
            (a : A) → N)
          a :
        N)
⊢ (r • D).compDer =
    HSMul.hSMul (α := A) (β := Derivation R A M →ₗ[A] Derivation R A N) ((RingHom.id A : (a : A) → A) r : A)
      (D.compDer : Derivation R A M →ₗ[A] Derivation R A N)

Tactic:
ext
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r_1 : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
x : Derivation R A M
a_1 : A
⊢ Eq.{u_5 + 1} (α := N)
    ((((((r • D).compDer : Derivation R A M →ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) x :
            Derivation R A N) :
          (a : A) → N)
        a_1 :
      N)
    ((((HSMul.hSMul (α := A) (β := Derivation R A M →ₗ[A] Derivation R A N) ((RingHom.id A : (a : A) → A) r : A)
                  (D.compDer : Derivation R A M →ₗ[A] Derivation R A N) :
                (a : Derivation R A M) → Derivation R A N)
              x :
            Derivation R A N) :
          (a : A) → N)
        a_1 :
      N)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
H :
  ∀ (a : A),
    Eq.{u_4 + 1} (α := M)
      ((((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
                  (a : Derivation R A N) → Derivation R A M)
                (AddHom.toFun (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
                  D) :
              Derivation R A M) :
            (a : A) → M)
          a :
        M)
      ((D : (a : A) → M) a : M)
⊢ (((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
        (a : Derivation R A N) → Derivation R A M)
      (AddHom.toFun (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N)) D) =
    D

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a_1 b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
a : A
⊢ Eq.{u_4 + 1} (α := M)
    ((((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
                (a : Derivation R A N) → Derivation R A M)
              (AddHom.toFun (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
                D) :
            Derivation R A M) :
          (a : A) → M)
        a :
      M)
    ((D : (a : A) → M) a : M)

Tactic:
e.symm_apply_apply (D a)

Premises used: LinearEquiv.symm_apply_apply, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a_1 b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
a : A
⊢ Eq.{u_4 + 1} (α := M)
    ((((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
                (a : Derivation R A N) → Derivation R A M)
              (AddHom.toFun (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
                D) :
            Derivation R A M) :
          (a : A) → M)
        a :
      M)
    ((D : (a : A) → M) a : M)

Tactic:
exact e.symm_apply_apply (D a)

Premises used: LinearEquiv.symm_apply_apply, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A N
H :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := N)
      ((AddHom.toFun (M := Derivation R A M)
              (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
              ((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
                  (a : Derivation R A N) → Derivation R A M)
                D) :
            (a : A) → N)
          a :
        N)
      ((D : (a : A) → N) a : N)
⊢ AddHom.toFun (M := Derivation R A M)
      (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
      ((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
          (a : Derivation R A N) → Derivation R A M)
        D) =
    D

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a_1 b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A N
a : A
⊢ Eq.{u_5 + 1} (α := N)
    ((AddHom.toFun (M := Derivation R A M)
            (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
            ((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
                (a : Derivation R A N) → Derivation R A M)
              D) :
          (a : A) → N)
        a :
      N)
    ((D : (a : A) → N) a : N)

Tactic:
e.apply_symm_apply (D a)

Premises used: LinearEquiv.apply_symm_apply, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a_1 b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A N
a : A
⊢ Eq.{u_5 + 1} (α := N)
    ((AddHom.toFun (M := Derivation R A M)
            (LinearMap.toAddHom ((↑e : M →ₗ[A] N).compDer : Derivation R A M →ₗ[A] Derivation R A N))
            ((((↑e.symm : N →ₗ[A] M).compDer : Derivation R A N →ₗ[A] Derivation R A M) :
                (a : Derivation R A N) → Derivation R A M)
              D) :
          (a : A) → N)
        a :
      N)
    ((D : (a : A) → N) a : N)

Tactic:
exact e.apply_symm_apply (D a)

Premises used: LinearEquiv.apply_symm_apply, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
N : Type u_5
inst_6 : AddCommMonoid N
inst_7 : Module A N
inst_8 : Module R N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
e : M ≃ₗ[A] N
⊢ Eq (α := A →ₗ[R] N)
    (↑(((e.compDer : Derivation R A M ≃ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) D) :
      A →ₗ[R] N)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑e : M →ₗ[A] N) ∘ₗ
      (↑D : A →ₗ[R] M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
N : Type u_5
inst_6 : AddCommMonoid N
inst_7 : Module A N
inst_8 : Module R N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
e : M ≃ₗ[A] N
⊢ Eq (α := (a : A) → N)
    (⇑(((e.compDer : Derivation R A M ≃ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) D :
          Derivation R A N) :
      (a : A) → N)
    (⇑((↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (↑e : M →ₗ[A] N) ∘ₗ
          (↑D : A →ₗ[R] M)) :
      (a : A) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower A B M
d : Derivation R B M
⊢ Eq.{u_4 + 1} (α := M) (((↑d : B →ₗ[R] M) ∘ₗ AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → M) 1 : M)
    (0 : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2 : Derivation R A M
r : R
a_1 b_1 : A
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower A B M
d : Derivation R B M
a b : A
⊢ ((↑d : B →ₗ[R] M) ∘ₗ AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → M) (a * b) =
    HSMul.hSMul (β := M) a
        (((↑d : B →ₗ[R] M) ∘ₗ AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → M) b : M) +
      HSMul.hSMul (β := M) b
        (((↑d : B →ₗ[R] M) ∘ₗ AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → M) a : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
S : Type u_5
inst_6 : CommSemiring S
inst_7 : Algebra S A
inst_8 : Module S M
inst_9 : LinearMap.CompatibleSMul A M R S
d : Derivation S A M
⊢ Eq (α := (a : A) → M) (⇑(Derivation.restrictScalars R d) : (a : A) → M) (⇑d : (a : A) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
S : Type u_5
inst_6 : CommSemiring S
inst_7 : Algebra S A
inst_8 : Module S M
inst_9 : LinearMap.CompatibleSMul A M R S
d : Derivation S A M
x : A
⊢ Eq.{u_4 + 1} (α := M) ((Derivation.restrictScalars R d : (a : A) → M) x : M) ((d : (a : A) → M) x : M)

Tactic:
rfl

Premises used: 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 : 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)
⊢ (f : (a : A) → M) ((d : (a : A) → A) (f_inv (x + y)) : A) =
    HAdd.hAdd (α := M) (β := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A) : M)
      ((f : (a : A) → M) ((d : (a : A) → A) (f_inv y) : 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 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)
⊢ (f : (a : A) → M) ((d : (a : A) → A) (f_inv (x + y)) : A) =
    HAdd.hAdd (α := M) (β := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv x) : A) : M)
      ((f : (a : A) → M) ((d : (a : A) → A) (f_inv y) : A) : M)

Tactic:
suffices f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 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 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 : R
y : M
this : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv (x • y) - x • f_inv y) : A) : M) (0 : M)
⊢ (f : (a : A) → M) ((d : (a : A) → A) (f_inv (x • y)) : A) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((f : (a : A) → M) ((d : (a : A) → A) (f_inv y) : 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 : R
y : M
suffices : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv (x • y) - x • f_inv y) : A) : M) (0 : M)
⊢ (f : (a : A) → M) ((d : (a : A) → A) (f_inv (x • y)) : A) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((f : (a : A) → M) ((d : (a : A) → A) (f_inv y) : A) : M)

Tactic:
suffices f (d (f_inv (x • y) - x • f_inv y)) = 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 : R
y : M
a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x • y) - x • f_inv y) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv (x • y) - x • f_inv y) : A) : M) (0 : M)

Tactic:
apply hd