[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (r_1 s : (i : I) → f i) (x : (i : I) → g i), (r_1 + s) • x = r_1 • x + s • x
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝ : (i : I) → g i
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
ext1
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝¹ : (i : I) → g i
x✝ : I
⊢ ((r✝ + s✝) • x✝¹) x✝ = (r✝ • x✝¹ + s✝ • x✝¹) x✝
[PROOFSTEP]
apply add_smul
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (x : (i : I) → g i), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝ : (i : I) → g i
⊢ 0 • x✝ = 0
[PROOFSTEP]
ext1
  -- Porting note: not sure why `apply zero_smul` fails here.
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ (0 • x✝¹) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
rw [zero_smul]
