internlm/Lean-Github huggingface dataset:
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
⊢ 0 < x ↔ 0 < t * x - 1
Tactic:
rw [h3, mul_zero, Int.lt_iff_add_one_le, sub_add_cancel, le_iff_eq_or_lt]
Proof state after:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
⊢ 0 = t * x - 1 ∨ 0 < t * x - 1 ↔ 0 < t * x - 1
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
⊢ 0 = t * x - 1 ∨ 0 < t * x - 1 ↔ 0 < t * x - 1
Tactic:
refine or_iff_right (λ h4 ↦ ne_of_gt ht ?_)
Proof state after:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
h4 : 0 = t * x - 1
⊢ t = 1
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
h4 : 0 = t * x - 1
⊢ t = 1
Tactic:
rw [eq_comm, sub_eq_zero] at h4
Proof state after:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
h4 : t * x = 1
⊢ t = 1
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
x : ℤ
h4 : t * x = 1
⊢ t = 1
Tactic:
exact Int.eq_one_of_mul_eq_one_right (le_of_lt h2) h4
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
case intro.intro.intro.intro.intro.left
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
h2 : ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
⊢ t * c - 1 < t * ↑a - 1
Tactic:
rwa [← mul_lt_mul_left (lt_trans h h0), ← h1, sq, mul_lt_mul_right h]
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
h2 : ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
⊢ 0 < t * c - 1
Tactic:
rw [← mul_lt_mul_left (lt_trans h h0), mul_zero, ← h1]
Proof state after:
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
h2 : ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
⊢ 0 < (t * ↑a - 1) ^ 2
Theorem: Imo2007P5.bad_exists_descent
Proof state before:
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
h2 : ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
⊢ 0 < (t * ↑a - 1) ^ 2
Tactic:
exact pow_pos h 2
Proof state after:
no goals
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Tactic:
let P : ℕ → Prop := λ k ↦ (0 < k ∧ ∃ m : ℕ, k < m ∧ n * k * m - 1 ∣ (n * k ^ 2 - 1) ^ 2)
Proof state after:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Tactic:
have h : ∀ k : ℕ, P k → ∃ m : ℕ, m < k ∧ P m :=
  λ k h ↦ Exists.elim (bad_exists_descent hn h)
    (λ c h0 ↦ ⟨c, h0.2.1, h0.1, k, h0.2.1, h0.2.2⟩)
Proof state after:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), P k → ∃ m < k, P m
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), P k → ∃ m < k, P m
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Tactic:
classical
replace h := nat_pred_descent h
intro a b ha hb h0
by_contra! h1
exact (lt_or_gt_of_ne h1).elim (λ h1 ↦ h a ⟨ha, b, h1, h0⟩)
  (λ h1 ↦ h b ⟨hb, a, h1, bad_symm h0⟩)
Proof state after:
no goals
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), P k → ∃ m < k, P m
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Tactic:
replace h := nat_pred_descent h
Proof state after:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
Tactic:
intro a b ha hb h0
Proof state after:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
a b : ℕ
ha : 0 < a
hb : 0 < b
h0 : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ a = b
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
a b : ℕ
ha : 0 < a
hb : 0 < b
h0 : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ a = b
Tactic:
by_contra! h1
Proof state after:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
a b : ℕ
ha : 0 < a
hb : 0 < b
h0 : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
h1 : a ≠ b
⊢ False
Theorem: Imo2007P5.generalized_imo2007_p5
Proof state before:
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
a b : ℕ
ha : 0 < a
hb : 0 < b
h0 : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
h1 : a ≠ b
⊢ False
Tactic:
exact (lt_or_gt_of_ne h1).elim (λ h1 ↦ h a ⟨ha, b, h1, h0⟩)
  (λ h1 ↦ h b ⟨hb, a, h1, bad_symm h0⟩)
Proof state after:
no goals
Theorem: Imo2009P6.lemma2
Proof state before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
⊢ ∃ p, ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
obtain ⟨p, hp⟩ := lemma1 n a
Proof state after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∃ p, ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Theorem: Imo2009P6.lemma2
Proof state before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∃ p, ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
refine ⟨p, ?_⟩
Proof state after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Theorem: Imo2009P6.lemma2
Proof state before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
intro i j hij
Proof state after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Theorem: Imo2009P6.lemma2
Proof state before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
have h0 := ne_of_lt hij
Proof state after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Theorem: Imo2009P6.lemma2
Proof state before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
have h2 := hp i j (le_of_lt hij)
Proof state after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Theorem: Imo2009P6.lemma2
Proof state before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
have h3 : p i ≠ p j := by
  intro hh; rw [EmbeddingLike.apply_eq_iff_eq] at hh; exact h0 hh
Proof state after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
h3 : p i ≠ p j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Theorem: Imo2009P6.lemma2
Proof state before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
h3 : p i ≠ p j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
exact lt_of_le_of_ne h2 fun a ↦ h3 (ainj a)
Proof state after:
no goals
Theorem: Imo2009P6.lemma2
Proof state before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ p i ≠ p j
Tactic:
intro hh
Proof state after:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : p i = p j
⊢ False
Theorem: Imo2009P6.lemma2
Proof state before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : p i = p j
⊢ False
Tactic:
rw [EmbeddingLike.apply_eq_iff_eq] at hh
Proof state after:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : i = j
⊢ False
Theorem: Imo2009P6.lemma2
Proof state before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : i = j
⊢ False
Tactic:
exact h0 hh
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
hM : ∑ i : Fin n, a i ∉ M
⊢ ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
revert a M hn
Proof state after:
n : ℕ
⊢ 0 < n →
    ∀ (a : Fin n → ℤ),
      Function.Injective a →
        (∀ (i : Fin n), 0 < a i) →
          (∀ (i j : Fin n), i < j → a i < a j) →
            ∀ (M : Finset ℤ),
              (∀ m ∈ M, 0 < m) →
                M.card ≤ n - 1 →
                  ∑ i : Fin n, a i ∉ M →
                    ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
n : ℕ
⊢ 0 < n →
    ∀ (a : Fin n → ℤ),
      Function.Injective a →
        (∀ (i : Fin n), 0 < a i) →
          (∀ (i j : Fin n), i < j → a i < a j) →
            ∀ (M : Finset ℤ),
              (∀ m ∈ M, 0 < m) →
                M.card ≤ n - 1 →
                  ∑ i : Fin n, a i ∉ M →
                    ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
induction' n using Nat.strongInductionOn with n ih
Proof state after:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
⊢ 0 < n →
    ∀ (a : Fin n → ℤ),
      Function.Injective a →
        (∀ (i : Fin n), 0 < a i) →
          (∀ (i j : Fin n), i < j → a i < a j) →
            ∀ (M : Finset ℤ),
              (∀ m ∈ M, 0 < m) →
                M.card ≤ n - 1 →
                  ∑ i : Fin n, a i ∉ M →
                    ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
⊢ 0 < n →
    ∀ (a : Fin n → ℤ),
      Function.Injective a →
        (∀ (i : Fin n), 0 < a i) →
          (∀ (i j : Fin n), i < j → a i < a j) →
            ∀ (M : Finset ℤ),
              (∀ m ∈ M, 0 < m) →
                M.card ≤ n - 1 →
                  ∑ i : Fin n, a i ∉ M →
                    ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
intro hn a ainj apos asorted M Mpos Mcard
Proof state after:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have h1 := Classical.em (x ∈ M)
Proof state after:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∈ M ∨ x ∉ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∈ M ∨ x ∉ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have h2 := Classical.em (∃ y, x < y ∧ y ∈ M)
Proof state after:
case ind
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∈ M ∨ x ∉ M
h2 : (∃ y, x < y ∧ y ∈ M) ∨ ¬∃ y, x < y ∧ y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inl.inl
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∈ M
h2 : ∃ y, x < y ∧ y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
sorry
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inl.inr
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∈ M
h2 : ¬∃ y, x < y ∧ y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
sorry
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∉ M
h2 : ∃ y, x < y ∧ y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
obtain ⟨y, hy1, hy2⟩ := h2
Proof state after:
case ind.inr.inl.intro.intro
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∉ M
y : ℤ
hy1 : x < y
hy2 : y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∉ M
y : ℤ
hy1 : x < y
hy2 : y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
let M' := M.filter (fun z ↦ z ≤ x)
Proof state after:
case ind.inr.inl.intro.intro
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∉ M
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M