awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A ⊤) ⊤
have simp : Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) { toSubmodule := ⊤, lie_mem := sorry } ⊤
Tactic: simp only [baseChange, top_toSubmodule, Submodule.baseChange_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
⊢ Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
have h : ∀ (x : A ⊗[R] M),
  Membership.mem (γ := Set (A ⊗[R] M))
      (Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
        {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m})
      x ↔
    x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (hypothesis)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A ⁅I, N⁆)
    (Bracket.bracket (L := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (baseChange A I) (baseChange A N))
have this : Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
    {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
  s
Tactic: have : (TensorProduct.mk R A M 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s := by ext; simp [s]
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A ⁅I, N⁆)
    (Bracket.bracket (L := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (baseChange A I) (baseChange A N))
have rw : Eq (α := Submodule A (A ⊗[R] M)) (Submodule.span A s)
  (Submodule.span A
    {x : A ⊗[R] M |
      ∃ (x_1 : A ⊗[R] L),
        Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
          ∃ (n : A ⊗[R] M),
            Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x})
Tactic: rw [← toSubmodule_inj, coe_baseChange, lieIdeal_oper_eq_linear_span',
    Submodule.baseChange_span, this, lieIdeal_oper_eq_linear_span']
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
⊢ Eq (α := Submodule A (A ⊗[R] M)) (Submodule.span A s)
    (Submodule.span A
      {x : A ⊗[R] M |
        ∃ (x_1 : A ⊗[R] L),
          Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
            ∃ (n : A ⊗[R] M),
              Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x})
have refine_1 : s ⊆
  {x : A ⊗[R] M |
    ∃ (x_1 : A ⊗[R] L),
      Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
        ∃ (n : A ⊗[R] M), Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x}
Tactic: refine le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
refine_1 :
  s ⊆
    {x : A ⊗[R] M |
      ∃ (x_1 : A ⊗[R] L),
        Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
          ∃ (n : A ⊗[R] M),
            Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x}
⊢ Eq (α := Submodule A (A ⊗[R] M)) (Submodule.span A s)
    (Submodule.span A
      {x : A ⊗[R] M |
        ∃ (x_1 : A ⊗[R] L),
          Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
            ∃ (n : A ⊗[R] M),
              Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x})
have refine_2 : {x : A ⊗[R] M |
    ∃ (x_1 : A ⊗[R] L),
      Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
        ∃ (n : A ⊗[R] M),
          Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x} ⊆
  (↑(Submodule.span A s) : Set (A ⊗[R] M))
Tactic: refine le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x
m : A ⊗[R] M
hm : Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) m
⊢ ⁅x, m⁆ ∈ (↑(Submodule.span A s) : Set (A ⊗[R] M))
have refine_2 : ∀
  (hx :
    Membership.mem (γ := Submodule A (A ⊗[R] L))
      (Submodule.span A
        (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
              (↑I : Submodule R L)) :
          Set (A ⊗[R] L)))
      x)
  (m : A ⊗[R] M)
  (hm :
    Membership.mem (γ := Submodule A (A ⊗[R] M))
      (Submodule.span A
        (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
              (↑N : Submodule R M)) :
          Set (A ⊗[R] M)))
      m),
  ⁅x, m⁆ ∈ (↑(Submodule.span A s) : Set (A ⊗[R] M))
Tactic: rw [mem_baseChange_iff] at hx hm
Cleared hypotheses: hx, m, hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
⊢ ⁅x, m⁆ ∈ (↑(Submodule.span A s) : Set (A ⊗[R] M))
have refine_2 : ∀ (x : A ⊗[R] L) (y : A ⊗[R] M)
  (hx :
    x ∈
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
  (hy :
    y ∈
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M))),
  (fun (x : A ⊗[R] L) (m : A ⊗[R] M)
        (x_1 :
          Membership.mem (γ := Submodule A (A ⊗[R] L))
            (Submodule.span A
              (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                    (↑I : Submodule R L)) :
                Set (A ⊗[R] L)))
            x)
        (x_2 :
          Membership.mem (γ := Submodule A (A ⊗[R] M))
            (Submodule.span A
              (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                    (↑N : Submodule R M)) :
                Set (A ⊗[R] M)))
            m) ↦
      Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, m⁆)
    x y sorry sorry
Tactic: refine Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s)
      ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (hypothesis)
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
have h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
Tactic: have h1 := leibniz_lie x y m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (hypothesis)
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
have h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
Tactic: have h2 := leibniz_lie y x m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
have h : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
Tactic: convert! congr($h1.symm - $h2) using 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
h : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
have h₁ : -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)
Tactic: convert! congr($h1.symm - $h2) using 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
inst : LieRing L
x y : L
⊢ ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0
have rw : ⁅x + y, x + y⁆ = 0
Tactic: rw [← lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (hypothesis)
Goal:
L : Type v
inst : LieRing L
x y : L
⊢ -⁅y, x⁆ = ⁅x, y⁆
have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0
Tactic: have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0 := by rw [← lie_add]; apply lie_self
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x m : L
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw : -⁅m, t • x⁆ = t • ⁅x, m⁆
Tactic: rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x m : L
rw : -⁅m, t • x⁆ = t • ⁅x, m⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw₁ : -⁅m, t • x⁆ = t • -⁅m, x⁆
Tactic: rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x m : L
rw : -⁅m, t • x⁆ = t • ⁅x, m⁆
rw₁ : -⁅m, t • x⁆ = t • -⁅m, x⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw₂ : -(t • ⁅m, x⁆) = t • -⁅m, x⁆
Tactic: rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x m : L
rw : -⁅m, t • x⁆ = t • ⁅x, m⁆
rw₁ : -⁅m, t • x⁆ = t • -⁅m, x⁆
rw₂ : -(t • ⁅m, x⁆) = t • -⁅m, x⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw₃ : -(t • ⁅m, x⁆) = -(t • ⁅m, x⁆)
Tactic: rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ = -⁅x, m⁆
have rw : ⁅-x + x, m⁆ = 0
Tactic: rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m⁆ = -⁅x, m⁆
have rw : ⁅x, -m + m⁆ = 0
Tactic: rw [← sub_eq_zero, sub_neg_eq_add, ← lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x y : L
m : M
⊢ ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
have rw : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
Tactic: rw [leibniz_lie, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x y : L
m : M
rw : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
have rw₁ : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆
Tactic: rw [leibniz_lie, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
inst : LieRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0
have rw : -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0
Tactic: rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x y z : L
m n : M
⊢ Eq.{w + 1} (α := M →+ M) { toFun := fun (m : M) ↦ Bracket.bracket.{v, w} (L := L) 0 m, map_zero' := ⋯, map_add' := ⋯ }
    0
have h : ∀ (n : M),
  Eq (α := M)
    (({ toFun := fun (m : M) ↦ Bracket.bracket.{v, w} (L := L) 0 m, map_zero' := sorry, map_add' := sorry } : (a : M) → M) n :
      M)
    ((0 : (a : M) → M) n : M)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x y_1 z_1 : L
m n : M
y z : L
⊢ { toFun := fun (m : M) ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } =
    HAdd.hAdd (α := M →+ M) { toFun := fun (m : M) ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M }
      { toFun := fun (m : M) ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M }
have h : ∀ (n : M),
  Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅y + z, m⁆, map_zero' := sorry, map_add' := sorry } : (a : M) → M) n : M)
    ((HAdd.hAdd (α := M →+ M) { toFun := fun (m : M) ↦ ⁅y, m⁆, map_zero' := sorry, map_add' := sorry : M →+ M }
            { toFun := fun (m : M) ↦ ⁅z, m⁆, map_zero' := sorry, map_add' := sorry : M →+ M } :
          (a : M) → M)
        n :
      M)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y z : L
m_1 n_1 : M
x : L
f : M →ₗ[R] N
m n : M
⊢ HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) (m + n)⁆ : N) ((f : (a : M) → N) ⁅x, m + n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N)
have simp : HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) (⁅x, (f : (a : M) → N) n⁆ : N) -
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, m⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) =
  HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N) +
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N)
Tactic: simp only [lie_add, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y_1 z : L
m n : M
x y : L
f : M →ₗ[R] N
⊢ {
      toFun := fun (m : M) ↦
        HSub.hSub (α := N) (β := N) (⁅x + y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x + y, m⁆ : N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] N)
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
have h : ∀ (n : M),
  Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N) (⁅x + y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x + y, m⁆ : N),
            map_add' := sorry, map_smul' := sorry } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := sorry, map_smul' := sorry : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
              map_add' := sorry, map_smul' := sorry : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y_1 z : L
m n_1 : M
x y : L
f : M →ₗ[R] N
n : M
⊢ Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N) (⁅x + y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x + y, m⁆ : N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)
have h : HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) (⁅y, (f : (a : M) → N) n⁆ : N) -
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, n⁆ : N) ((f : (a : M) → N) ⁅y, n⁆ : N) =
  HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) +
    HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅y, n⁆ : N)
Tactic: simp only [add_lie, coe_mk, AddHom.coe_mk, add_apply, map_add]