-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
    {xs : List α} → xs.min? = some a → a ∈ xs

Proof state:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs : List α
⊢ xs.min? = some a → a ∈ xs

Tactic:
match xs with
| nil => simp
| x :: xs =>
  simp only [min?_cons', Option.some.injEq, List.mem_cons]
  intro eq
  induction xs generalizing x with
  | nil =>
    simp at eq
    simp [eq]
  | cons y xs ind =>
    simp at eq
    have p := ind _ eq
    cases p with
    | inl p =>
      cases min_eq_or x y with | _ q => simp [p, q]
    | inr p => simp [p, mem_cons]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
⊢ ∀ {xs : List α}, xs.min? = some a → a ∈ xs

Tactic:
intro xs

Result:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs : List α
⊢ xs.min? = some a → a ∈ xs

Proof state:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
x : α
xs : List α
eq : foldl min x xs = a
⊢ a = x ∨ a ∈ xs

Tactic:
induction xs generalizing x with
| nil =>
  simp at eq
  simp [eq]
| cons y xs ind =>
  simp at eq
  have p := ind _ eq
  cases p with
  | inl p =>
    cases min_eq_or x y with | _ q => simp [p, q]
  | inr p => simp [p, mem_cons]

Result:
no goals

Proof state:
case cons.inl.inr
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
p : a = min x y
q : min x y = y
⊢ a = x ∨ a ∈ y :: xs

Tactic:
simp [p, q]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min x (y :: xs) = a
⊢ a = x ∨ a ∈ y :: xs

Tactic:
simp at eq

Result:
case cons
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
⊢ a = x ∨ a ∈ y :: xs

Proof state:
case cons.inl
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
p : a = min x y
⊢ a = x ∨ a ∈ y :: xs

Tactic:
cases min_eq_or x y with | _ q => simp [p, q]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
x : α
xs : List α
⊢ foldl min x xs = a → a = x ∨ a ∈ xs

Tactic:
intro eq

Result:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
x : α
xs : List α
eq : foldl min x xs = a
⊢ a = x ∨ a ∈ xs

Proof state:
case nil
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs : List α
x : α
eq : x = a
⊢ a = x ∨ a ∈ []

Tactic:
simp [eq]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
p : a = min x y ∨ a ∈ xs
⊢ a = x ∨ a ∈ y :: xs

Tactic:
cases p with
| inl p =>
  cases min_eq_or x y with | _ q => simp [p, q]
| inr p => simp [p, mem_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs : List α
x : α
eq : foldl min x [] = a
⊢ a = x ∨ a ∈ []

Tactic:
simp at eq

Result:
case nil
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs : List α
x : α
eq : x = a
⊢ a = x ∨ a ∈ []

Proof state:
case cons.inr
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
p : a ∈ xs
⊢ a = x ∨ a ∈ y :: xs

Tactic:
simp [p, mem_cons]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs : List α
⊢ [].min? = some a → a ∈ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
⊢ a = x ∨ a ∈ y :: xs

Tactic:
have p := ind _ eq

Result:
case cons
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
y : α
xs : List α
ind : ∀ (x : α), foldl min x xs = a → a = x ∨ a ∈ xs
x : α
eq : foldl min (min x y) xs = a
p : a = min x y ∨ a ∈ xs
⊢ a = x ∨ a ∈ y :: xs

Proof state:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
x : α
xs : List α
⊢ (x :: xs).min? = some a → a ∈ x :: xs

Tactic:
simp only [min?_cons', Option.some.injEq, List.mem_cons]

Result:
α : Type u_1
a : α
inst✝ : Min α
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
xs✝ : List α
x : α
xs : List α
⊢ foldl min x xs = a → a = x ∨ a ∈ xs