-- 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 : ℕ
g : { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) }
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) → α)) ⋯)
      (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) → α)) ⋯)
      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
have obtain : ∀ (lg : Fin n) (g : Fin ((↑lg : ℕ) + 1) → α)
  (mg :
    StrictMono.{0, u_1} (α :=
      Fin
        ((↑(Sigma.fst (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)
                (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lg g)) :
            ℕ) +
          1))
      (β := α)
      (Sigma.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)
        (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lg g)))
  (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)
        (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))),
  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)
Tactic: obtain ⟨⟨lg, g⟩, mg⟩ := g
Cleared hypotheses: g, e