-- Mathlib/Algebra/Lie/TraceForm.lean
lemma trace_eq_trace_restrict_of_le_idealizer
    (hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m _ ↦ N.lie_mem (N.mem_idealizer.mp (h hy) m)) :
    trace R M (φ x ∘ₗ φ y) = trace R N ((φ x ∘ₗ φ y).restrict hy')

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯
this✝ : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
this : (trace R ↥N) ((φ x ∘ₗ φ y).restrict ⋯) = (trace R M) (φ x ∘ₗ φ y)
⊢ (trace R M) (φ x ∘ₗ φ y) = (trace R ↥N) ((φ x ∘ₗ φ y).restrict hy')

Tactic:
simp [this]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯
⊢ (trace R M) (φ x ∘ₗ φ y) = (trace R ↥N) ((φ x ∘ₗ φ y).restrict hy')

Tactic:
suffices ∀ m, ⁅x, ⁅y, m⁆⁆ ∈ N by
  have : (trace R { x // x ∈ N }) ((φ x ∘ₗ φ y).restrict _) = (trace R M) (φ x ∘ₗ φ y) :=
    (φ x ∘ₗ φ y).trace_restrict_eq_of_forall_mem _ this
  simp [this]

Result:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯
⊢ ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯
this : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
⊢ (trace R M) (φ x ∘ₗ φ y) = (trace R ↥N) ((φ x ∘ₗ φ y).restrict hy')

Tactic:
have : (trace R { x // x ∈ N }) ((φ x ∘ₗ φ y).restrict _) = (trace R M) (φ x ∘ₗ φ y) :=
  (φ x ∘ₗ φ y).trace_restrict_eq_of_forall_mem _ this

Result:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯
this✝ : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
this : (trace R ↥N) ((φ x ∘ₗ φ y).restrict ⋯) = (trace R M) (φ x ∘ₗ φ y)
⊢ (trace R M) (φ x ∘ₗ φ y) = (trace R ↥N) ((φ x ∘ₗ φ y).restrict hy')

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯
⊢ ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N

Tactic:
exact fun m ↦ N.lie_mem (h hy m)

Result:
no goals