awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
h :
  ∀
    (x_1 :
      Fin
        (length (r := r)
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              ((fun (x : RelSeries r) ↦
                  (Subtype.mk (p := fun (x : List α) ↦
                      Membership.mem (γ := Set (List α))
                        {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                      (x.toList (r := r)) ⋯ :
                    { x : List α //
                      Membership.mem (γ := Set (List α))
                        {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
                x)) +
          1)),
    toFun (r := r)
        ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
            fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
          ((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            x))
        x_1 =
      (x.toFun (r := r) ∘ Fin.cast ⋯) x_1
⊢ toFun (r := r)
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        ((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) ⋯ :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          x)) =
    x.toFun (r := r) ∘ Fin.cast ⋯

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
x_1 :
  Fin
    (length (r := r)
        ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
            fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
          ((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            x)) +
      1)
h :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (↑x_1 : ℕ) ⋯ =
    x.toFun (r := r) (Fin.cast ⋯ x_1)
⊢ toFun (r := r)
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        ((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) ⋯ :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          x))
      x_1 =
    (x.toFun (r := r) ∘ Fin.cast ⋯) x_1

Tactic:
dsimp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
x_1 :
  Fin
    (length (r := r)
        ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
            fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
          ((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            x)) +
      1)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (↑x_1 : ℕ) ⋯ =
    x.toFun (r := r) (Fin.cast ⋯ x_1)

Tactic:
apply List.get_ofFn

Premises used: List.get_ofFn
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
n : ℕ
hn1 :
  n <
    List.length.{u_1} (α := α)
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α)
h : n < (↑x : List α).length
dsimp :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      ((fromListIsChain (r := r) (↑x : List α) ⋯ ⋯).toList (r := r)) n ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (↑x : List α) n ⋯
⊢ List.get
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α)
      (⟨n, hn1⟩ :
        Fin
          (List.length.{u_1} (α := α)
            (↑((fun (x : RelSeries r) ↦
                    (Subtype.mk (p := fun (x : List α) ↦
                        Membership.mem (γ := Set (List α))
                          {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                        (x.toList (r := r)) ⋯ :
                      { x : List α //
                        Membership.mem (γ := Set (List α))
                          {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
                  ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                      fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
                    x)) :
              List α))) =
    (↑x : List α).get (⟨n, h⟩ : Fin (↑x : List α).length)

Tactic:
dsimp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
n : ℕ
hn1 :
  n <
    List.length.{u_1} (α := α)
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α)
h : n < (↑x : List α).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      ((fromListIsChain (r := r) (↑x : List α) ⋯ ⋯).toList (r := r)) n ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (↑x : List α) n ⋯

Tactic:
apply List.get_ofFn

Premises used: List.get_ofFn
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
refine :
  List.length.{u_1} (α := α)
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α) =
    (↑x : List α).length
⊢ (fun (x : RelSeries r) ↦
        (Subtype.mk (p := fun (x : List α) ↦
            Membership.mem (γ := Set (List α)) {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x}
              x)
            (x.toList (r := r)) ⋯ :
          { x : List α //
            Membership.mem (γ := Set (List α)) {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x}
              x }))
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        x) =
    x

Tactic:
refine Subtype.ext (List.ext_get ?_ fun n hn1 _ => by dsimp; apply List.get_ofFn)

Premises used: List.ext_get, Subtype.ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
⊢ (↑x : List α).length.pred.succ = (↑x : List α).length

Tactic:
have := Nat.succ_pred_eq_of_pos <| List.length_pos_iff.mpr x.2.1
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
this : (↑x : List α).length.pred.succ = (↑x : List α).length
⊢ List.length.{u_1} (α := α)
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α) =
    (↑x : List α).length

Tactic:
simp_all [toList]

Premises used: RelSeries.toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := RelSeries r) (toList (r := r))

Tactic:
fun _ _ h ↦ (RelSeries.Equiv).injective <| Subtype.ext h

Premises used: RelSeries.Equiv, Equiv.injective, Function.Injective, Subtype.ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
x : RelSeries r
⊢ x.length (r := r) ≤ (RelSeries.longestOf r).length (r := r)

Tactic:
SetRel.FiniteDimensional.exists_longest_relSeries.choose_spec _

Premises used: Exists.choose_spec, SetRel.FiniteDimensional.exists_longest_relSeries
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.InfiniteDimensional
n : ℕ
⊢ (RelSeries.withLength r n).length (r := r) = n

Tactic:
(SetRel.InfiniteDimensional.exists_relSeries_with_length n).choose_spec

Premises used: Exists.choose_spec, SetRel.InfiniteDimensional.exists_relSeries_with_length
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.InfiniteDimensional
⊢ Nonempty α

Tactic:
⟨RelSeries.withLength r 0 0⟩

Premises used: Nonempty.intro, RelSeries.toFun, OfNat.ofNat, RelSeries.withLength
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
obtain : ∀ (p : RelSeries r), (∀ (y : RelSeries r), y.length (r := r) ≤ p.length (r := r)) → Nonempty α
⊢ Nonempty α

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

Premises used: SetRel.finiteDimensional_iff, Iff.mp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
p : RelSeries r
h : ∀ (y : RelSeries r), y.length (r := r) ≤ p.length (r := r)
⊢ Nonempty α

Tactic:
⟨p 0⟩

Premises used: Nonempty.intro, RelSeries.toFun, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
p : RelSeries r
h : ∀ (y : RelSeries r), y.length (r := r) ≤ p.length (r := r)
⊢ Nonempty α

Tactic:
exact ⟨p 0⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ s ↔ x ∈ Set.range (s.toFun (r := r))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
rw : x ∈ List.ofFn (s.toFun (r := r)) ↔ x ∈ s
rw₁ : x ∈ Set.range (s.toFun (r := r)) ↔ x ∈ s
rw₂ rw₃ : x ∈ Set.range (s.toFun (r := r)) ↔ x ∈ Set.range (s.toFun (r := r))
⊢ x ∈ s.toList (r := r) ↔ x ∈ s

Tactic:
rw [RelSeries.toList, List.mem_ofFn', RelSeries.mem_def]

Premises used: RelSeries.toList, RelSeries.mem_def, List.mem_ofFn'
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length (r := r) = 0
i j : Fin (s.length (r := r) + 1)
h : i = j
⊢ s.toFun (r := r) i = s.toFun (r := r) j

Tactic:
congr!
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length (r := r) = 0
i j : Fin (s.length (r := r) + 1)
rw : HAdd.hAdd (α := ℕ) 0 1 = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ s.length (r := r) + 1 = 1

Tactic:
rw [hs, zero_add]

Premises used: zero_add
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length (r := r) = 0
i j : Fin (s.length (r := r) + 1)
⊢ i = j

Tactic:
exact finCongr (by rw [hs, zero_add]) |>.injective <| Subsingleton.elim (α := Fin 1) _ _

Premises used: finCongr, Equiv.injective, Subsingleton.elim
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
h : Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s}
⊢ s.length (r := r) ≠ 0

Tactic:
fun hs ↦ h.not_subsingleton <| subsingleton_of_length_eq_zero hs

Premises used: Set.Nontrivial.not_subsingleton, RelSeries.subsingleton_of_length_eq_zero, Not
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
h : Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s}
⊢ 0 < s.length (r := r)

Tactic:
Nat.pos_iff_ne_zero.mpr <| length_ne_zero_of_nontrivial h

Premises used: Iff.mpr, RelSeries.length_ne_zero_of_nontrivial, Nat.pos_iff_ne_zero
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
⊢ Membership.mem (γ := Set α) {x : α | x ∈ s} (s.toFun (r := r) 0)

Tactic:
simp [mem_def]

Premises used: RelSeries.mem_def
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
⊢ Membership.mem (γ := Set α) {x : α | x ∈ s} (s.toFun (r := r) 1)

Tactic:
simp [mem_def]

Premises used: RelSeries.mem_def
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
refine :
  ∀ (h : s.length (r := r) ≠ 0) (rid : s.toFun (r := r) 0 = s.toFun (r := r) 1),
    (s.toFun (r := r) 0, s.toFun (r := r) 0) ∈ r
⊢ s.length (r := r) ≠ 0 ↔ Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s}

Tactic:
refine ⟨fun h ↦ ⟨s 0, by simp [mem_def], s 1, by simp [mem_def],
    fun rid ↦ r.irrefl (s 0) ?_⟩, length_ne_zero_of_nontrivial⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
nth_rw : (s.toFun (r := r) 0, s.toFun (r := r) 1) ∈ r
⊢ (s.toFun (r := r) 0, s.toFun (r := r) 0) ∈ r

Tactic:
nth_rw 2 [rid]
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
⊢ 0 < s.length (r := r)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
h₁ : 1 = (⟨0, ⋯⟩ : Fin (s.length (r := r))).succ
⊢ (s.toFun (r := r) 0, s.toFun (r := r) 1) ∈ r

Tactic:
convert! s.step ⟨0, by lia⟩

Premises used: Fin.mk, RelSeries.step, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
h₁ : (↑1 : ℕ) = (↑(⟨0, ⋯⟩ : Fin (s.length (r := r))).succ : ℕ)
⊢ 1 = (⟨0, ⋯⟩ : Fin (s.length (r := r))).succ

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
⊢ (↑1 : ℕ) = (↑(⟨0, ⋯⟩ : Fin (s.length (r := r))).succ : ℕ)

Tactic:
simpa [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
⊢ 0 < s.length (r := r) ↔ Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s}

Tactic:
Nat.pos_iff_ne_zero.trans length_ne_zero

Premises used: Nat.pos_iff_ne_zero, RelSeries.length_ne_zero, Iff.trans
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
rw : ¬s.length (r := r) ≠ 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
rw₁ : ¬Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s} ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
rw₂ rw₃ : Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s} ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
⊢ s.length (r := r) = 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}

Tactic:
rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]

Premises used: RelSeries.length_ne_zero, not_ne_iff, Set.not_nontrivial_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.toFun (r := r) 0 = p.head (r := r)

Tactic:
rfl

Premises used: RelSeries.head, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ x.toFun (r := r) (Fin.last (x.length (r := r))) = x.last (r := r)

Tactic:
rfl

Premises used: RelSeries.last, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ x.head (r := r) ∈ x

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ x.last (r := r) ∈ x

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).head (r := r) = x

Tactic:
simp [singleton, head]

Premises used: RelSeries.head, RelSeries.singleton
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).last (r := r) = x

Tactic:
simp [singleton, last]

Premises used: RelSeries.last, RelSeries.singleton
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.toList (r := r).head ⋯ = p.head (r := r)

Tactic:
simp [toList, apply_zero]

Premises used: RelSeries.apply_zero, RelSeries.toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
i : ℕ
hi : i < p.toList (r := r).length
⊢ i < p.length (r := r) + 1

Tactic:
simpa using hi
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : ℕ
hi : i < p.toList (r := r).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList (r := r)) i hi = p.toFun (r := r) ⟨i, ⋯⟩

Tactic:
simp only [toList, List.getElem_ofFn]

Premises used: RelSeries.toList, List.getElem_ofFn
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList (r := r)) (↑i : ℕ) ⋯ = p.toFun (r := r) i

Tactic:
p.toList_getElem _

Premises used: RelSeries.toList_getElem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
i : ℕ
hi : i < p.length (r := r) + 1
⊢ i < p.toList (r := r).length

Tactic:
simpa using hi
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : ℕ
hi : i < p.length (r := r) + 1
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList (r := r)) i ⋯ = p.toFun (r := r) ⟨i, hi⟩

Tactic:
p.toList_getElem _

Premises used: RelSeries.toList_getElem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList (r := r)) 0 ⋯ = p.head (r := r)

Tactic:
p.toList_getElem _

Premises used: Fin.ofNat, Nat.mod, RelSeries.toList_getElem, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) l
⊢ (fromListIsChain (r := r) l l_ne_nil hl).toList (r := r) = l

Tactic:
Subtype.ext_iff.mp <| RelSeries.Equiv.right_inv ⟨l, ⟨l_ne_nil, hl⟩⟩

Premises used: Nat.pow.match_1, Equiv.right_inv, List.ofFn, Fin.foldr.loop, RelSeries.toList, Subtype.ext_iff, Subtype.mk, RelSeries.Equiv, And.intro, Iff.mp, Nat.pred
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) l
⊢ (fromListIsChain (r := r) l l_ne_nil hl).head (r := r) = l.head l_ne_nil

Tactic:
simp [← apply_zero, List.getElem_zero_eq_head]

Premises used: RelSeries.apply_zero, List.getElem_zero_eq_head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
⊢ p.toList (r := r) ≠ []

Tactic:
simp [toList]

Premises used: RelSeries.toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.toList (r := r).getLast ⋯ = p.last (r := r)

Tactic:
grind [length_toList, last, Fin.last, toList_getElem]

Premises used: RelSeries.last, Fin.last, RelSeries.toList_getElem, RelSeries.length_toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
⊢ p.length (r := r) + q.length (r := r) + 1 + 1 = p.length (r := r) + 1 + (q.length (r := r) + 1)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (p.length (r := r) + q.length (r := r) + 1)
⊢ p.length (r := r) + 1 ≤ p.length (r := r) + q.length (r := r) + 1

Tactic:
lia