α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ ↑x = 0 ↔ x = 0
symm
no goals
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0
exact Subtype.ext_iff