awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r) + 1)
x : Fin (p.length (r := r) - (↑i : ℕ))
j : ℕ
h : j < p.length (r := r) - (↑i : ℕ)
h₁ :
  (↑(⟨j, h⟩ : Fin (p.length (r := r) - (↑i : ℕ))).succ : ℕ) + (↑i : ℕ) =
    (↑(⟨j + (↑i : ℕ), ⋯⟩ : Fin (p.length (r := r))).succ : ℕ)
⊢ Membership.mem (α := α × α) r
    ((match (motive := Fin (p.length (r := r) - (↑i : ℕ) + 1) → α)
          (⟨j, h⟩ : Fin (p.length (r := r) - (↑i : ℕ))).castSucc with
        | ⟨j, h⟩ => p.toFun (r := r) ⟨j + (↑i : ℕ), ⋯⟩,
        match (motive := Fin (p.length (r := r) - (↑i : ℕ) + 1) → α)
          (⟨j, h⟩ : Fin (p.length (r := r) - (↑i : ℕ))).succ with
        | ⟨j, h⟩ => p.toFun (r := r) ⟨j + (↑i : ℕ), ⋯⟩) :
      α × α)

Tactic:
convert! p.step ⟨j + i.1, by lia⟩

Premises used: Fin.mk, Fin.val, HAdd.hAdd, RelSeries.step
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r) + 1)
x : Fin (p.length (r := r) - (↑i : ℕ))
j : ℕ
h : j < p.length (r := r) - (↑i : ℕ)
⊢ j + 1 + (↑i : ℕ) = j + (↑i : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ (p.drop (r := r) i).head (r := r) = p.toFun (r := r) i

Tactic:
simp [drop, head]

Premises used: RelSeries.drop, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
simp :
  p.toFun (r := r) (⟨p.length (r := r) - (↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (p.length (r := r) + 1)) =
    p.toFun (r := r) ⟨p.length (r := r), ⋯⟩
⊢ (p.drop (r := r) i).last (r := r) = p.last (r := r)

Tactic:
simp only [last, drop, Fin.last]

Premises used: RelSeries.last, RelSeries.drop, Fin.last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
e_a : p.length (r := r) - (↑i : ℕ) + (↑i : ℕ) = p.length (r := r)
⊢ p.toFun (r := r) (⟨p.length (r := r) - (↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (p.length (r := r) + 1)) =
    p.toFun (r := r) ⟨p.length (r := r), ⋯⟩

Tactic:
congr
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ p.length (r := r) - (↑i : ℕ) + (↑i : ℕ) = p.length (r := r)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
rw :
  (¬∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length (r := r) ≤ x.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
⊢ ¬r.FiniteDimensional ↔ r.InfiniteDimensional

Tactic:
rw [finiteDimensional_iff, infiniteDimensional_iff]

Premises used: SetRel.finiteDimensional_iff, SetRel.infiniteDimensional_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
push :
  (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
⊢ (¬∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length (r := r) ≤ x.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
mp :
  (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) →
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
mpr :
  (∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n) →
    ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
⊢ (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n

Tactic:
constructor
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
⊢ ∀ (i : Fin 0), (![inst.some] i.castSucc, ![inst.some] i.succ) ∈ r

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
⊢ RelSeries.length (r := r) (RelSeries.mk (r := r) 0 ![inst.some] ⋯) = 0

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
⊢ ∃ (x : RelSeries r), x.length (r := r) = 0

Tactic:
refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
IH : ∃ (x : RelSeries r), x.length (r := r) = n
mp : ∀ (l : RelSeries r) (hl : l.length (r := r) = n), ∃ (x : RelSeries r), x.length (r := r) = n + 1
⊢ ∃ (x : RelSeries r), x.length (r := r) = n + 1

Tactic:
obtain ⟨l, hl⟩ := IH
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
l : RelSeries r
hl : l.length (r := r) = n
mp : ∀ (l' : RelSeries r) (hl' : l.length (r := r) < l'.length (r := r)), ∃ (x : RelSeries r), x.length (r := r) = n + 1
⊢ ∃ (x : RelSeries r), x.length (r := r) = n + 1

Tactic:
obtain ⟨l', hl'⟩ := H l
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
l : RelSeries r
hl : l.length (r := r) = n
l' : RelSeries r
hl' : l.length (r := r) < l'.length (r := r)
⊢ n + 1 < l'.length (r := r) + 1

Tactic:
simpa [hl] using hl'
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
l : RelSeries r
hl : l.length (r := r) = n
l' : RelSeries r
hl' : l.length (r := r) < l'.length (r := r)
⊢ ∃ (x : RelSeries r), x.length (r := r) = n + 1

Tactic:
exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
mp : ∃ (x : RelSeries r), x.length (r := r) = 0
mp₁ : ∀ (n : ℕ) (IH : ∃ (x : RelSeries r), x.length (r := r) = n), ∃ (x : RelSeries r), x.length (r := r) = n + 1
⊢ ∃ (x : RelSeries r), x.length (r := r) = n

Tactic:
induction n with
    | zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
    | succ n IH =>
      obtain ⟨l, hl⟩ := IH
      obtain ⟨l', hl'⟩ := H l
      exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
l : RelSeries r
mpr :
  ∀ (l' : RelSeries r) (hl' : l'.length (r := r) = l.length (r := r) + 1),
    ∃ (y : RelSeries r), l.length (r := r) < y.length (r := r)
⊢ ∃ (y : RelSeries r), l.length (r := r) < y.length (r := r)

Tactic:
obtain ⟨l', hl'⟩ := H (l.length + 1)

Premises used: RelSeries.length, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
l l' : RelSeries r
hl' : l'.length (r := r) = l.length (r := r) + 1
⊢ l.length (r := r) < l'.length (r := r)

Tactic:
simp [hl']
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
l l' : RelSeries r
hl' : l'.length (r := r) = l.length (r := r) + 1
⊢ ∃ (y : RelSeries r), l.length (r := r) < y.length (r := r)

Tactic:
exact ⟨l', by simp [hl']⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
rw : ¬¬r.FiniteDimensional ↔ r.FiniteDimensional
rw₁ rw₂ : r.FiniteDimensional ↔ r.FiniteDimensional
⊢ ¬r.InfiniteDimensional ↔ r.FiniteDimensional

Tactic:
rw [← not_finiteDimensional_iff, not_not]

Premises used: Classical.not_not, SetRel.not_finiteDimensional_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
rw : r.FiniteDimensional ∨ ¬r.FiniteDimensional
⊢ r.FiniteDimensional ∨ r.InfiniteDimensional

Tactic:
rw [← not_finiteDimensional_iff]

Premises used: SetRel.not_finiteDimensional_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional

Tactic:
em r.FiniteDimensional

Premises used: em, SetRel.FiniteDimensional
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional

Tactic:
exact em r.FiniteDimensional

Premises used: em, SetRel.FiniteDimensional
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : r.FiniteDimensional
⊢ r.inv.FiniteDimensional

Tactic:
⟨.reverse (.longestOf r), fun s ↦ s.reverse.length_le_length_longestOf r⟩

Premises used: RelSeries.reverse, RelSeries.longestOf, SetRel.FiniteDimensional.mk, Exists.intro, RelSeries.length_le_length_longestOf
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
⊢ r.inv.FiniteDimensional ↔ r.FiniteDimensional

Tactic:
⟨fun _ ↦ .inv r.inv, fun _ ↦ .inv _⟩

Premises used: SetRel.inv, Iff.intro, SetRel.FiniteDimensional.inv
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : r.InfiniteDimensional
⊢ r.inv.InfiniteDimensional

Tactic:
⟨fun n ↦ ⟨.reverse (.withLength r n), RelSeries.length_withLength r n⟩⟩

Premises used: RelSeries.reverse, SetRel.InfiniteDimensional.mk, RelSeries.length_withLength, Exists.intro, RelSeries.withLength
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
⊢ r.inv.InfiniteDimensional ↔ r.InfiniteDimensional

Tactic:
⟨fun _ ↦ .inv r.inv, fun _ ↦ .inv _⟩

Premises used: SetRel.inv, SetRel.InfiniteDimensional.inv, Iff.intro
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
rw : IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
⊢ r.inv.IsWellFounded

Tactic:
rw [IsWellFounded, wellFounded_iff_isEmpty_descending_chain]

Premises used: wellFounded_iff_isEmpty_descending_chain, SetRel.IsWellFounded
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
⊢ IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }

Tactic:
⟨fun ⟨f, hf⟩ ↦ ?_⟩

Premises used: False, _private.0.SetRel.IsWellFounded.inv_of_finiteDimensional.match_2, IsEmpty.mk
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
refine :
  ∀ (x : { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }) (f : ℕ → α) (hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv),
    False
⊢ IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }

Tactic:
refine ⟨fun ⟨f, hf⟩ ↦ ?_⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
x : { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
f : ℕ → α
hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv
s : RelSeries r :=
  RelSeries.mk (r := r) ((RelSeries.longestOf r).length (r := r) + 1)
    (fun (x : Fin ((RelSeries.longestOf r).length (r := r) + 1 + 1)) ↦ f (↑x : ℕ)) ⋯
⊢ False

Tactic:
(RelSeries.longestOf r).length.lt_succ_self.not_ge s.length_le_length_longestOf

Premises used: Nat.lt_succ_self, RelSeries.length, RelSeries.longestOf, RelSeries.length_le_length_longestOf, LT.lt.not_ge
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
x : { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
f : ℕ → α
hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv
s : RelSeries r :=
  RelSeries.mk (r := r) ((RelSeries.longestOf r).length (r := r) + 1)
    (fun (x : Fin ((RelSeries.longestOf r).length (r := r) + 1 + 1)) ↦ f (↑x : ℕ)) ⋯
⊢ False

Tactic:
exact (RelSeries.longestOf r).length.lt_succ_self.not_ge s.length_le_length_longestOf

Premises used: Nat.lt_succ_self, RelSeries.length, RelSeries.longestOf, RelSeries.length_le_length_longestOf, LT.lt.not_ge
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
⊢ r.IsWellFounded

Tactic:
.inv_of_finiteDimensional r.inv

Premises used: SetRel.IsWellFounded.inv_of_finiteDimensional, Set.Mem, SetRel.inv, setOf, Set.preimage, Prod.swap
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
γ : Type u_3
inst : Preorder γ
inst_1 : Unique γ
x :
  RelSeries (α := γ)
    {x : γ × γ |
      match (motive := γ × γ → Prop) x with
      | (a, b) => a < b}
by_contra! :
  ∀
    (r :
      RelSeries.length (r :=
          {x : γ × γ |
            match (motive := γ × γ → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {x : γ × γ |
              match (motive := γ × γ → Prop) x with
              | (a, b) => a < b}
            default) <
        x.length (r :=
          {x : γ × γ |
            match (motive := γ × γ → Prop) x with
            | (a, b) => a < b})),
    False
⊢ x.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b}) ≤
    RelSeries.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})
      (RelSeries.singleton
        {x : γ × γ |
          match (motive := γ × γ → Prop) x with
          | (a, b) => a < b}
        default)

Tactic:
by_contra! r
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r_1 : SetRel α α
β : Type u_2
s : SetRel β β
γ : Type u_3
inst : Preorder γ
inst_1 : Unique γ
x :
  RelSeries (α := γ)
    {x : γ × γ |
      match (motive := γ × γ → Prop) x with
      | (a, b) => a < b}
r :
  RelSeries.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})
      (RelSeries.singleton
        {x : γ × γ |
          match (motive := γ × γ → Prop) x with
          | (a, b) => a < b}
        default) <
    x.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})
⊢ 0 <
    x.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r_1 : SetRel α α
β : Type u_2
s : SetRel β β
γ : Type u_3
inst : Preorder γ
inst_1 : Unique γ
x :
  RelSeries (α := γ)
    {x : γ × γ |
      match (motive := γ × γ → Prop) x with
      | (a, b) => a < b}
r :
  RelSeries.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})
      (RelSeries.singleton
        {x : γ × γ |
          match (motive := γ × γ → Prop) x with
          | (a, b) => a < b}
        default) <
    x.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})
⊢ False

Tactic:
exact (x.step ⟨0, by lia⟩).ne <| Subsingleton.elim _ _

Premises used: Fin.mk, RelSeries.step, Subsingleton.elim, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
n : ℕ
⊢ RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (LTSeries.withLength α n) =
    n

Tactic:
RelSeries.length_withLength _ _

Premises used: RelSeries.length_withLength
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
⊢ Nonempty α

Tactic:
⟨LTSeries.withLength α 0 0⟩

Premises used: Nonempty.intro, LTSeries.withLength, RelSeries.toFun, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
obtain :
  ∀
    (p :
      RelSeries (α := α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}),
    (∀
        (y :
          RelSeries (α := α)
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}),
        y.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) ≤
          p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) →
      Nonempty α
⊢ Nonempty α

Tactic:
obtain ⟨p, _⟩ := (SetRel.finiteDimensional_iff _).mp ‹_›

Premises used: SetRel.finiteDimensional_iff, Iff.mp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
p :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
h :
  ∀
    (y :
      RelSeries (α := α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}),
    y.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≤
      p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
⊢ Nonempty α

Tactic:
⟨p 0⟩

Premises used: Nonempty.intro, RelSeries.toFun, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
p :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
h :
  ∀
    (y :
      RelSeries (α := α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}),
    y.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≤
      p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
⊢ Nonempty α

Tactic:
exact ⟨p 0⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
x : LTSeries α
⊢ x.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≤
    RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (LTSeries.longestOf α)

Tactic:
RelSeries.length_le_length_longestOf _ _

Premises used: RelSeries.length_le_length_longestOf
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
p : LTSeries α
is_longest :
  ∀ (q : LTSeries α),
    q.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≤
      p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (LTSeries.longestOf α)

Tactic:
le_antisymm (longestOf_is_longest _) (is_longest _)

Premises used: le_antisymm, LTSeries.longestOf_is_longest
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
x : LTSeries α
⊢ StrictMono
    (x.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))

Tactic:
fun _ _ h => x.rel_of_lt h

Premises used: StrictMono, Set.Mem, setOf, RelSeries.rel_of_lt
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
x : LTSeries α
⊢ Monotone
    (x.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))

Tactic:
x.strictMono.monotone

Premises used: StrictMono.monotone, LTSeries.strictMono
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
x : LTSeries α
n :
  Fin
    (x.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      x ≤
    x.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      n

Tactic:
x.monotone (Fin.zero_le n)

Premises used: Fin.zero_le, RelSeries.head, LTSeries.monotone
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
x : LTSeries α
⊢ RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      x ≤
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      x

Tactic:
x.head_le _

Premises used: RelSeries.last, LTSeries.head_le
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
f g :
  { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }
e :
  Eq.{u_1 + 1} (α := LTSeries α)
    ((fun
          (f :
            { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
              StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
        mk (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
          ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) ⋯)
      f)
    ((fun
          (f :
            { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
              StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
        mk (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
          ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) ⋯)
      g)
obtain :
  ∀ (lf : Fin n) (f : Fin ((↑lf : ℕ) + 1) → α)
    (mf :
      StrictMono.{0, u_1} (α :=
        Fin
          ((↑(Sigma.fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)
                  (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f)) :
              ℕ) +
            1))
        (β := α)
        (Sigma.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)
          (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f)))
    (e :
      Eq.{u_1 + 1} (α := LTSeries α)
        ((fun
              (f :
                { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
                  StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
            mk
              (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
              ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) ⋯)
          (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
            StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
            (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf))
        ((fun
              (f :
                { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
                  StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
            mk
              (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
              ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) ⋯)
          g)),
    Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
        StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
        (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf =
      g
⊢ f = g

Tactic:
obtain ⟨⟨lf, f⟩, mf⟩ := f