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