case H
α : Type u_1
β : Type u_2
i : α ⊕ β
⊢ ↑(sumCongr (Equiv.refl α) (Equiv.refl β)) i = ↑(Equiv.refl (α ⊕ β)) i
α : Type u_1
β : Type u_2
⊢ sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)
ext i
no goals
case H
α : Type u_1
β : Type u_2
i : α ⊕ β
⊢ ↑(sumCongr (Equiv.refl α) (Equiv.refl β)) i = ↑(Equiv.refl (α ⊕ β)) i
cases i <;> rfl