awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ HSub.hSub (β := P)
      (HSub.hSub (α := P) (β := P) (⁅x, (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n⁆ : P)
        ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) ⁅x, n⁆ : P))
      ((((f : (a : M) → N →ₗ[R] P) ⁅x, m⁆ : N →ₗ[R] P) : (a : N) → P) n : P) =
    HSub.hSub (α := P) (⁅x, (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n⁆ : P)
      (HAdd.hAdd (α := P) (β := P) ((((f : (a : M) → N →ₗ[R] P) ⁅x, m⁆ : N →ₗ[R] P) : (a : N) → P) n : P)
        ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) ⁅x, n⁆ : P))

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ Eq.{w₂ + 1} (α := P)
    ((((lift R L M N P : (a : M →ₗ[R] N →ₗ[R] P) → M ⊗[R] N →ₗ[R] P) f : M ⊗[R] N →ₗ[R] P) : (a : M ⊗[R] N) → P)
        (m ⊗ₜ[R] n) :
      P)
    ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
⊢ Eq (α := (a : M ⊗[R] N) → P)
    (⇑((liftLie R L M N P : (a : M →ₗ⁅R,L⁆ N →ₗ[R] P) → M ⊗[R] N →ₗ⁅R,L⁆ P) f : M ⊗[R] N →ₗ⁅R,L⁆ P) :
      (a : M ⊗[R] N) → P)
    (⇑((lift R L M N P : (a : M →ₗ[R] N →ₗ[R] P) → M ⊗[R] N →ₗ[R] P) (↑f : M →ₗ[R] N →ₗ[R] P) : M ⊗[R] N →ₗ[R] P) :
      (a : M ⊗[R] N) → P)

Tactic:
tauto
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
m : M
n : N
⊢ Eq.{w₂ + 1} (α := P)
    ((((liftLie R L M N P : (a : M →ₗ⁅R,L⁆ N →ₗ[R] P) → M ⊗[R] N →ₗ⁅R,L⁆ P) f : M ⊗[R] N →ₗ⁅R,L⁆ P) :
          (a : M ⊗[R] N) → P)
        (m ⊗ₜ[R] n) :
      P)
    ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
simp only [coe_liftLie_eq_lift_coe, LieModuleHom.coe_toLinearMap, lift_apply]

Premises used: LieModuleHom.coe_toLinearMap, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, TensorProduct.LieModule.lift_apply
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
⊢ Eq (α := P ⊗[R] Q)
    ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, t⁆ : P ⊗[R] Q)
    (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) t⁆ : P ⊗[R] Q)

Tactic:
t.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
refine_1 :
  Eq (α := P ⊗[R] Q) ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, 0⁆)
    ⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) 0⁆
refine_2 :
  ∀ (x_1 : M) (y : N),
    Eq (α := P ⊗[R] Q)
      ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, x_1 ⊗ₜ[R] y⁆ : P ⊗[R] Q)
      (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (x_1 ⊗ₜ[R] y)⁆ : P ⊗[R] Q)
refine_3 :
  ∀ (x_1 y : M ⊗[R] N),
    Eq (α := P ⊗[R] Q)
        ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, x_1⁆ : P ⊗[R] Q)
        (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) x_1⁆ : P ⊗[R] Q) →
      Eq (α := P ⊗[R] Q)
          ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, y⁆ : P ⊗[R] Q)
          (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) y⁆ : P ⊗[R] Q) →
        Eq (α := P ⊗[R] Q)
          ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, x_1 + y⁆ : P ⊗[R] Q)
          (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (x_1 + y)⁆ : P ⊗[R] Q)
⊢ Eq (α := P ⊗[R] Q)
    ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, t⁆ : P ⊗[R] Q)
    (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) t⁆ : P ⊗[R] Q)

Tactic:
refine t.induction_on ?_ ?_ ?_
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
⊢ Eq (α := P ⊗[R] Q) ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, 0⁆)
    ⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) 0⁆

Tactic:
simp only [map_zero, lie_zero]

Premises used: map_zero, lie_zero
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
m : M
n : N
⊢ Eq (α := P ⊗[R] Q)
    ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, m ⊗ₜ[R] n⁆ : P ⊗[R] Q)
    (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (m ⊗ₜ[R] n)⁆ : P ⊗[R] Q)

Tactic:
simp only [LieModuleHom.coe_toLinearMap, lie_tmul_right, LieModuleHom.map_lie, map_tmul,
          map_add]

Premises used: LieModuleHom.coe_toLinearMap, map_add, TensorProduct.LieModule.lie_tmul_right, TensorProduct.map_tmul, LieModuleHom.map_lie
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t t₁ t₂ : M ⊗[R] N
ht₁ :
  Eq (α := P ⊗[R] Q)
    ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, t₁⁆ : P ⊗[R] Q)
    (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) t₁⁆ : P ⊗[R] Q)
ht₂ :
  Eq (α := P ⊗[R] Q)
    ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, t₂⁆ : P ⊗[R] Q)
    (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) t₂⁆ : P ⊗[R] Q)
⊢ Eq (α := P ⊗[R] Q)
    ((TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) ⁅x, t₁ + t₂⁆ : P ⊗[R] Q)
    (⁅x, (TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (t₁ + t₂)⁆ : P ⊗[R] Q)

Tactic:
simp only [ht₁, ht₂, lie_add, map_add]

Premises used: map_add, lie_add
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
⊢ (↑(map f g) : M ⊗[R] N →ₗ[R] P ⊗[R] Q) = TensorProduct.map (↑f : M →ₗ[R] P) (↑g : N →ₗ[R] Q)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
m : M
n : N
⊢ Eq (α := P ⊗[R] Q) ((map f g : (a : M ⊗[R] N) → P ⊗[R] Q) (m ⊗ₜ[R] n) : P ⊗[R] Q)
    ((f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n : P ⊗[R] Q)

Tactic:
map_tmul _ _ _ _

Premises used: TensorProduct.map_tmul
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
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
M' : LieSubmodule R L M
N' : LieSubmodule R L N
⊢ Eq (α := TensorProduct.{u, w, w₁} R ↥M' ↥N' →ₗ⁅R,L⁆ M ⊗[R] N) (mapIncl M' N') (map M'.incl N'.incl)

Tactic:
rfl

Premises used: TensorProduct.LieModule.mapIncl, rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
x m : L
h :
  ∀ (n : M),
    Eq (α := M)
      ((AddHom.toFun (LinearMap.toAddHom (↑(toEnd R L M) : L →ₗ[R] Module.End R M)) ⁅x, m⁆ : (a : M) → M) n : M)
      ((⁅x, AddHom.toFun (LinearMap.toAddHom (↑(toEnd R L M) : L →ₗ[R] Module.End R M)) m⁆ : (a : M) → M) n : M)
⊢ Eq (α := M →ₗ[R] M) (AddHom.toFun (LinearMap.toAddHom (↑(toEnd R L M) : L →ₗ[R] Module.End R M)) ⁅x, m⁆)
    ⁅x, AddHom.toFun (LinearMap.toAddHom (↑(toEnd R L M) : L →ₗ[R] Module.End R M)) m⁆

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
x m : L
n : M
⊢ Eq (α := M) ((AddHom.toFun (LinearMap.toAddHom (↑(toEnd R L M) : L →ₗ[R] Module.End R M)) ⁅x, m⁆ : (a : M) → M) n : M)
    ((⁅x, AddHom.toFun (LinearMap.toAddHom (↑(toEnd R L M) : L →ₗ[R] Module.End R M)) m⁆ : (a : M) → M) n : M)

Tactic:
simp [LieRing.of_associative_ring_bracket]

Premises used: LieRing.of_associative_ring_bracket
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
x : L
m : M
⊢ (toModuleHom R L M : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] m) = ⁅x, m⁆

Tactic:
simp only [toModuleHom, TensorProduct.LieModule.liftLie_apply, LieModuleHom.coe_mk,
    LieHom.coe_toLinearMap, toEnd_apply_apply]

Premises used: TensorProduct.LieModule.liftLie_apply, LieModuleHom.coe_mk, LieModule.toModuleHom, LieHom.coe_toLinearMap, LieModule.toEnd_apply_apply
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
rw :
  Eq.{w + 1} (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    (Submodule.span R
      (Set.image (α := L ⊗[R] M) (⇑(↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
        {t : L ⊗[R] M |
          ∃ (m : ↥I) (n : ↥N),
            ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}))
⊢ ⁅I, N⁆ =
    LieModuleHom.range (LieModuleHom.comp (toModuleHom R L M) (mapIncl I N) : TensorProduct.{u, v, w} R ↥I ↥N →ₗ⁅R,L⁆ M)

Tactic:
rw [← toSubmodule_inj, lieIdeal_oper_eq_linear_span, LieModuleHom.toSubmodule_range,
    LieModuleHom.toLinearMap_comp, LinearMap.range_comp, mapIncl_def, toLinearMap_map,
    TensorProduct.range_map_eq_span_tmul, Submodule.map_span]

Premises used: TensorProduct.LieModule.mapIncl_def, LieModuleHom.toSubmodule_range, LinearMap.range_comp, LieModuleHom.toLinearMap_comp, LieSubmodule.toSubmodule_inj, TensorProduct.LieModule.toLinearMap_map, TensorProduct.range_map_eq_span_tmul, LieSubmodule.lieIdeal_oper_eq_linear_span, Submodule.map_span
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
e_s :
  Eq.{w + 1} (α := M → Prop) (fun (x : M) ↦ ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x) fun (x : M) ↦
    ∃ (a : L ⊗[R] M),
      Membership.mem (γ := Set (L ⊗[R] M))
          {t : L ⊗[R] M |
            ∃ (m : ↥I) (n : ↥N),
              ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
          a ∧
        ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a = x
⊢ Eq.{w + 1} (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    (Submodule.span R
      (Set.image (α := L ⊗[R] M) (⇑(↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
        {t : L ⊗[R] M |
          ∃ (m : ↥I) (n : ↥N),
            ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}))

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
e_s :
  ∀ (m : M),
    (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔
      ∃ (a : L ⊗[R] M),
        Membership.mem (γ := Set (L ⊗[R] M))
            {t : L ⊗[R] M |
              ∃ (m : ↥I) (n : ↥N),
                ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
            a ∧
          ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a = m
⊢ Eq.{w + 1} (α := M → Prop) (fun (x : M) ↦ ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x) fun (x : M) ↦
    ∃ (a : L ⊗[R] M),
      Membership.mem (γ := Set (L ⊗[R] M))
          {t : L ⊗[R] M |
            ∃ (m : ↥I) (n : ↥N),
              ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
          a ∧
        ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a = x

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
m : M
e_s :
  (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) →
    ∃ (a : L ⊗[R] M),
      Membership.mem (γ := Set (L ⊗[R] M))
          {t : L ⊗[R] M |
            ∃ (m : ↥I) (n : ↥N),
              ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
          a ∧
        ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a = m
e_s₁ :
  (∃ (a : L ⊗[R] M),
      Membership.mem (γ := Set (L ⊗[R] M))
          {t : L ⊗[R] M |
            ∃ (m : ↥I) (n : ↥N),
              ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
          a ∧
        ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a = m) →
    ∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m
⊢ (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔
    ∃ (a : L ⊗[R] M),
      Membership.mem (γ := Set (L ⊗[R] M))
          {t : L ⊗[R] M |
            ∃ (m : ↥I) (n : ↥N),
              ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
          a ∧
        ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a = m

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  Membership.mem (γ := Set (L ⊗[R] M))
      {t : L ⊗[R] M |
        ∃ (m : ↥I) (n : ↥N),
          ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
      (x ⊗ₜ[R] n) ∧
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] n) =
      ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆
⊢ ∃ (a : L ⊗[R] M),
    Membership.mem (γ := Set (L ⊗[R] M))
        {t : L ⊗[R] M |
          ∃ (m : ↥I) (n : ↥N),
            ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
        a ∧
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) a =
        ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆

Tactic:
use x ⊗ₜ n
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  Membership.mem (γ := Set (L ⊗[R] M))
    {t : L ⊗[R] M |
      ∃ (m : ↥I) (n : ↥N),
        ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
    (x ⊗ₜ[R] n)
h₁ :
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] n) =
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆
⊢ Membership.mem (γ := Set (L ⊗[R] M))
      {t : L ⊗[R] M |
        ∃ (m : ↥I) (n : ↥N),
          ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
      (x ⊗ₜ[R] n) ∧
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] n) =
      ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  Eq (α := L ⊗[R] M)
    (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
        ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
      L ⊗[R] M)
    (x ⊗ₜ[R] n : L ⊗[R] M)
⊢ Membership.mem (γ := Set (L ⊗[R] M))
    {t : L ⊗[R] M |
      ∃ (m : ↥I) (n : ↥N),
        ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
    (x ⊗ₜ[R] n)

Tactic:
use ⟨x, hx⟩, ⟨n, hn⟩
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ Eq (α := L ⊗[R] M)
    (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
        ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
      L ⊗[R] M)
    (x ⊗ₜ[R] n : L ⊗[R] M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
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
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] n) =
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆

Tactic:
simp