[GOAL]
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)
[PROOFSTEP]
ext x
[GOAL]
case h
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
val✝ : I
⊢ star (Sum.elim x y) (Sum.inl val✝) = Sum.elim (star x) (star y) (Sum.inl val✝)
[PROOFSTEP]
simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]
[GOAL]
case h.inr
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
val✝ : J
⊢ star (Sum.elim x y) (Sum.inr val✝) = Sum.elim (star x) (star y) (Sum.inr val✝)
[PROOFSTEP]
simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]
