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

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'
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'

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
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'

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
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'

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
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'

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
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'

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
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'

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 ↦ ?_⟩
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

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]
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

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]
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)

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]
State after:
no goals

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]
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

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]
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)

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⟩
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)

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)
State after:
no goals

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 _))
State after:
no goals

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']
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)

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
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)

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 _
State after:
no goals

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 _
State after:
no goals

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]
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

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]
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

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)
State after:
no goals

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'
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

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'
State after:
no goals