Theorem: Imo2009P6.imo2009_p6_aux1 (Compfiles/Imo2009P6.lean)

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⟩
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

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]
State after:
no goals

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 ⋯
x : Fin n
left✝ : x ∈ Finset.univ
h41 : ↑x < n - 1
⊢ ↑x < n'
Tactic:
omega
State after:
no goals

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
hM' : ∑ i : Fin n', a' i ∉ M'
⊢ n' < n
Tactic:
omega
State after:
no goals

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
hM' : ∑ i : Fin n', a' i ∉ M'
⊢ 0 < n'
Tactic:
omega
State after:
no goals

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
hM' : ∑ i : Fin n', a' i ∉ M'
⊢ M'.card ≤ n' - 1
Tactic:
omega
State after:
no goals

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
let i' : Fin n' := ⟨i.val, h30⟩
State after:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have h31 := hp i'
State after:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 : ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∉ M'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 : ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∉ M'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
rw [Finset.mem_filter] at h31
State after:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ≤ x)
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ≤ x)
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have h35 : n' ≤ n := Nat.sub_le n 1
State after:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ≤ x)
h35 : n' ≤ n
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ≤ x)
h35 : n' ≤ n
h33 :
  ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
rw [h33] at h31
State after:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x)
h35 : n' ≤ n
h33 :
  ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x)
h35 : n' ≤ n
h33 :
  ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
h34 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
intro H
State after:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x)
h35 : n' ≤ n
h33 :
  ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
h34 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x
H : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M
⊢ False

State before:
case ind.inr.inl.intro.intro.inr.intro.inl
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x)
h35 : n' ≤ n
h33 :
  ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
h34 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x
H : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M
⊢ False
Tactic:
exact (h31 ⟨H, h34⟩).elim
State after:
no goals

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) ≤ x)
h35 : n' ≤ n
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
Tactic:
sorry
State after:
no goals

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ↑i < n'
i' : Fin n' := ⟨↑i, h30⟩
h31 :
  ¬(∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∈ M ∧
      ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x)
h35 : n' ≤ n
h33 :
  ∑ j ∈ Finset.filter (fun x => x ≤ i') Finset.univ, a' (p' j) =
    ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j)
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ≤ x
Tactic:
sorry
State after:
no goals

State before:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have h31 : i.val = n' := by omega
State after:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have h32 : ∑ j ∈ Finset.filter (fun x ↦ x ≤ i) Finset.univ, a (p j) =
           ∑ i : Fin n, a i := by
  have pb : p.toFun.Bijective := EquivLike.bijective p
  rw [←Function.Bijective.sum_comp pb (fun j ↦ a j)]
  have h33 : i.val + 1 = n := by omega
  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
  rw [h10]
  dsimp
State after:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
h32 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
h32 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
rw [h32]
State after:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
h32 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i
⊢ ∑ i : Fin n, a i ∉ M

State before:
case ind.inr.inl.intro.intro.inr.intro.inr
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
h32 : ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i
⊢ ∑ i : Fin n, a i ∉ M
Tactic:
exact hM
State after:
no goals

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
⊢ ↑i = n'
Tactic:
omega
State after:
no goals

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i
Tactic:
have pb : p.toFun.Bijective := EquivLike.bijective p
State after:
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a i
Tactic:
rw [←Function.Bijective.sum_comp pb (fun j ↦ a j)]
State after:
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a (p.toFun i)

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a (p.toFun i)
Tactic:
have h33 : i.val + 1 = n := by omega
State after:
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a (p.toFun i)

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a (p.toFun i)
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
State after:
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a (p.toFun i)

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) = ∑ i : Fin n, a (p.toFun i)
Tactic:
rw [h10]
State after:
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j : Fin n, a (p j) = ∑ i : Fin n, a (p.toFun i)

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
h10 : Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
⊢ ∑ j : Fin n, a (p j) = ∑ i : Fin n, a (p.toFun i)
Tactic:
dsimp
State after:
no goals

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
⊢ ↑i + 1 = n
Tactic:
omega
State after:
no goals

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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
⊢ Finset.filter (fun x => x ≤ i) Finset.univ = Finset.univ
Tactic:
ext x
State after:
case a
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.filter (fun x => x ≤ i) Finset.univ ↔ x ∈ Finset.univ

State before:
case a
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.filter (fun x => x ≤ i) Finset.univ ↔ x ∈ Finset.univ
Tactic:
rw [Finset.mem_filter]
State after:
case a
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.univ ∧ x ≤ i ↔ x ∈ Finset.univ

State before:
case a
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑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
State after:
case a
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ≤ i

State before:
case a
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
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
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ≤ i
Tactic:
omega
State after:
no goals

State before:
case ind.inr.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
State after:
no goals