-- 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.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

Tactic:
obtain ⟨g', hg'⟩ := ih (f ∘ g)

Result:
case intro.refine_2.intro.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' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, ((f ∘ ⇑g) ∘ ⇑g') a x ≤ ((f ∘ ⇑g) ∘ ⇑g') b x
⊢ ∃ 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_2.intro.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' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ 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 ∈ s, (f ∘ ⇑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ⇑(RelEmbedding.trans g' g)) b x

Tactic:
exact ⟨hg (OrderHomClass.mono g' hab), hg' hab⟩

Result:
no goals

Proof state:
case intro.refine_2.intro.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' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, ((f ∘ ⇑g) ∘ ⇑g') a x ≤ ((f ∘ ⇑g) ∘ ⇑g') b x
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x_1 ∈ Finset.cons x s hx, (f ∘ ⇑g) a x_1 ≤ (f ∘ ⇑g) b x_1

Tactic:
refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩

Result:
case intro.refine_2.intro.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' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ 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 ∈ s, (f ∘ ⇑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ⇑(RelEmbedding.trans g' g)) b x