awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
⊢ (↑(minimum_of_length_pos h) : WithTop α) = l.minimum

Tactic:
WithTop.coe_untop _ _

Premises used: WithBot.some, WithBot, List.minimum, WithTop.coe_untop, List.minimum_of_length_pos, WithBot.unbot, List.argmin, OrderDual, List.maximum_of_length_pos
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : α
h : 0 < l.length
⊢ b ≤ maximum_of_length_pos h ↔ (↑b : WithBot α) ≤ l.maximum

Tactic:
WithBot.le_unbot_iff _

Premises used: WithBot.le_unbot_iff, List.maximum_of_length_pos
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : α
h : 0 < l.length
⊢ minimum_of_length_pos h ≤ b ↔ l.minimum ≤ (↑b : WithTop α)

Tactic:
WithTop.untop_le_iff _

Premises used: WithBot.some, WithBot, List.minimum, List.minimum_of_length_pos, WithBot.unbot, WithTop.untop_le_iff, List.argmin, OrderDual, List.maximum_of_length_pos
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
a : l.maximum = (↑(maximum_of_length_pos h) : WithBot α)
⊢ maximum_of_length_pos h ∈ l

Tactic:
apply maximum_mem

Premises used: List.maximum_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
⊢ l.maximum = (↑(maximum_of_length_pos h) : WithBot α)

Tactic:
simp only [coe_maximum_of_length_pos]

Premises used: List.coe_maximum_of_length_pos
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
⊢ minimum_of_length_pos h ∈ l

Tactic:
maximum_of_length_pos_mem (α := αᵒᵈ) h

Premises used: List.minimum_of_length_pos, List.maximum_of_length_pos_mem, OrderDual
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
simp : (↑a : WithBot α) ≤ l.maximum
⊢ a ≤ maximum_of_length_pos w

Tactic:
simp only [le_maximum_of_length_pos_iff]

Premises used: List.le_maximum_of_length_pos_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ (↑a : WithBot α) ≤ l.maximum

Tactic:
le_maximum_of_mem' h

Premises used: List.le_maximum_of_mem'
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ (↑a : WithBot α) ≤ l.maximum

Tactic:
exact le_maximum_of_mem' h

Premises used: List.le_maximum_of_mem'
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ minimum_of_length_pos w ≤ a

Tactic:
le_maximum_of_length_pos_of_mem (α := αᵒᵈ) h w

Premises used: List.le_maximum_of_length_pos_of_mem, List.minimum_of_length_pos
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w ∈ l
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w ≤ maximum_of_length_pos h

Tactic:
apply le_maximum_of_length_pos_of_mem

Premises used: List.le_maximum_of_length_pos_of_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w ∈ l

Tactic:
getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w ∈ l

Tactic:
exact getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ minimum_of_length_pos h ≤ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w

Tactic:
getElem_le_maximum_of_length_pos (α := αᵒᵈ) w

Premises used: List.minimum_of_length_pos, Nat.zero_lt_of_lt, OrderDual, List.getElem_le_maximum_of_length_pos
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
⊢ Eq.{u_1 + 1} (α := WithBot α) (maximum []) (maximum [])

Tactic:
grind [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
a_ih : l₁.maximum = l₂.maximum
⊢ (x :: l₁).maximum = (x :: l₂).maximum

Tactic:
grind [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
x y : α
l_1 : List α
⊢ (y :: x :: l_1).maximum = (x :: y :: l_1).maximum

Tactic:
grind [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
a_ih : l₁.maximum = l₂.maximum
a_ih_1 : l₂.maximum = l₃.maximum
⊢ l₁.maximum = l₃.maximum

Tactic:
grind [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithBot α) (maximum []) (maximum [])
cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.maximum = l₂.maximum → (x :: l₁).maximum = (x :: l₂).maximum
swap : ∀ (x y : α) (l : List α), (y :: x :: l).maximum = (x :: y :: l).maximum
trans :
  ∀ {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁.maximum = l₂.maximum → l₂.maximum = l₃.maximum → l₁.maximum = l₃.maximum
⊢ l.maximum = l'.maximum

Tactic:
induction h with grind [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
⊢ Eq.{u_1 + 1} (α := WithTop α) (minimum []) (minimum [])

Tactic:
grind [minimum_cons]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
a_ih : l₁.minimum = l₂.minimum
⊢ (x :: l₁).minimum = (x :: l₂).minimum

Tactic:
grind [minimum_cons]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
x y : α
l_1 : List α
⊢ (y :: x :: l_1).minimum = (x :: y :: l_1).minimum

Tactic:
grind [minimum_cons]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
a_ih : l₁.minimum = l₂.minimum
a_ih_1 : l₂.minimum = l₃.minimum
⊢ l₁.minimum = l₃.minimum

Tactic:
grind [minimum_cons]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithTop α) (minimum []) (minimum [])
cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.minimum = l₂.minimum → (x :: l₁).minimum = (x :: l₂).minimum
swap : ∀ (x y : α) (l : List α), (y :: x :: l).minimum = (x :: y :: l).minimum
trans :
  ∀ {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁.minimum = l₂.minimum → l₂.minimum = l₃.minimum → l₁.minimum = l₃.minimum
⊢ l.minimum = l'.minimum

Tactic:
induction h with grind [minimum_cons]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : 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]

Premises used: List.maximum_eq_bot, Iff.mp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : l.maximum = (↑y : WithBot α)
⊢ y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y

Tactic:
rw [List.maximum_eq_coe_iff] at hy

Premises used: List.maximum_eq_coe_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
coe : l.max?.getD d = y
⊢ l.max?.getD d = WithBot.unbotD d (↑y : WithBot α)

Tactic:
simp only [WithBot.unbotD_coe]

Premises used: WithBot.unbotD_coe
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
hz : l.max? = none
⊢ Option.getD none d = y

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

Premises used: List.max?_eq_none_iff, Iff.mp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
⊢ Std.Antisymm fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
-- Module: Mathlib.Data.List.MinMax
Goal:
α : 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
⊢ z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z

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

Premises used: List.max?_eq_some_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : 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
hz₁ : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
⊢ Std.Antisymm fun (x1 x2 : α) ↦ x1 ≤ x2

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

Premises used: List.max?_eq_some_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : 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
coe : z = y
⊢ (some z).getD d = y

Tactic:
rw [Option.getD_some]

Premises used: Option.getD_some
-- Module: Mathlib.Data.List.MinMax
Goal:
α : 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:
_root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Data.List.MinMax
Goal:
α : 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)

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
coe : ∀ (x : Option α) (hz : l.max? = x), x.getD d = y
⊢ l.max?.getD d = y

Tactic:
cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

Premises used: Option.some, Option.getD_some, List.max?, Option.none, List.max?_eq_some_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d : α
cases : ∀ (x : WithBot α) (hy : l.maximum = x), l.max?.getD d = WithBot.unbotD d x
⊢ l.max?.getD d = WithBot.unbotD d l.maximum

Tactic:
cases hy : l.maximum with
  | bot => simp [List.maximum_eq_bot.mp hy]
  | coe y =>
    rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

Premises used: List.maximum, Option.some, Option.getD_some, List.max?, Option.none, WithBot.unbotD_coe, List.maximum_eq_coe_iff, List.max?_eq_some_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d : α
⊢ l.min?.getD d = WithTop.untopD d l.minimum

Tactic:
getD_max?_eq_unbotD_maximum (α := αᵒᵈ) _ _

Premises used: List.getD_max?_eq_unbotD_maximum, List.min?, List.minimum, List.argmin, WithTop.untopD, OrderDual, WithTop.recTopCoe, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
h : Ne.{u_1 + 1} (α := List α) [] []
⊢ Eq.{u_1 + 1} (α := WithBot α) (↑(foldr max ⊥ []) : WithBot α) (maximum [])

Tactic:
contradiction
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h : hd :: tl ≠ []
cons : max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
⊢ (↑(foldr max ⊥ (hd :: tl)) : WithBot α) = (hd :: tl).maximum

Tactic:
rw [maximum_cons, foldr, WithBot.coe_max]

Premises used: List.maximum_cons, WithBot.coe_max, List.foldr
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h : hd :: tl ≠ []
pos : ∀ (h : tl = []), max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
neg : ∀ (h : ¬tl = []), max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
⊢ max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum

Tactic:
by_cases h : tl = []
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h_1 : hd :: tl ≠ []
h : tl = []
⊢ max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum

Tactic:
simp [h]
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h_1 : hd :: tl ≠ []
h : ¬tl = []
⊢ max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum

Tactic:
simp [IH h]
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
h : l ≠ []
nil :
  ∀ (h : Ne.{u_1 + 1} (α := List α) [] []), Eq.{u_1 + 1} (α := WithBot α) (↑(foldr max ⊥ []) : WithBot α) (maximum [])
cons :
  ∀ (hd : α) (tl : List α) (IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum) (h : hd :: tl ≠ []),
    (↑(foldr max ⊥ (hd :: tl)) : WithBot α) = (hd :: tl).maximum
⊢ (↑(foldr max ⊥ l) : WithBot α) = l.maximum

Tactic:
induction l with
  | nil => contradiction
  | cons hd tl IH =>
    rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]

Premises used: List.maximum_cons, List.cons, WithBot.coe_max, List.foldr, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a : α
h : ∀ (x : α), Membership.mem (γ := List α) [] x → x ≤ a
⊢ foldr max ⊥ [] ≤ a

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a y : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → x ≤ a), foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a

Tactic:
simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx

Premises used: List.mem_cons_of_mem, List.mem_cons_self
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → x ≤ a), foldr max ⊥ [] ≤ a
cons :
  ∀ (y : α) (l : List α) (IH : ∀ (h : ∀ (x : α), x ∈ l → x ≤ a), foldr max ⊥ l ≤ a) (h : ∀ (x : α), x ∈ y :: l → x ≤ a),
    foldr max ⊥ (y :: l) ≤ a
⊢ foldr max ⊥ l ≤ a

Tactic:
induction l with
  | nil => simp
  | cons y l IH => simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
hx : Membership.mem (γ := List α) [] x
⊢ a ≤ foldr max ⊥ []

Tactic:
absurd hx not_mem_nil

Premises used: absurd, List.not_mem_nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
hx : Membership.mem (γ := List α) [] x
⊢ a ≤ foldr max ⊥ []

Tactic:
exact absurd hx not_mem_nil

Premises used: absurd, List.not_mem_nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
hx : x ∈ y :: l
cons : a ≤ foldr max ⊥ (x :: l)
cons₁ : Mem x l → a ≤ foldr max ⊥ (y :: l)
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
obtain hl | hl := hx
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
cons : a ≤ max x (foldr max ⊥ l)
⊢ a ≤ foldr max ⊥ (x :: l)

Tactic:
simp only [foldr]

Premises used: List.foldr
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)

Tactic:
le_max_of_le_left h

Premises used: le_max_of_le_left
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)

Tactic:
exact le_max_of_le_left h

Premises used: le_max_of_le_left
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
h_1 : Mem x l
⊢ x ∈ l

Tactic:
assumption
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
h_1 : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
exact le_max_of_le_right (IH (by assumption))

Premises used: le_max_of_le_right
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
a x : α
hx : x ∈ l
h : a ≤ x
nil : ∀ (hx : Membership.mem (γ := List α) [] x), a ≤ foldr max ⊥ []
cons : ∀ (y : α) (l : List α) (IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l) (hx : x ∈ y :: l), a ≤ foldr max ⊥ (y :: l)
⊢ a ≤ foldr max ⊥ l

Tactic:
induction l with
  | nil => exact absurd hx not_mem_nil
  | cons y l IH =>
    obtain hl | hl := hx
    · simp only [foldr]
      exact le_max_of_le_left h
    · exact le_max_of_le_right (IH (by assumption))

Premises used: List.cons, absurd, le_max_of_le_left, List.foldr, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderTop α
l : List α
h : l ≠ []
⊢ (↑(foldr min ⊤ l) : WithTop α) = l.minimum

Tactic:
@foldr_max_of_ne_nil αᵒᵈ _ _ _ h

Premises used: List.foldr_max_of_ne_nil, List.minimum, WithTop.some, List.argmin, OrderDual, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderTop α
l : List α
a : α
h : ∀ (x : α), x ∈ l → a ≤ x
⊢ a ≤ foldr min ⊤ l

Tactic:
@max_le_of_forall_le αᵒᵈ _ _ _ _ h

Premises used: List.max_le_of_forall_le, OrderDual
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderTop α
l : List α
a x : α
hx : x ∈ l
h : x ≤ a
⊢ foldr min ⊤ l ≤ a

Tactic:
@le_max_of_le αᵒᵈ _ _ _ _ _ hx h

Premises used: List.le_max_of_le, OrderDual
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
hx : Membership.mem (γ := List α) [] x
⊢ a ≤ foldr max b []

Tactic:
absurd hx List.not_mem_nil

Premises used: absurd, List.not_mem_nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
hx : Membership.mem (γ := List α) [] x
⊢ a ≤ foldr max b []

Tactic:
exact absurd hx List.not_mem_nil

Premises used: absurd, List.not_mem_nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
cons : a ≤ max y (foldr max b l)
⊢ a ≤ foldr max b (y :: l)

Tactic:
simp only [List.foldr]

Premises used: List.foldr
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
cons : ∀ (hx : x ∈ x :: l), a ≤ max x (foldr max b l)
cons₁ : ∀ (hl : x ∈ l), a ≤ max y (foldr max b l)
⊢ a ≤ max y (foldr max b l)

Tactic:
obtain rfl | hl := mem_cons.mp hx

Premises used: Iff.mp, List.mem_cons, rfl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)

Tactic:
le_max_of_le_left h

Premises used: le_max_of_le_left
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)

Tactic:
exact le_max_of_le_left h

Premises used: le_max_of_le_left
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
le_max_of_le_right (IH hl)

Premises used: le_max_of_le_right
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
exact le_max_of_le_right (IH hl)

Premises used: le_max_of_le_right
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : a ≤ x
nil : ∀ (hx : Membership.mem (γ := List α) [] x), a ≤ foldr max b []
cons : ∀ (y : α) (l : List α) (IH : ∀ (hx : x ∈ l), a ≤ foldr max b l) (hx : x ∈ y :: l), a ≤ foldr max b (y :: l)
⊢ a ≤ foldr max b l

Tactic:
induction l with
  | nil => exact absurd hx List.not_mem_nil
  | cons y l IH =>
    simp only [List.foldr]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)

Premises used: List.cons, absurd, le_max_of_le_left, Iff.mp, List.mem_cons, List.foldr, rfl, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : x ≤ a
⊢ foldr min b l ≤ a

Tactic:
@le_max_of_le' αᵒᵈ _ _ _ _ _ hx h

Premises used: List.le_max_of_le', OrderDual
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (Array.toListAppend #[] [f a])

Tactic:
rfl
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
cons : go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (Array.push #[] hd))
rw rw₁ : tl ++ [a] = [] → False
⊢ go f (hd :: (tl ++ [a])) r = r.toListAppend (go f (hd :: (tl ++ [a])) #[])

Tactic:
rw [modifyLast.go, modifyLast.go]

Premises used: List.modifyLast.go
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Premises used: List.cons_ne_nil, Not, List.append_ne_nil_of_right_ne_nil, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Premises used: List.cons_ne_nil, List.append_ne_nil_of_right_ne_nil, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
cons :
  (r.push hd).toListAppend (go f (tl ++ [a]) #[]) =
    r.toListAppend ((Array.push #[] hd).toListAppend (go f (tl ++ [a]) #[]))
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (Array.push #[] hd))

Tactic:
rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]

Premises used: Array.push, List.toArray, List.nil