awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) < (↑i : ℕ)
⊢ m.succ < i.succ.castSucc
have h : (↑m : ℕ) + 1 < (↑i : ℕ) + 1
Tactic: change m.1 + 1 < i.1 + 1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) < (↑i : ℕ)
⊢ @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
have h : p.toFun (r := r) (m.succ.castPred sorry) = p.toFun (r := r) ⟨(↑m : ℕ) + 1, sorry⟩
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ 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
have rw : @Eq.rec _ (i.succ.castSucc.succAbove (m.castSucc.castPred sorry))
    (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.castSucc.castPred sorry) = x) ↦ α)
    (p.toFun (r := r) (m.castSucc.castPred sorry)) _ sorry =
  p.toFun (r := r) m
Tactic: rw [Fin.insertNth_apply_below]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑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
⊢ 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
have h : m.castSucc < i.succ.castSucc
Tactic: rw [Fin.insertNth_apply_below]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ m.castSucc < i.succ.castSucc
have h : (↑m : ℕ) < (↑i : ℕ) + 1
Tactic: change m.1 < i.1 + 1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ (x, y) ∈ r
have inr : (p.toFun (r := r) m, 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]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ (p.toFun (r := r) m, y) ∈ r
have h : m = i.castSucc
Tactic: convert! prev_connect
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
h : m = i.castSucc
⊢ (p.toFun (r := r) m, y) ∈ r
have h₁ : y = a
Tactic: convert! prev_connect
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ m = i.castSucc
have h : (↑m : ℕ) = (↑i.castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
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.succ = i.succ.castSucc
have h : (↑m.succ : ℕ) = (↑i.succ.castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
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.succ : ℕ) = (↑i.succ.castSucc : ℕ)
have h : (↑m : ℕ) + 1 = (↑i : ℕ) + 1
Tactic: change _ + 1 = _ + 1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ (↑m : ℕ) + 1 = (↑i : ℕ) + 1
have h : (↑i : ℕ) + 1 = (↑i : ℕ) + 1
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑m : ℕ) = (↑i : ℕ)
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ = a
have h : i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) i.succ.castSucc = a
Tactic: rw [show m.succ = i.succ.castSucc by ext; change _ + 1 = _ + 1; rw [hm],
          Fin.insertNth_apply_same]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑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
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ = a
have h₁ : a = a
Tactic: rw [show m.succ = i.succ.castSucc by ext; change _ + 1 = _ + 1; rw [hm],
          Fin.insertNth_apply_same]
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
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 : ℕ)
⊢ (x, y) ∈ r
have hm₁ : (↑i : ℕ) + 1 < (↑m : ℕ) ∨ (↑i : ℕ) + 1 = (↑m : ℕ)
Tactic: rw [Nat.lt_iff_add_one_le, le_iff_lt_or_eq] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ) ∨ (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ (x, y) ∈ r
have inr : ∀ (hm : (↑i : ℕ) + 1 < (↑m : ℕ)), (x, y) ∈ r
Tactic: obtain hm | hm := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ) ∨ (↑i : ℕ) + 1 = (↑m : ℕ)
inr : ∀ (hm : (↑i : ℕ) + 1 < (↑m : ℕ)), (x, y) ∈ r
⊢ (x, y) ∈ r
have inr₁ : ∀ (hm : (↑i : ℕ) + 1 = (↑m : ℕ)), (x, y) ∈ r
Tactic: obtain hm | hm := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
⊢ (x, y) ∈ r
have h : x = p.toFun (r := r) ⟨(↑m : ℕ) - 1, sorry⟩.castSucc
Tactic: convert! p.step ⟨m.1 - 1, Nat.sub_lt_right_of_lt_add (by lia) m.2⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
h : x = p.toFun (r := r) ⟨(↑m : ℕ) - 1, ⋯⟩.castSucc
⊢ (x, y) ∈ r
have h₁ : y = p.toFun (r := r) ⟨(↑m : ℕ) - 1, sorry⟩.succ
Tactic: convert! p.step ⟨m.1 - 1, Nat.sub_lt_right_of_lt_add (by lia) m.2⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
⊢ i.succ.castSucc.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
have h : @Eq.rec _ (i.succ.castSucc.succAbove (m.castSucc.pred sorry))
    (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.castSucc.pred sorry) = x) ↦ α)
    (p.toFun (r := r) (m.castSucc.pred sorry)) _ sorry =
  p.toFun (r := r) (⟨(↑m : ℕ) - 1, sorry⟩ : Fin (p.length (r := r))).castSucc
Tactic: rw [Fin.insertNth_apply_above (h := hm)]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
⊢ i.succ.castSucc.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
have h : @Eq.rec _ (i.succ.castSucc.succAbove (m.succ.pred sorry))
    (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.succ.pred sorry) = x) ↦ α)
    (p.toFun (r := r) (m.succ.pred sorry)) _ sorry =
  p.toFun (r := r) (⟨(↑m : ℕ) - 1, sorry⟩ : Fin (p.length (r := r))).succ
Tactic: rw [Fin.insertNth_apply_above]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
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
⊢ 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
have h₁ : i.succ.castSucc < m.succ
Tactic: rw [Fin.insertNth_apply_above]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
⊢ @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
have h : p.toFun (r := r) m = p.toFun (r := r) ⟨(↑m : ℕ) - 1 + 1, sorry⟩
Tactic: simp only [Fin.pred_succ, eq_rec_constant, Fin.succ_mk]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 < (↑m : ℕ)
⊢ p.toFun (r := r) m = p.toFun (r := r) ⟨(↑m : ℕ) - 1 + 1, ⋯⟩
have h : m = ⟨(↑m : ℕ) - 1 + 1, sorry⟩
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ (x, y) ∈ r
have h : x = a
Tactic: convert! connect_next
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
h : x = a
⊢ (x, y) ∈ r
have h₁ : y = p.toFun (r := r) i.succ
Tactic: convert! connect_next
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc = a
have h : i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) i.succ.castSucc = a
Tactic: rw [show m.castSucc = i.succ.castSucc from Fin.ext hm.symm, Fin.insertNth_apply_same]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
h :
  i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) i.succ.castSucc =
    a
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc = a
have h₁ : a = a
Tactic: rw [show m.castSucc = i.succ.castSucc from Fin.ext hm.symm, Fin.insertNth_apply_same]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r))
a : α
prev_connect : (p.toFun (r := r) i.castSucc, a) ∈ r
connect_next : (a, p.toFun (r := r) i.succ) ∈ r
m : Fin (p.length (r := r) + 1)
x : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.castSucc
y : α := i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ
hm : (↑i : ℕ) + 1 = (↑m : ℕ)
⊢ i.succ.castSucc.insertNth (α := fun (a : Fin (p.length (r := r) + 1 + 1)) ↦ α) a (p.toFun (r := r)) m.succ =
    p.toFun (r := r) i.succ
have h : Eq.rec (motive := fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.succ.pred sorry) = x) ↦ α)
    (p.toFun (r := r) (m.succ.pred sorry)) sorry =
  p.toFun (r := r) i.succ
Tactic: rw [Fin.insertNth_apply_above]