-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} :
    xs.nonzeroMinimum ≤ y ↔ xs.nonzeroMinimum = 0 ∨ ∃ x ∈ xs, x ≤ y ∧ x ≠ 0

Proof state:
xs : List Nat
y : Nat
h : xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0
x : Nat
m : x ∈ xs
le : x ≤ y
ne : x ≠ 0
⊢ xs.nonzeroMinimum ≤ y

Tactic:
exact Nat.le_trans (nonzeroMinimum_le m ne) le

Result:
no goals

Proof state:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
⊢ (∀ (x : Nat), x ∈ xs → x ≤ y → x = 0) → ∀ (x : Nat), x ∈ xs → x = 0

Tactic:
intro w

Result:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
w : ∀ (x : Nat), x ∈ xs → x ≤ y → x = 0
⊢ ∀ (x : Nat), x ∈ xs → x = 0

Proof state:
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
w : ∀ (x : Nat), x ∈ xs → x ≤ y → x = 0
p : ¬xs.nonzeroMinimum = 0
⊢ xs.nonzeroMinimum = 0

Tactic:
exact w _ (nonzeroMinimum_mem p) h

Result:
no goals

Proof state:
xs : List Nat
y : Nat
h✝ : xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0
h : xs.nonzeroMinimum = 0
⊢ xs.nonzeroMinimum ≤ y

Tactic:
simp [h]

Result:
no goals

Proof state:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
w : ∀ (x : Nat), x ∈ xs → x ≤ y → x = 0
⊢ xs.nonzeroMinimum = 0

Tactic:
if p : xs.nonzeroMinimum = 0 then
  exact p
else
  exact w _ (nonzeroMinimum_mem p) h

Result:
no goals

Proof state:
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
w : ∀ (x : Nat), x ∈ xs → x ≤ y → x = 0
p : xs.nonzeroMinimum = 0
⊢ xs.nonzeroMinimum = 0

Tactic:
exact p

Result:
no goals

Proof state:
case refine_2
xs : List Nat
y : Nat
h : xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0
⊢ xs.nonzeroMinimum ≤ y

Tactic:
match h with
| .inl h => simp [h]
| .inr ⟨x, m, le, ne⟩ => exact Nat.le_trans (nonzeroMinimum_le m ne) le

Result:
no goals

Proof state:
xs : List Nat
y : Nat
⊢ xs.nonzeroMinimum ≤ y ↔ xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
⊢ xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0

case refine_2
xs : List Nat
y : Nat
h : xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0
⊢ xs.nonzeroMinimum ≤ y

Proof state:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
w : ∀ (x : Nat), x ∈ xs → x ≤ y → x = 0
⊢ ∀ (x : Nat), x ∈ xs → x = 0

Tactic:
apply nonzeroMinimum_eq_zero_iff.mp

Result:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
w : ∀ (x : Nat), x ∈ xs → x ≤ y → x = 0
⊢ xs.nonzeroMinimum = 0

Proof state:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
⊢ xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0

Tactic:
rw [Classical.or_iff_not_imp_right]

Result:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
⊢ (¬∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0) → xs.nonzeroMinimum = 0

Proof state:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
⊢ (¬∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0) → xs.nonzeroMinimum = 0

Tactic:
simp only [ne_eq, not_exists, not_and, Classical.not_not, nonzeroMinimum_eq_zero_iff]

Result:
case refine_1
xs : List Nat
y : Nat
h : xs.nonzeroMinimum ≤ y
⊢ (∀ (x : Nat), x ∈ xs → x ≤ y → x = 0) → ∀ (x : Nat), x ∈ xs → x = 0