[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 0 ↔ ↑x = 0
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ ↑x = 1 ↔ x = 1
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 1 ↔ ↑x = 1
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1
[PROOFSTEP]
rw [mem_Icc] at *
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ 1 - ↑x
[PROOFSTEP]
simpa using x.2.2
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Icc 0 1)
⊢ 1 - ↑x ≤ 1
[PROOFSTEP]
simpa using x.2.1
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ioc 0 1)
⊢ ↑x = 1 ↔ x = 1
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ioc 0 1)
⊢ x = 1 ↔ ↑x = 1
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : t ∈ Ioo 0 1
⊢ 1 - t ∈ Ioo 0 1
[PROOFSTEP]
rw [mem_Ioo] at *
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 0 < 1 - t ∧ 1 - t < 1
[PROOFSTEP]
refine' ⟨sub_pos.2 ht.2, _⟩
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 1 - t < 1
[PROOFSTEP]
exact lt_of_le_of_ne ((sub_le_self_iff 1).2 ht.1.le) (mt sub_eq_self.mp ht.1.ne')
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < 1 - ↑x
[PROOFSTEP]
simpa using x.2.2
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Ioo 0 1)
⊢ 1 - ↑x < 1
[PROOFSTEP]
simpa using x.2.1
