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))
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))
letI := @Preorder.lift _ (Lex (Fin n → α)) _ fun σ : Equiv.Perm (Fin n) => toLex (f ∘ σ)
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 ∘ ↑σ)
σ : Equiv.Perm (Fin n)
hσ : (fun σ => f ∘ ↑σ) σ ≠ (fun σ => f ∘ ↑σ) (sort f)
hfσ : P ((fun σ => f ∘ ↑σ) σ)
⊢ ∃ c, c < σ ∧ P ((fun σ => f ∘ ↑σ) c)
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))
refine'
  @WellFounded.induction_bot' _ _ _ (@Finite.Preorder.wellFounded_lt (Equiv.Perm (Fin n)) _ _)
    (Equiv.refl _) (sort f) P (fun σ => f ∘ σ) (fun σ hσ hfσ => _) hf
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 ∘ ↑σ)
σ : Equiv.Perm (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)
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 ∘ ↑σ)
σ : Equiv.Perm (Fin n)
hσ : (fun σ => f ∘ ↑σ) σ ≠ (fun σ => f ∘ ↑σ) (sort f)
hfσ : P ((fun σ => f ∘ ↑σ) σ)
⊢ ∃ c, c < σ ∧ P ((fun σ => f ∘ ↑σ) c)
obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ
no goals
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 ∘ ↑σ)
σ : Equiv.Perm (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)
exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁ hij₂, h σ i j hij₁ hij₂ hfσ⟩