awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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'))
⊢ 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' ⋯))
have inr : { x : γ // x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι)} }
Tactic: convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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') ⋯) : ι)} }
⊢ 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' ⋯))
have inr₁ : Subrel
  (Function.onFun (β := π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι))
    (rπ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι))
    (g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι)))
  (fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι)})
  (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι)}) c h')
  (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' sorry)
Tactic: convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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'))
⊢ 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' ⋯)
have inr : Function.onFun (β := π (f c')) (rπ (f c')) (g (f c')) c c'
Tactic: dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
⊢ s.Finite
have by_contra! : ∀ (hi : s.Infinite), False
Tactic: by_contra! hi
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
⊢ False
have 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
Tactic: obtain ⟨m, n, hmn, h⟩ := hr fun n => hi.natEmbedding _ n
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Finite α
inst_1 : Std.Refl r
f : ℕ → α
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have obtain : ∀ (m n : ℕ) (h : m < n) (hf : 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 _
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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))
have 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))
Tactic: obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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))
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have 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))
Tactic: obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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))
have inl : ∀ (m n : ℕ) (hle : m ≤ n), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
Tactic: refine ⟨g, fun m n hle => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have inl : ∀ (hlt : m < n), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
Tactic: obtain hlt | rfl := hle.lt_or_eq
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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))
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have inl₁ : ∀ (hle : m ≤ m), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) m))
Tactic: obtain hlt | rfl := hle.lt_or_eq
Cleared hypotheses: n, hle
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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))
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have 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))
Tactic: obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
⊢ WellQuasiOrdered r ↔
    ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have mp : WellQuasiOrdered r →
  ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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))
⊢ WellQuasiOrdered r ↔
    ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have mpr : (∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
  WellQuasiOrdered r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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 : ℕ → α
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have 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)
Tactic: obtain ⟨g, gmon⟩ := h f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)
have 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)
Tactic: obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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 : ℕ), m < n ∧ (fun (a b : α × β) ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)
have 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)
Tactic: obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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)
⊢ WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have haveI : ∀ (this : Fintype ι), WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (hypothesis)
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 ι
⊢ WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have this₁ : 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) }
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this_2 : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
⊢ WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have rw : ∀ (f : ℕ → (i : ι) → α i),
  ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
Tactic: rw [wellQuasiOrdered_iff_exists_monotone_subseq]
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) 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)
have suffices : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i),
  ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
Tactic: suffices ∀ (s : Finset ι) (f : ℕ → ∀ i, α i),
    ∃ g : ℕ ↪o ℕ, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i, i ∈ s → r i ((f ∘ g) a i) ((f ∘ g) b i) by
    rw [wellQuasiOrdered_iff_exists_monotone_subseq]
    intro f
    simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
have refine_1 : ∀ (f : ℕ → (i : ι) → α i),
  ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ (i : ι),
          Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
Tactic: refine Finset.cons_induction ?_ ?_
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
refine_1 :
  ∀ (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ),
      ∀ ⦃a b : ℕ⦄,
        a ≤ b →
          ∀ (i : ι),
            Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
⊢ ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
have refine_2 : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  (∀ (f : ℕ → (i : ι) → α i),
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)) →
    ∀ (f : ℕ → (i : ι) → α i),
      ∃ (g : ℕ ↪o ℕ),
        ∀ ⦃a_2 b : ℕ⦄,
          a_2 ≤ b → ∀ i ∈ Finset.cons a s h, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a_2 i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
Tactic: refine Finset.cons_induction ?_ ?_
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
f : ℕ → (i : ι) → α i
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ (i : ι),
          Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
have refine_1 : ∀ ⦃a b : ℕ⦄,
  a ≤ b →
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        r i ((f ∘ (⇑(RelEmbedding.refl fun (x1 x2 : ℕ) ↦ x1 ≤ x2) : (a : ℕ) → ℕ)) a i)
          ((f ∘ (⇑(RelEmbedding.refl fun (x1 x2 : ℕ) ↦ x1 ≤ x2) : (a : ℕ) → ℕ)) b i)
Tactic: exists RelEmbedding.refl (· ≤ ·)
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
have refine_2 : ∀ (g : ℕ ↪o ℕ) (hg : ∀ (m n : ℕ), m ≤ n → r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)),
  ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
Tactic: obtain ⟨g, hg⟩ := (hr i).exists_monotone_subseq (f · i)
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
have refine_2 : ∀ (g' : ℕ ↪o ℕ)
  (hg' :
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ i ∈ s,
          r i (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) a i)
            (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) b i)),
  ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
Tactic: obtain ⟨g', hg'⟩ := ih (f ∘ g)
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
g' : ℕ ↪o ℕ
hg' :
  ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ i ∈ s,
        r i (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) a i)
          (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) b i)
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
have refine_2 : ∀ (a b : ℕ) (hab : a ≤ b),
  r i
      ((f ∘
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
            (a : ℕ) → ℕ))
        a i)
      ((f ∘
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
            (a : ℕ) → ℕ))
        b i) ∧
    ∀ x ∈ s,
      r x
        ((f ∘
            (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                  fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
              (a : ℕ) → ℕ))
          a x)
        ((f ∘
            (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                  fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
              (a : ℕ) → ℕ))
          b x)
Tactic: refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ WellQuasiOrdered r ↔ WellQuasiOrdered s
have apply : ∀ (a : ℕ → α),
  (∃ (m : ℕ) (n : ℕ), m < n ∧ r (a m) (a n)) ↔
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        s (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) a m)
          (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) a n)
Tactic: apply (Equiv.arrowCongr (.refl ℕ) f).forall_congr