Theorem: Weight.eq_of_dom_and_min' (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
⊢ w = w'
Tactic:
have hminw := (min_Monotone_iff_min_normalized w).mpr hmin
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
⊢ w = w'
Tactic:
have h₁ := hmin _ hw' h
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
⊢ w = w'
Tactic:
have hminw' := fun u (hum : Monotone u) (hu : u ≤d w') ↦ h.trans (hminw u hum (hu.trans h))
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
⊢ w = w'
Tactic:
have hb := balanced_of_min' hw hminw
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
⊢ w = w'
Tactic:
have hb' := balanced_of_min' hw' hminw'
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'
Tactic:
have hE := E_dom_eq hw.1 hw'.1 h₁ h
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'
Tactic:
exact lec_antisymm
  ((dom_iff_gec_of_balanced hw'.1 hb hE.symm).mp h) ((dom_iff_gec_of_balanced hw.1 hb' hE).mp h₁)
State after:
no goals