have h3 : p i ≠ p j := by
  intro hh; rw [EmbeddingLike.apply_eq_iff_eq] at hh; exact h0 hh
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
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