Theorem: Section20Sheet2Solutions.RepMap.id_comp (FormalisingMathematics2024/Solutions/Section20representationTheory/Sheet2.lean)

State before:
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
⊢ comp (id σ) φ = φ
Tactic:
ext
State after:
case toLinearMap.h
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
x✝ : V
⊢ (comp (id σ) φ).toLinearMap x✝ = φ.toLinearMap x✝

State before:
case toLinearMap.h
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
x✝ : V
⊢ (comp (id σ) φ).toLinearMap x✝ = φ.toLinearMap x✝
Tactic:
rfl
State after:
no goals