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

Proof state:
case mp.right
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
⊢ xs.nonzeroMinimum ≤ y ∨ y = 0

Tactic:
by_cases w : y = 0

Result:
case pos
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : y = 0
⊢ xs.nonzeroMinimum ≤ y ∨ y = 0

case neg
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : ¬y = 0
⊢ xs.nonzeroMinimum ≤ y ∨ y = 0

Proof state:
case mp
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ xs.nonzeroMinimum ∈ xs ∧ ∀ (x : Nat), x ∈ xs → xs.nonzeroMinimum ≤ x ∨ x = 0

Tactic:
constructor

Result:
case mp.left
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ xs.nonzeroMinimum ∈ xs

case mp.right
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ ∀ (x : Nat), x ∈ xs → xs.nonzeroMinimum ≤ x ∨ x = 0

Proof state:
case mpr.intro.h₂
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ y ≤ xs.nonzeroMinimum

Tactic:
have nz : xs.nonzeroMinimum ≠ 0 := by
  apply Nat.pos_iff_ne_zero.mp
  apply nonzeroMinimum_pos m h

Result:
case mpr.intro.h₂
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
nz : xs.nonzeroMinimum ≠ 0
⊢ y ≤ xs.nonzeroMinimum

Proof state:
case mpr.intro.h₂
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
nz : xs.nonzeroMinimum ≠ 0
⊢ y ≤ xs.nonzeroMinimum

Tactic:
specialize w (nonzeroMinimum xs) (nonzeroMinimum_mem nz)

Result:
case mpr.intro.h₂
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
nz : xs.nonzeroMinimum ≠ 0
w : y ≤ xs.nonzeroMinimum ∨ xs.nonzeroMinimum = 0
⊢ y ≤ xs.nonzeroMinimum

Proof state:
case mpr.intro.h₂.inl
xs : List Nat
y : Nat
h✝ : y ≠ 0
m : y ∈ xs
nz : xs.nonzeroMinimum ≠ 0
h : y ≤ xs.nonzeroMinimum
⊢ y ≤ xs.nonzeroMinimum

Tactic:
exact h

Result:
no goals

Proof state:
case pos
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : y = 0
⊢ xs.nonzeroMinimum ≤ y ∨ y = 0

Tactic:
right

Result:
case pos.h
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : y = 0
⊢ y = 0

Proof state:
case mpr.intro.h₂.inr
xs : List Nat
y : Nat
h✝ : y ≠ 0
m : y ∈ xs
nz : xs.nonzeroMinimum ≠ 0
h : xs.nonzeroMinimum = 0
⊢ y ≤ xs.nonzeroMinimum

Tactic:
exact False.elim (nz h)

Result:
no goals

Proof state:
xs : List Nat
y : Nat
h : y ≠ 0
⊢ xs.nonzeroMinimum = y ↔ y ∈ xs ∧ ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0

Tactic:
constructor

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

case mpr
xs : List Nat
y : Nat
h : y ≠ 0
⊢ (y ∈ xs ∧ ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0) → xs.nonzeroMinimum = y

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

Tactic:
rintro ⟨m, w⟩

Result:
case mpr.intro
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ xs.nonzeroMinimum = y

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

Tactic:
apply nonzeroMinimum_pos m h

Result:
no goals

Proof state:
case mpr.intro.h₂
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
nz : xs.nonzeroMinimum ≠ 0
w : y ≤ xs.nonzeroMinimum ∨ xs.nonzeroMinimum = 0
⊢ y ≤ xs.nonzeroMinimum

Tactic:
cases w with
| inl h => exact h
| inr h => exact False.elim (nz h)

Result:
no goals

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

Tactic:
rintro rfl

Result:
case mp
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ xs.nonzeroMinimum ∈ xs ∧ ∀ (x : Nat), x ∈ xs → xs.nonzeroMinimum ≤ x ∨ x = 0

Proof state:
case mpr.intro.h₁
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ xs.nonzeroMinimum ≤ y

Tactic:
exact nonzeroMinimum_le m h

Result:
no goals

Proof state:
case pos.h
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : y = 0
⊢ y = 0

Tactic:
exact w

Result:
no goals

Proof state:
case neg.h
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : ¬y = 0
⊢ xs.nonzeroMinimum ≤ y

Tactic:
apply nonzeroMinimum_le m w

Result:
no goals

Proof state:
case neg
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : ¬y = 0
⊢ xs.nonzeroMinimum ≤ y ∨ y = 0

Tactic:
left

Result:
case neg.h
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
w : ¬y = 0
⊢ xs.nonzeroMinimum ≤ y

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

Tactic:
apply Nat.pos_iff_ne_zero.mp

Result:
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ 0 < xs.nonzeroMinimum

Proof state:
case mp.right
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ ∀ (x : Nat), x ∈ xs → xs.nonzeroMinimum ≤ x ∨ x = 0

Tactic:
intro y m

Result:
case mp.right
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
y : Nat
m : y ∈ xs
⊢ xs.nonzeroMinimum ≤ y ∨ y = 0

Proof state:
case mp.left
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ xs.nonzeroMinimum ∈ xs

case mp.right
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ ∀ (x : Nat), x ∈ xs → xs.nonzeroMinimum ≤ x ∨ x = 0

Tactic:
exact nonzeroMinimum_mem h

Result:
case mp.right
xs : List Nat
h : xs.nonzeroMinimum ≠ 0
⊢ ∀ (x : Nat), x ∈ xs → xs.nonzeroMinimum ≤ x ∨ x = 0

Proof state:
case mpr.intro
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ xs.nonzeroMinimum = y

Tactic:
apply Nat.le_antisymm

Result:
case mpr.intro.h₁
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ xs.nonzeroMinimum ≤ y

case mpr.intro.h₂
xs : List Nat
y : Nat
h : y ≠ 0
m : y ∈ xs
w : ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
⊢ y ≤ xs.nonzeroMinimum