awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (p.length (r := r) + 1)
delta :
  toFun (r := r)
      (mk (r := r) (p.length (r := r) + q.length (r := r) + 1)
        (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) ⋯)
      (Fin.cast ⋯ (Fin.castAdd (q.length (r := r) + 1) i)) =
    p.toFun (r := r) i
⊢ (p.append (r := r) q connect).toFun (r := r) (Fin.cast ⋯ (Fin.castAdd (q.length (r := r) + 1) i)) = p.toFun (r := r) i

Tactic:
delta append

Premises used: RelSeries.append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (p.length (r := r) + 1)
simp :
  Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.cast ⋯ (Fin.cast ⋯ (Fin.castAdd (q.length (r := r) + 1) i))) =
    p.toFun (r := r) i
⊢ toFun (r := r)
      (mk (r := r) (p.length (r := r) + q.length (r := r) + 1)
        (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) ⋯)
      (Fin.cast ⋯ (Fin.castAdd (q.length (r := r) + 1) i)) =
    p.toFun (r := r) i

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (p.length (r := r) + 1)
⊢ Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) i) = p.toFun (r := r) i

Tactic:
Fin.append_left _ _ _

Premises used: Fin.append_left
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (p.length (r := r) + 1)
⊢ Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.cast ⋯ (Fin.cast ⋯ (Fin.castAdd (q.length (r := r) + 1) i))) =
    p.toFun (r := r) i

Tactic:
convert! Fin.append_left _ _ _

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

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (q.length (r := r) + 1)
⊢ (p.append (r := r) q connect).toFun (r := r) (Fin.cast ⋯ (Fin.natAdd (p.length (r := r) + 1) i)) = q.toFun (r := r) i

Tactic:
Fin.append_right _ _ _

Premises used: Fin.natAdd, Fin.addCases, Fin.append_right, dite, Nat.pred, Fin.append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
⊢ (p.append (r := r) q connect).head (r := r) = p.head (r := r)

Tactic:
append_apply_left p q connect 0

Premises used: Fin.ofNat, RelSeries.append_apply_left, Nat.mod, RelSeries.head, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
⊢ (p.append (r := r) q connect).toFun (r := r)
      (Fin.cast ⋯ (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))

Tactic:
append_apply_right p q connect (Fin.last _)

Premises used: RelSeries.append_apply_right, Fin.last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
h :
  Fin.last ((p.append (r := r) q connect).length (r := r)) =
    Fin.cast ⋯ (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))
⊢ (p.append (r := r) q connect).toFun (r := r) (Fin.last ((p.append (r := r) q connect).length (r := r))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))

Tactic:
convert! append_apply_right p q connect (Fin.last _)

Premises used: RelSeries.append_apply_right, Fin.last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
h :
  (↑(Fin.last ((p.append (r := r) q connect).length (r := r))) : ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))) : ℕ)
⊢ Fin.last ((p.append (r := r) q connect).length (r := r)) =
    Fin.cast ⋯ (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))

Tactic:
ext1
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
h : p.length (r := r) + q.length (r := r) + 1 = p.length (r := r) + 1 + q.length (r := r)
⊢ (↑(Fin.last ((p.append (r := r) q connect).length (r := r))) : ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
⊢ p.length (r := r) + q.length (r := r) + 1 = p.length (r := r) + 1 + q.length (r := r)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q w : RelSeries r
hpq : (p.last (r := r), q.head (r := r)) ∈ r
hqw : (q.last (r := r), w.head (r := r)) ∈ r
⊢ ((p.append (r := r) q hpq).last (r := r), w.head (r := r)) ∈ r

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

Tactic:
simpa
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last (r := r), q.head (r := r)) ∈ r
hqw : (q.last (r := r), w.head (r := r)) ∈ r
length_eq :
  ((p.append (r := r) q hpq).append (r := r) w ⋯).length (r := r) =
    (p.append (r := r) (q.append (r := r) w hqw) ⋯).length (r := r)
toFun_eq :
  ∀ (x : Fin (((p.append (r := r) q hpq).append (r := r) w ⋯).length (r := r) + 1)),
    ((p.append (r := r) q hpq).append (r := r) w ⋯).toFun (r := r) x =
      ((p.append (r := r) (q.append (r := r) w hqw) ⋯).toFun (r := r) ∘ Fin.cast ⋯) x
⊢ (p.append (r := r) q hpq).append (r := r) w ⋯ = p.append (r := r) (q.append (r := r) w hqw) ⋯

Tactic:
ext
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last (r := r), q.head (r := r)) ∈ r
hqw : (q.last (r := r), w.head (r := r)) ∈ r
length_eq :
  p.length (r := r) + q.length (r := r) + 1 + w.length (r := r) =
    p.length (r := r) + (q.length (r := r) + w.length (r := r) + 1)
⊢ ((p.append (r := r) q hpq).append (r := r) w ⋯).length (r := r) =
    (p.append (r := r) (q.append (r := r) w hqw) ⋯).length (r := r)

Tactic:
simp only [append_length, Nat.add_left_inj]

Premises used: RelSeries.append_length, Nat.add_left_inj
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last (r := r), q.head (r := r)) ∈ r
hqw : (q.last (r := r), w.head (r := r)) ∈ r
⊢ p.length (r := r) + q.length (r := r) + 1 + w.length (r := r) =
    p.length (r := r) + (q.length (r := r) + w.length (r := r) + 1)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last (r := r), q.head (r := r)) ∈ r
hqw : (q.last (r := r), w.head (r := r)) ∈ r
x : Fin (((p.append (r := r) q hpq).append (r := r) w ⋯).length (r := r) + 1)
⊢ ((p.append (r := r) q hpq).append (r := r) w ⋯).toFun (r := r) x =
    ((p.append (r := r) (q.append (r := r) w hqw) ⋯).toFun (r := r) ∘ Fin.cast ⋯) x

Tactic:
simp [append, Fin.append_assoc]

Premises used: Fin.append_assoc, RelSeries.append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
hl : (p.append (r := r) q connect).toList (r := r).length = (p.toList (r := r) ++ q.toList (r := r)).length
h :
  ∀ (i : ℕ) (h₁ : i < (p.append (r := r) q connect).toList (r := r).length)
    (h₂ : i < (p.toList (r := r) ++ q.toList (r := r)).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.append (r := r) q connect).toList (r := r)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList (r := r) ++ q.toList (r := r)) i h₂
⊢ (p.append (r := r) q connect).toList (r := r) = p.toList (r := r) ++ q.toList (r := r)

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
hl : p.length (r := r) + q.length (r := r) + 1 + 1 = p.length (r := r) + 1 + (q.length (r := r) + 1)
⊢ (p.append (r := r) q connect).toList (r := r).length = (p.toList (r := r) ++ q.toList (r := r)).length

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
⊢ p.length (r := r) + q.length (r := r) + 1 + 1 = p.length (r := r) + 1 + (q.length (r := r) + 1)

Tactic:
grind
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
⊢ ∀ (i : ℕ) (h₁ : i < (p.append (r := r) q connect).toList (r := r).length)
    (h₂ : i < (p.toList (r := r) ++ q.toList (r := r)).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.append (r := r) q connect).toList (r := r)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList (r := r) ++ q.toList (r := r)) i h₂

Tactic:
simp [List.getElem_append, Fin.append, Fin.addCases]

Premises used: List.getElem_append, Fin.append
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
f : r.Hom s
i : Fin (p.length (r := r) + 1)
⊢ (p.map (r := r) (s := s) f).toFun (r := s) i = (f : (a : α) → β) (p.toFun (r := r) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
f : r.Hom s
⊢ (p.map (r := r) (s := s) f).head (r := s) = (f : (a : α) → β) (p.head (r := r))

Tactic:
rfl

Premises used: RelSeries.head, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
f : r.Hom s
⊢ (p.map (r := r) (s := s) f).last (r := s) = (f : (a : α) → β) (p.last (r := r))

Tactic:
rfl

Premises used: RelSeries.last, rfl
-- 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
change : (x, y) ∈ r
⊢ Membership.mem (α := α × α) r
    ((i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc,
        i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ) :
      α × α)

Tactic:
change x ~[r] y
-- 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
inl : ∀ (hm : (↑m : ℕ) < (↑i : ℕ)), (x, y) ∈ r
inr : ∀ (hm : (↑m : ℕ) = (↑i : ℕ)), (x, y) ∈ r
inr₁ : ∀ (hm : (↑i : ℕ) < (↑m : ℕ)), (x, y) ∈ r
⊢ (x, y) ∈ r

Tactic:
obtain hm | hm | hm := lt_trichotomy m.1 i.1

Premises used: Fin.val, lt_trichotomy
-- 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) (⟨(↑m : ℕ), ⋯⟩ : Fin (p.length (r := r))).castSucc,
      p.toFun (r := r) (⟨(↑m : ℕ), ⋯⟩ : Fin (p.length (r := r))).succ) ∈
    r

Tactic:
p.step ⟨m, hm.trans i.2⟩

Premises used: Fin.isLt, Fin.mk, Fin.val, LT.lt.trans, RelSeries.step
-- 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 : x = p.toFun (r := r) ⟨(↑m : ℕ), ⋯⟩.castSucc
h₁ : y = p.toFun (r := r) ⟨(↑m : ℕ), ⋯⟩.succ
⊢ (x, y) ∈ r

Tactic:
convert! p.step ⟨m, hm.trans i.2⟩

Premises used: Fin.isLt, Fin.mk, Fin.val, LT.lt.trans, RelSeries.step
-- 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.castSucc =
    p.toFun (r := r) (⟨(↑m : ℕ), ⋯⟩ : Fin (p.length (r := r))).castSucc
⊢ x = p.toFun (r := r) ⟨(↑m : ℕ), ⋯⟩.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 : (↑m : ℕ) < (↑i : ℕ)
h :
  @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 : ℕ), ⋯⟩ : Fin (p.length (r := r))).castSucc
h₁ : m.castSucc < i.succ.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 : ℕ), ⋯⟩ : Fin (p.length (r := r))).castSucc

Tactic:
rw [Fin.insertNth_apply_below]

Premises used: Fin.insertNth_apply_below
-- 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.castSucc < i.succ.castSucc

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

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

Tactic:
rw [Fin.insertNth_apply_below]

Premises used: Fin.insertNth_apply_below
-- 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 m.1 + 1 < i.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 : (↑m : ℕ) < (↑i : ℕ)
h h₁ h₂ h₃ : (↑m : ℕ) < (↑i : ℕ)
⊢ (↑m : ℕ) + 1 < (↑i : ℕ) + 1

Tactic:
rwa [add_lt_add_iff_right]

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

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 : ℕ)
⊢ p.toFun (r := r) (m.succ.castPred ⋯) = p.toFun (r := r) ⟨(↑m : ℕ) + 1, ⋯⟩

Tactic:
rfl
-- 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 : ℕ)
rw :
  @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
h : m.castSucc < i.succ.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

Tactic:
rw [Fin.insertNth_apply_below]

Premises used: Fin.insertNth_apply_below
-- 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 : ℕ) + 1
⊢ m.castSucc < i.succ.castSucc

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

Premises used: Fin.val