Theorem: Weight.mem_S_le_of_proportional (Weights/Dimension2.lean)

State before:
d g : ℕ
a b : ℤ
hg : 0 < g
h : mem_S_le d (a * ↑g) (b * ↑g)
⊢ mem_S_le d a b
Tactic:
obtain ⟨h₁, i₁, i₂, h₂, h₃, h₄⟩ := h
State after:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : a * ↑g * (3 * ↑i₂ - ↑d) = b * ↑g * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ mem_S_le d a b

State before:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : a * ↑g * (3 * ↑i₂ - ↑d) = b * ↑g * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ mem_S_le d a b
Tactic:
simp_rw [mul_comm _ (g : ℤ), mul_assoc] at h₄
State after:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ mem_S_le d a b

State before:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ mem_S_le d a b
Tactic:
replace hg : (0 : ℤ) < g := Nat.cast_pos.mpr hg
State after:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
hg : 0 < ↑g
⊢ mem_S_le d a b

State before:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
hg : 0 < ↑g
⊢ mem_S_le d a b
Tactic:
exact ⟨(mul_pos_iff_of_pos_right hg).mp h₁, i₁, i₂, h₂, h₃, Int.eq_of_mul_eq_mul_left hg.ne' h₄⟩
State after:
no goals