awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.DifferentialRing
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
R₂ : Type u_3
inst_2 : CommRing R
inst_3 : CommRing R₂
inst_4 : Differential R₂
inst_5 : Algebra A R
inst_6 : Algebra A R₂
inst_7 : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
simp :
  Eq.{u_2 + 1} (α := R) ((h.toRingEquiv.symm : (a : R₂) → R) ((algebraMap A R₂ : (a : A) → R₂) (a′ : A) : R₂) : R)
    ((algebraMap A R : (a : A) → R) (a′ : A) : R)
⊢ Eq (α := R)
    ((h.toRingEquiv.symm.toAddMonoidHom.toIntLinearMap ∘ₗ
            (↑Differential.deriv : R₂ →ₗ[ℤ] R₂) ∘ₗ h.toRingEquiv.toAddMonoidHom.toIntLinearMap :
          (a : R) → R)
        ((algebraMap A R : (a : A) → R) a : R) :
      R)
    ((algebraMap A R : (a : A) → R) (a′ : A) : R)

Tactic:
simp only [RingHom.toAddMonoidHom_eq_coe,
      RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp,
      AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, RingHom.coe_coe, Derivation.coeFn_coe,
      Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]

Premises used: AlgEquiv.toRingEquiv_toRingHom, DifferentialAlgebra.deriv_algebraMap, RingHom.toAddMonoidHom_eq_coe, RingHom.coe_coe, AddMonoidHom.coe_coe, AlgEquiv.commutes, Derivation.coeFn_coe, LinearMap.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply, AddMonoidHom.coe_toIntLinearMap
-- Module: Mathlib.RingTheory.Derivation.DifferentialRing
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
R₂ : Type u_3
inst_2 : CommRing R
inst_3 : CommRing R₂
inst_4 : Differential R₂
inst_5 : Algebra A R
inst_6 : Algebra A R₂
inst_7 : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ Eq.{u_2 + 1} (α := R) ((h.toRingEquiv.symm : (a : R₂) → R) ((algebraMap A R₂ : (a : A) → R₂) (a′ : A) : R₂) : R)
    ((algebraMap A R : (a : A) → R) (a′ : A) : R)

Tactic:
apply h.symm.commutes

Premises used: AlgEquiv.symm, AlgEquiv.commutes
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1_1 D2_1 : Derivation R A A
a_1 : A
D1 D2 : Derivation R A A
a b : A
simp :
  HMul.hMul (β := A) a ((D1 : (a : A) → A) ((D2 : (a : A) → A) b : A) : A) +
          HMul.hMul (α := A) (β := A) ((D2 : (a : A) → A) b : A) ((D1 : (a : A) → A) a : A) +
        (HMul.hMul (β := A) b ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A) +
          HMul.hMul (α := A) (β := A) ((D2 : (a : A) → A) a : A) ((D1 : (a : A) → A) b : A)) -
      (HMul.hMul (β := A) a ((D2 : (a : A) → A) ((D1 : (a : A) → A) b : A) : A) +
          HMul.hMul (α := A) (β := A) ((D1 : (a : A) → A) b : A) ((D2 : (a : A) → A) a : A) +
        (HMul.hMul (β := A) b ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A) +
          HMul.hMul (α := A) (β := A) ((D1 : (a : A) → A) a : A) ((D2 : (a : A) → A) b : A))) =
    a *
        HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) b : A) : A)
          ((D2 : (a : A) → A) ((D1 : (a : A) → A) b : A) : A) +
      b *
        HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A)
          ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A)
⊢ (⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆ : (a : A) → A) (a * b) =
    HSMul.hSMul (β := A) a ((⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆ : (a : A) → A) b : A) +
      HSMul.hSMul (β := A) b ((⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆ : (a : A) → A) a : A)

Tactic:
simp only [Ring.lie_def, map_add, smul_eq_mul, Module.End.mul_apply, leibniz,
        coeFn_coe, LinearMap.sub_apply]

Premises used: map_add, Derivation.leibniz, Derivation.coeFn_coe, Ring.lie_def, LinearMap.sub_apply, smul_eq_mul, Module.End.mul_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1_1 D2_1 : Derivation R A A
a_1 : A
D1 D2 : Derivation R A A
a b : A
⊢ HMul.hMul (β := A) a ((D1 : (a : A) → A) ((D2 : (a : A) → A) b : A) : A) +
          HMul.hMul (α := A) (β := A) ((D2 : (a : A) → A) b : A) ((D1 : (a : A) → A) a : A) +
        (HMul.hMul (β := A) b ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A) +
          HMul.hMul (α := A) (β := A) ((D2 : (a : A) → A) a : A) ((D1 : (a : A) → A) b : A)) -
      (HMul.hMul (β := A) a ((D2 : (a : A) → A) ((D1 : (a : A) → A) b : A) : A) +
          HMul.hMul (α := A) (β := A) ((D1 : (a : A) → A) b : A) ((D2 : (a : A) → A) a : A) +
        (HMul.hMul (β := A) b ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A) +
          HMul.hMul (α := A) (β := A) ((D1 : (a : A) → A) a : A) ((D2 : (a : A) → A) b : A))) =
    a *
        HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) b : A) : A)
          ((D2 : (a : A) → A) ((D1 : (a : A) → A) b : A) : A) +
      b *
        HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A)
          ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A)

Tactic:
ring
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
⊢ (↑⁅D1, D2⁆ : A →ₗ[R] A) = ⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
⊢ (⁅D1, D2⁆ : (a : A) → A) a =
    HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A)
      ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
H : ∀ (a : A), Eq (α := A) ((⁅d + e, f⁆ : (a : A) → A) a : A) ((⁅d, f⁆ + ⁅e, f⁆ : (a : A) → A) a : A)
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
H :
  HAdd.hAdd (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) -
      HAdd.hAdd (α := A) (β := A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) =
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) +
      HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A)
⊢ Eq (α := A) ((⁅d + e, f⁆ : (a : A) → A) a : A) ((⁅d, f⁆ + ⁅e, f⁆ : (a : A) → A) a : A)

Tactic:
simp only [commutator_apply, add_apply, map_add]

Premises used: Derivation.add_apply, map_add, Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
⊢ HAdd.hAdd (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) -
      HAdd.hAdd (α := A) (β := A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) =
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) +
      HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A)

Tactic:
ring
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
H : ∀ (a : A), Eq (α := A) ((⁅d, e + f⁆ : (a : A) → A) a : A) ((⁅d, e⁆ + ⁅d, f⁆ : (a : A) → A) a : A)
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
H :
  HAdd.hAdd (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A)
        ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) -
      HAdd.hAdd (α := A) (β := A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A)
        ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) +
      HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A)
⊢ Eq (α := A) ((⁅d, e + f⁆ : (a : A) → A) a : A) ((⁅d, e⁆ + ⁅d, f⁆ : (a : A) → A) a : A)

Tactic:
simp only [commutator_apply, add_apply, map_add]

Premises used: Derivation.add_apply, map_add, Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
⊢ HAdd.hAdd (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A)
        ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) -
      HAdd.hAdd (α := A) (β := A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A)
        ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) +
      HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A)

Tactic:
ring
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d : Derivation R A A
H : ∀ (a : A), Eq (α := A) ((⁅d, d⁆ : (a : A) → A) a : A) ((0 : (a : A) → A) a : A)
⊢ ⁅d, d⁆ = 0

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d : Derivation R A A
a : A
H :
  HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A)
      ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
    (0 : (a : A) → A) a
⊢ Eq (α := A) ((⁅d, d⁆ : (a : A) → A) a : A) ((0 : (a : A) → A) a : A)

Tactic:
simp only [commutator_apply]

Premises used: Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d : Derivation R A A
a : A
H : Eq (α := A) (0 : A) ((0 : (a : A) → A) a : A)
⊢ HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A)
      ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
    (0 : (a : A) → A) a

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d : Derivation R A A
a : A
⊢ Eq (α := A) (0 : A) ((0 : (a : A) → A) a : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
H : ∀ (a : A), Eq (α := A) ((⁅d, ⁅e, f⁆⁆ : (a : A) → A) a : A) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : A) → A) a : A)
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
H :
  HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
        ((d : (a : A) → A) ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A) -
      HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) =
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
          ((e : (a : A) → A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A) -
        HSub.hSub (α := A) (β := A) ((f : (a : A) → A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A)
          ((f : (a : A) → A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) +
      (HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
          ((e : (a : A) → A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) -
        HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A)
          ((f : (a : A) → A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A))
⊢ Eq (α := A) ((⁅d, ⁅e, f⁆⁆ : (a : A) → A) a : A) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : A) → A) a : A)

Tactic:
simp only [commutator_apply, add_apply, map_sub]

Premises used: map_sub, Derivation.add_apply, Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
⊢ HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
        ((d : (a : A) → A) ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A) -
      HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) =
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
          ((e : (a : A) → A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A) -
        HSub.hSub (α := A) (β := A) ((f : (a : A) → A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A)
          ((f : (a : A) → A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) +
      (HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
          ((e : (a : A) → A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) -
        HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A)
          ((f : (a : A) → A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A))

Tactic:
ring
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
r : R
d e : Derivation R A A
H : ∀ (a : A), Eq (α := A) ((⁅d, r • e⁆ : (a : A) → A) a : A) ((r • ⁅d, e⁆ : (a : A) → A) a : A)
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
r : R
d e : Derivation R A A
a : A
⊢ Eq (α := A) ((⁅d, r • e⁆ : (a : A) → A) a : A) ((r • ⁅d, e⁆ : (a : A) → A) a : A)

Tactic:
simp only [commutator_apply, map_smul, smul_sub, smul_apply]

Premises used: Derivation.smul_apply, smul_sub, Derivation.map_smul, Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
x x_1 : Derivation R A A
x_2 : A
rw :
  (x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) =
    HAdd.hAdd (β := A)
      (HSub.hSub (α := A) (β := A) ((x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) : A)
        ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A))
      ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A)
⊢ (x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) =
    HAdd.hAdd (α := A) (β := A) ((⁅x, x_1⁆ : (a : A) → A) x_2 : A) ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A)

Tactic:
rw [commutator_apply]

Premises used: Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
x x_1 : Derivation R A A
x_2 : A
⊢ (x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) =
    HAdd.hAdd (β := A)
      (HSub.hSub (α := A) (β := A) ((x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) : A)
        ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A))
      ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A)

Tactic:
abel
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
X : Derivation R A A
a : A
⊢ ⁅X, a⁆ = (X : (a : A) → A) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
⊢ ∀ {a b : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)},
    Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
        {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
          Eq (α := Derivation R A A')
            (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                  (a : Derivation R A' A') → Derivation R A A')
                x.1 :
              Derivation R A A')
            (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                  (a : Derivation R A A) → Derivation R A A')
                x.2 :
              Derivation R A A')}
        a →
      Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
          {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
            Eq (α := Derivation R A A')
              (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                    (a : Derivation R A' A') → Derivation R A A')
                  x.1 :
                Derivation R A A')
              (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) :
                      Derivation R A A →ₗ[A] Derivation R A A') :
                    (a : Derivation R A A) → Derivation R A A')
                  x.2 :
                Derivation R A A')}
          b →
        Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
          {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
            Eq (α := Derivation R A A')
              (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                    (a : Derivation R A' A') → Derivation R A A')
                  x.1 :
                Derivation R A A')
              (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) :
                      Derivation R A A →ₗ[A] Derivation R A A') :
                    (a : Derivation R A A) → Derivation R A A')
                  x.2 :
                Derivation R A A')}
          (a + b)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
⊢ Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
⊢ ∀ (c : R) {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)},
    Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
        {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
          Eq (α := Derivation R A A')
            (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                  (a : Derivation R A' A') → Derivation R A A')
                x.1 :
              Derivation R A A')
            (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                  (a : Derivation R A A) → Derivation R A A')
                x.2 :
              Derivation R A A')}
        x →
      Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
        {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
          Eq (α := Derivation R A A')
            (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                  (a : Derivation R A' A') → Derivation R A A')
                x.1 :
              Derivation R A A')
            (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                  (a : Derivation R A A) → Derivation R A A')
                x.2 :
              Derivation R A A')}
        (c • x)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x y : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    x
hy :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    y
⊢ ∀ (a : A),
    Eq.{u_3 + 1} (α := A')
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
            (a : Derivation R A' A') → Derivation R A A')
          x.1))
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
            (a : Derivation R A A) → Derivation R A A')
          x.2))

Tactic:
have hxx (a : A) := congrArg (fun f => f a) hx