case h.h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ ↑(stdBasis R φ i) x j = ↑(pi (diag i)) x j
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
⊢ stdBasis R φ i = pi (diag i)
ext (x j)
case h.e'_2.h.e'_1
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = ↑id x
case h.h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ ↑(stdBasis R φ i) x j = ↑(pi (diag i)) x j
convert (update_apply (R := R) (φ := φ) (ι := ι) 0 x i j _).symm
no goals
case h.e'_2.h.e'_1
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = ↑id x
rfl