Theorem: IMOSL.IMO2017C1.latticeRect_weight (IMOSLLean4/IMO2017/C1/C1.lean)

State before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ weight (latticeRect q) = bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
rw [weight, latticeRect, sum_product]
State after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), ∑ y ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ (x, y).1 * (-1) ^ (x, y).2 =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

State before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), ∑ y ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ (x, y).1 * (-1) ^ (x, y).2 =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
simp_rw [← mul_sum]
State after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), (-1) ^ x * ∑ i ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ i =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

State before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), (-1) ^ x * ∑ i ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ i =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
rw [← sum_mul, sum_neg_one_pow_Ico, sum_neg_one_pow_Ico]
State after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif q.2.1.bodd then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

State before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif q.2.1.bodd then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
cases q.2.1.bodd
State after:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif false then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif false && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

State before:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif false then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif false && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
exact zero_mul _
State after:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

State before:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
cases q.2.2.bodd
State after:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif false then (-1) ^ q.1.2 else 0) =
    bif true && false then (-1) ^ (q.1.1 + q.1.2) else 0

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif true then (-1) ^ q.1.2 else 0) =
    bif true && true then (-1) ^ (q.1.1 + q.1.2) else 0

State before:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif false then (-1) ^ q.1.2 else 0) =
    bif true && false then (-1) ^ (q.1.1 + q.1.2) else 0

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif true then (-1) ^ q.1.2 else 0) =
    bif true && true then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
exacts [mul_zero _, (pow_add _ _ _).symm]
State after:
no goals