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 β β
x y : RelSeries r
length_eq : x.length (r := r) = y.length (r := r)
⊢ x.length (r := r) + 1 = y.length (r := r) + 1
have rw : y.length (r := r) + 1 = y.length (r := r) + 1
Tactic: rw [length_eq]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
x y : RelSeries r
length_eq : x.length (r := r) = y.length (r := r)
toFun_eq : x.toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯
⊢ x = y
have rcases : ∀ (nx : ℕ) (fx : Fin (nx + 1) → α) (step : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r)
  (length_eq : (mk (r := r) nx fx step).length (r := r) = y.length (r := r))
  (toFun_eq : (mk (r := r) nx fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast sorry), mk (r := r) nx fx step = y
Tactic: rcases x with ⟨nx, fx⟩
Cleared hypotheses: x, length_eq, toFun_eq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r
length_eq : nx = y.length (r := r)
toFun_eq : (mk (r := r) nx fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯
⊢ mk (r := r) nx fx step = y
have subst : ∀ (fx : Fin (y.length (r := r) + 1) → α) (step : ∀ (i : Fin (y.length (r := r))), (fx i.castSucc, fx i.succ) ∈ r)
  (toFun_eq : (mk (r := r) (y.length (r := r)) fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast sorry),
  mk (r := r) (y.length (r := r)) fx step = y
Tactic: subst length_eq
Cleared hypotheses: nx, fx, step, length_eq, toFun_eq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) (x.toList (r := r))
have simp_rw : ∀ (i : ℕ) (_hi : i < x.length (r := r)),
  (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i sorry,
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) sorry) ∈
    r
Tactic: simp_rw [List.isChain_iff_getElem, length_toList, add_lt_add_iff_right]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length (r := r)
⊢ (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯,
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) ⋯) ∈
    r
have h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i sorry = x.toFun (r := r) ⟨i, h⟩.castSucc
Tactic: convert! x.step ⟨i, by simpa [toList] using h⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length (r := r)
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯ =
    x.toFun (r := r) ⟨i, h⟩.castSucc
⊢ (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯,
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) ⋯) ∈
    r
have h₂ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) sorry =
  x.toFun (r := r) ⟨i, h⟩.succ
Tactic: convert! x.step ⟨i, by simpa [toList] using h⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
⊢ toFun (r := r)
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        ((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) ⋯ :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          x)) =
    x.toFun (r := r) ∘ Fin.cast ⋯
have h : ∀
  (x_1 :
    Fin
      (length (r := r)
          ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
              fromListIsChain (r := r) (↑x : List α) sorry sorry)
            ((fun (x : RelSeries r) ↦
                (Subtype.mk (p := fun (x : List α) ↦
                    Membership.mem (γ := Set (List α))
                      {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                    (x.toList (r := r)) sorry :
                  { x : List α //
                    Membership.mem (γ := Set (List α))
                      {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
              x)) +
        1)),
  toFun (r := r)
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) sorry sorry)
        ((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) sorry :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          x))
      x_1 =
    (x.toFun (r := r) ∘ Fin.cast sorry) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
x_1 :
  Fin
    (length (r := r)
        ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
            fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
          ((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            x)) +
      1)
⊢ toFun (r := r)
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        ((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) ⋯ :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          x))
      x_1 =
    (x.toFun (r := r) ∘ Fin.cast ⋯) x_1
have h : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (↑x_1 : ℕ) sorry =
  x.toFun (r := r) (Fin.cast sorry x_1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
n : ℕ
hn1 :
  n <
    List.length.{u_1} (α := α)
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α)
h : n < (↑x : List α).length
⊢ List.get
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α)
      (⟨n, hn1⟩ :
        Fin
          (List.length.{u_1} (α := α)
            (↑((fun (x : RelSeries r) ↦
                    (Subtype.mk (p := fun (x : List α) ↦
                        Membership.mem (γ := Set (List α))
                          {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                        (x.toList (r := r)) ⋯ :
                      { x : List α //
                        Membership.mem (γ := Set (List α))
                          {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
                  ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                      fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
                    x)) :
              List α))) =
    (↑x : List α).get (⟨n, h⟩ : Fin (↑x : List α).length)
have dsimp : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
    ((fromListIsChain (r := r) (↑x : List α) sorry sorry).toList (r := r)) n sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (↑x : List α) n sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
⊢ (fun (x : RelSeries r) ↦
        (Subtype.mk (p := fun (x : List α) ↦
            Membership.mem (γ := Set (List α)) {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x}
              x)
            (x.toList (r := r)) ⋯ :
          { x : List α //
            Membership.mem (γ := Set (List α)) {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x}
              x }))
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        x) =
    x
have refine : List.length.{u_1} (α := α)
    (↑((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) sorry :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
              fromListIsChain (r := r) (↑x : List α) sorry sorry)
            x)) :
      List α) =
  (↑x : List α).length
Tactic: refine Subtype.ext (List.ext_get ?_ fun n hn1 _ => by dsimp; apply List.get_ofFn)
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)
⊢ List.length.{u_1} (α := α)
      (↑((fun (x : RelSeries r) ↦
              (Subtype.mk (p := fun (x : List α) ↦
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                  (x.toList (r := r)) ⋯ :
                { x : List α //
                  Membership.mem (γ := Set (List α))
                    {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
            ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
                fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
              x)) :
        List α) =
    (↑x : List α).length
have this : (↑x : List α).length.pred.succ = (↑x : List α).length
Tactic: have := Nat.succ_pred_eq_of_pos <| List.length_pos_iff.mpr x.2.1
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
⊢ Nonempty α
have obtain : ∀ (p : RelSeries r), (∀ (y : RelSeries r), y.length (r := r) ≤ p.length (r := r)) → Nonempty α
Tactic: obtain ⟨p, _⟩ := (r.finiteDimensional_iff).mp ‹_›
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ s.toList (r := r) ↔ x ∈ s
have rw : x ∈ List.ofFn (s.toFun (r := r)) ↔ x ∈ s
Tactic: rw [RelSeries.toList, List.mem_ofFn', RelSeries.mem_def]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
rw : x ∈ List.ofFn (s.toFun (r := r)) ↔ x ∈ s
⊢ x ∈ s.toList (r := r) ↔ x ∈ s
have rw₁ : x ∈ Set.range (s.toFun (r := r)) ↔ x ∈ s
Tactic: rw [RelSeries.toList, List.mem_ofFn', RelSeries.mem_def]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
rw : x ∈ List.ofFn (s.toFun (r := r)) ↔ x ∈ s
rw₁ : x ∈ Set.range (s.toFun (r := r)) ↔ x ∈ s
⊢ x ∈ s.toList (r := r) ↔ x ∈ s
have rw₂ : x ∈ Set.range (s.toFun (r := r)) ↔ x ∈ Set.range (s.toFun (r := r))
Tactic: rw [RelSeries.toList, List.mem_ofFn', RelSeries.mem_def]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length (r := r) = 0
i j : Fin (s.length (r := r) + 1)
⊢ s.toFun (r := r) i = s.toFun (r := r) j
have h : i = j
Tactic: congr!
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length (r := r) = 0
i j : Fin (s.length (r := r) + 1)
⊢ s.length (r := r) + 1 = 1
have rw : HAdd.hAdd (α := ℕ) 0 1 = 1
Tactic: rw [hs, zero_add]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
⊢ s.length (r := r) ≠ 0 ↔ Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s}
have refine : ∀ (h : s.length (r := r) ≠ 0) (rid : s.toFun (r := r) 0 = s.toFun (r := r) 1),
  (s.toFun (r := r) 0, s.toFun (r := r) 0) ∈ r
Tactic: refine ⟨fun h ↦ ⟨s 0, by simp [mem_def], s 1, by simp [mem_def],
    fun rid ↦ r.irrefl (s 0) ?_⟩, length_ne_zero_of_nontrivial⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
⊢ (s.toFun (r := r) 0, s.toFun (r := r) 0) ∈ r
have nth_rw : (s.toFun (r := r) 0, s.toFun (r := r) 1) ∈ r
Tactic: nth_rw 2 [rid]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
⊢ (s.toFun (r := r) 0, s.toFun (r := r) 1) ∈ r
have h₁ : 1 = (⟨0, sorry⟩ : Fin (s.length (r := r))).succ
Tactic: convert! s.step ⟨0, by lia⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
h : s.length (r := r) ≠ 0
rid : s.toFun (r := r) 0 = s.toFun (r := r) 1
⊢ 1 = (⟨0, ⋯⟩ : Fin (s.length (r := r))).succ
have h₁ : (↑1 : ℕ) = (↑(⟨0, sorry⟩ : Fin (s.length (r := r))).succ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
⊢ s.length (r := r) = 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
have rw : ¬s.length (r := r) ≠ 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
Tactic: rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
rw : ¬s.length (r := r) ≠ 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
⊢ s.length (r := r) = 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
have rw₁ : ¬Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s} ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
Tactic: rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst : r.IsIrrefl
rw : ¬s.length (r := r) ≠ 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
rw₁ : ¬Set.Nontrivial.{u_1} (α := α) {x : α | x ∈ s} ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
⊢ s.length (r := r) = 0 ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
have rw₂ : Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s} ↔ Set.Subsingleton.{u_1} (α := α) {x : α | x ∈ s}
Tactic: rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]
-- 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)
⊢ ((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 inl : ∀ (hi : i < Fin.castLE sorry (Fin.last (p.length (r := r)))),
  ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.succ) ∈
    r
Tactic: obtain hi | rfl | hi :=
      lt_trichotomy i (Fin.castLE (by lia) (Fin.last _ : Fin (p.length + 1)))
-- 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)
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
⊢ ((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)) ∘ Fin.cast sorry) (Fin.castLE sorry (Fin.last (p.length (r := r)))).castSucc,
    (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry)
      (Fin.castLE sorry (Fin.last (p.length (r := r)))).succ) ∈
  r
Tactic: obtain hi | rfl | hi :=
      lt_trichotomy i (Fin.castLE (by lia) (Fin.last _ : Fin (p.length + 1)))
Cleared hypotheses: i
-- 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)
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
⊢ ((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₁ : ∀ (hi : Fin.castLE sorry (Fin.last (p.length (r := r))) < i),
  ((Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.castSucc,
      (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.succ) ∈
    r
Tactic: obtain hi | rfl | hi :=
      lt_trichotomy i (Fin.castLE (by lia) (Fin.last _ : Fin (p.length + 1)))
-- 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 : 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
have h : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.castSucc = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.castSucc
Tactic: convert! p.step ⟨i.1, 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 : 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
⊢ ((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 h₁ : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.succ = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.succ
Tactic: convert! p.step ⟨i.1, 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 : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.castSucc = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.castSucc
have h : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.castSucc =
  Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ), hi⟩.castSucc)
Tactic: convert! Fin.append_left 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 : i < Fin.castLE ⋯ (Fin.last (p.length (r := r)))
⊢ (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast ⋯) i.succ = p.toFun (r := r) ⟨(↑i : ℕ), hi⟩.succ
have h : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) i.succ =
  Fin.append (p.toFun (r := r)) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ), hi⟩.succ)
Tactic: convert! Fin.append_left 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
⊢ ((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
have h : (Fin.append (p.toFun (r := r)) (q.toFun (r := r)) ∘ Fin.cast sorry) (Fin.castLE sorry (Fin.last (p.length (r := r)))).castSucc =
  p.last (r := r)
Tactic: convert! connect
-- 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
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)
⊢ ((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
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 =
  q.head (r := r)
Tactic: convert! connect