awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
h :
  Eq.rec (motive := fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.succ.pred ⋯) = x) ↦ α)
      (p.toFun (r := r) (m.succ.pred ⋯)) ⋯ =
    p.toFun (r := r) i.succ
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ =
    p.toFun (r := r) i.succ
have h₁ : i.succ.castSucc < m.succ
Tactic: rw [Fin.insertNth_apply_above]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ i.succ.castSucc < m.succ
have h : (↑i : ℕ) + 1 < (↑m : ℕ) + 1
Tactic: change i.1 + 1 < m.1 + 1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ Eq.rec (motive := fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.succ.pred ⋯) = x) ↦ α)
      (p.toFun (r := r) (m.succ.pred ⋯)) ⋯ =
    p.toFun (r := r) i.succ
have h : p.toFun (r := r) m = p.toFun (r := r) i.succ
Tactic: simp only [Fin.pred_succ, eq_rec_constant]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ p.toFun (r := r) m = p.toFun (r := r) i.succ
have h : m = i.succ
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ m = i.succ
have h : (↑m : ℕ) = (↑i.succ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
⊢ ((p.toFun (r := r) ∘ Fin.rev) i.castSucc, (p.toFun (r := r) ∘ Fin.rev) i.succ) ∈ r.inv
have rw : (p.toFun (r := r) i.succ.rev, p.toFun (r := r) i.castSucc.rev) ∈ r
Tactic: rw [Function.comp_apply, Function.comp_apply, SetRel.mem_inv]
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
⊢ (p.toFun (r := r) i.succ.rev, p.toFun (r := r) i.castSucc.rev) ∈ r
have hi : (↑i : ℕ) + 1 ≤ p.length (r := r)
Tactic: have hi : i.1 + 1 ≤ p.length := by lia
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
hi : (↑i : ℕ) + 1 ≤ p.length (r := r)
⊢ (p.toFun (r := r) i.succ.rev, p.toFun (r := r) i.castSucc.rev) ∈ r
have h : i.succ.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), sorry⟩.castSucc
Tactic: convert! p.step ⟨p.length - (i.1 + 1), Nat.sub_lt_self (by lia) hi⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
hi : (↑i : ℕ) + 1 ≤ p.length (r := r)
h : i.succ.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩.castSucc
⊢ (p.toFun (r := r) i.succ.rev, p.toFun (r := r) i.castSucc.rev) ∈ r
have h₁ : i.castSucc.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), sorry⟩.succ
Tactic: convert! p.step ⟨p.length - (i.1 + 1), Nat.sub_lt_self (by lia) hi⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
hi : (↑i : ℕ) + 1 ≤ p.length (r := r)
⊢ i.succ.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩.castSucc
have h : (↑i.succ.rev : ℕ) = (↑(⟨p.length (r := r) - ((↑i : ℕ) + 1), sorry⟩ : Fin (p.length (r := r))).castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
hi : (↑i : ℕ) + 1 ≤ p.length (r := r)
⊢ i.castSucc.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩.succ
have h : (↑i.castSucc.rev : ℕ) = (↑(⟨p.length (r := r) - ((↑i : ℕ) + 1), sorry⟩ : Fin (p.length (r := r))).succ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
hi : (↑i : ℕ) + 1 ≤ p.length (r := r)
⊢ (↑i.castSucc.rev : ℕ) = (↑(⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩ : Fin (p.length (r := r))).succ : ℕ)
have h : p.length (r := r) + 1 - ((↑i : ℕ) + 1) = p.length (r := r) - ((↑i : ℕ) + 1) + 1
Tactic: simp only [Fin.val_rev, Fin.val_castSucc, Fin.val_succ]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.reverse (r := r).reverse (r := r.inv) = p
have length_eq : p.reverse (r := r).reverse (r := r.inv).length (r := r.inv.inv) = p.length (r := r.inv.inv)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
length_eq : p.reverse (r := r).reverse (r := r.inv).length (r := r.inv.inv) = p.length (r := r.inv.inv)
⊢ p.reverse (r := r).reverse (r := r.inv) = p
have toFun_eq : ∀ (x : Fin (p.reverse (r := r).reverse (r := r.inv).length (r := r.inv.inv) + 1)),
  p.reverse (r := r).reverse (r := r.inv).toFun (r := r.inv.inv) x = (p.toFun (r := r.inv.inv) ∘ Fin.cast sorry) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newHead : α
rel : (newHead, p.head (r := r)) ∈ r
⊢ ((singleton r newHead).append (r := r) p rel).last (r := r) = p.last (r := r)
have rw : p.last (r := r) = p.last (r := r)
Tactic: rw [last_append]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
⊢ (p.cons (r := r) x hx).toList (r := r) = x :: p.toList (r := r)
have rw : (singleton r x).toList (r := r) ++ p.toList (r := r) = x :: p.toList (r := r)
Tactic: rw [cons, toList_append]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ fromListIsChain (r := r) (x :: l) ⋯ ⋯ = (fromListIsChain (r := r) l l_ne_nil hl).cons (r := r) x ⋯
have a : (fromListIsChain (r := r) (x :: l) sorry sorry).toList (r := r) =
  ((fromListIsChain (r := r) l l_ne_nil hl).cons (r := r) x sorry).toList (r := r)
Tactic: apply toList_injective
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
hq : (p.last (r := r), q.head (r := r)) ∈ r
⊢ ((singleton r x).append (r := r) p hx).append (r := r) q ⋯ =
    (singleton r x).append (r := r) (p.append (r := r) q hq) ⋯
have rw : (singleton r x).append (r := r) (p.append (r := r) q hq) sorry = (singleton r x).append (r := r) (p.append (r := r) q hq) sorry
Tactic: rw [append_assoc]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
⊢ (p.append (r := r) (singleton r newLast) rel).head (r := r) = p.head (r := r)
have rw : p.head (r := r) = p.head (r := r)
Tactic: rw [head_append]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
x : α
⊢ x ∈ p.snoc (r := r) newLast rel ↔ x ∈ p ∨ x = newLast
have simp : (∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x) ↔
  (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
Tactic: simp only [snoc, append, singleton_length, Nat.add_zero, Nat.reduceAdd, Fin.cast_refl,
    Function.comp_id, mem_def, Set.mem_range]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
x : α
⊢ (∃ (y : Fin (p.length (r := r) + 1 + 1)),
      Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x) ↔
    (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
have mp : (∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x) →
  (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
x : α
mp :
  (∃ (y : Fin (p.length (r := r) + 1 + 1)),
      Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x) →
    (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
⊢ (∃ (y : Fin (p.length (r := r) + 1 + 1)),
      Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x) ↔
    (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
have mpr : (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast →
  ∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
x : α
h : (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
⊢ ∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x
have mpr : ∀ (i : Fin (p.length (r := r) + 1)),
  ∃ (y : Fin (p.length (r := r) + 1 + 1)),
    Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = p.toFun (r := r) i
Tactic: rcases h with (⟨i, rfl⟩ | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
x : α
h : (∃ (y : Fin (p.length (r := r) + 1)), p.toFun (r := r) y = x) ∨ x = newLast
mpr :
  ∀ (i : Fin (p.length (r := r) + 1)),
    ∃ (y : Fin (p.length (r := r) + 1 + 1)),
      Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = p.toFun (r := r) i
⊢ ∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x
have mpr₁ : ∀ {rel : (p.last (r := r), x) ∈ r},
  ∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r x).toFun (r := r)) y = x
Tactic: rcases h with (⟨i, rfl⟩ | rfl)
Cleared hypotheses: newLast, rel, h
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ (p.tail (r := r) len_pos).head (r := r) = p.toFun (r := r) 1
have change : p.toFun (r := r) (Fin.cast sorry 0).succ = p.toFun (r := r) 1
Tactic: change p (Fin.succ _) = p 1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ p.toFun (r := r) (Fin.cast ⋯ 0).succ = p.toFun (r := r) 1
have e_a : (Fin.cast sorry 0).succ = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ (Fin.cast ⋯ 0).succ = 1
have e_a : (↑(Fin.cast sorry 0).succ : ℕ) = (↑1 : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ 1 = 1 % (p.length (r := r) + 1)
have e_a : 1 < p.length (r := r) + 1
Tactic: rw [Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ (p.tail (r := r) len_pos).last (r := r) = p.last (r := r)
have change : p.toFun (r := r) (Fin.cast sorry (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ =
  p.toFun (r := r) (Fin.last (p.length (r := r)))
Tactic: change p _ = p _
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ 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)))
have e_a : (Fin.cast sorry (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ = Fin.last (p.length (r := r))
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ (Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ = Fin.last (p.length (r := r))
have e_a : (↑(Fin.cast sorry (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ : ℕ) = (↑(Fin.last (p.length (r := r))) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
⊢ (↑(Fin.cast ⋯ (Fin.last ((p.tail (r := r) len_pos).length (r := r)))).succ : ℕ) =
    (↑(Fin.last (p.length (r := r))) : ℕ)
have e_a : p.length (r := r) - 1 + 1 = p.length (r := r)
Tactic: simp only [tail_length, Fin.val_succ, Fin.val_cast, Fin.val_last]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
have refine_1 : (p.tail (r := r) hp).toList (r := r).length = p.toList (r := r).tail.length
Tactic: refine List.ext_getElem ?_ fun i h1 h2 ↦ ?_
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ (p.tail (r := r) hp).toList (r := r) = p.toList (r := r).tail
have 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
Tactic: refine List.ext_getElem ?_ fun i h1 h2 ↦ ?_
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
⊢ (p.tail (r := r) hp).toList (r := r).length = p.toList (r := r).tail.length
have refine_1 : p.length (r := r) - 1 + 1 = p.length (r := r)
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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) ⋯ = p
have a : ((p.cons (r := r) x hx).tail (r := r) sorry).toList (r := r) = p.toList (r := r)
Tactic: apply toList_injective
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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)) ⋯ = p
have a : ((p.tail (r := r) hp).cons (r := r) (p.head (r := r)) sorry).toList (r := r) = p.toList (r := r)
Tactic: apply toList_injective
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ motive p
have h : p = RelSeries.singleton r (p.head (r := r))
Tactic: convert! singleton p.head
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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 = RelSeries.singleton r (p.head (r := r))
have h : p.length (r := r) = (RelSeries.singleton r (p.head (r := r))).length (r := r)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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)
⊢ p = RelSeries.singleton r (p.head (r := r))
have 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 sorry) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ motive p
have succ : (lq : (p.tail (r := r) sorry).length (r := r) = p.length (r := r) - 1) → motive p
Tactic: have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
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
⊢ motive p
have lq₁ : (p.tail (r := r) sorry).length (r := r) = d + 1 - 1
Tactic: nth_rw 3 [heq] at lq
Cleared hypotheses: lq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ motive p
have h : p = (p.tail (r := r) sorry).cons (r := r) (p.head (r := r)) sorry
Tactic: convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ motive p
have zero : (p : RelSeries r) → (heq : p.length (r := r) = 0) → 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
Cleared hypotheses: p, n, heq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ motive p
have 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
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
Cleared hypotheses: p, n, heq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
⊢ (p.eraseLast (r := r).last (r := r), p.last (r := r)) ∈ r
have simp : (p.toFun (r := r) (⟨p.length (r := r) - 1, sorry⟩ : Fin (p.length (r := r) + 1)),
    p.toFun (r := r) (⟨p.length (r := r), sorry⟩ : Fin (p.length (r := r) + 1))) ∈
  r
Tactic: simp only [last, Fin.last, eraseLast_length, eraseLast_toFun]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length (r := r) ≠ 0
⊢ (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
have h₁ : p.length (r := r) = (↑(⟨p.length (r := r) - 1, sorry⟩ : Fin (p.length (r := r))).succ : ℕ)
Tactic: convert! p.step ⟨p.length - 1, by lia⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length (r := r) ≠ 0
⊢ p.eraseLast (r := r).toList (r := r) = p.toList (r := r).dropLast
have hl : p.eraseLast (r := r).toList (r := r).length = p.toList (r := r).dropLast.length
Tactic: apply List.ext_getElem