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 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 =
    q.head (r := r)
have h : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) (Fin.castLE sorry (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: convert! Fin.append_right p q _
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ ((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
have inr : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) x, Fin.append (p.toFun (r := r)) (q.toFun (r := r)) y) ∈ r
Tactic: change Fin.append p q x ~[r] Fin.append p q y
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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), ⋯⟩
have h : (↑x : ℕ) = (↑(Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), sorry⟩) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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), ⋯⟩) : ℕ)
have h : (↑i : ℕ) = p.length (r := r) + 1 + ((↑i : ℕ) - (p.length (r := r) + 1))
Tactic: dsimp [x, y]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ (↑i : ℕ) = p.length (r := r) + 1 + ((↑i : ℕ) - (p.length (r := r) + 1))
have h : p.length (r := r) + 1 ≤ (↑i : ℕ)
Tactic: rw [Nat.add_sub_cancel']
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
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
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) x, Fin.append (p.toFun (r := r)) (q.toFun (r := r)) y) ∈ r
have hx : x = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - (p.length (r := r) + 1), sorry⟩
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
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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), ⋯⟩
have h : (↑y : ℕ) = (↑(Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), sorry⟩) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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), ⋯⟩
| p.length (r := r) + 1 + ((↑i : ℕ) - p.length (r := r))
have rw : (↑i : ℕ) + 1
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]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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 : ℕ) = p.length (r := r) + 1 + ((↑i : ℕ) - p.length (r := r))
have h : (↑y : ℕ) = (↑i : ℕ) + 1
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]
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
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), ⋯⟩
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) x, Fin.append (p.toFun (r := r)) (q.toFun (r := r)) y) ∈ r
have hy : y = Fin.natAdd (p.length (r := r) + 1) ⟨(↑i : ℕ) - p.length (r := r), sorry⟩
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
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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), ⋯⟩
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) x, Fin.append (p.toFun (r := r)) (q.toFun (r := r)) y) ∈ r
have inr : (q.toFun (r := r) (⟨(↑i : ℕ) - (p.length (r := r) + 1), sorry⟩ : Fin (q.length (r := r) + 1)),
    q.toFun (r := r) (⟨(↑i : ℕ) - p.length (r := r), sorry⟩ : Fin (q.length (r := r) + 1))) ∈
  r
Tactic: rw [hx, Fin.append_right, hy, Fin.append_right]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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), ⋯⟩
⊢ (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
have h : (↑i : ℕ) - p.length (r := r) = (↑(⟨(↑i : ℕ) - (p.length (r := r) + 1), sorry⟩ : Fin (q.length (r := r))).succ : ℕ)
Tactic: convert! q.step ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <| by lia⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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) = (↑(⟨(↑i : ℕ) - (p.length (r := r) + 1), ⋯⟩ : Fin (q.length (r := r))).succ : ℕ)
have h : p.length (r := r) + 1 ≤ (↑i : ℕ)
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]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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)
⊢ (p.append (r := r) q connect).toFun (r := r) (Fin.cast ⋯ (Fin.castAdd (q.length (r := r) + 1) i)) = p.toFun (r := r) i
have 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 sorry) sorry)
    (Fin.cast sorry (Fin.castAdd (q.length (r := r) + 1) i)) =
  p.toFun (r := r) i
Tactic: delta append
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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)
⊢ 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
have simp : Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.cast sorry (Fin.cast sorry (Fin.castAdd (q.length (r := r) + 1) i))) =
  p.toFun (r := r) i
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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.last ((p.append (r := r) q connect).length (r := r))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))
have h : Fin.last ((p.append (r := r) q connect).length (r := r)) =
  Fin.cast sorry (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))
Tactic: convert! append_apply_right p q connect (Fin.last _)
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := 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))))
have h : (↑(Fin.last ((p.append (r := r) q connect).length (r := r))) : ℕ) =
  (↑(Fin.cast sorry (Fin.natAdd (p.length (r := r) + 1) (Fin.last (q.length (r := r))))) : ℕ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last (r := r), q.head (r := 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))))) : ℕ)
have h : p.length (r := r) + q.length (r := r) + 1 = p.length (r := r) + 1 + q.length (r := r)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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.append (r := r) q hpq).append (r := r) w ⋯ = p.append (r := r) (q.append (r := r) w hqw) ⋯
have length_eq : ((p.append (r := r) q hpq).append (r := r) w sorry).length (r := r) =
  (p.append (r := r) (q.append (r := r) w hqw) sorry).length (r := r)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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)
⊢ (p.append (r := r) q hpq).append (r := r) w ⋯ = p.append (r := r) (q.append (r := r) w hqw) ⋯
have toFun_eq : ∀ (x : Fin (((p.append (r := r) q hpq).append (r := r) w sorry).length (r := r) + 1)),
  ((p.append (r := r) q hpq).append (r := r) w sorry).toFun (r := r) x =
    ((p.append (r := r) (q.append (r := r) w hqw) sorry).toFun (r := r) ∘ Fin.cast sorry) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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.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)
have 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)
Tactic: simp only [append_length, Nat.add_left_inj]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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).toList (r := r) = p.toList (r := r) ++ q.toList (r := r)
have hl : (p.append (r := r) q connect).toList (r := r).length = (p.toList (r := r) ++ q.toList (r := r)).length
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ (p.append (r := r) q connect).toList (r := r) = p.toList (r := r) ++ q.toList (r := r)
have 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₂
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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).toList (r := r).length = (p.toList (r := r) ++ q.toList (r := r)).length
have hl : p.length (r := r) + q.length (r := r) + 1 + 1 = p.length (r := r) + 1 + (q.length (r := r) + 1)
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
⊢ (x, y) ∈ r
have inl : ∀ (hm : (↑m : ℕ) < (↑i : ℕ)), (x, y) ∈ r
Tactic: obtain hm | hm | hm := lt_trichotomy m.1 i.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
inl : ∀ (hm : (↑m : ℕ) < (↑i : ℕ)), (x, y) ∈ r
⊢ (x, y) ∈ r
have inr : ∀ (hm : (↑m : ℕ) = (↑i : ℕ)), (x, y) ∈ r
Tactic: obtain hm | hm | hm := lt_trichotomy m.1 i.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
inl : ∀ (hm : (↑m : ℕ) < (↑i : ℕ)), (x, y) ∈ r
inr : ∀ (hm : (↑m : ℕ) = (↑i : ℕ)), (x, y) ∈ r
⊢ (x, y) ∈ r
have inr₁ : ∀ (hm : (↑i : ℕ) < (↑m : ℕ)), (x, y) ∈ r
Tactic: obtain hm | hm | hm := lt_trichotomy m.1 i.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 h : x = p.toFun (r := r) ⟨(↑m : ℕ), sorry⟩.castSucc
Tactic: convert! p.step ⟨m, hm.trans i.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 : (↑m : ℕ) < (↑i : ℕ)
h : x = p.toFun (r := r) ⟨(↑m : ℕ), ⋯⟩.castSucc
⊢ (x, y) ∈ r
have h₁ : y = p.toFun (r := r) ⟨(↑m : ℕ), sorry⟩.succ
Tactic: convert! p.step ⟨m, hm.trans i.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 : (↑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 : ℕ), ⋯⟩ : Fin (p.length (r := r))).castSucc
have h : @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 : ℕ), sorry⟩ : Fin (p.length (r := r))).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 : ℕ)
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
⊢ 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
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 : ℕ)
⊢ 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
have h : @Eq.rec _ (i.succ.castSucc.succAbove (m.succ.castPred sorry))
    (fun (x : Fin (p.length (r := r) + 1 + 1)) (h : i.succ.castSucc.succAbove (m.succ.castPred sorry) = x) ↦ α)
    (p.toFun (r := r) (m.succ.castPred sorry)) _ sorry =
  p.toFun (r := r) (⟨(↑m : ℕ), sorry⟩ : Fin (p.length (r := r))).succ
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 : ℕ)
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
⊢ 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
have h₁ : m.succ < i.succ.castSucc
Tactic: rw [Fin.insertNth_apply_below]