awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
n : ℕ
inst_5 : Fact (0 < n)
⊢ Function.Injective.{u + 1, v + 1} (α :=
    HasQuotient.Quotient Rˣ (B := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))) (β :=
    ↥(selmerGroup (S := ∅)))
    (Function.comp (β :=
      HasQuotient.Quotient Rˣ (B := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit))
      (⇑(QuotientGroup.kerLift fromUnit) : (a : Rˣ ⧸ fromUnit.ker) → ↥selmerGroup)
      (⇑(MulEquiv.symm (QuotientGroup.quotientMulEquivOfEq ⋯)) : (a : Rˣ ⧸ (powMonoidHom n).range) → Rˣ ⧸ fromUnit.ker))

Tactic:
Function.Injective.comp (QuotientGroup.kerLift_injective _) (MulEquiv.injective _)

Premises used: QuotientGroup.kerLift_injective, Function.Injective.comp, MulEquiv.injective
-- Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
n : ℕ
inst_5 : Fact (0 < n)
⊢ Function.Injective.{u + 1, v + 1} (α :=
    HasQuotient.Quotient Rˣ (B := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))) (β :=
    ↥(selmerGroup (S := ∅)))
    (Function.comp (β :=
      HasQuotient.Quotient Rˣ (B := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit))
      (⇑(QuotientGroup.kerLift fromUnit) : (a : Rˣ ⧸ fromUnit.ker) → ↥selmerGroup)
      (⇑(MulEquiv.symm (QuotientGroup.quotientMulEquivOfEq ⋯)) : (a : Rˣ ⧸ (powMonoidHom n).range) → Rˣ ⧸ fromUnit.ker))

Tactic:
exact Function.Injective.comp (QuotientGroup.kerLift_injective _) (MulEquiv.injective _)

Premises used: QuotientGroup.kerLift_injective, Function.Injective.comp, MulEquiv.injective
-- 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_1 D2_1 : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
h : Eq (α := (a : A) → M) ((fun (D : Derivation R A M) ↦ D.toFun) D1) ((fun (D : Derivation R A M) ↦ D.toFun) D2)
mk :
  ∀ (toLinearMap : A →ₗ[R] M) (map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M))
    (leibniz' :
      ∀ (a b : A),
        (toLinearMap : (a : A) → M) (a * b) =
          HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
            HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M))
    (h :
      Eq (α := (a : A) → M)
        ((fun (D : Derivation R A M) ↦ D.toFun)
          { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
        ((fun (D : Derivation R A M) ↦ D.toFun) D2)),
    { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } = D2
⊢ D1 = D2

Tactic:
cases D1
-- 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_1 : Derivation R A M
r : R
a b : A
D2 : Derivation R A M
toLinearMap : A →ₗ[R] M
map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M)
leibniz' :
  ∀ (a b : A),
    (toLinearMap : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M)
h :
  Eq (α := (a : A) → M)
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
    ((fun (D : Derivation R A M) ↦ D.toFun) D2)
mk :
  ∀ (toLinearMap_1 : A →ₗ[R] M)
    (map_one_eq_zero'_1 : Eq.{u_4 + 1} (α := M) ((toLinearMap_1 : (a : A) → M) 1 : M) (0 : M))
    (leibniz'_1 :
      ∀ (a b : A),
        (toLinearMap_1 : (a : A) → M) (a * b) =
          HSMul.hSMul (β := M) a ((toLinearMap_1 : (a : A) → M) b : M) +
            HSMul.hSMul (β := M) b ((toLinearMap_1 : (a : A) → M) a : M))
    (h :
      Eq (α := (a : A) → M)
        ((fun (D : Derivation R A M) ↦ D.toFun)
          { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
        ((fun (D : Derivation R A M) ↦ D.toFun)
          { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 })),
    { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } =
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 }
⊢ { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } = D2

Tactic:
cases D2
-- 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
toLinearMap : A →ₗ[R] M
map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M)
leibniz' :
  ∀ (a b : A),
    (toLinearMap : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M)
toLinearMap_1 : A →ₗ[R] M
map_one_eq_zero'_1 : Eq.{u_4 + 1} (α := M) ((toLinearMap_1 : (a : A) → M) 1 : M) (0 : M)
leibniz'_1 :
  ∀ (a b : A),
    (toLinearMap_1 : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap_1 : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap_1 : (a : A) → M) a : M)
h :
  Eq (α := (a : A) → M)
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 })
mk : toLinearMap = toLinearMap_1
⊢ { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } =
    { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 }

Tactic:
congr
-- 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
toLinearMap : A →ₗ[R] M
map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M)
leibniz' :
  ∀ (a b : A),
    (toLinearMap : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M)
toLinearMap_1 : A →ₗ[R] M
map_one_eq_zero'_1 : Eq.{u_4 + 1} (α := M) ((toLinearMap_1 : (a : A) → M) 1 : M) (0 : M)
leibniz'_1 :
  ∀ (a b : A),
    (toLinearMap_1 : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap_1 : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap_1 : (a : A) → M) a : M)
h :
  Eq (α := (a : A) → M)
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 })
⊢ toLinearMap = toLinearMap_1

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- 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
toLinearMap : A →ₗ[R] M
map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M)
leibniz' :
  ∀ (a b : A),
    (toLinearMap : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M)
toLinearMap_1 : A →ₗ[R] M
map_one_eq_zero'_1 : Eq.{u_4 + 1} (α := M) ((toLinearMap_1 : (a : A) → M) 1 : M) (0 : M)
leibniz'_1 :
  ∀ (a b : A),
    (toLinearMap_1 : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap_1 : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap_1 : (a : A) → M) a : M)
h :
  Eq (α := (a : A) → M)
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 })
⊢ toLinearMap = toLinearMap_1

Tactic:
exact DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- 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
⊢ D.toFun = (⇑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
f : A →ₗ[R] M
h₁ : Eq.{u_4 + 1} (α := M) ((f : (a : A) → M) 1 : M) (0 : M)
h₂ :
  ∀ (a b : A),
    (f : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((f : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((f : (a : A) → M) a : M)
⊢ Eq (α := (a : A) → M) (⇑{ toLinearMap := f, map_one_eq_zero' := h₁, leibniz' := h₂ : Derivation R A M } : (a : A) → M)
    (⇑f : (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
f : Derivation R A M
⊢ Eq (α := (a : A) → M) (⇑(↑f : A →ₗ[R] M) : (a : A) → M) (⇑f : (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
⊢ Function.Injective (α := Derivation R A M) (β := A → M) (DFunLike.coe (β := fun (a : A) ↦ M))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- 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
D1 D2 : Derivation R A M
H : ∀ (a : A), Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) a : M) ((D2 : (a : A) → M) a : M)
⊢ D1 = D2

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- 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
D1 D2 : Derivation R A M
h : D1 = D2
a : A
⊢ Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) a : M) ((D2 : (a : A) → M) a : M)

Tactic:
DFunLike.congr_fun h a

Premises used: DFunLike.congr_fun
-- 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
a b : A
⊢ (D : (a : A) → M) (a + b) = HAdd.hAdd (α := M) (β := M) ((D : (a : A) → M) a : M) ((D : (a : A) → M) b : M)

Tactic:
map_add D a b

Premises used: map_add
-- 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
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) 0 : M) (0 : M)

Tactic:
map_zero D

Premises used: map_zero
-- 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
r : R
a : A
⊢ (D : (a : A) → M) (r • a) = HSMul.hSMul (β := M) r ((D : (a : A) → M) a : M)

Tactic:
D.toLinearMap.map_smul r a

Premises used: Derivation.toLinearMap, LinearMap.map_smul
-- 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
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)

Tactic:
D.leibniz' _ _

Premises used: Derivation.leibniz'
-- 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 : SMul S A
inst_7 : SMul S M
inst_8 : LinearMap.CompatibleSMul A M S R
D : Derivation R A M
r : S
a : A
⊢ (D : (a : A) → M) (r • a) = HSMul.hSMul (β := M) r ((D : (a : A) → M) a : M)

Tactic:
D.toLinearMap.map_smul_of_tower r a

Premises used: Derivation.toLinearMap, LinearMap.map_smul_of_tower
-- 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
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) 1 : M) (0 : M)

Tactic:
D.map_one_eq_zero'

Premises used: Derivation.map_one_eq_zero'
-- 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
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
      M)
    (0 : M)
rw₂ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M) (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A)) : M) (0 : M)
rw₃ : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) r 1) : M) (0 : M)
rw₄ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
rw₅ : HSMul.hSMul (β := M) r 0 = 0
rw₆ rw₇ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)

Tactic:
rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]

Premises used: Derivation.map_one_eq_zero, smul_zero, map_mul, map_one, Derivation.map_smul, Algebra.smul_def, mul_one
-- 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 : ℕ
rw : Eq.{u_4 + 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_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)

Tactic:
rw [← nsmul_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, nsmul_one
-- 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
a : A
zero :
  (D : (a : A) → M) 1 =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
zero₁ : 0 = HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
zero₂ zero₃ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))

Tactic:
rw [pow_zero, map_one_eq_zero, zero_smul]

Premises used: Derivation.map_one_eq_zero, pow_zero, zero_smul
-- 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
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
succ :
  ∀
    (ihn :
      (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
        HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))),
    (D : (a : A) → M) (a ^ HAdd.hAdd (α := ℕ) 0 1) =
      HAdd.hAdd (α := ℕ) 0 1 • HSMul.hSMul (β := M) (a ^ (HAdd.hAdd (α := ℕ) 0 1 - 1)) ((D : (a : A) → M) a : M)
succ₁ :
  ∀ (hpos : 0 < n),
    (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
⊢ (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)

Tactic:
rcases eq_zero_or_pos n with (rfl | hpos)

Premises used: eq_zero_or_pos, 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
a : A
ihn :
  (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
⊢ (D : (a : A) → M) (a ^ HAdd.hAdd (α := ℕ) 0 1) =
    HAdd.hAdd (α := ℕ) 0 1 • HSMul.hSMul (β := M) (a ^ (HAdd.hAdd (α := ℕ) 0 1 - 1)) ((D : (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
D : Derivation R A M
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
hpos : 0 < n
rw : a ^ (n - 1 + 1) = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
rw [← pow_succ', Nat.sub_add_cancel hpos]

Premises used: Nat.sub_add_cancel, pow_succ'
-- 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
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
-- 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
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
hpos : 0 < n
this : a * a ^ (n - 1) = a ^ n
⊢ (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)

Tactic:
simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]

Premises used: smul_smul, Derivation.leibniz, Nat.add_succ_sub_one, add_smul, SMulCommClass.smul_comm, add_zero, one_nsmul, pow_succ'
-- 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
a : A
n : ℕ
zero :
  (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
succ :
  ∀ (n : ℕ) (ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)),
    (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
⊢ (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)

Tactic:
induction n with
  | zero => rw [pow_zero, map_one_eq_zero, zero_smul]
  | succ n ihn =>
    rcases eq_zero_or_pos n with (rfl | hpos)
    · simp
    · have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
      simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]

Premises used: Derivation.map_one_eq_zero, smul_smul, pow_zero, Derivation.leibniz, eq_zero_or_pos, zero_smul, Nat.add_succ_sub_one, add_smul, SMulCommClass.smul_comm, add_zero, one_nsmul, pow_succ', rfl