awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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)
rw :
  ∀ (f : ℕ → (i : ι) → α i),
    ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
⊢ WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
rw [wellQuasiOrdered_iff_exists_monotone_subseq]

Premises used: wellQuasiOrdered_iff_exists_monotone_subseq
-- 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_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)
f : ℕ → (i : ι) → α i
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)

Tactic:
simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f

Premises used: Finset.mem_univ, Finset.univ, true_imp_iff
-- 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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
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)
⊢ WellQuasiOrdered fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (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
-- 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_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)

Tactic:
Finset.cons_induction ?_ ?_

Premises used: Finset.cons_induction
-- 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_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)
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)
⊢ ∀ (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:
refine Finset.cons_induction ?_ ?_
-- 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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
f : ℕ → (i : ι) → α i
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)
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ (i : ι),
          Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)

Tactic:
exists RelEmbedding.refl (· ≤ ·)

Premises used: RelEmbedding.refl, LE.le
-- 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_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
f : ℕ → (i : ι) → α i
⊢ ∀ ⦃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:
simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

Premises used: imp_true_iff, Finset.notMem_empty, IsEmpty.forall_iff
-- 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_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
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)
⊢ ∃ (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)

Premises used: WellQuasiOrdered.exists_monotone_subseq
-- 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_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)
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)
⊢ ∃ (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)

Premises used: Function.comp, DFunLike.coe
-- 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_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)

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

Premises used: Iff.mpr, Function.comp, Finset.forall_mem_cons, Exists.intro, RelEmbedding.trans, DFunLike.coe
-- 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_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)
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)
⊢ ∃ (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:
refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
-- 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_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)
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:
⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

Premises used: OrderHomClass.mono, And.intro
-- 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_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)
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:
exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
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)
⊢ WellQuasiOrdered r ↔ WellQuasiOrdered s

Tactic:
apply (Equiv.arrowCongr (.refl ℕ) f).forall_congr

Premises used: Equiv.arrowCongr, Nat, Equiv.forall_congr, Equiv.refl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
a :
  ∀ (g : ℕ → α) (a b : ℕ),
    r (g a) (g b) ↔
      s (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) g a)
        (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) g b)
⊢ ∀ (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:
congr! with g a b
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
g : ℕ → α
a b : ℕ
⊢ r (g a) (g b) ↔
    s (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) g a)
      (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) g b)

Tactic:
simp [f.map_rel_iff]

Premises used: RelIso.map_rel_iff
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : LE α
h : WellQuasiOrderedLE α
⊢ WellQuasiOrdered fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
h.wqo

Premises used: WellQuasiOrderedLE.wqo
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
β : Type u_4
inst : LE α
inst_1 : LE β
f : α ≃o β
⊢ WellQuasiOrderedLE α ↔ WellQuasiOrderedLE β

Tactic:
simpa [wellQuasiOrderedLE_def] using f.wellQuasiOrdered_iff

Premises used: wellQuasiOrderedLE_def, RelIso.wellQuasiOrdered_iff
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
rw : IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)
⊢ WellFoundedLT α

Tactic:
rw [WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]

Premises used: WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
⊢ IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
⟨fun f ↦ ?_⟩

Premises used: IsEmpty.mk
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
refine : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2), False
⊢ IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
refine ⟨fun f ↦ ?_⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
obtain : ∀ (a b : ℕ) (h : a < b) (hf : LE.le (α := α) ((f : (a : ℕ) → α) a : α) ((f : (a : ℕ) → α) b : α)), False
⊢ False

Tactic:
obtain ⟨a, b, h, hf⟩ := wellQuasiOrdered_le f

Premises used: DFunLike.coe, wellQuasiOrdered_le
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
a b : ℕ
h : a < b
hf : LE.le (α := α) ((f : (a : ℕ) → α) a : α) ((f : (a : ℕ) → α) b : α)
⊢ False

Tactic:
(f.map_rel_iff.2 h).not_ge hf

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, LT.lt.not_ge
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
a b : ℕ
h : a < b
hf : LE.le (α := α) ((f : (a : ℕ) → α) a : α) ((f : (a : ℕ) → α) b : α)
⊢ False

Tactic:
exact (f.map_rel_iff.2 h).not_ge hf

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, LT.lt.not_ge
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
x : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
⊢ WellQuasiOrderedLE α

Tactic:
have : WellQuasiOrderedLE α := ⟨h⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
x : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
this : WellQuasiOrderedLE α
⊢ WellFounded fun (a b : α) ↦ r a b ∧ ¬r b a

Tactic:
wellFounded_lt

Premises used: wellFounded_lt
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_3
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
x : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
this : WellQuasiOrderedLE α
⊢ WellFounded fun (a b : α) ↦ r a b ∧ ¬r b a

Tactic:
exact wellFounded_lt

Premises used: wellFounded_lt
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
s : Set α
h : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ s.Finite

Tactic:
h.finite_of_wellQuasiOrdered wellQuasiOrdered_le

Premises used: IsAntichain.finite_of_wellQuasiOrdered, wellQuasiOrdered_le
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite

Tactic:
⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩,
    fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩

Premises used: WellQuasiOrderedLE.finite_of_isAntichain, WellQuasiOrderedLE.mk, _private.0.wellQuasiOrderedLE_iff.match_1, And.intro, Iff.intro, WellQuasiOrderedLE.to_wellFoundedLT, WellQuasiOrderedLE
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
refine :
  (WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite) →
    ∀ (hwf : WellFoundedLT α) (hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite) (f : ℕ → α),
      ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite

Tactic:
refine ⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩,
    fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
inl :
  ∀ (g : ℕ ↪o ℕ) (h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
inr :
  ∀ (g : ℕ ↪o ℕ) (h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)

Tactic:
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (· > ·) f

Premises used: exists_increasing_or_nonincreasing_subseq, GT.gt
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
inl : False
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)

Tactic:
exfalso
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
apply : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
⊢ False

Tactic:
apply RelEmbedding.not_wellFounded _ hwf.wf

Premises used: IsWellFounded.wf, RelEmbedding.not_wellFounded
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
⊢ (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2

Tactic:
exact (RelEmbedding.ofMonotone _ h1).swap

Premises used: RelEmbedding.swap, RelEmbedding.ofMonotone