[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
⊢ P (f ∘ ↑(sort f))
[PROOFSTEP]
letI := @Preorder.lift _ (Lex (Fin n → α)) _ fun σ : Equiv.Perm (Fin n) => toLex (f ∘ σ)
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => ↑toLex (f ∘ ↑σ)
⊢ P (f ∘ ↑(sort f))
[PROOFSTEP]
refine'
  @WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·)) (Equiv.refl _) (sort f) P (fun σ => f ∘ σ)
    (fun σ hσ hfσ => _) hf
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => ↑toLex (f ∘ ↑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ↑σ) σ ≠ (fun σ => f ∘ ↑σ) (sort f)
hfσ : P ((fun σ => f ∘ ↑σ) σ)
⊢ ∃ c, c < σ ∧ P ((fun σ => f ∘ ↑σ) c)
[PROOFSTEP]
obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ
[GOAL]
case intro.intro.intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => ↑toLex (f ∘ ↑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ↑σ) σ ≠ (fun σ => f ∘ ↑σ) (sort f)
hfσ : P ((fun σ => f ∘ ↑σ) σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ ↑σ) j < (f ∘ ↑σ) i
⊢ ∃ c, c < σ ∧ P ((fun σ => f ∘ ↑σ) c)
[PROOFSTEP]
exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩
