Theorem: IMOSL.IMO2020A6.good_zero (IMOSLLean4/IMO2020/A6/A6.lean)

State before:
a b : ℤ
⊢ (fun x => 0)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => 0) a + b * (fun x => 0) b
Tactic:
rw [const_iterate, ← Int.add_mul, Int.mul_zero]
State after:
a b : ℤ
⊢ (bif (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 then a + b else 0) = 0

State before:
a b : ℤ
⊢ (bif (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 then a + b else 0) = 0
Tactic:
cases h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0
State after:
case false
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = false
⊢ (bif false then a + b else 0) = 0

case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
⊢ (bif true then a + b else 0) = 0

State before:
case false
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = false
⊢ (bif false then a + b else 0) = 0
Tactic:
rfl
State after:
no goals

State before:
case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
⊢ (bif true then a + b else 0) = 0
Tactic:
have h0 : ∀ c : ℤ, c.natAbs ^ 2 = 0 ↔ c = 0 :=
  λ c ↦ by rw [sq_eq_zero_iff, Int.natAbs_eq_zero]
State after:
case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0

State before:
case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0
Tactic:
rw [Nat.beq_eq, add_eq_zero, h0, h0] at h
State after:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0

State before:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0
Tactic:
rw [h.1, h.2]
State after:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then 0 + 0 else 0) = 0

State before:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then 0 + 0 else 0) = 0
Tactic:
rfl
State after:
no goals

State before:
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
c : ℤ
⊢ c.natAbs ^ 2 = 0 ↔ c = 0
Tactic:
rw [sq_eq_zero_iff, Int.natAbs_eq_zero]
State after:
no goals