awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
S : Type u_5
T : Type u_6
inst_9 : Monoid S
inst_10 : DistribMulAction S M
inst_11 : SMulCommClass R S M
inst_12 : SMulCommClass S A M
inst_13 : Monoid T
inst_14 : DistribMulAction T M
inst_15 : SMulCommClass R T M
inst_16 : SMulCommClass T A M
r : S
D : Derivation R A M
rw : HSMul.hSMul (β := M) r (((↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) = 0
rw₁ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
rw₂ : HSMul.hSMul (β := M) r 0 = 0
⊢ Eq.{u_4 + 1} (α := M) ((r • (↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) (0 : M)
have rw₃ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : Derivation R A M
a_1 : A
⊢ Eq.{u_5 + 1} (α := N)
    ((let __LinearMap : A →ₗ[R] N :=
            (↑R :
                  {S : Type u_2} →
                    {M : Type u_4} →
                      {M₂ : Type u_5} →
                        [inst : Semiring R] →
                          [inst_14 : Semiring S] →
                            [inst_15 : AddCommMonoid M] →
                              [inst_16 : AddCommMonoid M₂] →
                                [inst_17 : Module R M] →
                                  [inst_18 : Module R M₂] →
                                    [inst_19 : Module S M] →
                                      [inst_20 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                f ∘ₗ
              (↑(r • D) : A →ₗ[R] M);
          { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ } :
          (a : A) → N)
        a_1 :
      N)
    ((HSMul.hSMul (α := A) (β := Derivation R A N) ((RingHom.id A : (a : A) → A) r : A)
            (let __LinearMap : A →ₗ[R] N :=
              (↑R :
                    {S : Type u_2} →
                      {M : Type u_4} →
                        {M₂ : Type u_5} →
                          [inst : Semiring R] →
                            [inst_14 : Semiring S] →
                              [inst_15 : AddCommMonoid M] →
                                [inst_16 : AddCommMonoid M₂] →
                                  [inst_17 : Module R M] →
                                    [inst_18 : Module R M₂] →
                                      [inst_19 : Module S M] →
                                        [inst_20 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  f ∘ₗ
                (↑D : A →ₗ[R] M);
            { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ : Derivation R A N }) :
          (a : A) → N)
        a_1 :
      N)
have H : (f : (a : M) → N) (HSMul.hSMul (β := M) r ((D : (a : A) → M) a_1 : M)) =
  HSMul.hSMul (β := N) r ((f : (a : M) → N) ((D : (a : A) → M) a_1 : M) : N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (((↑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
have 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)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ 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
have 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)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (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)
have 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)
Tactic: suffices f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0 by simpa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) ((d : (a : A) → A) (f_inv (x + y) - (f_inv x + f_inv y)) : A) : M) (0 : M)
have a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x + y) - (f_inv x + f_inv y)) : M) (0 : M)
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (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)
have 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)
Tactic: suffices f (d (f_inv (x • y) - x • f_inv y)) = 0 by simpa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) ((d : (a : A) → A) (f_inv (x • y) - x • f_inv y) : A) : M) (0 : M)
have a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x • y) - x • f_inv y) : M) (0 : M)
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
    (({ 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)
have suffices : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) ((d : (a : A) → A) (f_inv 1 - 1) : A) : M) (0 : M)
Tactic: suffices f (d (f_inv 1 - 1)) = 0 by simpa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) ((d : (a : A) → A) (f_inv 1 - 1) : A) : M) (0 : M)
have a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv 1 - 1) : M) (0 : M)
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ ({ 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)
have 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)
Tactic: suffices f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0 by simpa [sub_eq_zero, hf _]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) ((d : (a : A) → A) (f_inv (x * y) - f_inv x * f_inv y) : A) : M) (0 : M)
have a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv (x * y) - f_inv x * f_inv y) : M) (0 : M)
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 (α := 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)
have 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)
Tactic: suffices f (d (f_inv (f x) - x)) = 0 by simpa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) ((d : (a : A) → A) (f_inv ((f : (a : A) → M) x) - x) : A) : M) (0 : M)
have a : Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) (f_inv ((f : (a : A) → M) x) - x) : M) (0 : M)
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ 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₂)
have 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)
Tactic: ext _ _ x
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : M
⊢ Eq (α := M) ((liftOfRightInverse hf₁ h : (a : M) → M) x : M) ((liftOfRightInverse hf₂ h : (a : M) → M) x : M)
have h : ∀ (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: obtain ⟨x, rfl⟩ := hf₁.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : ℤ
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw : Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) n 1) : M) (0 : M)
Tactic: rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw₁ : HSMul.hSMul (β := M) n ((D : (a : A) → M) 1 : M) = 0
Tactic: rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw₂ : HSMul.hSMul (β := M) n 0 = 0
Tactic: rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw₃ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
have rw : (D : (a : A) → M) a = -HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)
Tactic: rw [neg_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
have refine : HAdd.hAdd (α := M) ((D : (a : A) → M) a : M) (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
  0
Tactic: refine eq_neg_of_add_eq_zero_left ?_
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ 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)
have 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))
Tactic: rw [leibniz, smul_add, add_comm]