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

State before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
⊢ ∃ p, ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
obtain ⟨p, hp⟩ := lemma1 n a
State after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∃ p, ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j

State before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∃ p, ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
refine ⟨p, ?_⟩
State after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j

State before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
⊢ ∀ (i j : Fin n), i < j → (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
intro i j hij
State after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j

State before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
have h0 := ne_of_lt hij
State after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j

State before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
have h2 := hp i j (le_of_lt hij)
State after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j

State before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
have h3 : p i ≠ p j := by
  intro hh; rw [EmbeddingLike.apply_eq_iff_eq] at hh; exact h0 hh
State after:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
h3 : p i ≠ p j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j

State before:
case intro
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
h3 : p i ≠ p j
⊢ (a ∘ ⇑p) i < (a ∘ ⇑p) j
Tactic:
exact lt_of_le_of_ne h2 fun a ↦ h3 (ainj a)
State after:
no goals

State before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ p i ≠ p j
Tactic:
intro hh
State after:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : p i = p j
⊢ False

State before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : p i = p j
⊢ False
Tactic:
rw [EmbeddingLike.apply_eq_iff_eq] at hh
State after:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : i = j
⊢ False

State before:
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : i = j
⊢ False
Tactic:
exact h0 hh
State after:
no goals