internlm/Lean-Github huggingface dataset:
Theorem: Weight.index_exists
Proof 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 ↦ ?_⟩
Proof 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
Theorem: Weight.index_exists
Proof 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]
Proof 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
Theorem: Weight.index_exists
Proof 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]
Proof 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
Theorem: Weight.index_exists
Proof 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]
Proof state after:
no goals
Theorem: Weight.index_exists
Proof 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
Proof 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
Theorem: Weight.index_exists
Proof 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]
Proof 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)
Theorem: Weight.index_exists
Proof 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₀
Proof state after:
no goals
Theorem: Weight.index_exists
Proof 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)]
Proof 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
Theorem: Weight.index_exists
Proof 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
Proof state after:
no goals
Theorem: Weight.index_exists
Proof 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)
Proof 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
Theorem: Weight.index_exists
Proof 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)
Proof 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
Theorem: Weight.index_exists
Proof 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
Proof 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
Theorem: Weight.index_exists
Proof 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
Proof state after:
no goals
Theorem: Weight.index_exists
Proof 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
Proof state after:
no goals
Theorem: Weight.index_exists
Proof 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
Proof state after:
no goals
Theorem: Weight.balanced_of_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
⊢ balanced w
Tactic:
by_contra hb
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
hb : ¬balanced w
⊢ False
Theorem: Weight.balanced_of_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
hb : ¬balanced w
⊢ False
Tactic:
obtain ⟨hE', hb', hc, hne⟩ :=
  exists_balanced_ltc w hb (E_trunc_eq_E_of_dom (hmin _ (trunc_dom w)) hw) hw
Proof state after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
hb : ¬balanced w
hE' : E (Function.update (trunc w) 0 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) 0 1)
hc : trunc w ≤ Function.update (trunc w) 0 1
hne : trunc w ≠ Function.update (trunc w) 0 1
⊢ False
Theorem: Weight.balanced_of_min
Proof state before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
hb : ¬balanced w
hE' : E (Function.update (trunc w) 0 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) 0 1)
hc : trunc w ≤ Function.update (trunc w) 0 1
hne : trunc w ≠ Function.update (trunc w) 0 1
⊢ False
Tactic:
exact hne (lec_antisymm hc <| (dom_iff_gec_of_balanced (trunc_zero hw) hb' hE'.symm).mp <|
            (trunc_dom w).trans <| hmin _  <| (dom_of_gec hE' hc).trans $ trunc_dom w)
Proof state after:
no goals
Theorem: Weight.balanced_of_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
⊢ balanced w
Tactic:
by_contra hb
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
⊢ False
Theorem: Weight.balanced_of_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
⊢ False
Tactic:
obtain ⟨k, hk₁, hk₂⟩ := index_exists hw
Proof state after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
⊢ False
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
⊢ False
Tactic:
obtain ⟨hE', hb', hc, hne⟩ :=
  exists_balanced_ltc w hb
    (E_trunc_eq_E_of_dom (hmin _ (trunc_normalized hw).2 w.trunc_dom) hw.1) hk₁
Proof state after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ False
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ False
Tactic:
refine hne <| lec_antisymm hc <|
  (dom_iff_gec_of_balanced (trunc_normalized hw).1 hb' hE'.symm).mp <|
  w.trunc_dom.trans <| hmin _ ?_ <| (dom_of_gec hE' hc).trans w.trunc_dom
Proof state after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ Monotone (Function.update (trunc w) k 1)
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ Monotone (Function.update (trunc w) k 1)
Tactic:
intro i j hij
Proof state after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ Function.update (trunc w) k 1 i ≤ Function.update (trunc w) k 1 j
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ Function.update (trunc w) k 1 i ≤ Function.update (trunc w) k 1 j
Tactic:
simp only [Function.update_apply, trunc_apply]
Proof state after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if i = k then 1 else min (w i) (E w)) ≤ if j = k then 1 else min (w j) (E w)
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if i = k then 1 else min (w i) (E w)) ≤ if j = k then 1 else min (w j) (E w)
Tactic:
cases' eq_or_ne i k with hi hi <;> cases' eq_or_ne j k with hj hj <;> simp [hi, hj]
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ 1 ≤ w j ∧ 1 ≤ E w

case intro.intro.intro.intro.intro.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j = k
⊢ w i ≤ 1 ∨ E w ≤ 1

case intro.intro.intro.intro.intro.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
⊢ w i ≤ w j ∨ E w ≤ w j
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ 1 ≤ w j ∧ 1 ≤ E w
Tactic:
have : w j = Function.update w k 1 j := by simp only [Function.update_apply, hj, if_false]
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j ∧ 1 ≤ E w