Theorem: Usa2015P1.abc (Compfiles/Usa2015P1.lean)

State before:
a b c : ℤ
hb : b ≠ 0
⊢ a ^ 2 = b ^ 2 * c → ∃ d, c = d ^ 2
Tactic:
intro h
State after:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ ∃ d, c = d ^ 2

State before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ ∃ d, c = d ^ 2
Tactic:
have h1 : b ^ 2 ∣ a ^ 2 := by simp_all only [ne_eq, dvd_mul_right]
State after:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ ∃ d, c = d ^ 2

State before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ ∃ d, c = d ^ 2
Tactic:
have h2 : b ∣ a := by apply (Int.pow_dvd_pow_iff (by positivity)).mp h1
State after:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
h2 : b ∣ a
⊢ ∃ d, c = d ^ 2

State before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
h2 : b ∣ a
⊢ ∃ d, c = d ^ 2
Tactic:
obtain ⟨d, rfl⟩ := h2
State after:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : (b * d) ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2

State before:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : (b * d) ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
Tactic:
rw [mul_pow, mul_right_inj' (by positivity)] at h
State after:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2

State before:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
Tactic:
use d
State after:
case h
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ c = d ^ 2

State before:
case h
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ c = d ^ 2
Tactic:
exact h.symm
State after:
no goals

State before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ b ^ 2 ∣ a ^ 2
Tactic:
simp_all only [ne_eq, dvd_mul_right]
State after:
no goals

State before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ b ∣ a
Tactic:
apply (Int.pow_dvd_pow_iff (by positivity)).mp h1
State after:
no goals

State before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ 2 ≠ 0
Tactic:
positivity
State after:
no goals

State before:
b c : ℤ
hb : b ≠ 0
d : ℤ
h : b ^ 2 * d ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ b ^ 2 ≠ 0
Tactic:
positivity
State after:
no goals