-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem le_min?_iff [Min α] [LE α]
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
    {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
  | nil => by simp
  | cons x xs => by
    rw [min?]
    intro eq y
    simp only [Option.some.injEq] at eq
    induction xs generalizing x with
    | nil =>
      simp at eq
      simp [eq]
    | cons z xs ih =>
      simp at eq
      simp [ih _ eq, le_min_iff, and_assoc]

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
eq : some (foldl min x xs) = some a
y : α
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b

Tactic:
simp only [Option.some.injEq] at eq

Result:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
y : α
eq : foldl min x xs = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
y z : α
xs : List α
ih : ∀ (x : α), foldl min x xs = a → (y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b)
x : α
eq : foldl min (min x z) xs = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: z :: xs → y ≤ b

Tactic:
simp [ih _ eq, le_min_iff, and_assoc]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
y : α
eq : foldl min x xs = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b

Tactic:
induction xs generalizing x with
| nil =>
  simp at eq
  simp [eq]
| cons z xs ih =>
  simp at eq
  simp [ih _ eq, le_min_iff, and_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
y x : α
eq : x = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ [x] → y ≤ b

Tactic:
simp [eq]

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
y x : α
eq : foldl min x [] = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ [x] → y ≤ b

Tactic:
simp at eq

Result:
case nil
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
y x : α
eq : x = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ [x] → y ≤ b

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
⊢ some (foldl min x xs) = some a → ∀ {x_1 : α}, x_1 ≤ a ↔ ∀ (b : α), b ∈ x :: xs → x_1 ≤ b

Tactic:
intro eq y

Result:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
eq : some (foldl min x xs) = some a
y : α
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
y z : α
xs : List α
ih : ∀ (x : α), foldl min x xs = a → (y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b)
x : α
eq : foldl min x (z :: xs) = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: z :: xs → y ≤ b

Tactic:
simp at eq

Result:
case cons
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
y z : α
xs : List α
ih : ∀ (x : α), foldl min x xs = a → (y ≤ a ↔ ∀ (b : α), b ∈ x :: xs → y ≤ b)
x : α
eq : foldl min (min x z) xs = a
⊢ y ≤ a ↔ ∀ (b : α), b ∈ x :: z :: xs → y ≤ b

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
⊢ (x :: xs).min? = some a → ∀ {x_1 : α}, x_1 ≤ a ↔ ∀ (b : α), b ∈ x :: xs → x_1 ≤ b

Tactic:
rw [min?]

Result:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
⊢ some (foldl min x xs) = some a → ∀ {x_1 : α}, x_1 ≤ a ↔ ∀ (b : α), b ∈ x :: xs → x_1 ≤ b

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
⊢ [].min? = some a → ∀ {x : α}, x ≤ a ↔ ∀ (b : α), b ∈ [] → x ≤ b

Tactic:
simp

Result:
no goals