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

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

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

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

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