simp_rw [mul_comm _ g, mul_assoc]
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₂ = b' * g * I.a₂
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ g * (a' * I.b₂) = g * (b' * I.a₂)