Theorem: Weight.index_exists (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
Tactic:
let P : ℕ → Prop := (fun i ↦ if hi : i < n.succ then w ⟨i, hi⟩ = 0 else False)
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
Tactic:
have hP : ∀ m (hm : m < n.succ), P m ↔ w ⟨m, hm⟩ = 0 := fun  m hm ↦ by simp only [hm, dif_pos]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
Tactic:
let m : Fin n.succ := ⟨Nat.findGreatest P n, Nat.lt_succ_of_le (Nat.findGreatest_le n)⟩
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
Tactic:
have hm : w m = 0
State after:
case hm
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ w m = 0

n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
Tactic:
refine ⟨m, hm, fun i j hij ↦ ?_⟩
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ Function.update w m 1 i ≤ Function.update w m 1 j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ Function.update w m 1 i ≤ Function.update w m 1 j
Tactic:
simp only [Function.update_apply]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if
        i =
          { val := Nat.findGreatest (fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False) n,
            isLt := (_ : Nat.findGreatest P n < Nat.succ n) } then
      1
    else w i) ≤
    if
        j =
          { val := Nat.findGreatest (fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False) n,
            isLt := (_ : Nat.findGreatest P n < Nat.succ n) } then
      1
    else w j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if
        i =
          { val := Nat.findGreatest (fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False) n,
            isLt := (_ : Nat.findGreatest P n < Nat.succ n) } then
      1
    else w i) ≤
    if
        j =
          { val := Nat.findGreatest (fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False) n,
            isLt := (_ : Nat.findGreatest P n < Nat.succ n) } then
      1
    else w j
Tactic:
by_cases hi : i = m <;> by_cases hj : j = m <;> simp [hi, hj]
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
⊢ 1 ≤ w j

case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : ¬i = m
hj : j = m
⊢ w i ≤ 1

case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : ¬i = m
hj : ¬j = m
⊢ w i ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
m : ℕ
hm : m < Nat.succ n
⊢ P m ↔ w { val := m, isLt := hm } = 0
Tactic:
simp only [hm, dif_pos]
State after:
no goals

State before:
case hm
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ w m = 0
Tactic:
have h₀ : P 0 := by rw [hP 0 (Nat.zero_lt_succ n)]; exact hw.1
State after:
case hm
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
h₀ : P 0
⊢ w m = 0

State before:
case hm
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
h₀ : P 0
⊢ w m = 0
Tactic:
rw [← hP]
State after:
case hm
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
h₀ : P 0
⊢ P (Nat.findGreatest P n)

State before:
case hm
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
h₀ : P 0
⊢ P (Nat.findGreatest P n)
Tactic:
exact Nat.findGreatest_spec (Nat.zero_le n) h₀
State after:
no goals

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ P 0
Tactic:
rw [hP 0 (Nat.zero_lt_succ n)]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
Tactic:
exact hw.1
State after:
no goals

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
⊢ 1 ≤ w j
Tactic:
have hij' : m < j := hi.symm ▸ lt_of_le_of_ne hij (hi.symm ▸ Ne.symm hj)
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
⊢ 1 ≤ w j

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
⊢ 1 ≤ w j
Tactic:
have := Nat.findGreatest_is_greatest hij' (Nat.le_of_lt_succ j.2)
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
this : ¬P ↑j
⊢ 1 ≤ w j

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
this : ¬P ↑j
⊢ 1 ≤ w j
Tactic:
simp only [Fin.is_lt, Fin.eta, dite_eq_ite, ite_true, ← Ne.def] at this
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
this : w j ≠ 0
⊢ 1 ≤ w j

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
this : w j ≠ 0
⊢ 1 ≤ w j
Tactic:
exact Nat.one_le_iff_ne_zero.mpr this
State after:
no goals

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : ¬i = m
hj : j = m
⊢ w i ≤ 1
Tactic:
exact (le_of_le_of_eq (hw.2 (le_of_le_of_eq hij hj)) hm).trans zero_le_one
State after:
no goals

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : ¬i = m
hj : ¬j = m
⊢ w i ≤ w j
Tactic:
exact hw.2 hij
State after:
no goals