α✝ : Type u
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ x⁺ = x
α✝ : Type u
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x⁺
⊢ x⁺ = x
rw [m_pos_part_def, right_lt_sup, not_le] at hx
α✝ : Type u
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ 1 ≤ x
α✝ : Type u
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ x⁺ = x
rw [m_pos_part_def, sup_eq_left]
no goals
α✝ : Type u
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ 1 ≤ x
exact hx.le