internlm/Lean-Github huggingface dataset:
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi1 : ↑i < n - 1
z : ℤ := ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a j
h49 : ∀ (i : Fin n), 0 ≤ a i
x : Fin n
hx : x ∈ Finset.filter (fun x => x ≤ i) Finset.univ
⊢ x ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ
Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hx ⊢
Proof state after:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi1 : ↑i < n - 1
z : ℤ := ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a j
h49 : ∀ (i : Fin n), 0 ≤ a i
x : Fin n
hx : x ≤ i
⊢ ↑x < n - 1
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi1 : ↑i < n - 1
z : ℤ := ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a j
h49 : ∀ (i : Fin n), 0 ≤ a i
x : Fin n
hx : x ≤ i
⊢ ↑x < n - 1
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi1 : ↑i < n - 1
z : ℤ := ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a j
h9 : z ≤ x
h10 : z ∈ M
⊢ z ∈ M'
Tactic:
rw [Finset.mem_filter]
Proof state after:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi1 : ↑i < n - 1
z : ℤ := ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a j
h9 : z ≤ x
h10 : z ∈ M
⊢ z ∈ M ∧ z ≤ x
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi1 : ↑i < n - 1
z : ℤ := ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a j
h9 : z ≤ x
h10 : z ∈ M
⊢ z ∈ M ∧ z ≤ x
Tactic:
exact ⟨h10, h9⟩
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a ((Equiv.refl (Fin n)) j) ∉ M
Tactic:
have h9 : i.val + 1 = n := by omega
Proof state after:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a ((Equiv.refl (Fin n)) j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a ((Equiv.refl (Fin n)) j) ∉ M
Tactic:
have h10 : Finset.filter (fun x ↦ x ≤ i) Finset.univ =
            Finset.univ (α := Fin n) := by
  ext x
  rw [Finset.mem_filter]
  suffices x ≤ i from and_iff_left_of_imp fun a ↦ this
  omega
Proof state after:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a ((Equiv.refl (Fin n)) j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a ((Equiv.refl (Fin n)) j) ∉ M
Tactic:
rw [h10]
Proof state after:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j : Fin n, a ((Equiv.refl (Fin n)) j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
y : ℤ
hy1 : x < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j : Fin n, a ((Equiv.refl (Fin n)) j) ∉ M
Tactic:
exact hM
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
⊢ ↑i + 1 = n
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
⊢ Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
Tactic:
ext x
Proof state after:
case a
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.filter (fun x => x ≤ i) Finset.univ ↔ x ∈ Finset.univ
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.filter (fun x => x ≤ i) Finset.univ ↔ x ∈ Finset.univ
Tactic:
rw [Finset.mem_filter]
Proof state after:
case a
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.univ ∧ x ≤ i ↔ x ∈ Finset.univ
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.univ ∧ x ≤ i ↔ x ∈ Finset.univ
Tactic:
suffices x ≤ i from and_iff_left_of_imp fun a ↦ this
Proof state after:
case a
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
x : Fin n
⊢ x ≤ i
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card = 0
i : Fin n
hi2 : ¬↑i < n - 1
h9 : ↑i + 1 = n
x : Fin n
⊢ x ≤ i
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
i : Fin n'
⊢ ↑i < n
Tactic:
omega
Proof state after:
no goals