awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
mp :
  Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a →
    ∀ (x y z : L),
      (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
mpr :
  (∀ (x y z : L),
      (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)) →
    Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a ↔
    ∀ (x y z : L),
      (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h : Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a
x y z : L
mp :
  ∀
    (h :
      Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
        ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
        (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M))
    (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)

Tactic:
rw [mem_twoCocycle_iff] at h

Premises used: LieModule.Cohomology.mem_twoCocycle_iff
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
x y z : L
⊢ Eq.{u_3 + 1} (α := M)
    ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)
    (0 : M)

Tactic:
have : (d₂₃ R L M) a x y z = 0 := (congrArg (fun b ↦ b x y z = 0) h).mpr rfl
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
x y z : L
this :
  Eq.{u_3 + 1} (α := M)
    ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)
    (0 : M)
⊢ HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    0

Tactic:
simp only [d₂₃_apply, trivial_lie_zero, sub_self, add_zero, zero_sub] at this

Premises used: sub_self, LieModule.Cohomology.d₂₃_apply, trivial_lie_zero, add_zero, zero_sub
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
x y z : L
this :
  HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    0
⊢ HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M) =
    (((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x

Tactic:
rw [sub_eq_zero] at this

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
x y z : L
this :
  HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M) =
    (((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x
mp :
  -HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M) =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      (-(((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M)
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)

Tactic:
rw [← twoCochain_skew a _ x, ← twoCochain_skew a _ y, ← this]

Premises used: LieModule.Cohomology.twoCochain_skew
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
x y z : L
this :
  HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M) =
    (((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x
⊢ -HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M) =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      (-(((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  ∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
mpr :
  ∀ (x y z : L),
    Eq.{u_3 + 1} (α := M)
      ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                        (a : L) → L →ₗ[R] L →ₗ[R] M)
                      x :
                    L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                y :
              L →ₗ[R] M) :
            (a : L) → M)
          z :
        M)
      ((((((0 : (a : L) → L →ₗ[R] L →ₗ[R] M) x : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M)
          z :
        M)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a

Tactic:
ext x y z
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  ∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
x y z : L
mpr :
  HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    0
⊢ Eq.{u_3 + 1} (α := M)
    ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)
    ((((((0 : (a : L) → L →ₗ[R] L →ₗ[R] M) x : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M)
        z :
      M)

Tactic:
simp only [d₂₃_apply, trivial_lie_zero, sub_self, add_zero, zero_sub, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, sub_self, LieModule.Cohomology.d₂₃_apply, trivial_lie_zero, add_zero, zero_sub
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  ∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
x y z : L
mpr :
  HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        (-(((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M) -
      -HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M) =
    0
⊢ HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    0

Tactic:
rw [← twoCochain_skew a x, ← twoCochain_skew a y, h x y z]

Premises used: LieModule.Cohomology.twoCochain_skew
-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  ∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
x y z : L
⊢ HAdd.hAdd (α := M) (β := M) (-(((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        (-(((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M) -
      -HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M) =
    0

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x + y) =
      HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
        ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x : A ⊗[R] L)
        ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y : A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
⊢ ∀ (m : R) (x : A ⊗[R] L),
    (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (m • x) =
      HSMul.hSMul (α := R) (β := A ⊗[R] L) ((RingHom.id R : (a : R) → R) m : R)
        ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x : A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
simp :
  (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x⁆ : A ⊗[R] L)
⊢ ({ toFun := (⇑(LinearMap.rTensor L (↑d : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯ } :
        (a : A ⊗[R] L) → A ⊗[R] L)
      ⁅x, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x,
          ({ toFun := (⇑(LinearMap.rTensor L (↑d : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯ : A ⊗[R] L →ₗ[R] A ⊗[R] L } :
              (a : A ⊗[R] L) → A ⊗[R] L)
            y⁆ :
        A ⊗[R] L)
      (⁅y,
          ({ toFun := (⇑(LinearMap.rTensor L (↑d : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯ : A ⊗[R] L →ₗ[R] A ⊗[R] L } :
              (a : A ⊗[R] L) → A ⊗[R] L)
            x⁆ :
        A ⊗[R] L)

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, AddHom.coe_mk
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (Bracket.bracket (L := A ⊗[R] L) 0 y) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) 0 ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
        A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) 0⁆ : A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
refine_1 :
  ∀ (x : A) (l : L),
    (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] l) y) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] l)
            ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
          A ⊗[R] L)
        (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x ⊗ₜ[R] l)⁆ : A ⊗[R] L)
refine_2 :
  ∀ (x x_1 : A ⊗[R] L)
    (h1 :
      (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x, y⁆ =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (⁅x, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
          (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x⁆ : A ⊗[R] L))
    (h2 :
      (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x_1, y⁆ =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (⁅x_1, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
          (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_1⁆ : A ⊗[R] L)),
    (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x + x_1, y⁆ =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (⁅x + x_1, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
        (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x + x_1)⁆ : A ⊗[R] L)
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x⁆ : A ⊗[R] L)

Tactic:
refine x.induction_on (by simp) (fun _ l ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x_1 : A
l : L
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) 0) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) 0) :
        A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) 0
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)) :
        A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x_1 : A
l : L
refine_1 :
  ∀ (x : A) (l' : L),
    (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) (x ⊗ₜ[R] l')) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
            ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x ⊗ₜ[R] l')) :
          A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] l')
            ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)) :
          A ⊗[R] L)
refine_1₁ :
  ∀ (x x_2 : A ⊗[R] L)
    (h1 :
      (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) x) =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
              ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x) :
            A ⊗[R] L)
          (⁅x, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L))
    (h2 :
      (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) x_2) =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
              ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
            A ⊗[R] L)
          (⁅x_2, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L)),
    (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) (x + x_2)) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
            ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x + x_2)) :
          A ⊗[R] L)
        (⁅x + x_2, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L)
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) y) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
        A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L)

Tactic:
refine y.induction_on (by simp) (fun _ l' ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x_1 : A
l : L
x_2 : A
l' : L
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) (x_2 ⊗ₜ[R] l')) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_2 ⊗ₜ[R] l')) :
        A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_2 ⊗ₜ[R] l')
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)) :
        A ⊗[R] L)

Tactic:
simp [← lie_skew l' l, -lie_skew, add_tmul, tmul_neg]

Premises used: lie_skew, TensorProduct.add_tmul, TensorProduct.tmul_neg