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))
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 :
  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
⊢ y = p.toFun (r := r) i.succ

Tactic:
change Fin.insertNth _ _ _ _ = _

Premises used: Fin.insertNth
-- Module: Mathlib.Order.RelSeries
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
h₁ : i.succ.castSucc < m.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

Tactic:
rw [Fin.insertNth_apply_above]

Premises used: Fin.insertNth_apply_above
-- Module: Mathlib.Order.RelSeries
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 : (↑i : ℕ) + 1 < (↑m : ℕ) + 1
⊢ i.succ.castSucc < m.succ

Tactic:
change i.1 + 1 < m.1 + 1

Premises used: Fin.val
-- Module: Mathlib.Order.RelSeries
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 : ℕ) + 1 < (↑m : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
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 : p.toFun (r := r) m = p.toFun (r := r) i.succ
⊢ 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

Tactic:
simp only [Fin.pred_succ, eq_rec_constant]

Premises used: Fin.pred_succ, eq_rec_constant
-- Module: Mathlib.Order.RelSeries
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 : m = i.succ
⊢ p.toFun (r := r) m = p.toFun (r := r) i.succ

Tactic:
congr
-- Module: Mathlib.Order.RelSeries
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 : (↑m : ℕ) = (↑i.succ : ℕ)
⊢ m = i.succ

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
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 : ℕ)

Tactic:
hm.symm

Premises used: Eq.symm
-- Module: Mathlib.Order.RelSeries
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 : ℕ)

Tactic:
exact hm.symm

Premises used: Eq.symm
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
rw : (p.toFun (r := r) i.succ.rev, p.toFun (r := r) i.castSucc.rev) ∈ r
⊢ ((p.toFun (r := r) ∘ Fin.rev) i.castSucc, (p.toFun (r := r) ∘ Fin.rev) i.succ) ∈ r.inv

Tactic:
rw [Function.comp_apply, Function.comp_apply, SetRel.mem_inv]

Premises used: SetRel.mem_inv, Function.comp_apply
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
⊢ (↑i : ℕ) + 1 ≤ p.length (r := r)

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

Tactic:
have hi : i.1 + 1 ≤ p.length := by lia
-- Module: Mathlib.Order.RelSeries
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)
⊢ 0 < (↑i : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
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
h₁ : i.castSucc.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩.succ
⊢ (p.toFun (r := r) i.succ.rev, p.toFun (r := r) i.castSucc.rev) ∈ r

Tactic:
convert! p.step ⟨p.length - (i.1 + 1), Nat.sub_lt_self (by lia) hi⟩

Premises used: HSub.hSub, Fin.mk, RelSeries.length, Nat.sub_lt_self, Fin.val, HAdd.hAdd, RelSeries.step, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
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), ⋯⟩ : Fin (p.length (r := r))).castSucc : ℕ)
⊢ i.succ.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩.castSucc

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
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), ⋯⟩ : Fin (p.length (r := r))).castSucc : ℕ)

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
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.castSucc.rev : ℕ) = (↑(⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩ : Fin (p.length (r := r))).succ : ℕ)
⊢ i.castSucc.rev = ⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩.succ

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
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 : p.length (r := r) + 1 - ((↑i : ℕ) + 1) = p.length (r := r) - ((↑i : ℕ) + 1) + 1
⊢ (↑i.castSucc.rev : ℕ) = (↑(⟨p.length (r := r) - ((↑i : ℕ) + 1), ⋯⟩ : Fin (p.length (r := r))).succ : ℕ)

Tactic:
simp only [Fin.val_rev, Fin.val_castSucc, Fin.val_succ]

Premises used: Fin.val_succ, Fin.val_rev, Fin.val_castSucc
-- Module: Mathlib.Order.RelSeries
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.length (r := r) + 1 - ((↑i : ℕ) + 1) = p.length (r := r) - ((↑i : ℕ) + 1) + 1

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.reverse (r := r).last (r := r.inv) = p.head (r := r)

Tactic:
simp [RelSeries.last, RelSeries.head]

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

Tactic:
simp [RelSeries.last, RelSeries.head]

Premises used: RelSeries.last, RelSeries.head
-- Module: Mathlib.Order.RelSeries
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)
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 ⋯) x
⊢ p.reverse (r := r).reverse (r := r.inv) = p

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.reverse (r := r).reverse (r := r.inv).length (r := r.inv.inv) = p.length (r := r.inv.inv)

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
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 ⋯) x

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newHead : α
rel : (newHead, p.head (r := r)) ∈ r
⊢ (p.cons (r := r) newHead rel).head (r := r) = newHead

Tactic:
rfl

Premises used: Fin.addCases, dite, RelSeries.head, Fin.append, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newHead : α
rel : (newHead, p.head (r := r)) ∈ r
rw rw₁ : p.last (r := r) = p.last (r := r)
⊢ ((singleton r newHead).append (r := r) p rel).last (r := r) = p.last (r := r)

Tactic:
rw [last_append]

Premises used: RelSeries.last_append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
s : RelSeries r
a : α
h : (a, s.head (r := r)) ∈ r
i : Fin (s.length (r := r) + 1)
⊢ s.length (r := r) + 1 + 1 = (s.cons (r := r) a h).length (r := r) + 1

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
a : α
h : (a, s.head (r := r)) ∈ r
i : Fin (s.length (r := r) + 1)
⊢ (s.cons (r := r) a h).toFun (r := r) (Fin.cast ⋯ i.succ) = s.toFun (r := r) i

Tactic:
simp [cons, Fin.append, Fin.addCases, Fin.subNat]

Premises used: Fin.subNat, RelSeries.cons, Fin.append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
⊢ (singleton r x).append (r := r) p hx = p.cons (r := r) x hx

Tactic:
rfl

Premises used: RelSeries.cons, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
rw : (singleton r x).toList (r := r) ++ p.toList (r := r) = x :: p.toList (r := r)
⊢ (p.cons (r := r) x hx).toList (r := r) = x :: p.toList (r := r)

Tactic:
rw [cons, toList_append]

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

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : 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
⊢ x :: l ≠ []

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : 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
⊢ (x, (fromListIsChain (r := r) l l_ne_nil hl).head (r := r)) ∈ r

Tactic:
simpa
-- 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
x : α
hx : (x, l.head l_ne_nil) ∈ r
a :
  (fromListIsChain (r := r) (x :: l) ⋯ ⋯).toList (r := r) =
    ((fromListIsChain (r := r) l l_ne_nil hl).cons (r := r) x ⋯).toList (r := r)
⊢ fromListIsChain (r := r) (x :: l) ⋯ ⋯ = (fromListIsChain (r := r) l l_ne_nil hl).cons (r := r) x ⋯

Tactic:
apply toList_injective

Premises used: RelSeries.toList_injective
-- 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
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ (fromListIsChain (r := r) (x :: l) ⋯ ⋯).toList (r := r) =
    ((fromListIsChain (r := r) l l_ne_nil hl).cons (r := r) x ⋯).toList (r := r)

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
hq : (p.last (r := r), q.head (r := r)) ∈ r
⊢ ((p.cons (r := r) x hx).last (r := r), q.head (r := r)) ∈ r

Tactic:
simpa
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
x : α
hx : (x, p.head (r := r)) ∈ r
hq : (p.last (r := r), q.head (r := r)) ∈ r
⊢ (x, (p.append (r := r) q hq).head (r := r)) ∈ r

Tactic:
simpa
-- Module: Mathlib.Order.RelSeries
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
rw :
  (singleton r x).append (r := r) (p.append (r := r) q hq) ⋯ =
    (singleton r x).append (r := r) (p.append (r := r) q hq) ⋯
hqw : (p.last (r := r), q.head (r := r)) ∈ r
rw₁ :
  (singleton r x).append (r := r) (p.append (r := r) q hq) ⋯ =
    (singleton r x).append (r := r) (p.append (r := r) q hq) ⋯
hqw₁ : (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) ⋯

Tactic:
rw [append_assoc]

Premises used: RelSeries.append_assoc
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
rw rw₁ : p.head (r := r) = p.head (r := r)
⊢ (p.append (r := r) (singleton r newLast) rel).head (r := r) = p.head (r := r)

Tactic:
rw [head_append]

Premises used: RelSeries.head_append
-- 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).last (r := r) = newLast

Tactic:
last_append _ _ _

Premises used: RelSeries.last, RelSeries.last_append, RelSeries.snoc
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
s : RelSeries r
a : α
h : (s.last (r := r), a) ∈ r
i : Fin (s.length (r := r) + 1)
⊢ s.length (r := r) + 1 + 1 = (s.snoc (r := r) a h).length (r := r) + 1

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
a : α
h : (s.last (r := r), a) ∈ r
i : Fin (s.length (r := r) + 1)
⊢ (s.snoc (r := r) a h).toFun (r := r) (Fin.cast ⋯ i.castSucc) = s.toFun (r := r) i

Tactic:
append_apply_left s (singleton r a) h i

Premises used: RelSeries.append_apply_left, RelSeries.singleton
-- 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).toFun (r := r) (Fin.last (p.length (r := r) + 1)) = newLast

Tactic:
last_append _ _ _

Premises used: RelSeries.last, RelSeries.last_append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
a : α
connect : (s.last (r := r), a) ∈ r
i : Fin (s.length (r := r) + 1)
⊢ (s.snoc (r := r) a connect).toFun (r := r) i.castSucc = s.toFun (r := r) i

Tactic:
Fin.append_left _ _ i

Premises used: Fin.natAdd, Fin.addCases, dite, Fin.append_left, Fin.append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
x : α
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
⊢ x ∈ p.snoc (r := r) newLast rel ↔ x ∈ p ∨ 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]

Premises used: Set.mem_range, Function.comp_id, Nat.reduceAdd, RelSeries.snoc, RelSeries.singleton_length, RelSeries.mem_def, RelSeries.append, Nat.add_zero, Fin.cast_refl
-- Module: Mathlib.Order.RelSeries
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
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
⊢ (∃ (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
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
i : Fin (p.length (r := r) + 1 + 1)
⊢ (∃ (y : Fin (p.length (r := r) + 1)),
      p.toFun (r := r) y = Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) i) ∨
    Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) i = newLast

Tactic:
Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
      (Fin.append_left _ _ _).symm⟩) i

Premises used: Fin.lastCases
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
i : Fin (p.length (r := r) + 1 + 1)
⊢ (∃ (y : Fin (p.length (r := r) + 1)),
      p.toFun (r := r) y = Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) i) ∨
    Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) i = newLast

Tactic:
exact Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
      (Fin.append_left _ _ _).symm⟩) i
-- Module: Mathlib.Order.RelSeries
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
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
⊢ ∃ (y : Fin (p.length (r := r) + 1 + 1)), Fin.append (p.toFun (r := r)) ((singleton r newLast).toFun (r := r)) y = x

Tactic:
rcases h with (⟨i, rfl⟩ | 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
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:
⟨i.castSucc, Fin.append_left _ _ _⟩

Premises used: Fin.append_left, Exists.intro, Fin.castSucc
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last (r := r), newLast) ∈ r
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:
exact ⟨i.castSucc, Fin.append_left _ _ _⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
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:
⟨Fin.last _, Fin.append_right _ _ 0⟩

Premises used: Fin.append_right, Fin.last, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
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:
exact ⟨Fin.last _, Fin.append_right _ _ 0⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
change : p.toFun (r := r) (Fin.cast ⋯ 0).succ = p.toFun (r := r) 1
⊢ (p.tail (r := r) len_pos).head (r := r) = p.toFun (r := r) 1

Tactic:
change p (Fin.succ _) = p 1

Premises used: Fin.succ, RelSeries.toFun, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
e_a : (Fin.cast ⋯ 0).succ = 1
⊢ p.toFun (r := r) (Fin.cast ⋯ 0).succ = p.toFun (r := r) 1

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 ⋯ 0).succ : ℕ) = (↑1 : ℕ)
⊢ (Fin.cast ⋯ 0).succ = 1

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
e_a : 1 < p.length (r := r) + 1
⊢ 1 = 1 % (p.length (r := r) + 1)

Tactic:
rw [Nat.mod_eq_of_lt]

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

Tactic:
simpa only [lt_add_iff_pos_left, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero, lt_add_iff_pos_left
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length (r := r) ≠ 0
change :
  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)))
⊢ (p.tail (r := r) len_pos).last (r := r) = p.last (r := r)

Tactic:
change p _ = p _

Premises used: RelSeries.toFun