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

State before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : latticeRect ((0, 0), m, n) = I.disjiUnion (latticeRect ∘ Q) h
⊢ ∃ i ∈ I, ((Q i).2.1.bodd = true ∧ (Q i).2.2.bodd = true) ∧ ((Q i).1.1 + (Q i).1.2).bodd = false
Tactic:
suffices ∃ i ∈ I, 0 < weight (latticeRect (Q i))
  from this.elim λ i h3 ↦ ⟨i, h3.1, latticeRect_weight_pos_imp h3.2⟩
State after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : latticeRect ((0, 0), m, n) = I.disjiUnion (latticeRect ∘ Q) h
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))

State before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : latticeRect ((0, 0), m, n) = I.disjiUnion (latticeRect ∘ Q) h
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
apply_fun weight at h1
State after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : weight (latticeRect ((0, 0), m, n)) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))

State before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : weight (latticeRect ((0, 0), m, n)) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
rw [latticeRect_weight] at h1
State after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 :
  (bif ((0, 0), m, n).2.1.bodd && ((0, 0), m, n).2.2.bodd then (-1) ^ (((0, 0), m, n).1.1 + ((0, 0), m, n).1.2)
    else 0) =
    weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))

State before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 :
  (bif ((0, 0), m, n).2.1.bodd && ((0, 0), m, n).2.2.bodd then (-1) ^ (((0, 0), m, n).1.1 + ((0, 0), m, n).1.2)
    else 0) =
    weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
simp only at h1
State after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif m.bodd && n.bodd then (-1) ^ (0 + 0) else 0) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))

State before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif m.bodd && n.bodd then (-1) ^ (0 + 0) else 0) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
rw [disjiUnion_weight_eq, Function.comp, h0.1, h0.2, add_zero] at h1
State after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))

State before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
apply exists_lt_of_sum_lt
State after:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∑ i ∈ I, 0 < ∑ i ∈ I, weight (latticeRect (Q i))

State before:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∑ i ∈ I, 0 < ∑ i ∈ I, weight (latticeRect (Q i))
Tactic:
rw [sum_const_zero, ← h1]
State after:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ 0 < bif true && true then (-1) ^ 0 else 0

State before:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ 0 < bif true && true then (-1) ^ 0 else 0
Tactic:
exact Int.zero_lt_one
State after:
no goals