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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : ∃ w', normalized w' ∧ w' ≤ w ∧ w' ≠ w
⊢ w ∉ M n d
Tactic:
obtain ⟨w', hw'₁, hw'₂, hw'₃⟩ := hw
State after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
⊢ w ∉ M n d

State before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
⊢ w ∉ M n d
Tactic:
by_contra! hf
State after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
hf : w ∈ M n d
⊢ False

State before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
hf : w ∈ M n d
⊢ False
Tactic:
exact hw'₃ (eq_of_dom_in_M hw'₁ hw'₂ hf)
State after:
no goals