-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem nonzeroMininum_map_le_nonzeroMinimum (f : α → β) (p : α → Nat) (q : β → Nat) (xs : List α)
    (h : ∀ a, a ∈ xs → (p a = 0 ↔ q (f a) = 0))
    (w : ∀ a, a ∈ xs → p a ≠ 0 → q (f a) ≤ p a) :
    ((xs.map f).map q).nonzeroMinimum ≤ (xs.map p).nonzeroMinimum

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
a : α
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ q (f a) ≠ 0

Tactic:
rwa [Ne, ← h _ m, ← eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
this : ∃ x, (∃ a, a ∈ xs ∧ p a = x) ∧ (map p xs).nonzeroMinimum = x
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Tactic:
obtain ⟨x, ⟨a, m, rfl⟩, eq⟩ := this

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
a : α
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : (map p xs).nonzeroMinimum = 0
⊢ (∀ (x : Nat), x ∈ map q (map f xs) → x = 0) ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
a : α
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ q (f a) ≤ (map p xs).nonzeroMinimum

Tactic:
rw [eq] at z ⊢

Result:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
a : α
z : ¬p a = 0
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ q (f a) ≤ p a

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Tactic:
have := nonzeroMinimum_eq_of_nonzero z

Result:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
this : ∃ x, x ∈ map p xs ∧ (map p xs).nonzeroMinimum = x
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
⊢ (map q (map f xs)).nonzeroMinimum ≤ (map p xs).nonzeroMinimum

Tactic:
rw [nonzeroMinimum_le_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
this : ∃ x, x ∈ map p xs ∧ (map p xs).nonzeroMinimum = x
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Tactic:
simp only [mem_map] at this

Result:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
this : ∃ x, (∃ a, a ∈ xs ∧ p a = x) ∧ (map p xs).nonzeroMinimum = x
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
a : α
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Tactic:
refine .inr ⟨q (f a), List.mem_map_of_mem _ (List.mem_map_of_mem _ m), ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
a : α
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ q (f a) ≤ (map p xs).nonzeroMinimum

case intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : ¬(map p xs).nonzeroMinimum = 0
a : α
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ q (f a) ≠ 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : (map p xs).nonzeroMinimum = 0
⊢ (map q (map f xs)).nonzeroMinimum = 0 ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Tactic:
rw [nonzeroMinimum_eq_zero_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
z : (map p xs).nonzeroMinimum = 0
⊢ (∀ (x : Nat), x ∈ map q (map f xs) → x = 0) ∨ ∃ x, x ∈ map q (map f xs) ∧ x ≤ (map p xs).nonzeroMinimum ∧ x ≠ 0

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
f : α → β
p : α → Nat
q : β → Nat
xs : List α
h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)
w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a
a : α
z : ¬p a = 0
m : a ∈ xs
eq : (map p xs).nonzeroMinimum = p a
⊢ q (f a) ≤ p a

Tactic:
apply w _ m z

Result:
no goals