-- Mathlib/Algebra/Lie/TensorProduct.lean
theorem coe_liftLie_eq_lift_coe (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) :
    ⇑(liftLie R L M N P f) = lift R L M N P f

Proof state:
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
⊢ ↑((liftLie R L M N P) f) = (lift R L M N P) ↑f

Tactic:
ext m n

Result:
case a.h.h
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
m : M
n : N
⊢ ((AlgebraTensorModule.curry ↑((liftLie R L M N P) f)) m) n = ((AlgebraTensorModule.curry ((lift R L M N P) ↑f)) m) n

Proof state:
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
⊢ ⇑((liftLie R L M N P) f) = ⇑((lift R L M N P) ↑f)

Tactic:
suffices (liftLie R L M N P f : M ⊗[R] N →ₗ[R] P) = lift R L M N P f by
  rw [← this, LieModuleHom.coe_toLinearMap]

Result:
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
⊢ ↑((liftLie R L M N P) f) = (lift R L M N P) ↑f

Proof state:
case a.h.h
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
m : M
n : N
⊢ ((AlgebraTensorModule.curry ↑((liftLie R L M N P) f)) m) n = ((AlgebraTensorModule.curry ((lift R L M N P) ↑f)) m) n

Tactic:
simp only [liftLie, LinearEquiv.trans_apply, LieModuleEquiv.coe_toLinearEquiv,
  toLinearMap_maxTrivLinearMapEquivLieModuleHom, coe_maxTrivEquiv_apply,
  toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm]

Result:
no goals

Proof state:
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
this : ↑((liftLie R L M N P) f) = (lift R L M N P) ↑f
⊢ ⇑((liftLie R L M N P) f) = ⇑((lift R L M N P) ↑f)

Tactic:
rw [← this, LieModuleHom.coe_toLinearMap]

Result:
no goals