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
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)
ext x
no goals
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
cases x <;> simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]