internlm/Lean-Github huggingface dataset:
Theorem: Weight.trunc_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (j : Fin (Nat.succ n)), trunc w j ≤ ↑(E w) j
Tactic:
exact trunc_le_E w
Proof state after:
no goals
Theorem: Weight.dom_of_gec
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ w ≤ w'
Tactic:
simp only [dom_iff, f_le_iff, f_apply, SetCoe.forall, Subtype.coe_mk, hE]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ ∀ x ∈ testvecs n d, E w' - pair w x ≤ E w' - pair w' x
Theorem: Weight.dom_of_gec
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ ∀ x ∈ testvecs n d, E w' - pair w x ≤ E w' - pair w' x
Tactic:
exact fun a _ ↦ Nat.sub_le_sub_left (pair_le_pair_of_lec _ _ _ h) _
Proof state after:
no goals
Theorem: Weight.dom_iff_gec_of_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
⊢ w ≤ w' ↔ w' ≤ w
Tactic:
refine ⟨fun h ↦ (lec_iff _ _).mpr (fun j ↦ ?_), dom_of_gec hE⟩
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
⊢ w' j ≤ w j
Theorem: Weight.dom_iff_gec_of_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
⊢ w' j ≤ w j
Tactic:
have hw₃ := eval_f_tw w j
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - (d - 1) * w 0 - w j
⊢ w' j ≤ w j
Theorem: Weight.dom_iff_gec_of_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - (d - 1) * w 0 - w j
⊢ w' j ≤ w j
Tactic:
simp only [hw₁, mul_zero, tsub_zero] at hw₃
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
⊢ w' j ≤ w j
Theorem: Weight.dom_iff_gec_of_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
⊢ w' j ≤ w j
Tactic:
have h' := h (tw n d j)
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : f w (tw n d j) ≤ f w' (tw n d j)
⊢ w' j ≤ w j
Theorem: Weight.dom_iff_gec_of_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : f w (tw n d j) ≤ f w' (tw n d j)
⊢ w' j ≤ w j
Tactic:
rw [hw₃, eval_f_tw w' j, hE, Nat.sub_sub, add_comm, ← Nat.sub_sub] at h'
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : E w' - w j ≤ E w' - w' j - (d - 1) * w' 0
⊢ w' j ≤ w j
Theorem: Weight.dom_iff_gec_of_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : E w' - w j ≤ E w' - w' j - (d - 1) * w' 0
⊢ w' j ≤ w j
Tactic:
exact (tsub_le_tsub_iff_left (hw'₂ j)).mp (h'.trans $ Nat.sub_le _ _)
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hb : ¬balanced w
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
⊢ let w' := Function.update (trunc w) k 1;
  E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
intro w'
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hb : ¬balanced w
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Theorem: Weight.exists_balanced_ltc
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hb : ¬balanced w
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
simp only [balanced] at hb
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hb : ¬∀ (j : Fin (Nat.succ n)), w j ≤ E w
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Theorem: Weight.exists_balanced_ltc
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hb : ¬∀ (j : Fin (Nat.succ n)), w j ≤ E w
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
push_neg at hb
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
hb : ∃ j, E w < w j
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Theorem: Weight.exists_balanced_ltc
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
hb : ∃ j, E w < w j
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
obtain ⟨j, hj⟩ := hb
Proof state after:
case intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
have hsum' : w'.sum = w.trunc.sum + 1
Proof state after:
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ Weight.sum w' = Weight.sum (trunc w) + 1

case intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
have hE' : w'.E = w.trunc.E
Proof state after:
case hE'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ E w' = E (trunc w)

case intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
Tactic:
refine ⟨hE', fun j ↦ ?_, (lec_iff _ _).mpr (fun j ↦ ?_), fun hf ↦ ?_⟩
Proof state after:
case intro.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ w' j ≤ E w'

case intro.refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ trunc w j ≤ w' j

case intro.refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
hf : trunc w = w'
⊢ False
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ Weight.sum w' = Weight.sum (trunc w) + 1
Tactic:
simp only [Weight.sum, ne_eq, Function.update_apply, trunc_apply, ge_iff_le, Finset.sum_ite,
  Finset.mem_univ, forall_true_left, Finset.filter_eq', ite_true, Finset.sum_const,
  Finset.card_singleton, smul_eq_mul, mul_one, forall_eq, Finset.filter_ne', not_true]
Proof state after:
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ 1 + ∑ x in Finset.erase Finset.univ k, min (w x) (E w) = ∑ x : Fin (Nat.succ n), min (w x) (E w) + 1
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ 1 + ∑ x in Finset.erase Finset.univ k, min (w x) (E w) = ∑ x : Fin (Nat.succ n), min (w x) (E w) + 1
Tactic:
rw [← Finset.sum_erase_add _ _ (Finset.mem_univ k), add_comm, add_left_inj, hk]
Proof state after:
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ ∑ x in Finset.erase Finset.univ k, min (w x) (E w) = ∑ x in Finset.erase Finset.univ k, min (w x) (E w) + min 0 (E w)
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ ∑ x in Finset.erase Finset.univ k, min (w x) (E w) = ∑ x in Finset.erase Finset.univ k, min (w x) (E w) + min 0 (E w)
Tactic:
simp only [Finset.mem_univ, not_true, ge_iff_le, zero_le, min_eq_left, add_zero]
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hE'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ E w' = E (trunc w)
Tactic:
rw [E, hsum', hE]
Proof state after:
case hE'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) + 1 = E w
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hE'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) + 1 = E w
Tactic:
refine le_antisymm ?_ (le_of_eq_of_le hE.symm ?_) <;> rw [E, add_le_add_iff_right]
Proof state after:
case hE'.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) ≤ Weight.sum w * d / (n + 1)

case hE'.refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ Weight.sum (trunc w) * d / (n + 1) ≤ (Weight.sum (trunc w) + 1) * d / (n + 1)
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hE'.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) ≤ Weight.sum w * d / (n + 1)
Tactic:
have hsum : w.trunc.sum < w.sum :=
  Finset.sum_lt_sum (fun j _ ↦ (lec_iff _ _).mp (trunc_lec w) j)
                    ⟨j, Finset.mem_univ j, lt_of_le_of_lt (trunc_le_E w j) hj⟩
Proof state after:
case hE'.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hsum : Weight.sum (trunc w) < Weight.sum w
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) ≤ Weight.sum w * d / (n + 1)
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hE'.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hsum : Weight.sum (trunc w) < Weight.sum w
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) ≤ Weight.sum w * d / (n + 1)
Tactic:
exact Nat.div_le_div_right (Nat.mul_le_mul_right _ $ Nat.succ_le_iff.mpr hsum)
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
case hE'.refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ Weight.sum (trunc w) * d / (n + 1) ≤ (Weight.sum (trunc w) + 1) * d / (n + 1)
Tactic:
exact Nat.div_le_div_right (Nat.mul_le_mul_right _ (Nat.le_succ _))
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ w' j ≤ E w'
Tactic:
simp only [ne_eq, Function.update_apply, trunc_apply, ge_iff_le, hE']
Proof state after:
case intro.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ (if j = k then 1 else min (w j) (E w)) ≤ E (trunc w)
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro.refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ (if j = k then 1 else min (w j) (E w)) ≤ E (trunc w)
Tactic:
split_ifs
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
h✝ : j = k
⊢ 1 ≤ E (trunc w)

case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
h✝ : ¬j = k
⊢ min (w j) (E w) ≤ E (trunc w)
Theorem: Weight.exists_balanced_ltc
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
h✝ : j = k
⊢ 1 ≤ E (trunc w)
Tactic:
exact one_le_E _
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
h✝ : ¬j = k
⊢ min (w j) (E w) ≤ E (trunc w)
Tactic:
exact trunc_balanced hE _
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro.refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ trunc w j ≤ w' j
Tactic:
simp only [Function.update_apply]
Proof state after:
case intro.refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ trunc w j ≤ if j = k then 1 else trunc w j
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro.refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ trunc w j ≤ if j = k then 1 else trunc w j
Tactic:
by_cases hjk : j = k <;>
  simp only [hjk, (Nat.eq_zero_of_le_zero (le_of_le_of_eq (trunc_lec w k) hk)),
    zero_le', if_false]
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
hjk : ¬j = k
⊢ trunc w j ≤ trunc w j
Theorem: Weight.exists_balanced_ltc
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j✝ : Fin (Nat.succ n)
hj : E w < w j✝
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
hjk : ¬j = k
⊢ trunc w j ≤ trunc w j
Tactic:
exact Nat.le_refl (trunc w j)
Proof state after:
no goals
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro.refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
hE' : E w' = E (trunc w)
hf : trunc w = w'
⊢ False
Tactic:
rw [hf, self_eq_add_right] at hsum'
Proof state after:
case intro.refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : 1 = 0
hE' : E w' = E (trunc w)
hf : trunc w = w'
⊢ False
Theorem: Weight.exists_balanced_ltc
Proof state before:
case intro.refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
hsum' : 1 = 0
hE' : E w' = E (trunc w)
hf : trunc w = w'
⊢ False
Tactic:
exact Nat.one_ne_zero hsum'
Proof state after:
no goals
Theorem: Weight.index_exists
Proof 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)
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
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
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
⊢ ∃ 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]
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
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
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
⊢ ∃ 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)⟩
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) }
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
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) }
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
Tactic:
have hm : w m = 0
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) }
⊢ 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)