case intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ IsPwo s
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ IsPwo s
cases nonempty_fintype ι
case intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
case intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ IsPwo s
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
case intro.refine'_1
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ ∅ → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x

case intro.refine'_2
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι} (h : ¬a ∈ s),
    (∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x) →
      ∀ (f : ℕ → (s : ι) → α s),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ (x : ι), x ∈ Finset.cons a s h → (f ∘ ↑g) a_2 x ≤ (f ∘ ↑g) b x
case intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
refine' Finset.cons_induction _ _
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this :
  ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (i : ι) → α i
x✝ : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, Monotone (f ∘ ↑g)
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this :
  ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
⊢ IsPwo s
refine isPwo_iff_exists_monotone_subseq.2 fun f _ => ?_
no goals
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this :
  ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (i : ι) → α i
x✝ : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, Monotone (f ∘ ↑g)
simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f
case intro.refine'_1
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ ∅ → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
case intro.refine'_1
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ ∅ → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
intro f
no goals
case intro.refine'_1
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
f : ℕ → (s : ι) → α s
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ (x : ι),
        x ∈ ∅ →
          (f ∘ ↑(RelEmbedding.refl fun x x_1 => x ≤ x_1)) a x ≤ (f ∘ ↑(RelEmbedding.refl fun x x_1 => x ≤ x_1)) b x
simp only [IsEmpty.forall_iff, imp_true_iff, forall_const, Finset.not_mem_empty]
case intro.refine'_2
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
case intro.refine'_2
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι} (h : ¬a ∈ s),
    (∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x) →
      ∀ (f : ℕ → (s : ι) → α s),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ (x : ι), x ∈ Finset.cons a s h → (f ∘ ↑g) a_2 x ≤ (f ∘ ↑g) b x
intro x s hx ih f
case intro.refine'_2.intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), 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 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
case intro.refine'_2
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
obtain ⟨g, hg⟩ :=
  (IsWellFounded.wf.isWf univ).isPwo.exists_monotone_subseq (fun n => f n x) mem_univ
case intro.refine'_2.intro.intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → ((f ∘ ↑g) ∘ ↑g') a x ≤ ((f ∘ ↑g) ∘ ↑g') b x
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
case intro.refine'_2.intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), 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 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
obtain ⟨g', hg'⟩ := ih (f ∘ g)
case intro.refine'_2.intro.intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → ((f ∘ ↑g) ∘ ↑g') a x ≤ ((f ∘ ↑g) ∘ ↑g') b x
a b : ℕ
hab : a ≤ b
⊢ (f ∘ ↑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ↑(RelEmbedding.trans g' g)) b x ∧
    ∀ (x : ι), x ∈ s → (f ∘ ↑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ↑(RelEmbedding.trans g' g)) b x
case intro.refine'_2.intro.intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → ((f ∘ ↑g) ∘ ↑g') a x ≤ ((f ∘ ↑g) ∘ ↑g') b x
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
refine' ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 _⟩
no goals
case intro.refine'_2.intro.intro
ι : Type u_2
α✝ : Type ?u.162951
β : Type ?u.162954
α : ι → Type u_1
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → ((f ∘ ↑g) ∘ ↑g') a x ≤ ((f ∘ ↑g) ∘ ↑g') b x
a b : ℕ
hab : a ≤ b
⊢ (f ∘ ↑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ↑(RelEmbedding.trans g' g)) b x ∧
    ∀ (x : ι), x ∈ s → (f ∘ ↑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ↑(RelEmbedding.trans g' g)) b x
exact ⟨hg (OrderHomClass.mono g' hab), hg' hab⟩