-- Mathlib/Data/List/MinMax.lean
lemma getD_max?_eq_unbotD_maximum (l : List α) (d : α) : l.max?.getD d = l.maximum.unbotD d

Proof state:
case coe.some.max_le_iff
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a b c : α), b ⊔ c ≤ a ↔ b ≤ a ∧ c ≤ a

Tactic:
simp [le_total]

Result:
no goals

Proof state:
case bot
α : Type u_1
inst✝ : LinearOrder α
l : List α
d : α
hy : l.maximum = ⊥
⊢ l.max?.getD d = WithBot.unbotD d ⊥

Tactic:
simp [List.maximum_eq_bot.mp hy]

Result:
no goals

Proof state:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ (some z).getD d = y

Tactic:
rw [Option.getD_some]

Result:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ z = y

Proof state:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : l.maximum = ↑y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Tactic:
rw [List.maximum_eq_coe_iff] at hy

Result:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Proof state:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ (some z).getD d = y

Tactic:
rw [List.max?_eq_some_iff] at hz

Result:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ (some z).getD d = y

case coe.some.le_refl
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a : α), a ≤ a

case coe.some.max_eq_or
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b

case coe.some.max_le_iff
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a b c : α), b ⊔ c ≤ a ↔ b ≤ a ∧ c ≤ a

Proof state:
case coe.some.le_refl
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a : α), a ≤ a

case coe.some.max_eq_or
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b

case coe.some.max_le_iff
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ ∀ (a b c : α), b ⊔ c ≤ a ↔ b ≤ a ∧ c ≤ a

Tactic:
all_goals simp [le_total]

Result:
no goals

Proof state:
case coe.none
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
hz : l.max? = none
⊢ none.getD d = y

Tactic:
simp [List.max?_eq_none_iff.mp hz] at hy

Result:
no goals

Proof state:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 => x1 ≤ x2
⊢ z = y

Tactic:
exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

Result:
no goals

Proof state:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Tactic:
simp only [WithBot.unbotD_coe]

Result:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = y