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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ balanced w ↔ trunc w = w
Tactic:
simp_rw [balanced]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (j : Fin (Nat.succ n)), w j ≤ E w) ↔ trunc w = w

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (j : Fin (Nat.succ n)), w j ≤ E w) ↔ trunc w = w
Tactic:
constructor <;> intro h
State after:
case mp
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
⊢ trunc w = w

case mpr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : trunc w = w
⊢ ∀ (j : Fin (Nat.succ n)), w j ≤ E w

State before:
case mp
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
⊢ trunc w = w
Tactic:
ext j
State after:
case mp.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
j : Fin (Nat.succ n)
⊢ trunc w j = w j

State before:
case mp.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
j : Fin (Nat.succ n)
⊢ trunc w j = w j
Tactic:
exact min_eq_left_iff.mpr (h j)
State after:
no goals

State before:
case mpr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : trunc w = w
⊢ ∀ (j : Fin (Nat.succ n)), w j ≤ E w
Tactic:
exact fun j ↦ min_eq_left_iff.mp (congr_fun h j)
State after:
no goals