awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
h' : f c = f c'
h'' :
  rπ (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
    (Eq.rec (motive :=
      fun (x : ι)
        (x_1 :
          Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c) =
            x) ↦
      π x) (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
      h')
    (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
h₁ :
  Eq (α := (a : { x : ι // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c ⋯))
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯)
      (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)}) c h'))
inr : { x : γ // x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)} }
inr₁ :
  Subrel
    (Function.onFun (β := π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι))
      (rπ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι))
      (g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)))
    (fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)})
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)}) c h')
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' ⋯)
⊢ PSigma.Lex (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (Subrel rι fun (x : ι) ↦ x ∈ range f)
    (fun (a : { x : ι // x ∈ range f }) ↦
      Subrel (Function.onFun (β := π (↑a : ι)) (rπ (↑a : ι)) (g (↑a : ι))) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : ι)})
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c ⋯))
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' ⋯))

Tactic:
convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1

Premises used: PSigma.Lex.right, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
h' : f c = f c'
h'' :
  rπ (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
    (Eq.rec (motive :=
      fun (x : ι)
        (x_1 :
          Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c) =
            x) ↦
      π x) (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
      h')
    (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
⊢ { x : γ // x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)} }

Tactic:
exact ⟨c, h'⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
h' : f c = f c'
h'' :
  rπ (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
    (Eq.rec (motive :=
      fun (x : ι)
        (x_1 :
          Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c) =
            x) ↦
      π x) (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
      h')
    (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
⊢ Eq (α := (a : { x : ι // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c ⋯))
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯)
      (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)}) c h'))

Tactic:
PSigma.subtype_ext (Subtype.ext h') rfl

Premises used: PSigma.subtype_ext, rfl, Subtype.ext
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
h' : f c = f c'
h'' :
  rπ (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
    (Eq.rec (motive :=
      fun (x : ι)
        (x_1 :
          Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c) =
            x) ↦
      π x) (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
      h')
    (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
⊢ Eq (α := (a : { x : ι // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c ⋯))
    (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯)
      (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)}) c h'))

Tactic:
exact PSigma.subtype_ext (Subtype.ext h') rfl

Premises used: PSigma.subtype_ext, rfl, Subtype.ext
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
h' : f c = f c'
h'' :
  rπ (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
    (Eq.rec (motive :=
      fun (x : ι)
        (x_1 :
          Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c) =
            x) ↦
      π x) (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
      h')
    (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
inr : Function.onFun (β := π (f c')) (rπ (f c')) (g (f c')) c c'
⊢ Subrel
    (Function.onFun (β := π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι))
      (rπ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι))
      (g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)))
    (fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)})
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') ⋯) : ι)}) c h')
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' ⋯)

Tactic:
dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *

Premises used: Subtype.coe_mk, Subrel, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
h' : f c = f c'
h'' : rπ (f c') (Eq.rec (motive := fun (x : ι) (x_1 : f c = x) ↦ π x) (g (f c) c) h') (g (f c') c')
⊢ Function.onFun (β := π (f c')) (rπ (f c')) (g (f c')) c c'

Tactic:
grind
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ WellFounded.{u_4 + 1} (α := (↑s : Type u_4))
    (Sigma.Lex (α := π) rι rπ on fun (c : (↑s : Type u_4)) ↦
      Sigma.mk (β := fun (i : ι) ↦ π i) (f (↑c : γ)) (g (f (↑c : γ)) (↑c : γ)))

Tactic:
@WellFounded.sigma_lex_of_wellFoundedOn_fiber _ s _ _ rπ (fun c => f c) (fun i c => g _ c) hι
      fun i => ((hπ i).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun b c h => ‹_›)

Premises used: WellFounded.onFun, WellFounded.sigma_lex_of_wellFoundedOn_fiber, WellFounded.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ WellFounded.{u_4 + 1} (α := (↑s : Type u_4))
    (Sigma.Lex (α := π) rι rπ on fun (c : (↑s : Type u_4)) ↦
      Sigma.mk (β := fun (i : ι) ↦ π i) (f (↑c : γ)) (g (f (↑c : γ)) (↑c : γ)))

Tactic:
exact
    @WellFounded.sigma_lex_of_wellFoundedOn_fiber _ s _ _ rπ (fun c => f c) (fun i c => g _ c) hι
      fun i => ((hπ i).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun b c h => ‹_›)

Premises used: WellFounded.onFun, WellFounded.sigma_lex_of_wellFoundedOn_fiber, WellFounded.mono
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : IsEmpty α
r : α → α → Prop
⊢ WellQuasiOrdered r

Tactic:
fun f ↦ isEmptyElim (f 0)

Premises used: isEmptyElim, WellQuasiOrdered, OfNat.ofNat
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
by_contra! : ∀ (hi : s.Infinite), False
⊢ s.Finite

Tactic:
by_contra! hi
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
obtain :
  ∀ (m n : ℕ) (hmn : m < n)
    (h :
      r (↑((Set.Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_1)) m) : α)
        (↑((Set.Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_1)) n) : α)),
    False
⊢ False

Tactic:
obtain ⟨m, n, hmn, h⟩ := hr fun n => hi.natEmbedding _ n

Premises used: Set.Infinite.natEmbedding, Subtype.val, DFunLike.coe
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
m n : ℕ
hmn : m < n
h :
  r (↑((Set.Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_1)) m) : α)
    (↑((Set.Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_1)) n) : α)
⊢ False

Tactic:
hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    hs.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Premises used: Subtype.val_injective, Set.Infinite.natEmbedding, Function.Embedding.injective, IsAntichain.eq, DFunLike.coe, LT.lt.ne, Subtype.property
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
m n : ℕ
hmn : m < n
h :
  r (↑((Set.Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_1)) m) : α)
    (↑((Set.Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_1)) n) : α)
⊢ False

Tactic:
exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    hs.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Premises used: Subtype.val_injective, Set.Infinite.natEmbedding, Function.Embedding.injective, IsAntichain.eq, DFunLike.coe, LT.lt.ne, Subtype.property
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : Finite α
inst_1 : Std.Refl r
f : ℕ → α
obtain : ∀ (m n : ℕ) (h : m < n) (hf : f m = f n), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨m, n, h, hf⟩ := Set.finite_univ.exists_lt_map_eq_of_forall_mem (f := f)
    fun _ ↦ Set.mem_univ _

Premises used: Set.finite_univ, Set.Finite.exists_lt_map_eq_of_forall_mem, Set.mem_univ
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : Finite α
inst_1 : Std.Refl r
f : ℕ → α
m n : ℕ
h : m < n
hf : f m = f n
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
⟨m, n, h, hf ▸ refl _⟩

Premises used: Eq.rec, And.intro, Exists.intro, refl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : Finite α
inst_1 : Std.Refl r
f : ℕ → α
m n : ℕ
h : m < n
hf : f m = f n
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
exact ⟨m, n, h, hf ▸ refl _⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
inl :
  ∀ (g : ℕ ↪o ℕ) (h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))),
    ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
inr :
  ∀ (g : ℕ ↪o ℕ) (h2 : ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))),
    ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f

Premises used: exists_increasing_or_nonincreasing_subseq
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
⟨g, fun m n hle => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
inl : ∀ (m n : ℕ) (hle : m ≤ n), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
refine ⟨g, fun m n hle => ?_⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
m n : ℕ
hle : m ≤ n
inl : ∀ (hlt : m < n), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
inl₁ : ∀ (hle : m ≤ m), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) m))
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
obtain hlt | rfl := hle.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
h1 m n hlt
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
m : ℕ
hle : m ≤ m
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) m))

Tactic:
refl_of r _

Premises used: refl_of
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
exacts [h1 m n hlt, refl_of r _]

Premises used: refl_of
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
inr :
  ∀ (m n : ℕ) (hlt : m < n) (hle : r ((f ∘ (⇑g : (a : ℕ) → ℕ)) m) ((f ∘ (⇑g : (a : ℕ) → ℕ)) n)),
    ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)

Premises used: Function.comp, DFunLike.coe
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
m n : ℕ
hlt : m < n
hle : r ((f ∘ (⇑g : (a : ℕ) → ℕ)) m) ((f ∘ (⇑g : (a : ℕ) → ℕ)) n)
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
cases h2 m n hlt hle
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
mp :
  WellQuasiOrdered r →
    ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
mpr :
  (∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    WellQuasiOrdered r
⊢ WellQuasiOrdered r ↔
    ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
constructor
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
h.exists_monotone_subseq f

Premises used: WellQuasiOrdered.exists_monotone_subseq
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
exact h.exists_monotone_subseq f

Premises used: WellQuasiOrdered.exists_monotone_subseq
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
f : ℕ → α
mpr :
  ∀ (g : ℕ ↪o ℕ) (gmon : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨g, gmon⟩ := h f
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
f : ℕ → α
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

Premises used: Nat.zero_le, OrderEmbedding.strictMono, And.intro, Exists.intro, OfNat.ofNat, Nat.zero_lt_one
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
f : ℕ → α
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
obtain :
  ∀ (g : ℕ ↪o ℕ)
    (h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) m)) ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) n))),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)

Premises used: Function.comp, Prod.fst, WellQuasiOrdered.exists_monotone_subseq
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) m)) ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) n))
obtain :
  ∀ (m n : ℕ) (h : m < n) (hf : s ((Prod.snd ∘ f ∘ (⇑g : (a : ℕ) → ℕ)) m) ((Prod.snd ∘ f ∘ (⇑g : (a : ℕ) → ℕ)) n)),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)

Premises used: Function.comp, Prod.snd, DFunLike.coe
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) m)) ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) n))
m n : ℕ
h : m < n
hf : s ((Prod.snd ∘ f ∘ (⇑g : (a : ℕ) → ℕ)) m) ((Prod.snd ∘ f ∘ (⇑g : (a : ℕ) → ℕ)) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩

Premises used: OrderEmbedding.strictMono, LT.lt.le, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) m)) ((Prod.fst ∘ f) ((g : (a : ℕ) → ℕ) n))
m n : ℕ
h : m < n
hf : s ((Prod.snd ∘ f ∘ (⇑g : (a : ℕ) → ℕ)) m) ((Prod.snd ∘ f ∘ (⇑g : (a : ℕ) → ℕ)) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
ι : Type u_3
α : ι → Type u_4
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
haveI : ∀ (this : Fintype ι), WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
⊢ WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
ι : Type u_3
α : ι → Type u_4
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this : Fintype ι
⊢ IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
haveI : IsPreorder (∀ i, α i) (fun a b : ∀ i, α i => ∀ i, r i (a i) (b i)) :=
    { refl a i := refl (a i)
      trans a b c hab hbc i := _root_.trans (hab i) (hbc i) }