Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Jeremy Avigad, Leonardo de Moura
-/

import Mathlib.Init.Algebra.Order

universe u

section

variable {α: Type uα : Type u: Type (u+1)Type u} [LinearOrder: Type ?u.3811 → Type ?u.3811LinearOrder α: Type uα]

lemma min_def: ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def (a: αa b: αb : α: Type uα) : min: {α : Type ?u.17} → [self : Min α] → α → α → αmin a: αa b: αb = if a: αa ≤ b: αb then a: αa else b: αb := LinearOrder.min_def: ∀ {α : Type ?u.70} [self : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bLinearOrder.min_def ..

lemma min_le_left: ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_left (a: αa b: αb : α: Type uα) : min: {α : Type ?u.104} → [self : Min α] → α → α → αmin a: αa b: αb ≤ a: αa := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ aif h: ?m.188h : a: αa ≤ b: αb
α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ athenα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b ≤ a α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ asimp [min_def: ∀ {α : Type ?u.195} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def, if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.210} {t e : α}, (if c then t else e) = tif_pos h: ?m.181h, le_refl: ∀ {α : Type ?u.245} [inst : Preorder α] (a : α), a ≤ ale_refl]Goals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ aelseα: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bmin a b ≤ a α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ asimp [min_def: ∀ {α : Type ?u.497} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.508} {t e : α}, (if c then t else e) = eif_neg h: ?m.188h]α: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bb ≤ a;α: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bb ≤ a α: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bmin a b ≤ aexact le_of_not_le: ∀ {α : Type ?u.661} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → b ≤ ale_of_not_le h: ?m.188hGoals accomplished! 🐙

lemma min_le_right: ∀ (a b : α), min a b ≤ bmin_le_right (a: αa b: αb : α: Type uα) : min: {α : Type ?u.708} → [self : Min α] → α → α → αmin a: αa b: αb ≤ b: αb := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ bif h: ?m.792h : a: αa ≤ b: αb
α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ bthenα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b ≤ b α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ bsimp [min_def: ∀ {α : Type ?u.799} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def, if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.814} {t e : α}, (if c then t else e) = tif_pos h: ?m.785h]α: Type uinst✝: LinearOrder αa, b: αh: a ≤ ba ≤ b;α: Type uinst✝: LinearOrder αa, b: αh: a ≤ ba ≤ b α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b ≤ bexact h: ?m.785hGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ belseα: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bmin a b ≤ b α: Type uinst✝: LinearOrder αa, b: αmin a b ≤ bsimp [min_def: ∀ {α : Type ?u.1031} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1042} {t e : α}, (if c then t else e) = eif_neg h: ?m.792h, le_refl: ∀ {α : Type ?u.1069} [inst : Preorder α] (a : α), a ≤ ale_refl]Goals accomplished! 🐙

lemma le_min: ∀ {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_min {a: αa b: αb c: αc : α: Type uα} (h₁: c ≤ ah₁ : c: αc ≤ a: αa) (h₂: c ≤ bh₂ : c: αc ≤ b: αb) : c: αc ≤ min: {α : Type ?u.1309} → [self : Min α] → α → α → αmin a: αa b: αb := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bc ≤ min a bif h: ?m.1380h : a: αa ≤ b: αb
α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bc ≤ min a bthenα: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: a ≤ bc ≤ min a b α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bc ≤ min a bsimp [min_def: ∀ {α : Type ?u.1387} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def, if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1402} {t e : α}, (if c then t else e) = tif_pos h: ?m.1373h]α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: a ≤ bc ≤ a;α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: a ≤ bc ≤ a α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: a ≤ bc ≤ min a bexact h₁: c ≤ ah₁Goals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bc ≤ min a belseα: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: ¬a ≤ bc ≤ min a b α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bc ≤ min a bsimp [min_def: ∀ {α : Type ?u.1617} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1628} {t e : α}, (if c then t else e) = eif_neg h: ?m.1380h]α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: ¬a ≤ bc ≤ b;α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: ¬a ≤ bc ≤ b α: Type uinst✝: LinearOrder αa, b, c: αh₁: c ≤ ah₂: c ≤ bh: ¬a ≤ bc ≤ min a bexact h₂: c ≤ bh₂Goals accomplished! 🐙

lemma max_def: ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def (a: αa b: αb : α: Type uα) : max: {α : Type ?u.1812} → [self : Max α] → α → α → αmax a: αa b: αb = if a: αa ≤ b: αb then b: αb else a: αa := LinearOrder.max_def: ∀ {α : Type ?u.1865} [self : LinearOrder α] (a b : α), max a b = if a ≤ b then b else aLinearOrder.max_def ..

lemma le_max_left: ∀ (a b : α), a ≤ max a ble_max_left (a: αa b: αb : α: Type uα) : a: αa ≤ max: {α : Type ?u.1899} → [self : Max α] → α → α → αmax a: αa b: αb := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αa ≤ max a bif h: ?m.1976h : a: αa ≤ b: αb
α: Type uinst✝: LinearOrder αa, b: αa ≤ max a bthenα: Type uinst✝: LinearOrder αa, b: αh: a ≤ ba ≤ max a b α: Type uinst✝: LinearOrder αa, b: αa ≤ max a bsimp [max_def: ∀ {α : Type ?u.1990} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def, if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.2005} {t e : α}, (if c then t else e) = tif_pos h: ?m.1976h]α: Type uinst✝: LinearOrder αa, b: αh: a ≤ ba ≤ b;α: Type uinst✝: LinearOrder αa, b: αh: a ≤ ba ≤ b α: Type uinst✝: LinearOrder αa, b: αh: a ≤ ba ≤ max a bexact h: ?m.1976hGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αa ≤ max a belseα: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ ba ≤ max a b α: Type uinst✝: LinearOrder αa, b: αa ≤ max a bsimp [max_def: ∀ {α : Type ?u.2220} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.2231} {t e : α}, (if c then t else e) = eif_neg h: ?m.1983h, le_refl: ∀ {α : Type ?u.2258} [inst : Preorder α] (a : α), a ≤ ale_refl]Goals accomplished! 🐙

lemma le_max_right: ∀ {α : Type u} [inst : LinearOrder α] (a b : α), b ≤ max a ble_max_right (a: αa b: αb : α: Type uα) : b: αb ≤ max: {α : Type ?u.2465} → [self : Max α] → α → α → αmax a: αa b: αb := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αb ≤ max a bif h: ?m.2549h : a: αa ≤ b: αb
α: Type uinst✝: LinearOrder αa, b: αb ≤ max a bthenα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bb ≤ max a b α: Type uinst✝: LinearOrder αa, b: αb ≤ max a bsimp [max_def: ∀ {α : Type ?u.2556} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def, if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.2571} {t e : α}, (if c then t else e) = tif_pos h: ?m.2542h, le_refl: ∀ {α : Type ?u.2606} [inst : Preorder α] (a : α), a ≤ ale_refl]Goals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b: αb ≤ max a belseα: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bb ≤ max a b α: Type uinst✝: LinearOrder αa, b: αb ≤ max a bsimp [max_def: ∀ {α : Type ?u.2839} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.2850} {t e : α}, (if c then t else e) = eif_neg h: ?m.2549h]α: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bb ≤ a;α: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bb ≤ a α: Type uinst✝: LinearOrder αa, b: αh: ¬a ≤ bb ≤ max a bexact le_of_not_le: ∀ {α : Type ?u.2998} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → b ≤ ale_of_not_le h: ?m.2549hGoals accomplished! 🐙

lemma max_le: ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ cmax_le {a: αa b: αb c: αc : α: Type uα} (h₁: a ≤ ch₁ : a: αa ≤ c: αc) (h₂: b ≤ ch₂ : b: αb ≤ c: αc) : max: {α : Type ?u.3074} → [self : Max α] → α → α → αmax a: αa b: αb ≤ c: αc := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ cmax a b ≤ cif h: ?m.3145h : a: αa ≤ b: αb
α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ cmax a b ≤ cthenα: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: a ≤ bmax a b ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ cmax a b ≤ csimp [max_def: ∀ {α : Type ?u.3152} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def, if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.3167} {t e : α}, (if c then t else e) = tif_pos h: ?m.3138h]α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: a ≤ bb ≤ c;α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: a ≤ bb ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: a ≤ bmax a b ≤ cexact h₂: b ≤ ch₂Goals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ cmax a b ≤ celseα: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: ¬a ≤ bmax a b ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ cmax a b ≤ csimp [max_def: ∀ {α : Type ?u.3384} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.3395} {t e : α}, (if c then t else e) = eif_neg h: ?m.3145h]α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: ¬a ≤ ba ≤ c;α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: ¬a ≤ ba ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₁: a ≤ ch₂: b ≤ ch: ¬a ≤ bmax a b ≤ cexact h₁: a ≤ ch₁Goals accomplished! 🐙

lemma eq_min: ∀ {a b c : α}, c ≤ a → c ≤ b → (∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) → c = min a beq_min {a: αa b: αb c: αc : α: Type uα} (h₁: c ≤ ah₁ : c: αc ≤ a: αa) (h₂: c ≤ bh₂ : c: αc ≤ b: αb) (h₃: ∀ {d : α}, d ≤ a → d ≤ b → d ≤ ch₃ : ∀{d: ?m.3612d}, d: ?m.3612d ≤ a: αa → d: ?m.3612d ≤ b: αb → d: ?m.3612d ≤ c: αc) :
c: αc = min: {α : Type ?u.3634} → [self : Min α] → α → α → αmin a: αa b: αb :=
le_antisymm: ∀ {α : Type ?u.3654} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm (le_min: ∀ {α : Type ?u.3668} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_min h₁: c ≤ ah₁ h₂: c ≤ bh₂) (h₃: ∀ {d : α}, d ≤ a → d ≤ b → d ≤ ch₃ (min_le_left: ∀ {α : Type ?u.3696} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_left a: αa b: αb) (min_le_right: ∀ {α : Type ?u.3699} [inst : LinearOrder α] (a b : α), min a b ≤ bmin_le_right a: αa b: αb))

lemma min_comm: ∀ (a b : α), min a b = min b amin_comm (a: αa b: αb : α: Type uα) : min: {α : Type ?u.3727} → [self : Min α] → α → α → αmin a: αa b: αb = min: {α : Type ?u.3739} → [self : Min α] → α → α → αmin b: αb a: αa :=
eq_min: ∀ {α : Type ?u.3746} [inst : LinearOrder α] {a b c : α},
c ≤ a → c ≤ b → (∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) → c = min a beq_min (min_le_right: ∀ {α : Type ?u.3762} [inst : LinearOrder α] (a b : α), min a b ≤ bmin_le_right a: αa b: αb) (min_le_left: ∀ {α : Type ?u.3765} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_left a: αa b: αb) (λ {_: ?m.3769_} h₁: ?m.3772h₁ h₂: ?m.3775h₂ => le_min: ∀ {α : Type ?u.3777} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_min h₂: ?m.3775h₂ h₁: ?m.3772h₁)

lemma min_assoc: ∀ (a b c : α), min (min a b) c = min a (min b c)min_assoc (a: αa b: αb c: αc : α: Type uα) : min: {α : Type ?u.3821} → [self : Min α] → α → α → αmin (min: {α : Type ?u.3824} → [self : Min α] → α → α → αmin a: αa b: αb) c: αc = min: {α : Type ?u.3839} → [self : Min α] → α → α → αmin a: αa (min: {α : Type ?u.3842} → [self : Min α] → α → α → αmin b: αb c: αc) :=
byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b, c: αmin (min a b) c = min a (min b c)apply eq_min: ∀ {α : Type ?u.3855} [inst : LinearOrder α] {a b c : α},
c ≤ a → c ≤ b → (∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) → c = min a beq_minα: Type uinst✝: LinearOrder αa, b, c: αh₁min (min a b) c ≤ aα: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b cα: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) c
α: Type uinst✝: LinearOrder αa, b, c: αmin (min a b) c = min a (min b c).α: Type uinst✝: LinearOrder αa, b, c: αh₁min (min a b) c ≤ a α: Type uinst✝: LinearOrder αa, b, c: αh₁min (min a b) c ≤ aα: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b cα: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply le_trans: ∀ {α : Type ?u.3883} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_transα: Type uinst✝: LinearOrder αa, b, c: αh₁.amin (min a b) c ≤ ?h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₁.a?h₁.b ≤ aα: Type uinst✝: LinearOrder αa, b, c: αh₁.bα;α: Type uinst✝: LinearOrder αa, b, c: αh₁.amin (min a b) c ≤ ?h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₁.a?h₁.b ≤ aα: Type uinst✝: LinearOrder αa, b, c: αh₁.bα α: Type uinst✝: LinearOrder αa, b, c: αh₁min (min a b) c ≤ aapply min_le_left: ∀ {α : Type ?u.3912} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_leftα: Type uinst✝: LinearOrder αa, b, c: αh₁.amin a b ≤ a;α: Type uinst✝: LinearOrder αa, b, c: αh₁.amin a b ≤ a α: Type uinst✝: LinearOrder αa, b, c: αh₁min (min a b) c ≤ aapply min_le_left: ∀ {α : Type ?u.3931} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_leftGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αmin (min a b) c = min a (min b c).α: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b c α: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b cα: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply le_min: ∀ {α : Type ?u.3950} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_minα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁min (min a b) c ≤ bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁min (min a b) c ≤ bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b capply le_trans: ∀ {α : Type ?u.3975} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_transα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.amin (min a b) c ≤ ?h₂.h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.a?h₂.h₁.b ≤ bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.bαα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.amin (min a b) c ≤ ?h₂.h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.a?h₂.h₁.b ≤ bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.bαα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b capply min_le_left: ∀ {α : Type ?u.3994} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_leftα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.amin a b ≤ bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.amin a b ≤ bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b capply min_le_right: ∀ {α : Type ?u.4013} [inst : LinearOrder α] (a b : α), min a b ≤ bmin_le_rightα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂min (min a b) c ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₂min (min a b) c ≤ min b capply min_le_right: ∀ {α : Type ?u.4032} [inst : LinearOrder α] (a b : α), min a b ≤ bmin_le_rightGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αmin (min a b) c = min a (min b c).α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) cintros d: ?αd h₁: d ≤ ?ah₁ h₂: d ≤ ?bh₂α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃d ≤ min (min a b) c;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃d ≤ min (min a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply le_min: ∀ {α : Type ?u.4056} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_minα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₁d ≤ min a bα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₁d ≤ min a bα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply le_min: ∀ {α : Type ?u.4081} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_min h₁: d ≤ ?ah₁α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₁d ≤ bα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₁d ≤ bα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply le_trans: ∀ {α : Type ?u.4098} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_trans h₂: d ≤ ?bh₂α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₁min b c ≤ bα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₁min b c ≤ bα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply min_le_left: ∀ {α : Type ?u.4111} [inst : LinearOrder α] (a b : α), min a b ≤ amin_le_leftα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂d ≤ c
α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply le_trans: ∀ {α : Type ?u.4130} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_trans h₂: d ≤ ?bh₂α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂min b c ≤ c;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: d ≤ ah₂: d ≤ min b ch₃.h₂min b c ≤ c α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) capply min_le_right: ∀ {α : Type ?u.4143} [inst : LinearOrder α] (a b : α), min a b ≤ bmin_le_rightGoals accomplished! 🐙

lemma min_left_comm: ∀ {α : Type u} [inst : LinearOrder α], LeftCommutative minmin_left_comm : @LeftCommutative: {α : Type ?u.4177} → {β : Type ?u.4176} → (α → β → β) → PropLeftCommutative α: Type uα α: Type uα min: {α : Type ?u.4178} → [self : Min α] → α → α → αmin :=
left_comm: ∀ {α : Type ?u.4200} (f : α → α → α), Commutative f → Associative f → LeftCommutative fleft_comm min: {α : Type ?u.4202} → [self : Min α] → α → α → αmin (@min_comm: ∀ {α : Type ?u.4226} [inst : LinearOrder α] (a b : α), min a b = min b amin_comm α: Type uα _) (@min_assoc: ∀ {α : Type ?u.4229} [inst : LinearOrder α] (a b c : α), min (min a b) c = min a (min b c)min_assoc α: Type uα _)

@[simp]
lemma min_self: ∀ {α : Type u} [inst : LinearOrder α] (a : α), min a a = amin_self (a: αa : α: Type uα) : min: {α : Type ?u.4245} → [self : Min α] → α → α → αmin a: αa a: αa = a: αa := byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa: αmin a a = asimp [min_def: ∀ {α : Type ?u.4262} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_def]Goals accomplished! 🐙

lemma min_eq_left: ∀ {a b : α}, a ≤ b → min a b = amin_eq_left {a: αa b: αb : α: Type uα} (h: a ≤ bh : a: αa ≤ b: αb) : min: {α : Type ?u.4505} → [self : Min α] → α → α → αmin a: αa b: αb = a: αa :=
byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b = aapply Eq.symm: ∀ {α : Sort ?u.4521} {a b : α}, a = b → b = aEq.symmα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bha = min a b;α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bha = min a b α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b = aapply eq_min: ∀ {α : Type ?u.4533} [inst : LinearOrder α] {a b c : α},
c ≤ a → c ≤ b → (∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) → c = min a beq_min (le_refl: ∀ {α : Type ?u.4539} [inst : Preorder α] (a : α), a ≤ ale_refl _: ?m.4540_) h: a ≤ bhα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bh∀ {d : α}, d ≤ a → d ≤ b → d ≤ a;α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bh∀ {d : α}, d ≤ a → d ≤ b → d ≤ a α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b = aintrosα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bd✝: αa✝¹: d✝ ≤ aa✝: d✝ ≤ bhd✝ ≤ a;α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bd✝: αa✝¹: d✝ ≤ aa✝: d✝ ≤ bhd✝ ≤ a α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmin a b = aassumptionGoals accomplished! 🐙

lemma min_eq_right: ∀ {a b : α}, b ≤ a → min a b = bmin_eq_right {a: αa b: αb : α: Type uα} (h: b ≤ ah : b: αb ≤ a: αa) : min: {α : Type ?u.4651} → [self : Min α] → α → α → αmin a: αa b: αb = b: αb :=
byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amin a b = brw [α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amin a b = bmin_comm: ∀ {α : Type ?u.4667} [inst : LinearOrder α] (a b : α), min a b = min b amin_commα: Type uinst✝: LinearOrder αa, b: αh: b ≤ amin b a = b]α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amin b a = b
α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amin a b = bexact min_eq_left: ∀ {α : Type ?u.4689} [inst : LinearOrder α] {a b : α}, a ≤ b → min a b = amin_eq_left h: b ≤ ahGoals accomplished! 🐙

lemma eq_max: ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → (∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) → c = max a beq_max {a: αa b: αb c: αc : α: Type uα} (h₁: a ≤ ch₁ : a: αa ≤ c: αc) (h₂: b ≤ ch₂ : b: αb ≤ c: αc) (h₃: ∀ {d : α}, a ≤ d → b ≤ d → c ≤ dh₃ : ∀{d: ?m.4751d}, a: αa ≤ d: ?m.4751d → b: αb ≤ d: ?m.4751d → c: αc ≤ d: ?m.4751d) :
c: αc = max: {α : Type ?u.4773} → [self : Max α] → α → α → αmax a: αa b: αb :=
le_antisymm: ∀ {α : Type ?u.4793} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm (h₃: ∀ {d : α}, a ≤ d → b ≤ d → c ≤ dh₃ (le_max_left: ∀ {α : Type ?u.4816} [inst : LinearOrder α] (a b : α), a ≤ max a ble_max_left a: αa b: αb) (le_max_right: ∀ {α : Type ?u.4820} [inst : LinearOrder α] (a b : α), b ≤ max a ble_max_right a: αa b: αb)) (max_le: ∀ {α : Type ?u.4823} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ cmax_le h₁: a ≤ ch₁ h₂: b ≤ ch₂)

lemma max_comm: ∀ (a b : α), max a b = max b amax_comm (a: αa b: αb : α: Type uα) : max: {α : Type ?u.4866} → [self : Max α] → α → α → αmax a: αa b: αb = max: {α : Type ?u.4878} → [self : Max α] → α → α → αmax b: αb a: αa :=
eq_max: ∀ {α : Type ?u.4885} [inst : LinearOrder α] {a b c : α},
a ≤ c → b ≤ c → (∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) → c = max a beq_max (le_max_right: ∀ {α : Type ?u.4901} [inst : LinearOrder α] (a b : α), b ≤ max a ble_max_right a: αa b: αb) (le_max_left: ∀ {α : Type ?u.4904} [inst : LinearOrder α] (a b : α), a ≤ max a ble_max_left a: αa b: αb) (λ {_: ?m.4908_} h₁: ?m.4911h₁ h₂: ?m.4914h₂ => max_le: ∀ {α : Type ?u.4916} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ cmax_le h₂: ?m.4914h₂ h₁: ?m.4911h₁)

lemma max_assoc: ∀ (a b c : α), max (max a b) c = max a (max b c)max_assoc (a: αa b: αb c: αc : α: Type uα) : max: {α : Type ?u.4960} → [self : Max α] → α → α → αmax (max: {α : Type ?u.4963} → [self : Max α] → α → α → αmax a: αa b: αb) c: αc = max: {α : Type ?u.4978} → [self : Max α] → α → α → αmax a: αa (max: {α : Type ?u.4981} → [self : Max α] → α → α → αmax b: αb c: αc) := byGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αmax (max a b) c = max a (max b c)apply eq_max: ∀ {α : Type ?u.4994} [inst : LinearOrder α] {a b c : α},
a ≤ c → b ≤ c → (∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) → c = max a beq_maxα: Type uinst✝: LinearOrder αa, b, c: αh₁a ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ d
α: Type uinst✝: LinearOrder αa, b, c: αmax (max a b) c = max a (max b c)·α: Type uinst✝: LinearOrder αa, b, c: αh₁a ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₁a ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dapply le_trans: ∀ {α : Type ?u.5022} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_transα: Type uinst✝: LinearOrder αa, b, c: αh₁.aa ≤ ?h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₁.a?h₁.b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₁.bα;α: Type uinst✝: LinearOrder αa, b, c: αh₁.aa ≤ ?h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₁.a?h₁.b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₁.bα α: Type uinst✝: LinearOrder αa, b, c: αh₁a ≤ max (max a b) capply le_max_left: ∀ {α : Type ?u.5051} [inst : LinearOrder α] (a b : α), a ≤ max a ble_max_left a: αa b: αbα: Type uinst✝: LinearOrder αa, b, c: αh₁.amax a b ≤ max (max a b) c;α: Type uinst✝: LinearOrder αa, b, c: αh₁.amax a b ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₁a ≤ max (max a b) capply le_max_left: ∀ {α : Type ?u.5058} [inst : LinearOrder α] (a b : α), a ≤ max a ble_max_leftGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αmax (max a b) c = max a (max b c)·α: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dapply max_le: ∀ {α : Type ?u.5077} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ cmax_leα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) capply le_trans: ∀ {α : Type ?u.5102} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_transα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.ab ≤ ?h₂.h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.a?h₂.h₁.b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.bαα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.ab ≤ ?h₂.h₁.bα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.a?h₂.h₁.b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.bαα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) capply le_max_right: ∀ {α : Type ?u.5121} [inst : LinearOrder α] (a b : α), b ≤ max a ble_max_right a: αa b: αbα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.amax a b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₁.amax a b ≤ max (max a b) cα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) capply le_max_left: ∀ {α : Type ?u.5124} [inst : LinearOrder α] (a b : α), a ≤ max a ble_max_leftα: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c;α: Type uinst✝: LinearOrder αa, b, c: αh₂.h₂c ≤ max (max a b) c α: Type uinst✝: LinearOrder αa, b, c: αh₂max b c ≤ max (max a b) capply le_max_right: ∀ {α : Type ?u.5143} [inst : LinearOrder α] (a b : α), b ≤ max a ble_max_rightGoals accomplished! 🐙
α: Type uinst✝: LinearOrder αa, b, c: αmax (max a b) c = max a (max b c)·α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ d α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dintros d: ?αd h₁: ?a ≤ dh₁ h₂: ?b ≤ dh₂α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃max (max a b) c ≤ d;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃max (max a b) c ≤ d α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dapply max_le: ∀ {α : Type ?u.5167} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ cmax_leα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₁max a b ≤ dα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₂c ≤ d;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₁max a b ≤ dα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₂c ≤ d α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dapply max_le: ∀ {α : Type ?u.5192} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ cmax_le h₁: ?a ≤ dh₁α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₁b ≤ dα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₂c ≤ d;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₁b ≤ dα: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₂c ≤ d α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dapply le_trans: ∀ {α : Type ?u.5205} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_trans (le_max_left: ∀ {α : Type ?u.5211} [inst : LinearOrder α] (a b : α), a ≤ max a ble_max_left _: ?m.5212_ _: ?m.5212_) h₂: ?b ≤ dh₂α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₂c ≤ d;α: Type uinst✝: LinearOrder αa, b, c, d: αh₁: a ≤ dh₂: max b c ≤ dh₃.h₂c ≤ d
α: Type uinst✝: LinearOrder αa, b, c: αh₃∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ dapply le_trans: ∀ {α : Type ?u.5249} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_trans (le_max_right: ∀ {α : Type ?u.5255} [inst : LinearOrder α] (a b : α), b ≤ max a ble_max_right _: ?m.5256_ _: ?m.5256_) h₂: ?b ≤ dh₂Goals accomplished! 🐙

lemma max_left_comm: ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max a (max b c) = max b (max a c)max_left_comm : ∀ (a: αa b: αb c: αc : α: Type uα), max: {α : Type ?u.5315} → [self : Max α] → α → α → αmax a: αa (max: {α : Type ?u.5318} → [self : Max α] → α → α → αmax b: αb c: αc) = max: {α : Type ?u.5333} → [self : Max α] → α → α → αmax b: αb (max: {α : Type ?u.5336} → [self : Max α] → α → α → αmax a: αa c: αc) :=
left_comm: ∀ {α : Type ?u.5344} (f : α → α → α), Commutative f → Associative f → LeftCommutative fleft_comm max: {α : Type ?u.5346} → [self : Max α] → α → α → αmax (@max_comm: ∀ {α : Type ?u.5373} [inst : LinearOrder α] (a b : α), max a b = max b amax_comm α: Type uα _) (@max_assoc: ∀ {α : Type ?u.5376} [inst : LinearOrder α] (a b c : α), max (max a b) c = max a (max b c)max_assoc α: Type uα _)

@[simp] lemma max_self: ∀ {α : Type u} [inst : LinearOrder α] (a : α), max a a = amax_self (a: αa : α: Type uα) : max: {α : Type ?u.5392} → [self : Max α] → α → α → αmax a: αa a: αa = a: αa := byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa: αmax a a = asimp [max_def: ∀ {α : Type ?u.5409} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_def]Goals accomplished! 🐙

lemma max_eq_left: ∀ {a b : α}, b ≤ a → max a b = amax_eq_left {a: αa b: αb : α: Type uα} (h: b ≤ ah : b: αb ≤ a: αa) : max: {α : Type ?u.5652} → [self : Max α] → α → α → αmax a: αa b: αb = a: αa :=
byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amax a b = aapply Eq.symm: ∀ {α : Sort ?u.5668} {a b : α}, a = b → b = aEq.symmα: Type uinst✝: LinearOrder αa, b: αh: b ≤ aha = max a b;α: Type uinst✝: LinearOrder αa, b: αh: b ≤ aha = max a b α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amax a b = aapply eq_max: ∀ {α : Type ?u.5680} [inst : LinearOrder α] {a b c : α},
a ≤ c → b ≤ c → (∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) → c = max a beq_max (le_refl: ∀ {α : Type ?u.5686} [inst : Preorder α] (a : α), a ≤ ale_refl _: ?m.5687_) h: b ≤ ahα: Type uinst✝: LinearOrder αa, b: αh: b ≤ ah∀ {d : α}, a ≤ d → b ≤ d → a ≤ d;α: Type uinst✝: LinearOrder αa, b: αh: b ≤ ah∀ {d : α}, a ≤ d → b ≤ d → a ≤ d α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amax a b = aintrosα: Type uinst✝: LinearOrder αa, b: αh: b ≤ ad✝: αa✝¹: a ≤ d✝a✝: b ≤ d✝ha ≤ d✝;α: Type uinst✝: LinearOrder αa, b: αh: b ≤ ad✝: αa✝¹: a ≤ d✝a✝: b ≤ d✝ha ≤ d✝ α: Type uinst✝: LinearOrder αa, b: αh: b ≤ amax a b = aassumptionGoals accomplished! 🐙

lemma max_eq_right: ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = bmax_eq_right {a: αa b: αb : α: Type uα} (h: a ≤ bh : a: αa ≤ b: αb) : max: {α : Type ?u.5798} → [self : Max α] → α → α → αmax a: αa b: αb = b: αb :=
byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmax a b = brw [α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmax a b = b←max_comm: ∀ {α : Type ?u.5814} [inst : LinearOrder α] (a b : α), max a b = max b amax_comm b: αb a: αaα: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmax b a = b]α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmax b a = b;α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmax b a = b α: Type uinst✝: LinearOrder αa, b: αh: a ≤ bmax a b = bexact max_eq_left: ∀ {α : Type ?u.5825} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = amax_eq_left h: a ≤ bhGoals accomplished! 🐙

/- these rely on lt_of_lt -/

lemma min_eq_left_of_lt: ∀ {a b : α}, a < b → min a b = amin_eq_left_of_lt {a: αa b: αb : α: Type uα} (h: a < bh : a: αa < b: αb) : min: {α : Type ?u.5880} → [self : Min α] → α → α → αmin a: αa b: αb = a: αa :=
min_eq_left: ∀ {α : Type ?u.5894} [inst : LinearOrder α] {a b : α}, a ≤ b → min a b = amin_eq_left (le_of_lt: ∀ {α : Type ?u.5909} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt h: a < bh)

lemma min_eq_right_of_lt: ∀ {a b : α}, b < a → min a b = bmin_eq_right_of_lt {a: αa b: αb : α: Type uα} (h: b < ah : b: αb < a: αa) : min: {α : Type ?u.5976} → [self : Min α] → α → α → αmin a: αa b: αb = b: αb :=
min_eq_right: ∀ {α : Type ?u.5990} [inst : LinearOrder α] {a b : α}, b ≤ a → min a b = bmin_eq_right (le_of_lt: ∀ {α : Type ?u.6005} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt h: b < ah)

lemma max_eq_left_of_lt: ∀ {a b : α}, b < a → max a b = amax_eq_left_of_lt {a: αa b: αb : α: Type uα} (h: b < ah : b: αb < a: αa) : max: {α : Type ?u.6072} → [self : Max α] → α → α → αmax a: αa b: αb = a: αa :=
max_eq_left: ∀ {α : Type ?u.6086} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = amax_eq_left (le_of_lt: ∀ {α : Type ?u.6101} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt h: b < ah)

lemma max_eq_right_of_lt: ∀ {a b : α}, a < b → max a b = bmax_eq_right_of_lt {a: αa b: αb : α: Type uα} (h: a < bh : a: αa < b: αb) : max: {α : Type ?u.6168} → [self : Max α] → α → α → αmax a: αa b: αb = b: αb :=
max_eq_right: ∀ {α : Type ?u.6182} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = bmax_eq_right (le_of_lt: ∀ {α : Type ?u.6197} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt h: a < bh)

/- these use the fact that it is a linear ordering -/

lemma lt_min: ∀ {a b c : α}, a < b → a < c → a < min b clt_min {a: αa b: αb c: αc : α: Type uα} (h₁: a < bh₁ : a: αa < b: αb) (h₂: a < ch₂ : a: αa < c: αc) : a: αa < min: {α : Type ?u.6271} → [self : Min α] → α → α → αmin b: αb c: αc :=
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → cOr.elim (le_or_gt: ∀ {α : Type ?u.6296} [inst : LinearOrder α] (a b : α), a ≤ b ∨ a > ble_or_gt b: αb c: αc)
(λ h: b ≤ ch : b: αb ≤ c: αc => byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b ≤ ca < min b crwa [α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b ≤ ca < min b cmin_eq_left: ∀ {α : Type ?u.6338} [inst : LinearOrder α] {a b : α}, a ≤ b → min a b = amin_eq_left h: b ≤ chα: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b ≤ ca < b]α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b ≤ ca < b)
(λ h: b > ch : b: αb > c: αc => byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b > ca < min b crwa [α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b > ca < min b cmin_eq_right_of_lt: ∀ {α : Type ?u.6356} [inst : LinearOrder α] {a b : α}, b < a → min a b = bmin_eq_right_of_lt h: b > chα: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b > ca < c]α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < bh₂: a < ch: b > ca < c)

lemma max_lt: ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < c → b < c → max a b < cmax_lt {a: αa b: αb c: αc : α: Type uα} (h₁: a < ch₁ : a: αa < c: αc) (h₂: b < ch₂ : b: αb < c: αc) : max: {α : Type ?u.6423} → [self : Max α] → α → α → αmax a: αa b: αb < c: αc :=
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → cOr.elim (le_or_gt: ∀ {α : Type ?u.6448} [inst : LinearOrder α] (a b : α), a ≤ b ∨ a > ble_or_gt a: αa b: αb)
(λ h: a ≤ bh : a: αa ≤ b: αb => byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a ≤ bmax a b < crwa [α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a ≤ bmax a b < cmax_eq_right: ∀ {α : Type ?u.6490} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = bmax_eq_right h: a ≤ bhα: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a ≤ bb < c]α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a ≤ bb < c)
(λ h: a > bh : a: αa > b: αb => byGoals accomplished! 🐙 α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a > bmax a b < crwa [α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a > bmax a b < cmax_eq_left_of_lt: ∀ {α : Type ?u.6506} [inst : LinearOrder α] {a b : α}, b < a → max a b = amax_eq_left_of_lt h: a > bhα: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a > ba < c]α: Type uinst✝: LinearOrder αa, b, c: αh₁: a < ch₂: b < ch: a > ba < c)

end
```