-- Mathlib/Order/WellFoundedSet.lean
theorem Pi.isPWO {α : ι → Type*} [∀ i, LinearOrder (α i)] [∀ i, IsWellOrder (α i) (· < ·)]
    [Finite ι] (s : Set (∀ i, α i)) : s.IsPWO

Proof state:
case intro.refine_2
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : x ∉ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x_1 ∈ Finset.cons x s hx, (f ∘ ⇑g) a x_1 ≤ (f ∘ ⇑g) b x_1

Tactic:
obtain ⟨g, hg⟩ :=
  (IsWellFounded.wf.isWF univ).isPWO.exists_monotone_subseq (fun n => f n x) mem_univ

Result:
case intro.refine_2.intro
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : x ∉ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ⇑g)
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x_1 ∈ Finset.cons x s hx, (f ∘ ⇑g) a x_1 ≤ (f ∘ ⇑g) b x_1

Proof state:
case intro.refine_1
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ ∅, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x

Tactic:
intro f

Result:
case intro.refine_1
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ ∅, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x

Proof state:
case intro.refine_2
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x) →
      ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ x ∈ Finset.cons a s h, (f ∘ ⇑g) a_2 x ≤ (f ∘ ⇑g) b x

Tactic:
intro x s hx ih f

Result:
case intro.refine_2
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : x ∉ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x_1 ∈ Finset.cons x s hx, (f ∘ ⇑g) a x_1 ≤ (f ∘ ⇑g) b x_1

Proof state:
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ s.IsPWO

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ s.IsPWO

Proof state:
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this : ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
⊢ s.IsPWO

Tactic:
refine isPWO_iff_exists_monotone_subseq.2 fun f _ => ?_

Result:
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this : ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
f : ℕ → (i : ι) → α i
x✝ : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, Monotone (f ∘ ⇑g)

Proof state:
case intro.refine_1
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
f : ℕ → (s : ι) → α s
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ x ∈ ∅, (f ∘ ⇑(RelEmbedding.refl fun x1 x2 => x1 ≤ x2)) a x ≤ (f ∘ ⇑(RelEmbedding.refl fun x1 x2 => x1 ≤ x2)) b x

Tactic:
simp only [IsEmpty.forall_iff, imp_true_iff, forall_const, Finset.not_mem_empty]

Result:
no goals

Proof state:
case intro
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ s.IsPWO

Tactic:
suffices ∀ (s : Finset ι) (f : ℕ → ∀ s, α s),
  ∃ g : ℕ ↪o ℕ, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x, x ∈ s → (f ∘ g) a x ≤ (f ∘ g) b x by
  refine isPWO_iff_exists_monotone_subseq.2 fun f _ => ?_
  simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f

Result:
case intro
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x

Proof state:
case intro
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x

Tactic:
refine Finset.cons_induction ?_ ?_

Result:
case intro.refine_1
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ ∅, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x

case intro.refine_2
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x) →
      ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ x ∈ Finset.cons a s h, (f ∘ ⇑g) a_2 x ≤ (f ∘ ⇑g) b x

Proof state:
ι : Type u_1
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x1 x2 => x1 < x2
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this : ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
f : ℕ → (i : ι) → α i
x✝ : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, Monotone (f ∘ ⇑g)

Tactic:
simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f

Result:
no goals