α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → indexOf m l ≤ indexOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a m : α
⊢ maximum l = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]
α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → indexOf m l ≤ indexOf a l
α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → indexOf m l ≤ indexOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]
α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a✝¹ m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ indexOf m l ≤ indexOf a l
α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → indexOf m l ≤ indexOf a l
intro _ h a hal hma
no goals
α : Type u_1
β : Type ?u.104435
inst✝ : LinearOrder α
l : List α
a✝¹ m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ indexOf m l ≤ indexOf a l
rw [_root_.le_antisymm hma (h a hal)]