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

State before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ 0 < weight (latticeRect q) → (q.2.1.bodd = true ∧ q.2.2.bodd = true) ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
rw [latticeRect_weight, ← Bool.and_eq_true]
State after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0) →
    (q.2.1.bodd && q.2.2.bodd) = true ∧ (q.1.1 + q.1.2).bodd = false

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

case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ (q.1.1 + q.1.2) else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false

State before:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif false then (-1) ^ (q.1.1 + q.1.2) else 0) → false = true ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
exact λ h ↦ absurd h (le_refl 0).not_lt
State after:
no goals

State before:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ (q.1.1 + q.1.2) else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
rw [neg_one_pow_eq_pow_mod_two (R := ℤ), Nat.mod_two_of_bodd]
State after:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif (q.1.1 + q.1.2).bodd then 1 else 0 else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false

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

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif true then 1 else 0 else 0) → true = true ∧ true = false

State before:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif false then 1 else 0 else 0) → true = true ∧ false = false

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif true then 1 else 0 else 0) → true = true ∧ true = false
Tactic:
exacts [λ _ ↦ ⟨rfl, rfl⟩, λ h ↦ absurd neg_one_lt_zero h.not_lt]
State after:
no goals