Theorem: Usa1987P1.lemma2 (Compfiles/Usa1987P1.lean)

State before:
a b c : ℤ
h : a * b ^ 2 = c ^ 2
⊢ IsSquare a ∨ b = 0
Tactic:
obtain rfl | hb := eq_or_ne b 0
State after:
case inl
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ IsSquare a ∨ 0 = 0

case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a ∨ b = 0

State before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a ∨ b = 0
Tactic:
simp only [hb, or_false]
State after:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a

State before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a
Tactic:
have h1 : b^2 ∣ c^2 := Dvd.intro_left a h
State after:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ^ 2 ∣ c ^ 2
⊢ IsSquare a

State before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ^ 2 ∣ c ^ 2
⊢ IsSquare a
Tactic:
rw [Int.pow_dvd_pow_iff two_ne_zero] at h1
State after:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ∣ c
⊢ IsSquare a

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

State before:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a * b ^ 2 = (b * k) ^ 2
⊢ IsSquare a
Tactic:
rw [mul_pow, mul_comm, mul_right_inj' (pow_ne_zero _ hb)] at h
State after:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare a

State before:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare a
Tactic:
rw [h]
State after:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare (k ^ 2)

State before:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare (k ^ 2)
Tactic:
exact ⟨k, sq k⟩
State after:
no goals

State before:
case inl
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ IsSquare a ∨ 0 = 0
Tactic:
right
State after:
case inl.h
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ 0 = 0

State before:
case inl.h
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ 0 = 0
Tactic:
rfl
State after:
no goals