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

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

State before:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : b * g * I.a₁ ≤ a * g * I.b₁
h₂ : a * g * I.b₂ ≤ b * g * I.a₂
⊢ mem a b I
Tactic:
simp_rw [mul_comm _ g, mul_assoc] at h₁ h₂
State after:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : g * (b * I.a₁) ≤ g * (a * I.b₁)
h₂ : g * (a * I.b₂) ≤ g * (b * I.a₂)
⊢ mem a b I

State before:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : g * (b * I.a₁) ≤ g * (a * I.b₁)
h₂ : g * (a * I.b₂) ≤ g * (b * I.a₂)
⊢ mem a b I
Tactic:
exact ⟨Nat.le_of_mul_le_mul_left h₁ hg, Nat.le_of_mul_le_mul_left h₂ hg⟩
State after:
no goals