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

State before:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ (∃ d, a = d ^ k) ∧ ∃ e, b = e ^ k
Tactic:
obtain ⟨k, rfl⟩ := hk.exists_bit1
State after:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd (bit1 k)
h : a * b = c ^ bit1 k
⊢ (∃ d, a = d ^ bit1 k) ∧ ∃ e, b = e ^ bit1 k

State before:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd (bit1 k)
h : a * b = c ^ bit1 k
⊢ (∃ d, a = d ^ bit1 k) ∧ ∃ e, b = e ^ bit1 k
Tactic:
exact Int.eq_pow_of_mul_eq_pow_bit1 hab h
State after:
no goals