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

State before:
a b : ℕ
I : BasicInterval
h : mem_interior a b I
⊢ mem a b I
Tactic:
simp only [mem, mem_interior] at h ⊢
State after:
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂

State before:
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
Tactic:
constructor <;> linarith
State after:
no goals