-- Mathlib/Algebra/Lie/TraceForm.lean
lemma traceForm_eq_of_le_idealizer :
    traceForm R I N = (traceForm R L M).restrict I

Proof state:
case H.mk.mk
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 : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ =
    (((traceForm R L M).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule) ⟨x, hx⟩) ⟨y, hy⟩

Tactic:
change _ = trace R M (φ x ∘ₗ φ y)

Result:
case H.mk.mk
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 : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R M) (φ x ∘ₗ φ y)

Proof state:
case H.mk.mk
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 : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R M) (φ x ∘ₗ φ y)

Tactic:
rw [N.trace_eq_trace_restrict_of_le_idealizer I h x hy]

Result:
case H.mk.mk
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 : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R ↥N) ((φ x ∘ₗ φ y).restrict ⋯)

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
⊢ traceForm R ↥I ↥N = (traceForm R L M).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule

Tactic:
ext ⟨x, hx⟩ ⟨y, hy⟩

Result:
case H.mk.mk
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 : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ =
    (((traceForm R L M).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule) ⟨x, hx⟩) ⟨y, hy⟩

Proof state:
case H.mk.mk
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 : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R ↥N) ((φ x ∘ₗ φ y).restrict ⋯)

Tactic:
rfl

Result:
no goals