α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a : α
h : 1 ≤ a
⊢ a ⊔ 1 = a
α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a : α
h : 1 ≤ a
⊢ a⁺ = a
rw [m_pos_part_def]
no goals
α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a : α
h : 1 ≤ a
⊢ a ⊔ 1 = a
exact sup_of_le_left h