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

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
cases' le_or_lt (a + b) d with h h
State after:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : a + b ≤ d
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

case inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

State before:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : a + b ≤ d
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
exact ⟨a, b, h, Eq.le rfl⟩
State after:
no goals

State before:
case inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
obtain ⟨I, hI, hIab⟩ := mem_feasible d a b
State after:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

State before:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
have hab : a ≠ 0 ∨ b ≠ 0 := by by_contra! hab; linarith
State after:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

State before:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
cases' dom_of_mem d hab hIab (condition_of_feasible hI) with H H
State after:
case inr.intro.intro.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

case inr.intro.intro.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
⊢ a ≠ 0 ∨ b ≠ 0
Tactic:
by_contra! hab
State after:
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a = 0 ∧ b = 0
⊢ False

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a = 0 ∧ b = 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case inr.intro.intro.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
exact ⟨I.a₁, I.b₁, hI.1, H⟩
State after:
no goals

State before:
case inr.intro.intro.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
exact ⟨I.a₂, I.b₂, hI.2.1, H⟩
State after:
no goals