case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a✝¹ : ℕ →o α
x✝ a✝ : ℕ
⊢ x✝ ≤ a✝ → ¬↑a✝¹ x✝ < ↑a✝¹ a✝ ↔ x✝ ≤ a✝ → ↑a✝¹ x✝ = ↑a✝¹ a✝
α : Type u_1
inst✝ : PartialOrder α
⊢ (∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m
congr! 4
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
⊢ n ≤ m → ¬↑a n < ↑a m ↔ n ≤ m → ↑a n = ↑a m
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a✝¹ : ℕ →o α
x✝ a✝ : ℕ
⊢ x✝ ≤ a✝ → ¬↑a✝¹ x✝ < ↑a✝¹ a✝ ↔ x✝ ≤ a✝ → ↑a✝¹ x✝ = ↑a✝¹ a✝
rename_i a n m
no goals
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
⊢ n ≤ m → ¬↑a n < ↑a m ↔ n ≤ m → ↑a n = ↑a m
simp (config := {contextual := true}) [lt_iff_le_and_ne, fun h => a.mono h]