[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * (b✝ + c✝)) x✝ = (a✝ * b✝ + a✝ * c✝) x✝
[PROOFSTEP]
exact mul_add _ _ _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ ((a✝ + b✝) * c✝) x✝ = (a✝ * c✝ + b✝ * c✝) x✝
[PROOFSTEP]
exact add_mul _ _ _
