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
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
h40 : Finset.map f Finset.univ = Finset.filter (fun x => ↑x < n - 1) Finset.univ
⊢ ∑ i : Fin n', a' i = ∑ x : Fin n', a (f x)
Tactic:
congr
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
⊢ Finset.map f Finset.univ = Finset.filter (fun x => ↑x < n - 1) 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
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
⊢ x ∈ Finset.map f Finset.univ ↔ x ∈ Finset.filter (fun x => ↑x < n - 1) 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
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
⊢ x ∈ Finset.map f Finset.univ ↔ x ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ
Tactic:
rw [Finset.mem_map, 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
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
⊢ (∃ a ∈ Finset.univ, f a = x) ↔ x ∈ Finset.univ ∧ ↑x < n - 1
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mp
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
⊢ (∃ a ∈ Finset.univ, f a = x) → x ∈ Finset.univ ∧ ↑x < n - 1
Tactic:
rintro ⟨y, hy1, hy2⟩
Proof state after:
case a.mp.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
hyM' : y✝ ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y : Fin n'
hy1 : y ∈ Finset.univ
hy2 : f y = x
⊢ x ∈ Finset.univ ∧ ↑x < n - 1
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mp.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
hyM' : y✝ ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y : Fin n'
hy1 : y ∈ Finset.univ
hy2 : f y = x
⊢ x ∈ Finset.univ ∧ ↑x < n - 1
Tactic:
simp only [Finset.mem_univ, true_and]
Proof state after:
case a.mp.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
hyM' : y✝ ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y : Fin n'
hy1 : y ∈ Finset.univ
hy2 : f y = x
⊢ ↑x < n - 1
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mp.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
hyM' : y✝ ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y : Fin n'
hy1 : y ∈ Finset.univ
hy2 : f y = x
⊢ ↑x < n - 1
Tactic:
rw [←hy2]
Proof state after:
case a.mp.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
hyM' : y✝ ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y : Fin n'
hy1 : y ∈ Finset.univ
hy2 : f y = x
⊢ ↑(f y) < n - 1
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mp.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
hyM' : y✝ ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y : Fin n'
hy1 : y ∈ Finset.univ
hy2 : f y = x
⊢ ↑(f y) < n - 1
Tactic:
obtain ⟨y', hy'⟩ := y
Proof state after:
case a.mp.intro.intro.mk
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y' : ℕ
hy' : y' < n'
hy1 : ⟨y', hy'⟩ ∈ Finset.univ
hy2 : f ⟨y', hy'⟩ = x
⊢ ↑(f ⟨y', hy'⟩) < n - 1
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mp.intro.intro.mk
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
y' : ℕ
hy' : y' < n'
hy1 : ⟨y', hy'⟩ ∈ Finset.univ
hy2 : f ⟨y', hy'⟩ = x
⊢ ↑(f ⟨y', hy'⟩) < n - 1
Tactic:
exact hy'
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mpr
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
⊢ x ∈ Finset.univ ∧ ↑x < n - 1 → ∃ a ∈ Finset.univ, f a = x
Tactic:
rintro ⟨_, h41⟩
Proof state after:
case a.mpr.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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
left✝ : x ∈ Finset.univ
h41 : ↑x < n - 1
⊢ ∃ a ∈ Finset.univ, f a = x
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a.mpr.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
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
left✝ : x ∈ Finset.univ
h41 : ↑x < n - 1
⊢ ∃ a ∈ Finset.univ, f a = x
Tactic:
use ⟨x.val, by omega⟩
Proof state after:
case h
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
left✝ : x ∈ Finset.univ
h41 : ↑x < n - 1
⊢ ⟨↑x, ⋯⟩ ∈ Finset.univ ∧ f ⟨↑x, ⋯⟩ = x
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case h
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
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
f : Fin n' ↪ Fin n := embedFinLE ⋯
x : Fin n
left✝ : x ∈ Finset.univ
h41 : ↑x < n - 1
⊢ ⟨↑x, ⋯⟩ ∈ Finset.univ ∧ f ⟨↑x, ⋯⟩ = x
Tactic:
simp [f, embedFinLE]
Proof state after:
no goals