replace hg : (0 : ℤ) < g := Nat.cast_pos.mpr hg
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
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