Theorem: Weight.theorem_1_6 (Weights/Dimension2.lean)

State before:
d : ℕ
inst✝ : NeZero d
⊢ ∀ w ∈ M 2 d, ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
intro w hw
State after:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d

State before:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
obtain ⟨a, b, hab⟩ := ex_of_fraction hw.1
State after:
case intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d

State before:
case intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
obtain ⟨s, t, hle, hdom⟩ := dom_by_max_le_d d a b
State after:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d

State before:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
contrapose! hw
State after:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
hw : ∃ i, d < w i
⊢ w ∉ M 2 d

State before:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
hw : ∃ i, d < w i
⊢ w ∉ M 2 d
Tactic:
obtain ⟨i, hi⟩ := hw
State after:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
⊢ w ∉ M 2 d

State before:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
⊢ w ∉ M 2 d
Tactic:
refine not_in_M_of_dom_ne ⟨of_fraction d s t, normalized_of_of_fraction d s t, hab ▸ hdom,
                           fun H ↦ ?_⟩
State after:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
H : of_fraction d s t = w
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
H : of_fraction d s t = w
⊢ False
Tactic:
subst H
State after:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hab : of_fraction d s t = of_fraction d a b
hi : d < of_fraction d s t i
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hab : of_fraction d s t = of_fraction d a b
hi : d < of_fraction d s t i
⊢ False
Tactic:
exact lt_irrefl d <| hi.trans_le <| (of_fraction_le d s t i).trans hle
State after:
no goals