rwa [← HA]
case intro.intro.intro.intro.intro.intro.refine'_1
a b c s : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hcoprimeab : IsCoprime a b
hcoprimeac : IsCoprime a c
hcoprimebc : IsCoprime b c
hs : a * b * c = s ^ 3
this : Odd 3
AB : ℤ
HAB : a * b = AB ^ 3
C : ℤ
HC : c = C ^ 3
A : ℤ
HA : a = A ^ 3
B : ℤ
HB : b = B ^ 3
⊢ A ^ 3 ≠ 0
no goals