internlm/Lean-Github huggingface dataset:
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
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 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a ((Equiv.refl (Fin n)) j) ∈ M
⊢ False
Tactic:
change z ∈ M at h10
Proof state after:
case ind.inr.inl.intro.intro.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
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
⊢ False
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
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
⊢ False
Tactic:
have h11 : z ∈ M' := by
  rw [Finset.mem_filter]
  exact ⟨h10, h9⟩
Proof state after:
case ind.inr.inl.intro.intro.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
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
h11 : z ∈ M'
⊢ False
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
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
h11 : z ∈ M'
⊢ False
Tactic:
rw [Finset.card_eq_zero] at h7
Proof state after:
case ind.inr.inl.intro.intro.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
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' = ∅
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
h11 : z ∈ M'
⊢ False
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
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' = ∅
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
h11 : z ∈ M'
⊢ False
Tactic:
have h12 := Finset.not_mem_empty z
Proof state after:
case ind.inr.inl.intro.intro.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
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' = ∅
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
h11 : z ∈ M'
h12 : z ∉ ∅
⊢ False
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
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' = ∅
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
h11 : z ∈ M'
h12 : z ∉ ∅
⊢ False
Tactic:
rw [h7] at h11
Proof state after:
case ind.inr.inl.intro.intro.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
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' = ∅
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
h11 : z ∈ ∅
h12 : z ∉ ∅
⊢ False
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inl.intro.intro.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
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' = ∅
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
h11 : z ∈ ∅
h12 : z ∉ ∅
⊢ False
Tactic:
exact h12 h11
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
⊢ z ≤ x
Tactic:
have h49 : ∀ i, 0 ≤ a i := by intro i; exact le_of_lt (apos i)
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
⊢ 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
h49 : ∀ (i : Fin n), 0 ≤ a i
⊢ z ≤ x
Tactic:
have h50 : Finset.filter (fun x ↦ x ≤ i) Finset.univ ⊆
           Finset.filter (fun x ↦ ↑x < n - 1) Finset.univ := by
  intro x hx
  simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hx ⊢
  omega
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
h50 : Finset.filter (fun x => x ≤ i) Finset.univ ⊆ Finset.filter (fun x => ↑x < n - 1) Finset.univ
⊢ 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
h49 : ∀ (i : Fin n), 0 ≤ a i
h50 : Finset.filter (fun x => x ≤ i) Finset.univ ⊆ Finset.filter (fun x => ↑x < n - 1) Finset.univ
⊢ z ≤ x
Tactic:
exact Finset.sum_le_sum_of_subset_of_nonneg h50 fun i_1 a a ↦ h49 i_1
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
⊢ ∀ (i : Fin n), 0 ≤ a i
Tactic:
intro i
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
i : Fin n
⊢ 0 ≤ a i
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
i : Fin n
⊢ 0 ≤ a i
Tactic:
exact le_of_lt (apos i)
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
h49 : ∀ (i : Fin n), 0 ≤ a i
⊢ Finset.filter (fun x => x ≤ i) Finset.univ ⊆ Finset.filter (fun x => ↑x < n - 1) Finset.univ
Tactic:
intro x 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 ∈ Finset.filter (fun x => x ≤ i) Finset.univ
⊢ x ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ