awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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 y : L
t : M ⊗[R] N
this :
  hasBracketAux x ∘ₗ hasBracketAux y =
    HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)
⊢ (hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) t) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)
have rw : (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x) :
      (a : M ⊗[R] N) → M ⊗[R] N)
    t =
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
    ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)
Tactic: rw [← LinearMap.comp_apply, this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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 y : L
t : M ⊗[R] N
⊢ (hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) t) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)
have suffices : hasBracketAux x ∘ₗ hasBracketAux y =
  HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)
Tactic: suffices (hasBracketAux x).comp (hasBracketAux y) =
        hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x) by
      rw [← LinearMap.comp_apply, this]; rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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 y : L
t : M ⊗[R] N
⊢ hasBracketAux x ∘ₗ hasBracketAux y =
    HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)
have a : ∀ (m : M) (n : N),
  Eq (α := M ⊗[R] N)
    (((((AlgebraTensorModule.curry (hasBracketAux x ∘ₗ hasBracketAux y) : M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              m :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)
    (((((AlgebraTensorModule.curry
                    (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆)
                      (hasBracketAux y ∘ₗ hasBracketAux x)) :
                  M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              m :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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 y : L
t : M ⊗[R] N
m : M
n : N
⊢ Eq (α := M ⊗[R] N)
    (((((AlgebraTensorModule.curry (hasBracketAux x ∘ₗ hasBracketAux y) : M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              m :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)
    (((((AlgebraTensorModule.curry
                    (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆)
                      (hasBracketAux y ∘ₗ hasBracketAux x)) :
                  M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              m :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)
have a : HAdd.hAdd (α := M ⊗[R] N) (⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n) (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆) +
    HAdd.hAdd (α := M ⊗[R] N) (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆) (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) =
  HSub.hSub (α := M ⊗[R] N) (⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n) (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n) +
      HSub.hSub (α := M ⊗[R] N) (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) (m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆) +
    (HAdd.hAdd (α := M ⊗[R] N) (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n) (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆) +
      HAdd.hAdd (α := M ⊗[R] N) (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆) (m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆))
Tactic: simp only [hasBracketAux, AlgebraTensorModule.curry_apply, curry_apply, sub_tmul, tmul_sub,
      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, LieHom.map_lie, toEnd_apply_apply, LinearMap.add_apply,
      map_add, LieHom.lie_apply, Module.End.lie_apply, LinearMap.lTensor_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ AddHom.toFun (LinearMap.toAddHom (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
      ⁅x, f⁆ =
    ⁅x,
      AddHom.toFun
        (LinearMap.toAddHom (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P)) f⁆
have a : ∀ (m : M) (n : N),
  Eq.{w₂ + 1} (α := P)
    (((((AlgebraTensorModule.curry
                    (AddHom.toFun
                      (LinearMap.toAddHom
                        (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                      ⁅x, f⁆) :
                  M →ₗ[R] N →ₗ[R] P) :
                (a : M) → N →ₗ[R] P)
              m :
            N →ₗ[R] P) :
          (a : N) → P)
        n :
      P)
    (((((AlgebraTensorModule.curry
                    ⁅x,
                      AddHom.toFun
                        (LinearMap.toAddHom
                          (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                        f⁆ :
                  M →ₗ[R] N →ₗ[R] P) :
                (a : M) → N →ₗ[R] P)
              m :
            N →ₗ[R] P) :
          (a : N) → P)
        n :
      P)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ Eq.{w₂ + 1} (α := P)
    (((((AlgebraTensorModule.curry
                    (AddHom.toFun
                      (LinearMap.toAddHom
                        (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                      ⁅x, f⁆) :
                  M →ₗ[R] N →ₗ[R] P) :
                (a : M) → N →ₗ[R] P)
              m :
            N →ₗ[R] P) :
          (a : N) → P)
        n :
      P)
    (((((AlgebraTensorModule.curry
                    ⁅x,
                      AddHom.toFun
                        (LinearMap.toAddHom
                          (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                        f⁆ :
                  M →ₗ[R] N →ₗ[R] P) :
                (a : M) → N →ₗ[R] P)
              m :
            N →ₗ[R] P) :
          (a : N) → P)
        n :
      P)
have a : 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: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
        AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
        lift.equiv_apply, LieHom.lie_apply, LinearMap.sub_apply, lie_tmul_right, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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)
have 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⁆
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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⁆
⊢ 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)
have 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)
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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)
⊢ 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)
have 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)
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ 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⁆
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ ⁅I, N⁆ =
    LieModuleHom.range (LieModuleHom.comp (toModuleHom R L M) (mapIncl I N) : TensorProduct.{u, v, w} R ↥I ↥N →ₗ⁅R,L⁆ M)
have 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}))
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ 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}))
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ 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
have 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
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ ∃ (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)⁆
have 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)⁆
Tactic: use x ⊗ₜ n
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
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
⊢ 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)⁆
have 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)
Tactic: constructor