-- Module: Mathlib.Order.RelSeries
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)
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) → α)) ⋯)
          (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) → α)) ⋯)
          (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)
⊢ 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 ⟨⟨lg, g⟩, mg⟩ := g