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

State before:
n d : ℕ
inst✝ : NeZero d
⊢ complete_set (M n d)
Tactic:
intro w
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ normalized w → ∃ w' ∈ M n d, w' ≤ w

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ normalized w → ∃ w' ∈ M n d, w' ≤ w
Tactic:
refine WellFoundedLT.induction (α := Weight n d)
  (C := fun w ↦ normalized w → ∃ w', w' ∈ M n d ∧ w' ≤ w) w (fun w₁ h ↦ ?_)
State after:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
⊢ (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) w₁

State before:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
⊢ (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) w₁
Tactic:
intro hw₁n
State after:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

State before:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
by_cases hw₁ : ∃ w₂ : Weight n d, w₂.normalized ∧ w₂ < w₁
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ¬∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
obtain ⟨w₂, hw₂n, hw₂⟩ := hw₁
State after:
case pos.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

State before:
case pos.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
obtain ⟨w', hw'₁, hw'₂⟩ := h w₂ hw₂ hw₂n
State after:
case pos.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
w' : Weight n d
hw'₁ : w' ∈ M n d
hw'₂ : w' ≤ w₂
⊢ ∃ w' ∈ M n d, w' ≤ w₁

State before:
case pos.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
w' : Weight n d
hw'₁ : w' ∈ M n d
hw'₂ : w' ≤ w₂
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
exact ⟨w', hw'₁, hw'₂.trans <| le_of_lt hw₂⟩
State after:
no goals

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ¬∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
push_neg at hw₁
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
refine ⟨w₁, ⟨hw₁n, fun w' hw' h' ↦ ?_⟩, le_refl w₁⟩
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
⊢ w₁ ≤ w'

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
⊢ w₁ ≤ w'
Tactic:
by_contra hf
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
⊢ False

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
⊢ False
Tactic:
have := hw₁ w' hw'
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬w' < w₁
⊢ False

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬w' < w₁
⊢ False
Tactic:
rw [lt_iff_le_not_le] at this
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬(w' ≤ w₁ ∧ ¬w₁ ≤ w')
⊢ False

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬(w' ≤ w₁ ∧ ¬w₁ ≤ w')
⊢ False
Tactic:
push_neg at this
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : w' ≤ w₁ → w₁ ≤ w'
⊢ False

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : w' ≤ w₁ → w₁ ≤ w'
⊢ False
Tactic:
exact hf (this h')
State after:
no goals