awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
this : f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ) : ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ) : ℕ) ∧
    f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))

Tactic:
simpa
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
h : f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ) : ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ) : ℕ) ∧
    f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))

Tactic:
suffices (f (g (g' 0))) ≤ (f (g (g' 1))) by simpa
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
⊢ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))

Tactic:
Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, Prod.Lex.toLex_le_toLex, Or.inr
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
h : (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).1 = (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).1
h₁ : (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).2 ≤ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).2
⊢ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))

Tactic:
refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩

Premises used: Iff.mpr, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
⊢ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).1 = (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).1

Tactic:
(hhc (g' 0)).symm.trans (hhc (g' 1))

Premises used: OfNat.ofNat, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
⊢ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).1 = (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).1

Tactic:
exact (hhc (g' 0)).symm.trans (hhc (g' 1))

Premises used: OfNat.ofNat, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
⊢ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).2 ≤ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).2

Tactic:
hg' (Nat.zero_le 1)

Premises used: Nat.zero_le, OfNat.ofNat
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
⊢ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).2 ≤ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).2

Tactic:
exact hg' (Nat.zero_le 1)

Premises used: Nat.zero_le, OfNat.ofNat
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
⊢ IsPWO.{u_2} (α := α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s)

Tactic:
IsPWO.image_of_monotone hαβ Prod.Lex.monotone_fst

Premises used: Prod.Lex.monotone_fst, Set.IsPWO.image_of_monotone
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  ∀ (x : β),
    Membership.mem (γ := Set β)
        {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} x ↔
      x ∈ f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
⊢ {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})

Tactic:
ext x
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
x : β
⊢ Membership.mem (γ := Set β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} x ↔
    x ∈ f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})

Tactic:
simp [f]
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
⊢ {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})

Tactic:
have h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a}) := by
    ext x
    simp [f]
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
rw : (f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})).IsPWO
⊢ IsPWO.{u_3} (α := β)
    {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}

Tactic:
rw [h]
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
apply : MonotoneOn f (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
⊢ (f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})).IsPWO

Tactic:
apply IsPWO.image_of_monotoneOn (hαβ.mono inter_subset_left)

Premises used: Set.IsPWO.image_of_monotoneOn, Set.inter_subset_left, Set.IsPWO.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b : Lex (α × β)
hb :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) b
c : Lex (α × β)
hc :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) c
hbc : b ≤ c
⊢ ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a

Tactic:
simp only [mem_preimage, mem_singleton_iff] at hb hc

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b : Lex (α × β)
hb :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) b
c : Lex (α × β)
hc :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) c
hbc : b ≤ c
hb₁ : ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a
⊢ ((ofLex : (a : Lex (α × β)) → α × β) c).1 = a

Tactic:
simp only [mem_preimage, mem_singleton_iff] at hb hc

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a
hc : ((ofLex : (a : Lex (α × β)) → α × β) c).1 = a
⊢ LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) b).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1 ∨
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) b).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1 ∧
      f b ≤ f c

Tactic:
have : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c :=
    Prod.Lex.toLex_le_toLex.mp hbc
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a
hc : ((ofLex : (a : Lex (α × β)) → α × β) c).1 = a
this :
  LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) b).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1 ∨
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) b).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1 ∧
      f b ≤ f c
⊢ f b ≤ f c

Tactic:
simp_all only [lt_self_iff_false, true_and, false_or]

Premises used: false_or, lt_self_iff_false, true_and
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
⊢ s.IsPWO ↔
    IsPWO.{u_2} (α := α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) ∧
      ∀ (a : α),
        IsPWO.{u_3} (α := β)
          {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}

Tactic:
⟨fun h ↦ ⟨imageProdLex h, fiberProdLex h⟩, fun h ↦ subsetProdLex h.1 h.2⟩

Premises used: Set.PartiallyWellOrderedOn.subsetProdLex, Set.PartiallyWellOrderedOn.imageProdLex, Set.PartiallyWellOrderedOn.fiberProdLex, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
⊢ WellFounded.{u_4 + 1} (α := γ) (Prod.Lex rα rβ on fun (c : γ) ↦ (f c, g c))

Tactic:
((psigma_lex (wellFoundedOn_range.2 hα) fun a => hβ a).onFun
    (f := fun c => ⟨⟨_, c, rfl⟩, c, rfl⟩)).mono fun c c' h => ?_

Premises used: Iff.mpr, WellFounded.psigma_lex, Set.wellFoundedOn_range, WellFounded.onFun, WellFounded.mono, Subtype.val