case h
ι : Type u_4
R : Type u_3
S : Type ?u.109793
M : ι → Type ?u.109798
N : Type ?u.109801
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.109888
β₁ : ι → Type u_2
β₂ : ι → Type u_1
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 → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ ↑(mapRange f hf (r • g)) i✝ = ↑(r • mapRange f hf g) i✝
ι : Type u_4
R : Type u_3
S : Type ?u.109793
M : ι → Type ?u.109798
N : Type ?u.109801
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.109888
β₁ : ι → Type u_2
β₂ : ι → Type u_1
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 → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (r • g) = r • mapRange f hf g
ext
no goals
case h
ι : Type u_4
R : Type u_3
S : Type ?u.109793
M : ι → Type ?u.109798
N : Type ?u.109801
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.109888
β₁ : ι → Type u_2
β₂ : ι → Type u_1
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 → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ ↑(mapRange f hf (r • g)) i✝ = ↑(r • mapRange f hf g) i✝
simp only [mapRange_apply f, coe_smul, Pi.smul_apply, hf']