no goals
ι : Type u_5
R : Type u_1
S : Type ?u.248835
M : ι → Type ?u.248840
N : Type ?u.248843
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_2
β₁ : ι → Type u_3
β₂ : ι → Type u_4
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)
f : (i : ι) → β i ≃ₗ[R] β₁ i
f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i
⊢ ∀ (i : ι), ((fun i x => ↑(f₂ i) x) i ∘ (fun i x => ↑(f i) x) i) 0 = 0
simp