Theorem: ContinuousLinearMap.proj_comp_single (ForML/ContinuousLinearMap.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
⊢ comp (proj i) (single i) = id R (φ i)
Tactic:
ext
State after:
case h
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x✝ : φ i
⊢ (comp (proj i) (single i)) x✝ = (id R (φ i)) x✝

State before:
case h
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x✝ : φ i
⊢ (comp (proj i) (single i)) x✝ = (id R (φ i)) x✝
Tactic:
simp
State after:
no goals