Theorem: Weight.w1_unique (Weights/Degree1.lean)

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
⊢ w = w1 n
Tactic:
have h₁ := w1_minimal hw
State after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
⊢ w = w1 n

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
⊢ w = w1 n
Tactic:
have h₂ := hmin _ h₁
State after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ w = w1 n

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ w = w1 n
Tactic:
have hE : w.E = 1
State after:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = 1

n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
⊢ w = w1 n

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
⊢ w = w1 n
Tactic:
ext j
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
⊢ w j = w1 n j
Tactic:
have hc₁ := (lec_iff _ _).mp
              ((dom_iff_gec_of_balanced hw (w1_balanced n) (hE.trans (E_w1 n).symm)).mp h₂)
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
⊢ w j = w1 n j
Tactic:
have hsum : (w1 n).sum ≤ w.sum := Finset.sum_le_sum (fun j _ ↦ hc₁ j)
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : Weight.sum (w1 n) ≤ Weight.sum w
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : Weight.sum (w1 n) ≤ Weight.sum w
⊢ w j = w1 n j
Tactic:
rw [sum_w1] at hsum
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j
Tactic:
rw [E] at hE
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : Weight.sum w * 1 / (n + 1) + 1 = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : Weight.sum w * 1 / (n + 1) + 1 = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j
Tactic:
simp [Nat.div_eq_zero_iff] at hE
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
⊢ w j = w1 n j
Tactic:
have hn : w.sum = n := Nat.eq_of_le_of_lt_succ hsum hE
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ w j = w1 n j

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ w j = w1 n j
Tactic:
refine ((Finset.sum_eq_sum_iff_of_le (fun k _ ↦ hc₁ k)).mp ?_ j (Finset.mem_univ j)).symm
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i
Tactic:
rw [Weight.sum] at hn
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i
Tactic:
rw [hn]
State after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = n

State before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = n
Tactic:
exact sum_w1 n
State after:
no goals

State before:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = 1
Tactic:
conv_rhs => rw [← E_w1 n]
State after:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = E (w1 n)

State before:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = E (w1 n)
Tactic:
exact E_dom_eq hw (w1_zero n) h₂ h₁
State after:
no goals