case h.h.h
ι : Type u_1
R : Type u_3
S : Type ?u.140242
M : ι → Type ?u.140247
N : Type ?u.140250
dec_ι : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → Module R (M i)
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
β : ι → Type ?u.140337
β₁ : ι → Type ?u.140342
β₂ : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
i✝¹ : ι
x✝ : β₂ i✝¹
i✝ : ι
⊢ ↑(↑(LinearMap.comp (linearMap fun i => LinearMap.id) (lsingle i✝¹)) x✝) i✝ =
    ↑(↑(LinearMap.comp LinearMap.id (lsingle i✝¹)) x✝) i✝
ι : Type u_1
R : Type u_3
S : Type ?u.140242
M : ι → Type ?u.140247
N : Type ?u.140250
dec_ι : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → Module R (M i)
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
β : ι → Type ?u.140337
β₁ : ι → Type ?u.140342
β₂ : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
⊢ (linearMap fun i => LinearMap.id) = LinearMap.id
ext
no goals
case h.h.h
ι : Type u_1
R : Type u_3
S : Type ?u.140242
M : ι → Type ?u.140247
N : Type ?u.140250
dec_ι : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → Module R (M i)
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
β : ι → Type ?u.140337
β₁ : ι → Type ?u.140342
β₂ : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
i✝¹ : ι
x✝ : β₂ i✝¹
i✝ : ι
⊢ ↑(↑(LinearMap.comp (linearMap fun i => LinearMap.id) (lsingle i✝¹)) x✝) i✝ =
    ↑(↑(LinearMap.comp LinearMap.id (lsingle i✝¹)) x✝) i✝
simp [linearMap]