R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type ?u.2779
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (if i' = i then 1 else 0) = if i = i' then 1 else 0
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type ?u.2779
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ ↑(stdBasis R (fun _x => R) i) 1 i' = if i = i' then 1 else 0
rw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply]
case e_c
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type ?u.2779
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (i' = i) = (i = i')
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type ?u.2779
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (if i' = i then 1 else 0) = if i = i' then 1 else 0
congr 1
no goals
case e_c
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type ?u.2779
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (i' = i) = (i = i')
rw [eq_iff_iff, eq_comm]