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 : (↑m : ℕ) = (↑i : ℕ)
⊢ (↑m : ℕ) < (↑i : ℕ) + 1

Tactic:
hm ▸ lt_add_one _

Premises used: lt_add_one, Eq.rec
-- 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 : (↑m : ℕ) = (↑i : ℕ)
⊢ (↑m : ℕ) < (↑i : ℕ) + 1

Tactic:
exact hm ▸ lt_add_one _
-- 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 : (↑m : ℕ) = (↑i : ℕ)
⊢ @Eq.rec _ (i.succ.castSucc.succAbove (m.castSucc.castPred ⋯))
      (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.castSucc.castPred ⋯) = x) ↦ α)
      (p.toFun (r := r) (m.castSucc.castPred ⋯)) _ ⋯ =
    p.toFun (r := r) m

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))
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 : (↑m : ℕ) = (↑i : ℕ)
inr : (p.toFun (r := r) m, y) ∈ r
⊢ (x, y) ∈ r

Tactic:
rw [show x = p m from show Fin.insertNth _ _ _ _ = _ by
        rw [Fin.insertNth_apply_below]
        pick_goal 2
        · change m.1 < i.1 + 1; exact hm ▸ lt_add_one _
        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))
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 : (↑m : ℕ) = (↑i : ℕ)
⊢ (p.toFun (r := r) i.castSucc, a) ∈ r

Tactic:
prev_connect
-- 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 : (↑m : ℕ) = (↑i : ℕ)
h : m = i.castSucc
h₁ : y = a
⊢ (p.toFun (r := r) m, y) ∈ r

Tactic:
convert! prev_connect
-- 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 : (↑m : ℕ) = (↑i : ℕ)
h : (↑m : ℕ) = (↑i.castSucc : ℕ)
⊢ m = i.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))
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 : (↑m : ℕ) = (↑i : ℕ)
⊢ (↑m : ℕ) = (↑i.castSucc : ℕ)

Tactic:
hm
-- 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 : (↑m : ℕ) = (↑i : ℕ)
⊢ (↑m : ℕ) = (↑i.castSucc : ℕ)

Tactic:
exact hm
-- 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 : (↑m : ℕ) = (↑i : ℕ)
h : i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ = a
⊢ y = a

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 : (↑m : ℕ) = (↑i : ℕ)
h : (↑m.succ : ℕ) = (↑i.succ.castSucc : ℕ)
⊢ m.succ = i.succ.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))
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 : (↑m : ℕ) = (↑i : ℕ)
h : (↑m : ℕ) + 1 = (↑i : ℕ) + 1
⊢ (↑m.succ : ℕ) = (↑i.succ.castSucc : ℕ)

Tactic:
change _ + 1 = _ + 1
-- 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 : (↑m : ℕ) = (↑i : ℕ)
h h₁ : (↑i : ℕ) + 1 = (↑i : ℕ) + 1
⊢ (↑m : ℕ) + 1 = (↑i : ℕ) + 1

Tactic:
rw [hm]
-- 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 : (↑m : ℕ) = (↑i : ℕ)
h :
  i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) i.succ.castSucc =
    a
h₁ h₂ : a = a
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ = a

Tactic:
rw [show m.succ = i.succ.castSucc by ext; change _ + 1 = _ + 1; rw [hm],
          Fin.insertNth_apply_same]

Premises used: Fin.insertNth_apply_same
-- 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 : ℕ) < (↑m : ℕ)
⊢ (↑i : ℕ) + 1 < (↑m : ℕ) ∨ (↑i : ℕ) + 1 = (↑m : ℕ)

Tactic:
rw [Nat.lt_iff_add_one_le, le_iff_lt_or_eq] at hm

Premises used: Nat.lt_iff_add_one_le, le_iff_lt_or_eq
-- 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 : ℕ)
inr : ∀ (hm : (↑i : ℕ) + 1 < (↑m : ℕ)), (x, y) ∈ r
inr₁ : ∀ (hm : (↑i : ℕ) + 1 = (↑m : ℕ)), (x, y) ∈ r
⊢ (x, y) ∈ r

Tactic:
obtain hm | hm := hm
-- 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 : ℕ)
⊢ 1 ≤ (↑m : ℕ)

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 : x = p.toFun (r := r) ⟨(↑m : ℕ) - 1, ⋯⟩.castSucc
h₁ : y = p.toFun (r := r) ⟨(↑m : ℕ) - 1, ⋯⟩.succ
⊢ (x, y) ∈ r

Tactic:
convert! p.step ⟨m.1 - 1, Nat.sub_lt_right_of_lt_add (by lia) m.2⟩

Premises used: Nat.sub_lt_right_of_lt_add, HSub.hSub, Fin.isLt, Fin.mk, Fin.val, 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))
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.castSucc =
    p.toFun (r := r) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).castSucc
⊢ x = p.toFun (r := r) ⟨(↑m : ℕ) - 1, ⋯⟩.castSucc

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 _ (i.succ.castSucc.succAbove (m.castSucc.pred ⋯))
      (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.castSucc.pred ⋯) = x) ↦ α)
      (p.toFun (r := r) (m.castSucc.pred ⋯)) _ ⋯ =
    p.toFun (r := r) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).castSucc
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc =
    p.toFun (r := r) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).castSucc

Tactic:
rw [Fin.insertNth_apply_above (h := hm)]

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 : ℕ)
⊢ @Eq.rec _ (i.succ.castSucc.succAbove (m.castSucc.pred ⋯))
      (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.castSucc.pred ⋯) = x) ↦ α)
      (p.toFun (r := r) (m.castSucc.pred ⋯)) _ ⋯ =
    p.toFun (r := r) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).castSucc

Tactic:
aesop
-- 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) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).succ
⊢ y = p.toFun (r := r) ⟨(↑m : ℕ) - 1, ⋯⟩.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 _ (i.succ.castSucc.succAbove (m.succ.pred ⋯))
      (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) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).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) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).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 : ℕ)
⊢ i.succ.castSucc < m.succ

Tactic:
hm.trans (lt_add_one _)

Premises used: lt_add_one, LT.lt.trans
-- 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.succ.castSucc < m.succ

Tactic:
exact hm.trans (lt_add_one _)

Premises used: lt_add_one, LT.lt.trans
-- 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) ⟨(↑m : ℕ) - 1 + 1, ⋯⟩
⊢ @Eq.rec _ (i.succ.castSucc.succAbove (m.succ.pred ⋯))
      (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) (⟨(↑m : ℕ) - 1, ⋯⟩ : Fin (p.length (r := r))).succ

Tactic:
simp only [Fin.pred_succ, eq_rec_constant, Fin.succ_mk]

Premises used: Fin.pred_succ, Fin.succ_mk, 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 = ⟨(↑m : ℕ) - 1 + 1, ⋯⟩
⊢ p.toFun (r := r) m = p.toFun (r := r) ⟨(↑m : ℕ) - 1 + 1, ⋯⟩

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 : ℕ)
⊢ m = ⟨(↑m : ℕ) - 1 + 1, ⋯⟩

Tactic:
Fin.ext <| Eq.symm <| Nat.succ_pred_eq_of_pos (lt_trans (Nat.zero_lt_succ _) hm)

Premises used: Nat.succ_pred_eq_of_pos, Nat.zero_lt_succ, lt_trans, Fin.ext, 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 = ⟨(↑m : ℕ) - 1 + 1, ⋯⟩

Tactic:
exact Fin.ext <| Eq.symm <| Nat.succ_pred_eq_of_pos (lt_trans (Nat.zero_lt_succ _) hm)

Premises used: Nat.succ_pred_eq_of_pos, Nat.zero_lt_succ, lt_trans, Fin.ext, 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 : ℕ)
⊢ (a, p.toFun (r := r) i.succ) ∈ r

Tactic:
connect_next
-- 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 : x = a
h₁ : y = p.toFun (r := r) i.succ
⊢ (x, y) ∈ r

Tactic:
convert! connect_next
-- 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.castSucc = a
⊢ x = a

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 :
  i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) i.succ.castSucc =
    a
h₁ h₂ : a = a
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc = a

Tactic:
rw [show m.castSucc = i.succ.castSucc from Fin.ext hm.symm, Fin.insertNth_apply_same]

Premises used: Fin.ext, Fin.insertNth_apply_same, Eq.symm