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

State before:
a b : ℕ
I : BasicInterval
h : mem a b (right I)
⊢ mem a b I
Tactic:
obtain ⟨h₁, h₂⟩ := h
State after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
h₂ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ mem a b I

State before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
h₂ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ mem a b I
Tactic:
simp at h₁ h₂
State after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂)
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ mem a b I

State before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂)
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ mem a b I
Tactic:
exact ⟨by linarith, h₂⟩
State after:
no goals

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