awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
e_a : (Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ = Fin.last (p.length (r := r))
⊢ p.toFun (r := r) (Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ =
    p.toFun (r := r) (Fin.last (p.length (r := r)))

Tactic:
congr
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
e_a :
  (↑(Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ : ℕ) =
    (↑(Fin.last (p.length (r := r))) : ℕ)
⊢ (Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ = Fin.last (p.length (r := r))

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
e_a : p.length (r := r) - 1 + 1 = p.length (r := r)
⊢ (↑(Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ : ℕ) =
    (↑(Fin.last (p.length (r := r))) : ℕ)

Tactic:
simp only [tail_length, Fin.val_succ, Fin.val_cast, Fin.val_last]

Premises used: Fin.val_succ, RelSeries.tail_length, Fin.val_cast, Fin.val_last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ 0 < p.length (r := r).sub 0

Tactic:
simpa [Nat.pos_iff_ne_zero] using len_pos

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ p.length (r := r) - 1 + 1 = p.length (r := r)

Tactic:
exact Nat.succ_pred_eq_of_pos (by simpa [Nat.pos_iff_ne_zero] using len_pos)

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
⊢ (p.tail (r := r) hp).toList (r := r) = p.toList (r := r).tail

Tactic:
List.ext_getElem ?_ fun i h1 h2 ↦ ?_

Premises used: List.ext_getElem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
refine_1 : (p.tail (r := r) hp).toList (r := r).length = p.toList (r := r).tail.length
refine_2 :
  ∀ (i : ℕ) (h1 : i < (p.tail (r := r) hp).toList (r := r).length) (h2 : i < p.toList (r := r).tail.length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.tail (r := r) hp).toList (r := r)) i h1 =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) p.toList (r := r).tail i h2
⊢ (p.tail (r := r) hp).toList (r := r) = p.toList (r := r).tail

Tactic:
refine List.ext_getElem ?_ fun i h1 h2 ↦ ?_

Premises used: List.ext_getElem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
refine_1 : p.length (r := r) - 1 + 1 = p.length (r := r)
⊢ (p.tail (r := r) hp).toList (r := r).length = p.toList (r := r).tail.length

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
⊢ p.length (r := r) - 1 + 1 = p.length (r := r)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
i : ℕ
h1 : i < (p.tail (r := r) hp).toList (r := r).length
h2 : i < p.toList (r := r).tail.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.tail (r := r) hp).toList (r := r)) i h1 =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) p.toList (r := r).tail i h2

Tactic:
simp [Fin.tail]

Premises used: Fin.tail
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
⊢ (p.cons (r := r) x hx).length (r := r) ≠ 0

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
a : ((p.cons (r := r) x hx).tail (r := r) ⋯).toList (r := r) = p.toList (r := r)
⊢ (p.cons (r := r) x hx).tail (r := r) ⋯ = p

Tactic:
apply toList_injective

Premises used: RelSeries.toList_injective
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
⊢ ((p.cons (r := r) x hx).tail (r := r) ⋯).toList (r := r) = p.toList (r := r)

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
a : ((p.tail (r := r) hp).cons (r := r) (p.head (r := r)) ⋯).toList (r := r) = p.toList (r := r)
⊢ (p.tail (r := r) hp).cons (r := r) (p.head (r := r)) ⋯ = p

Tactic:
apply toList_injective

Premises used: RelSeries.toList_injective
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
⊢ ((p.tail (r := r) hp).cons (r := r) (p.head (r := r)) ⋯).toList (r := r) = p.toList (r := r)

Tactic:
simp [← head_toList]

Premises used: RelSeries.head_toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
h : p = RelSeries.singleton r (p.head (r := r))
⊢ motive p

Tactic:
convert! singleton p.head

Premises used: RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
h : p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)
h₁ :
  ∀ (n : Fin (p.length (r := r) + 1)),
    p.toFun (r := r) n = ((RelSeries.singleton r (p.head (r := r))).toFun (r := r) ∘ Fin.cast ⋯) n
⊢ p = RelSeries.singleton r (p.head (r := r))

Tactic:
ext n
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
⊢ p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)

Tactic:
heq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
⊢ p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)

Tactic:
exact heq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
n : Fin (p.length (r := r) + 1)
⊢ n = 0

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
n : Fin (p.length (r := r) + 1)
⊢ p.toFun (r := r) n = ((RelSeries.singleton r (p.head (r := r))).toFun (r := r) ∘ Fin.cast ⋯) n

Tactic:
simp [show n = 0 by lia, apply_zero]

Premises used: RelSeries.apply_zero
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
succ : (lq : (p.tail (r := r) ⋯).length (r := r) = p.length (r := r) - 1) → motive p
⊢ motive p

Tactic:
have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
lq : (p.tail (r := r) ⋯).length (r := r) = p.length (r := r) - 1
⊢ (p.tail (r := r) ⋯).length (r := r) = d + 1 - 1

Tactic:
nth_rw 3 [heq] at lq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
lq : (p.tail (r := r) ⋯).length (r := r) = d + 1 - 1
h : p = (p.tail (r := r) ⋯).cons (r := r) (p.head (r := r)) ⋯
⊢ motive p

Tactic:
convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)

Premises used: Nat.zero_lt_succ, Eq.rec, Fin.mk, Ne.symm, RelSeries.head, RelSeries.tail, RelSeries.step, OfNat.ofNat, Eq.symm, Nat.zero_ne_add_one
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
lq : (p.tail (r := r) ⋯).length (r := r) = d + 1 - 1
⊢ p = (p.tail (r := r) ⋯).cons (r := r) (p.head (r := r)) ⋯

Tactic:
(p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm

Premises used: Eq.rec, RelSeries.cons_self_tail, Ne.symm, Eq.symm, Nat.zero_ne_add_one
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
lq : (p.tail (r := r) ⋯).length (r := r) = d + 1 - 1
⊢ p = (p.tail (r := r) ⋯).cons (r := r) (p.head (r := r)) ⋯

Tactic:
exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm

Premises used: Eq.rec, RelSeries.cons_self_tail, Ne.symm, Eq.symm, Nat.zero_ne_add_one
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
n : ℕ
heq : p.length (r := r) = n
zero : (p : RelSeries r) → (heq : p.length (r := r) = 0) → motive p
succ :
  (d : ℕ) →
    (hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p) →
      (p : RelSeries r) → (heq : p.length (r := r) = d + 1) → motive p
⊢ motive p

Tactic:
induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
      nth_rw 3 [heq] at lq
      convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)
      exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm

Premises used: RelSeries.apply_zero, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
let : motive p
⊢ motive p

Tactic:
let this {n : ℕ} (heq : p.length = n) : motive p := by
    induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
      nth_rw 3 [heq] at lq
      convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)
      exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head (r := r)) ∈ r) → (hp : motive p) → motive (p.cons (r := r) x hx)
p : RelSeries r
this : {n : ℕ} → (heq : p.length (r := r) = n) → motive p :=
  fun {n : ℕ} (heq : p.length (r := r) = n) ↦
    Nat.recAux (motive := fun {n : ℕ} ↦ (p : RelSeries r) → (heq : p.length (r := r) = n) → motive p)
      (fun (p : RelSeries r) (heq : p.length (r := r) = 0) ↦
        Eq.mpr (β := motive (RelSeries.singleton r (p.head (r := r)))) ⋯ (singleton (p.head (r := r))))
      (fun (d : ℕ) (hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p) (p : RelSeries r)
          (heq : p.length (r := r) = d + 1) ↦
        have lq : (p.tail (r := r) ⋯).length (r := r) = p.length (r := r) - 1 := ⋯;
        Eq.mpr (β := motive ((p.tail (r := r) ⋯).cons (r := r) (p.head (r := r)) ⋯)) ⋯
          (cons (p.tail (r := r) ⋯) (p.head (r := r)) ⋯ (hd (p.tail (r := r) ⋯) ⋯)))
      n p heq
⊢ motive p

Tactic:
exact this rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
⊢ (p.snoc (r := r) newLast rel).toList (r := r) = p.toList (r := r) ++ [newLast]

Tactic:
simp [snoc]

Premises used: RelSeries.snoc
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.eraseLast (r := r).head (r := r) = p.head (r := r)

Tactic:
rfl

Premises used: Fin.ofNat, RelSeries.eraseLast, Nat.mod, RelSeries.head, Nat.pred, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.eraseLast (r := r).last (r := r) = p.toFun (r := r) ⟨p.length (r := r).pred, ⋯⟩

Tactic:
rfl

Premises used: RelSeries.last, Nat.pred, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
simp :
  (p.toFun (r := r) (⟨p.length (r := r) - 1, ⋯⟩ : Fin (p.length (r := r) + 1)),
      p.toFun (r := r) (⟨p.length (r := r), ⋯⟩ : Fin (p.length (r := r) + 1))) ∈
    r
⊢ (p.eraseLast (r := r).last (r := r), p.last (r := r)) ∈ r

Tactic:
simp only [last, Fin.last, eraseLast_length, eraseLast_toFun]

Premises used: RelSeries.last, RelSeries.eraseLast_toFun, RelSeries.eraseLast_length, Fin.last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
⊢ p.length (r := r) - 1 < p.length (r := r)

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

Tactic:
convert! p.step ⟨p.length - 1, by lia⟩

Premises used: HSub.hSub, Fin.mk, RelSeries.length, RelSeries.step, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
⊢ p.length (r := r) = p.length (r := r) - 1 + 1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
hl : p.eraseLast (r := r).toList (r := r).length = p.toList (r := r).dropLast.length
h :
  ∀ (i : ℕ) (h₁ : i < p.eraseLast (r := r).toList (r := r).length) (h₂ : i < p.toList (r := r).dropLast.length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.eraseLast (r := r).toList (r := r)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) p.toList (r := r).dropLast i h₂
⊢ p.eraseLast (r := r).toList (r := r) = p.toList (r := r).dropLast

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
⊢ p.eraseLast (r := r).toList (r := r).length = p.toList (r := r).dropLast.length

Tactic:
simpa using Nat.succ_pred_eq_of_ne_zero hp

Premises used: Nat.succ_pred_eq_of_ne_zero
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
i : ℕ
hi : i < p.eraseLast (r := r).toList (r := r).length
h2 : i < p.toList (r := r).dropLast.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.eraseLast (r := r).toList (r := r)) i hi =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) p.toList (r := r).dropLast i h2

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
a : (p.eraseLast (r := r).snoc (r := r) (p.last (r := r)) ⋯).toList (r := r) = p.toList (r := r)
⊢ p.eraseLast (r := r).snoc (r := r) (p.last (r := r)) ⋯ = p

Tactic:
apply toList_injective

Premises used: RelSeries.toList_injective
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
a : p.eraseLast (r := r).toList (r := r) ++ [p.last (r := r)] = p.toList (r := r)
a₁ : p.eraseLast (r := r).toList (r := r) ++ [p.toList (r := r).getLast ⋯] = p.toList (r := r)
a₂ : p.toList (r := r).dropLast ++ [p.toList (r := r).getLast ⋯] = p.toList (r := r)
a₃ a₄ : p.toList (r := r) = p.toList (r := r)
⊢ (p.eraseLast (r := r).snoc (r := r) (p.last (r := r)) ⋯).toList (r := r) = p.toList (r := r)

Tactic:
rw [toList_snoc, ← getLast_toList, toList_eraseLast _ h, List.dropLast_append_getLast]

Premises used: RelSeries.getLast_toList, RelSeries.toList_eraseLast, RelSeries.toList_snoc, List.dropLast_append_getLast
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
h : p = RelSeries.singleton r (p.head (r := r))
⊢ motive p

Tactic:
convert! singleton p.head

Premises used: RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
h : p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)
h₁ :
  ∀ (n : Fin (p.length (r := r) + 1)),
    p.toFun (r := r) n = ((RelSeries.singleton r (p.head (r := r))).toFun (r := r) ∘ Fin.cast ⋯) n
⊢ p = RelSeries.singleton r (p.head (r := r))

Tactic:
ext n
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
⊢ p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)

Tactic:
heq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
⊢ p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)

Tactic:
exact heq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
n : Fin (p.length (r := r) + 1)
⊢ n = 0

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
heq : p.length (r := r) = 0
n : Fin (p.length (r := r) + 1)
⊢ p.toFun (r := r) n = ((RelSeries.singleton r (p.head (r := r))).toFun (r := r) ∘ Fin.cast ⋯) n

Tactic:
simp [show n = 0 by lia, apply_zero]

Premises used: RelSeries.apply_zero
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
⊢ p.length (r := r) ≠ 0

Tactic:
simp [heq]
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
succ : (ne0 : p.length (r := r) ≠ 0) → motive p
⊢ motive p

Tactic:
have ne0 : p.length ≠ 0 := by simp [heq]
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
ne0 : p.length (r := r) ≠ 0
⊢ p.eraseLast (r := r).length (r := r) = d

Tactic:
simp [heq]
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
ne0 : p.length (r := r) ≠ 0
⊢ p.eraseLast (r := r).length (r := r) = d

Tactic:
have len : p.eraseLast.length = d := by simp [heq]