awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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 : LieDerivation R L L
x y : A ⊗[R] L
x_1 : A
y_1 : L
refine_1 :
  ∀ (x : A) (y : L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) (x ⊗ₜ[R] y)) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
            ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x ⊗ₜ[R] y)) :
          A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] y)
            ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)) :
          A ⊗[R] L)
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) y) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
        A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
have refine_1₁ : ∀ (x y : A ⊗[R] L),
  (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) x) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
            ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x) :
          A ⊗[R] L)
        (⁅x, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L) →
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) y) =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
              ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
            A ⊗[R] L)
          (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L) →
      (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) (x + y)) =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
              ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x + y)) :
            A ⊗[R] L)
          (⁅x + y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
Tactic: refine y.induction_on (by simp) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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 : LieDerivation R L L
x y : A ⊗[R] L
x_1 : A
y_1 : L
x_2 y_2 : A ⊗[R] L
h1 :
  (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) x_2) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
        A ⊗[R] L)
      (⁅x_2, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
h2 :
  (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) y_2) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_2) :
        A ⊗[R] L)
      (⁅y_2, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) (x_2 + y_2)) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_2 + y_2)) :
        A ⊗[R] L)
      (⁅x_2 + y_2, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
have refine_1 : HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
        A ⊗[R] L)
      (⁅x_2, x_1 ⊗ₜ[R] (d : (a : L) → L) y_1⁆ : A ⊗[R] L) +
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_2) :
        A ⊗[R] L)
      (⁅y_2, x_1 ⊗ₜ[R] (d : (a : L) → L) y_1⁆ : A ⊗[R] L) =
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
        A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_2) :
        A ⊗[R] L) -
    HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L) (⁅x_2, x_1 ⊗ₜ[R] (d : (a : L) → L) y_1⁆ : A ⊗[R] L)
      (⁅y_2, x_1 ⊗ₜ[R] (d : (a : L) → L) y_1⁆ : A ⊗[R] L)
Tactic: simp [h1, h2]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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 : LieDerivation R L L
x y x_1 y_1 : A ⊗[R] L
h1 :
  (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x_1, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x_1⁆ : A ⊗[R] L)
h2 :
  (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅y_1, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅y_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_1⁆ : A ⊗[R] L)
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x_1 + y_1, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_1 + y_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 + y_1)⁆ : A ⊗[R] L)
have refine_2 : HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x_1⁆ : A ⊗[R] L) +
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅y_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_1⁆ : A ⊗[R] L) =
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L) -
    HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x_1⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_1⁆ : A ⊗[R] L)
Tactic: simp [h1, h2]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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
x x_1 : LieDerivation R L L
⊢ { toFun := (⇑(LinearMap.lTensor A (↑(x + x_1) : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
      map_smul' := ⋯, leibniz' := ⋯ } =
    HAdd.hAdd (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
      { toFun := (⇑(LinearMap.lTensor A (↑x : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
      { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
have H : ∀ (a : A ⊗[R] L),
  Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.lTensor A (↑(x + x_1) : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
            map_smul' := sorry, leibniz' := sorry } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)
    ((HAdd.hAdd (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
            { toFun := (⇑(LinearMap.lTensor A (↑x : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
            { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)
Tactic: ext _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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
x : R
x_1 : LieDerivation R L L
⊢ { toFun := (⇑(LinearMap.lTensor A (↑(x • x_1) : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
      map_smul' := ⋯, leibniz' := ⋯ } =
    HSMul.hSMul (α := R) (β := LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) ((RingHom.id R : (a : R) → R) x : R)
      { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
have H : ∀ (a : A ⊗[R] L),
  Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.lTensor A (↑(x • x_1) : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
            map_smul' := sorry, leibniz' := sorry } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)
    ((HSMul.hSMul (α := R) (β := LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) ((RingHom.id R : (a : R) → R) x : R)
            { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)
Tactic: ext _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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
x x_1 : LieDerivation R L L
⊢ Eq (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
    { toFun := (⇑(LinearMap.lTensor A (↑⁅x, x_1⁆ : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
      map_smul' := ⋯, leibniz' := ⋯ }
    (Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
      { toFun := (⇑(LinearMap.lTensor A (↑x : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ }
      { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ })
have H : ∀ (z : A ⊗[R] L),
  Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.lTensor A (↑⁅x, x_1⁆ : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
            map_smul' := sorry, leibniz' := sorry } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z :
      A ⊗[R] L)
    ((Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
            { toFun := (⇑(LinearMap.lTensor A (↑x : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry }
            { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z :
      A ⊗[R] L)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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
x x_1 : LieDerivation R L L
z : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.lTensor A (↑⁅x, x_1⁆ : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
            map_smul' := ⋯, leibniz' := ⋯ } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z :
      A ⊗[R] L)
    ((Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
            { toFun := (⇑(LinearMap.lTensor A (↑x : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ }
            { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z :
      A ⊗[R] L)
have H : ∀ (a : A) (l : L),
  Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.lTensor A (↑⁅x, x_1⁆ : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
            map_smul' := sorry, leibniz' := sorry } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        (a ⊗ₜ[R] l) :
      A ⊗[R] L)
    ((Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
            { toFun := (⇑(LinearMap.lTensor A (↑x : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry }
            { toFun := (⇑(LinearMap.lTensor A (↑x_1 : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := sorry,
              map_smul' := sorry, leibniz' := sorry } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        (a ⊗ₜ[R] l) :
      A ⊗[R] L)
Tactic: refine z.induction_on (by simp) (fun a l ↦ ?_) (fun _ _ hx hy ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
D D1_1 D2_1 : LieDerivation R L M
a b : L
D1 D2 : LieDerivation R L M
h : Eq (α := (a : L) → M) ((fun (D : LieDerivation R L M) ↦ D.toFun) D1) ((fun (D : LieDerivation R L M) ↦ D.toFun) D2)
⊢ D1 = D2
have mk : ∀ (toLinearMap : L →ₗ[R] M)
  (leibniz' :
    ∀ (a b : L),
      (toLinearMap : (a : L) → M) ⁅a, b⁆ =
        HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap : (a : L) → M) a⁆ : M))
  (h :
    Eq (α := (a : L) → M)
      ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
      ((fun (D : LieDerivation R L M) ↦ D.toFun) D2)),
  { toLinearMap := toLinearMap, leibniz' := leibniz' } = D2
Tactic: cases D1
Cleared hypotheses: D1, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
D D1 D2_1 : LieDerivation R L M
a b : L
D2 : LieDerivation R L M
toLinearMap : L →ₗ[R] M
leibniz' :
  ∀ (a b : L),
    (toLinearMap : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap : (a : L) → M) a⁆ : M)
h :
  Eq (α := (a : L) → M) ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
    ((fun (D : LieDerivation R L M) ↦ D.toFun) D2)
⊢ { toLinearMap := toLinearMap, leibniz' := leibniz' } = D2
have mk : ∀ (toLinearMap_1 : L →ₗ[R] M)
  (leibniz'_1 :
    ∀ (a b : L),
      (toLinearMap_1 : (a : L) → M) ⁅a, b⁆ =
        HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap_1 : (a : L) → M) b⁆ : M)
          (⁅b, (toLinearMap_1 : (a : L) → M) a⁆ : M))
  (h :
    Eq (α := (a : L) → M)
      ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
      ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 })),
  Eq (α := LieDerivation R L M) { toLinearMap := toLinearMap, leibniz' := leibniz' }
    { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 }
Tactic: cases D2
Cleared hypotheses: D2, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap : L →ₗ[R] M
leibniz' :
  ∀ (a b : L),
    (toLinearMap : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap : (a : L) → M) a⁆ : M)
toLinearMap_1 : L →ₗ[R] M
leibniz'_1 :
  ∀ (a b : L),
    (toLinearMap_1 : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap_1 : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap_1 : (a : L) → M) a⁆ : M)
h :
  Eq (α := (a : L) → M) ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
    ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 })
⊢ Eq (α := LieDerivation R L M) { toLinearMap := toLinearMap, leibniz' := leibniz' }
    { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 }
have mk : toLinearMap = toLinearMap_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ (D : (a : L) → L) ⁅a, b⁆ =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
have rw : HSub.hSub (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (⁅b, (D : (a : L) → L) a⁆ : L) =
  HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
Tactic: rw [LieDerivation.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
rw :
  HSub.hSub (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (⁅b, (D : (a : L) → L) a⁆ : L) =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
⊢ (D : (a : L) → L) ⁅a, b⁆ =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
have rw₁ : HAdd.hAdd (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (-⁅b, (D : (a : L) → L) a⁆ : L) =
  HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
Tactic: rw [LieDerivation.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
rw :
  HSub.hSub (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (⁅b, (D : (a : L) → L) a⁆ : L) =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
rw₁ :
  HAdd.hAdd (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (-⁅b, (D : (a : L) → L) a⁆ : L) =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
⊢ (D : (a : L) → L) ⁅a, b⁆ =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
have rw₂ : HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b) =
  HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
Tactic: rw [LieDerivation.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x : L
hx : x ∈ (↑(LieSubalgebra.lieSpan R L s) : Set L)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
have mem : ∀ (x : L) (hx : x ∈ s), Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
Tactic: induction hx using LieSubalgebra.lieSpan_induction with
  | mem x hx => exact h hx
  | zero => simp
  | add x y _ _ hx hy => simp [hx, hy]
  | smul t x _ hx => simp [hx]
  | lie x y _ _ hx hy => simp [hx, hy]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x : L
hx : x ∈ (↑(LieSubalgebra.lieSpan R L s) : Set L)
mem : ∀ (x : L) (hx : x ∈ s), Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
have zero : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) 0 : M) ((D2 : (a : L) → M) 0 : M)
Tactic: induction hx using LieSubalgebra.lieSpan_induction with
  | mem x hx => exact h hx
  | zero => simp
  | add x y _ _ hx hy => simp [hx, hy]
  | smul t x _ hx => simp [hx]
  | lie x y _ _ hx hy => simp [hx, hy]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x : L
hx : x ∈ (↑(LieSubalgebra.lieSpan R L s) : Set L)
mem : ∀ (x : L) (hx : x ∈ s), Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
zero : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) 0 : M) ((D2 : (a : L) → M) 0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
have add : ∀ (x y : L),
  Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x →
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) y →
      ∀ (hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M))
        (hy : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) y : M) ((D2 : (a : L) → M) y : M)),
        Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) (x + y) : M) ((D2 : (a : L) → M) (x + y) : M)
Tactic: induction hx using LieSubalgebra.lieSpan_induction with
  | mem x hx => exact h hx
  | zero => simp
  | add x y _ _ hx hy => simp [hx, hy]
  | smul t x _ hx => simp [hx]
  | lie x y _ _ hx hy => simp [hx, hy]
Cleared hypotheses: hx