awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (p.length (r := r) + q.length (r := r) + 1)
inl :
  ∀ (hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))),
    ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc,
        (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ) ∈
      r
inr :
  ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯)
        (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯)
        (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).succ) ∈
    r
inr₁ :
  ∀ (hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i),
    ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc,
        (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ) ∈
      r
⊢ ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ) ∈
    r

Tactic:
obtain hi | rfl | hi :=
      lt_trichotomy i (Fin.castLE (by lia) (Fin.last _ : Fin (p.length + 1)))

Premises used: Fin.castLE, Fin.last, rfl, lt_trichotomy
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ (p.toFun (r := r) (⟨(↑i : ℕ), hi⟩ : Fin (p.length (r := r))).castSucc,
      p.toFun (r := r) (⟨(↑i : ℕ), hi⟩ : Fin (p.length (r := r))).succ) ∈
    r

Tactic:
p.step ⟨i.1, hi⟩

Premises used: Fin.mk, Fin.val, RelSeries.step
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
h :
  (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.castSucc
h₁ : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.succ
⊢ ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ) ∈
    r

Tactic:
convert! p.step ⟨i.1, hi⟩

Premises used: Fin.mk, Fin.val, RelSeries.step
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ Fin.append (p.toFun (r := r)) (q.toFun (r := r))
      (Fin.castAdd (q.length (r := r) + 1) (⟨(↑i : ℕ), hi⟩ : Fin (p.length (r := r))).castSucc) =
    p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.castSucc

Tactic:
Fin.append_left p q _

Premises used: Fin.append_left, RelSeries.toFun
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
h :
  (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc =
    Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ), hi⟩.castSucc)
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.castSucc

Tactic:
convert! Fin.append_left p q _

Premises used: Fin.append_left, RelSeries.toFun
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ Fin.append (p.toFun (r := r)) (q.toFun (r := r))
      (Fin.castAdd (q.length (r := r) + 1) (⟨(↑i : ℕ), hi⟩ : Fin (p.length (r := r))).succ) =
    p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.succ

Tactic:
Fin.append_left p q _

Premises used: Fin.append_left, RelSeries.toFun
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
h :
  (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ =
    Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ), hi⟩.succ)
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.succ

Tactic:
convert! Fin.append_left p q _

Premises used: Fin.append_left, RelSeries.toFun
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc =
    Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ), hi⟩.castSucc)

Tactic:
rfl
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ =
    Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ), hi⟩.succ)

Tactic:
rfl
-- 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
⊢ (p.last (r := r), q.head (r := r)) ∈ r

Tactic:
connect
-- 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
h :
  (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯)
      (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).castSucc =
    p.last (r := r)
h₁ :
  (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).succ =
    q.head (r := r)
⊢ ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯)
        (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯)
        (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).succ) ∈
    r

Tactic:
convert! connect
-- 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
⊢ Fin.append (p.toFun (r := r)) (q.toFun (r := r))
      (Fin.castAdd (q.length (r := r) + 1) (Fin.last (p.length (r := r)))) =
    p.toFun (r := r) (Fin.last (p.length (r := r)))

Tactic:
Fin.append_left p q _

Premises used: Fin.append_left, RelSeries.toFun
-- 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
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯)
      (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).castSucc =
    p.last (r := r)

Tactic:
convert! Fin.append_left p q _

Premises used: Fin.append_left, RelSeries.toFun
-- 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
⊢ Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r) + 1) 0) = q.toFun (r := r) 0

Tactic:
Fin.append_right p q _

Premises used: Fin.append_right, RelSeries.toFun
-- 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
h :
  (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).succ =
    Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r) + 1) 0)
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).succ =
    q.head (r := r)

Tactic:
convert! Fin.append_right p q _

Premises used: Fin.append_right, RelSeries.toFun
-- 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
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) (Fin.castLE ⋯ (Fin.last (p.length (r := r)))).succ =
    Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r) + 1) 0)

Tactic:
rfl
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
inr : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) x, Fin.append (p.toFun (r := r)) (q.toFun (r := r)) y) ∈ r
⊢ ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ) ∈
    r

Tactic:
change Fin.append p q x ~[r] Fin.append p q y

Premises used: RelSeries.toFun, Fin.append
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
⊢ p.length (r := r) + q.length (r := r) + 1 < p.length (r := r) + 1 + (q.length (r := r) + 1)

Tactic:
lia
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
h : (↑x : ℕ) = (↑(Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩) : ℕ)
⊢ x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩

Tactic:
ext
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
h : (↑i : ℕ) = p.length (r := r) + 1 + ((↑i : ℕ) - (p.length (r := r) + 1))
⊢ (↑x : ℕ) = (↑(Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩) : ℕ)

Tactic:
dsimp [x, y]
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
h : p.length (r := r) + 1 ≤ (↑i : ℕ)
⊢ (↑i : ℕ) = p.length (r := r) + 1 + ((↑i : ℕ) - (p.length (r := r) + 1))

Tactic:
rw [Nat.add_sub_cancel']

Premises used: Nat.add_sub_cancel'
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
⊢ p.length (r := r) + 1 ≤ (↑i : ℕ)

Tactic:
hi

Premises used: Nat.lt
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
⊢ p.length (r := r) + 1 ≤ (↑i : ℕ)

Tactic:
exact hi
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
⊢ x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩

Tactic:
have hx : x = Fin.natAdd _ ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <|
          i.2.trans <| by lia⟩ := by
        ext; dsimp [x, y]; rw [Nat.add_sub_cancel']; exact hi
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
⊢ (↑i : ℕ) < p.length (r := r) + (q.length (r := r) + 1)

Tactic:
i.2

Premises used: Fin.isLt
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
⊢ (↑i : ℕ) < p.length (r := r) + (q.length (r := r) + 1)

Tactic:
exact i.2

Premises used: Fin.isLt
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
h : (↑y : ℕ) = (↑(Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩) : ℕ)
⊢ y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩

Tactic:
ext
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
rw : (↑i : ℕ) + 1
| p.length (r := r) + 1 + ((↑i : ℕ) - p.length (r := r))

Tactic:
rw [Nat.add_comm p.length 1, add_assoc,
          Nat.add_sub_cancel' <| le_of_lt (show p.length < i.1 from hi), add_comm]

Premises used: add_assoc, le_of_lt, RelSeries.length, add_comm, Nat.add_sub_cancel', OfNat.ofNat, Nat.add_comm
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
h : (↑y : ℕ) = (↑i : ℕ) + 1
⊢ (↑y : ℕ) = p.length (r := r) + 1 + ((↑i : ℕ) - p.length (r := r))

Tactic:
conv_rhs => rw [Nat.add_comm p.length 1, add_assoc,
          Nat.add_sub_cancel' <| le_of_lt (show p.length < i.1 from hi), add_comm]

Premises used: add_assoc, le_of_lt, RelSeries.length, add_comm, Nat.add_sub_cancel', OfNat.ofNat, Nat.add_comm
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
⊢ (↑y : ℕ) = (↑i : ℕ) + 1

Tactic:
rfl
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
⊢ y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩

Tactic:
have hy : y = Fin.natAdd _ ⟨i - p.length, Nat.sub_lt_left_of_lt_add (le_of_lt hi)
          (by exact i.2)⟩ := by
        ext
        dsimp
        conv_rhs => rw [Nat.add_comm p.length 1, add_assoc,
          Nat.add_sub_cancel' <| le_of_lt (show p.length < i.1 from hi), add_comm]
        rfl
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩
inr :
  (q.toFun (r := r) (⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩ : Fin (q.length (r := r) + 1)),
      q.toFun (r := r) (⟨(↑i : ℕ) - p.length (r := r), ⋯⟩ : Fin (q.length (r := r) + 1))) ∈
    r
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) x, Fin.append (p.toFun (r := r)) (q.toFun (r := r)) y) ∈ r

Tactic:
rw [hx, Fin.append_right, hy, Fin.append_right]

Premises used: Fin.append_right
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩
⊢ (↑i : ℕ) < 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 : RelSeries r
connect : (p.last (r := r), q.head (r := r)) ∈ r
i : Fin (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩
h : (↑i : ℕ) - p.length (r := r) = (↑(⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩ : Fin (q.length (r := r))).succ : ℕ)
⊢ (q.toFun (r := r) (⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩ : Fin (q.length (r := r) + 1)),
      q.toFun (r := r) (⟨(↑i : ℕ) - p.length (r := r), ⋯⟩ : Fin (q.length (r := r) + 1))) ∈
    r

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

Premises used: HSub.hSub, Fin.mk, RelSeries.length, Fin.val, HAdd.hAdd, RelSeries.step, OfNat.ofNat, Nat.sub_lt_left_of_lt_add
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩
h : p.length (r := r) + 1 ≤ (↑i : ℕ)
⊢ (↑i : ℕ) - p.length (r := r) = (↑(⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩ : Fin (q.length (r := r))).succ : ℕ)

Tactic:
rw [Fin.succ_mk, Nat.sub_eq_iff_eq_add (le_of_lt hi : p.length ≤ i),
        Nat.add_assoc _ 1, add_comm 1, Nat.sub_add_cancel]

Premises used: le_of_lt, Nat.sub_eq_iff_eq_add, add_comm, Fin.succ_mk, Nat.sub_add_cancel, Nat.add_assoc, OfNat.ofNat
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩
⊢ p.length (r := r) + 1 ≤ (↑i : ℕ)

Tactic:
hi

Premises used: Nat.lt
-- 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 (p.length (r := r) + q.length (r := r) + 1)
hi : Fin.castLE ⋯ (Fin.last (p.length (r := r))) < i
x : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length (r := r) + 1 + (q.length (r := r) + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩
hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), ⋯⟩
⊢ p.length (r := r) + 1 ≤ (↑i : ℕ)

Tactic:
exact hi
-- 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 (p.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