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

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

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

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

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