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

State before:
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
⊢ S = M n d
Tactic:
ext w
State after:
case h
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
⊢ w ∈ S ↔ w ∈ M n d

State before:
case h
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
⊢ w ∈ S ↔ w ∈ M n d
Tactic:
refine ⟨fun h ↦ ⟨hS₁ w h, fun w' hw'₁ hw'₂ ↦ ?_⟩, fun h ↦ ?_⟩
State after:
case h.refine_1
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
⊢ w ≤ w'

case h.refine_2
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ M n d
⊢ w ∈ S

State before:
case h.refine_1
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
⊢ w ≤ w'
Tactic:
obtain ⟨w₁, hw₁, hle⟩ := hS₂.1 w' hw'₁
State after:
case h.refine_1.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
w₁ : Weight n d
hw₁ : w₁ ∈ S
hle : w₁ ≤ w'
⊢ w ≤ w'

State before:
case h.refine_1.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
w₁ : Weight n d
hw₁ : w₁ ∈ S
hle : w₁ ≤ w'
⊢ w ≤ w'
Tactic:
exact le_of_eq_of_le (hS₂.2 w₁ w hw₁ h (hle.trans hw'₂)).symm hle
State after:
no goals

State before:
case h.refine_2
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ M n d
⊢ w ∈ S
Tactic:
obtain ⟨hw₁, hw₂⟩ := h
State after:
case h.refine_2.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
⊢ w ∈ S

State before:
case h.refine_2.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
⊢ w ∈ S
Tactic:
obtain ⟨w', hw'₁, hw'₂⟩ := hS₂.1 w hw₁
State after:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w ∈ S

State before:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w ∈ S
Tactic:
suffices heq : w' = w
State after:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
heq : w' = w
⊢ w ∈ S

case heq
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w' = w

State before:
case heq
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w' = w
Tactic:
exact eq_of_dom_and_min' (hS₁ w' hw'₁) hw₁ (hw₂ w' (hS₁ w' hw'₁) hw'₂)
                         (fun u hu₁ hu₂ ↦ hw'₂.trans (hw₂ u hu₁ (hu₂.trans hw'₂)))
State after:
no goals

State before:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
heq : w' = w
⊢ w ∈ S
Tactic:
exact heq ▸ hw'₁
State after:
no goals