Theorem: Int.cube_of_coprime (Flt/Euler.lean)

State before:
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
⊢ ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3
Tactic:
have : Odd 3 := by norm_num
State after:
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
⊢ ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3

State before:
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
⊢ ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3
Tactic:
obtain ⟨⟨AB, HAB⟩, ⟨C, HC⟩⟩ :=
  Int.eq_pow_of_mul_eq_pow_odd (IsCoprime.mul_left hcoprimeac hcoprimebc) this hs
State after:
case intro.intro.intro
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 B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3

State before:
case intro.intro.intro
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 B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3
Tactic:
obtain ⟨⟨A, HA⟩, ⟨B, HB⟩⟩ := Int.eq_pow_of_mul_eq_pow_odd hcoprimeab this HAB
State after:
case intro.intro.intro.intro.intro.intro
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 B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3

State before:
case intro.intro.intro.intro.intro.intro
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 B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3
Tactic:
refine' ⟨A, B, C, _, _, _, HA, HB, HC⟩ <;> apply ne_zero_pow three_ne_zero
State after:
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

case intro.intro.intro.intro.intro.intro.refine'_2
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
⊢ B ^ 3 ≠ 0

case intro.intro.intro.intro.intro.intro.refine'_3
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
⊢ C ^ 3 ≠ 0

State before:
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
⊢ Odd 3
Tactic:
norm_num
State after:
no goals

State before:
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
Tactic:
rwa [← HA]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_2
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
⊢ B ^ 3 ≠ 0
Tactic:
rwa [← HB]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_3
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
⊢ C ^ 3 ≠ 0
Tactic:
rwa [← HC]
State after:
no goals