α : Type ?u.62843
inst✝¹ : StrictOrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 0 < 1 - t ∧ 1 - t < 1
α : Type ?u.62843
inst✝¹ : StrictOrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : t ∈ Ioo 0 1
⊢ 1 - t ∈ Ioo 0 1
rw [mem_Ioo] at *
α : Type ?u.62843
inst✝¹ : StrictOrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 1 - t < 1
α : Type ?u.62843
inst✝¹ : StrictOrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 0 < 1 - t ∧ 1 - t < 1
refine' ⟨sub_pos.2 ht.2, _⟩
no goals
α : Type ?u.62843
inst✝¹ : StrictOrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 1 - t < 1
exact lt_of_le_of_ne ((sub_le_self_iff 1).2 ht.1.le) (mt sub_eq_self.mp ht.1.ne')