Theorem: Weight.BasicInterval.mem_left_or_mem_right (Weights/BasicInterval.lean)

State before:
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ mem a b (left I) ∨ mem a b (right I)
Tactic:
by_cases hl : mem a b I.left
State after:
case pos
a b : ℕ
I : BasicInterval
h : mem a b I
hl : mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)

case neg
a b : ℕ
I : BasicInterval
h : mem a b I
hl : ¬mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)

State before:
case pos
a b : ℕ
I : BasicInterval
h : mem a b I
hl : mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)
Tactic:
exact Or.inl hl
State after:
no goals

State before:
case neg
a b : ℕ
I : BasicInterval
h : mem a b I
hl : ¬mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)
Tactic:
unfold mem at h hl ⊢
State after:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬(b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂)
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂

State before:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬(b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂)
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂
Tactic:
rw [@not_and_or] at hl
State after:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬b * (left I).a₁ ≤ a * (left I).b₁ ∨ ¬a * (left I).b₂ ≤ b * (left I).a₂
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂

State before:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬b * (left I).a₁ ≤ a * (left I).b₁ ∨ ¬a * (left I).b₂ ≤ b * (left I).a₂
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂
Tactic:
cases' hl with hl hl <;> push_neg at hl <;> simp at hl ⊢
State after:
case neg.inl
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂

case neg.inr
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : b * (I.a₁ + I.a₂) < a * (I.b₁ + I.b₂)
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂

State before:
case neg.inl
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂
Tactic:
exact Or.inl ⟨h.1, by linarith⟩
State after:
no goals

State before:
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂)
Tactic:
linarith
State after:
no goals

State before:
case neg.inr
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : b * (I.a₁ + I.a₂) < a * (I.b₁ + I.b₂)
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂
Tactic:
refine Or.inr ⟨hl.le, h.2⟩
State after:
no goals