awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.last (p.length (r := r) + q.length (r := r))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))
have rw : Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
    (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
    (Fin.natAdd (p.length (r := r)) (Fin.last (q.length (r := r)))) =
  q.toFun (r := r) (Fin.last (q.length (r := r)))
Tactic: rw [← Fin.natAdd_last, Fin.addCases_right]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
rw :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
      (Fin.natAdd (p.length (r := r)) (Fin.last (q.length (r := r)))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.last (p.length (r := r) + q.length (r := r))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))
have rw₁ : q.toFun (r := r) (Fin.last (q.length (r := r))) = q.toFun (r := r) (Fin.last (q.length (r := r)))
Tactic: rw [← Fin.natAdd_last, Fin.addCases_right]
-- 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) + 1)
x : Fin (p.length (r := r) - (↑i : ℕ))
j : ℕ
h : j < p.length (r := r) - (↑i : ℕ)
⊢ Membership.mem (α := α × α) r
    ((match (motive := Fin (p.length (r := r) - (↑i : ℕ) + 1) → α)
          (⟨j, h⟩ : Fin (p.length (r := r) - (↑i : ℕ))).castSucc with
        | ⟨j, h⟩ => p.toFun (r := r) ⟨j + (↑i : ℕ), ⋯⟩,
        match (motive := Fin (p.length (r := r) - (↑i : ℕ) + 1) → α)
          (⟨j, h⟩ : Fin (p.length (r := r) - (↑i : ℕ))).succ with
        | ⟨j, h⟩ => p.toFun (r := r) ⟨j + (↑i : ℕ), ⋯⟩) :
      α × α)
have h₁ : (↑(⟨j, h⟩ : Fin (p.length (r := r) - (↑i : ℕ))).succ : ℕ) + (↑i : ℕ) =
  (↑(⟨j + (↑i : ℕ), sorry⟩ : Fin (p.length (r := r))).succ : ℕ)
Tactic: convert! p.step ⟨j + i.1, by lia⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ (p.drop (r := r) i).last (r := r) = p.last (r := r)
have simp : p.toFun (r := r) (⟨p.length (r := r) - (↑i : ℕ) + (↑i : ℕ), sorry⟩ : Fin (p.length (r := r) + 1)) =
  p.toFun (r := r) ⟨p.length (r := r), sorry⟩
Tactic: simp only [last, drop, Fin.last]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ p.toFun (r := r) (⟨p.length (r := r) - (↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (p.length (r := r) + 1)) =
    p.toFun (r := r) ⟨p.length (r := r), ⋯⟩
have e_a : p.length (r := r) - (↑i : ℕ) + (↑i : ℕ) = p.length (r := r)
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ ¬r.FiniteDimensional ↔ r.InfiniteDimensional
have rw : (¬∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length (r := r) ≤ x.length (r := r)) ↔
  ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
Tactic: rw [finiteDimensional_iff, infiniteDimensional_iff]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ (¬∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length (r := r) ≤ x.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
have push : (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) ↔
  ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
have mp : (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) →
  ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
mp :
  (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) →
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
⊢ (∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)) ↔
    ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
have mpr : (∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n) →
  ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
IH : ∃ (x : RelSeries r), x.length (r := r) = n
⊢ ∃ (x : RelSeries r), x.length (r := r) = n + 1
have mp : ∀ (l : RelSeries r) (hl : l.length (r := r) = n), ∃ (x : RelSeries r), x.length (r := r) = n + 1
Tactic: obtain ⟨l, hl⟩ := IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
l : RelSeries r
hl : l.length (r := r) = n
⊢ ∃ (x : RelSeries r), x.length (r := r) = n + 1
have mp : ∀ (l' : RelSeries r) (hl' : l.length (r := r) < l'.length (r := r)), ∃ (x : RelSeries r), x.length (r := r) = n + 1
Tactic: obtain ⟨l', hl'⟩ := H l
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
⊢ ∃ (x : RelSeries r), x.length (r := r) = n
have mp : ∃ (x : RelSeries r), x.length (r := r) = 0
Tactic: induction n with
    | zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
    | succ n IH =>
      obtain ⟨l, hl⟩ := IH
      obtain ⟨l', hl'⟩ := H l
      exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (x : RelSeries r), ∃ (y : RelSeries r), x.length (r := r) < y.length (r := r)
n : ℕ
mp : ∃ (x : RelSeries r), x.length (r := r) = 0
⊢ ∃ (x : RelSeries r), x.length (r := r) = n
have mp₁ : ∀ (n : ℕ) (IH : ∃ (x : RelSeries r), x.length (r := r) = n), ∃ (x : RelSeries r), x.length (r := r) = n + 1
Tactic: induction n with
    | zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
    | succ n IH =>
      obtain ⟨l, hl⟩ := IH
      obtain ⟨l', hl'⟩ := H l
      exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
H : ∀ (n : ℕ), ∃ (x : RelSeries r), x.length (r := r) = n
l : RelSeries r
⊢ ∃ (y : RelSeries r), l.length (r := r) < y.length (r := r)
have mpr : ∀ (l' : RelSeries r) (hl' : l'.length (r := r) = l.length (r := r) + 1),
  ∃ (y : RelSeries r), l.length (r := r) < y.length (r := r)
Tactic: obtain ⟨l', hl'⟩ := H (l.length + 1)
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ ¬r.InfiniteDimensional ↔ r.FiniteDimensional
have rw : ¬¬r.FiniteDimensional ↔ r.FiniteDimensional
Tactic: rw [← not_finiteDimensional_iff, not_not]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
rw : ¬¬r.FiniteDimensional ↔ r.FiniteDimensional
⊢ ¬r.InfiniteDimensional ↔ r.FiniteDimensional
have rw₁ : r.FiniteDimensional ↔ r.FiniteDimensional
Tactic: rw [← not_finiteDimensional_iff, not_not]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : Nonempty α
⊢ r.FiniteDimensional ∨ r.InfiniteDimensional
have rw : r.FiniteDimensional ∨ ¬r.FiniteDimensional
Tactic: rw [← not_finiteDimensional_iff]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
⊢ r.inv.IsWellFounded
have rw : IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
Tactic: rw [IsWellFounded, wellFounded_iff_isEmpty_descending_chain]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
inst : r.FiniteDimensional
⊢ IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
have refine : ∀ (x : { f : ℕ → α // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }) (f : ℕ → α) (hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv),
  False
Tactic: refine ⟨fun ⟨f, hf⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
γ : Type u_3
inst : Preorder γ
inst_1 : Unique γ
x :
  RelSeries (α := γ)
    {x : γ × γ |
      match (motive := γ × γ → Prop) x with
      | (a, b) => a < b}
⊢ x.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b}) ≤
    RelSeries.length (r :=
      {x : γ × γ |
        match (motive := γ × γ → Prop) x with
        | (a, b) => a < b})
      (RelSeries.singleton
        {x : γ × γ |
          match (motive := γ × γ → Prop) x with
          | (a, b) => a < b}
        default)
have by_contra! : ∀
  (r :
    RelSeries.length (r :=
        {x : γ × γ |
          match (motive := γ × γ → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : γ × γ |
            match (motive := γ × γ → Prop) x with
            | (a, b) => a < b}
          default) <
      x.length (r :=
        {x : γ × γ |
          match (motive := γ × γ → Prop) x with
          | (a, b) => a < b})),
  False
Tactic: by_contra! r
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ Nonempty α
have obtain : ∀
  (p :
    RelSeries (α := α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}),
  (∀
      (y :
        RelSeries (α := α)
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}),
      y.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) →
    Nonempty α
Tactic: obtain ⟨p, _⟩ := (SetRel.finiteDimensional_iff _).mp ‹_›
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
f g :
  { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }
e :
  Eq.{u_1 + 1} (α := LTSeries α)
    ((fun
          (f :
            { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
              StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
        mk (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
          ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) ⋯)
      f)
    ((fun
          (f :
            { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
              StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
        mk (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
          ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) ⋯)
      g)
⊢ f = g
have obtain : ∀ (lf : Fin n) (f : Fin ((↑lf : ℕ) + 1) → α)
  (mf :
    StrictMono.{0, u_1} (α :=
      Fin
        ((↑(Sigma.fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)
                (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f)) :
            ℕ) +
          1))
      (β := α)
      (Sigma.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)
        (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f)))
  (e :
    Eq.{u_1 + 1} (α := LTSeries α)
      ((fun
            (f :
              { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
                StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
          mk (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
            ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) sorry)
        (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
          StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
          (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf))
      ((fun
            (f :
              { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
                StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }) ↦
          mk (↑((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) : ℕ)
            ((↑f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)).snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) sorry)
        g)),
  Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf =
    g
Tactic: obtain ⟨⟨lf, f⟩, mf⟩ := f
Cleared hypotheses: f, e
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin ((↑lg : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lg : ℕ) g ⋯)
⊢ Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lg g) mg)
have leq : RelSeries.length (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (mk (↑lf : ℕ) f sorry) =
  RelSeries.length (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (mk (↑lg : ℕ) g sorry)
Tactic: have leq := congr($(e).length)
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin ((↑lg : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lg : ℕ) g ⋯)
leq :
  RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lf : ℕ) f ⋯) =
    RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lg : ℕ) g ⋯)
⊢ Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lg g) mg)
have leq₁ : lf = lg
Tactic: rw [mk_length lf f mf, mk_length lg g mg, Fin.val_eq_val] at leq
Cleared hypotheses: leq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin ((↑lg : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lg : ℕ) g ⋯)
leq : lf = lg
⊢ Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lg g) mg)
have subst : ∀ (g : Fin ((↑lf : ℕ) + 1) → α) (mg : StrictMono g) (e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f sorry) (mk (↑lf : ℕ) g sorry)),
  Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf g) mg)
Tactic: subst leq
Cleared hypotheses: lg, g, mg, e, leq
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
g : Fin ((↑lf : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lf : ℕ) g ⋯)
⊢ Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf g) mg)
have simp_rw : f = g
Tactic: simp_rw [Subtype.mk_eq_mk, Sigma.mk.inj_iff, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
g : Fin ((↑lf : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lf : ℕ) g ⋯)
⊢ f = g
have feq : ∀
  (i :
    Fin
      (RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (mk (↑lf : ℕ) f sorry) +
        1)),
  RelSeries.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lf : ℕ) f sorry) i =
    RelSeries.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lf : ℕ) g sorry) i
Tactic: have feq := fun i ↦ congr($(e).toFun i)
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
h₁ :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊥
h₂ :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊤
t :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1) ↪
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1)
hit :
  t.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
hi₁ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) 0) 0
hi₂ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
    (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
⊢ t.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊥
have refine_1 : t.head (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}) =
  RelSeries.head (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    s
Tactic: rw [← h₁, RelSeries.head, RelSeries.head, ← hi₁, ← hit, Function.comp]