⊢ Subtype.val '' range (IccExtend arcsin.proof_2 ↑(OrderIso.symm sinOrderIso)) = Icc (-(π / 2)) (π / 2)
⊢ range arcsin = Icc (-(π / 2)) (π / 2)
rw [arcsin, range_comp Subtype.val]
no goals
⊢ Subtype.val '' range (IccExtend arcsin.proof_2 ↑(OrderIso.symm sinOrderIso)) = Icc (-(π / 2)) (π / 2)
simp [Icc]