-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
⊢ Membership.mem (γ := Set β)
    {b : β |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r (motive := fun (a : α) ↦ { b : β // ¬s ((f : (a : α) → β) a) b })
                  (fun (a : α) (IH : (y : α) → r y a → { b : β // ¬s ((f : (a : α) → β) y) b }) ↦
                    have H := ⋯;
                    (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                        (WellFounded.min (r := s) ⋯ {b : β | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h) : β) b} ⋯) ⋯ :
                      { b : β // ¬s ((f : (a : α) → β) a) b }))
                  a') :
              β)
            b}
    (↑(have H :
          Membership.mem.{u_2, u_2} (α := β) (γ := Set β)
            {b : β |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun (y : α) (x : r y a) ↦
                          (IsWellFounded.fix r (motive := fun (a : α) ↦ { b : β // ¬s ((f : (a : α) → β) a) b })
                              (fun (a : α) (IH : (y : α) → r y a → { b : β // ¬s ((f : (a : α) → β) y) b }) ↦
                                have H := ⋯;
                                (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                                    (WellFounded.min (r := s) ⋯
                                      {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} ⋯)
                                    ⋯ :
                                  { b : β // ¬s ((f : (a : α) → β) a) b }))
                              y :
                            { b : β // ¬s ((f : (a : α) → β) y) b }))
                        a_1 h) :
                    β)
                  b}
            ((f : (a : α) → β) a : β) :=
          ⋯;
        Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
          (WellFounded.min (r := s) ⋯
            {b : β |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun (y : α) (x : r y a) ↦
                          (IsWellFounded.fix r (motive := fun (a : α) ↦ { b : β // ¬s ((f : (a : α) → β) a) b })
                              (fun (a : α) (IH : (y : α) → r y a → { b : β // ¬s ((f : (a : α) → β) y) b }) ↦
                                have H := ⋯;
                                (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                                    (WellFounded.min (r := s) ⋯
                                      {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} ⋯)
                                    ⋯ :
                                  { b : β // ¬s ((f : (a : α) → β) a) b }))
                              y :
                            { b : β // ¬s ((f : (a : α) → β) y) b }))
                        a_1 h) :
                    β)
                  b}
            ⋯)
          ⋯) :
      β)
have dsimp : Membership.mem (γ := Set β)
  {b : β |
    ∀ (a' : α),
      r a' a →
        s
          (↑(IsWellFounded.fix r (motive := fun (a : α) ↦ { b : β // ¬s ((f : (a : α) → β) a) b })
                (fun (a : α) (IH : (y : α) → r y a → { b : β // ¬s ((f : (a : α) → β) y) b }) ↦
                  (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                      (WellFounded.min (r := s) sorry {b : β | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h) : β) b} sorry) sorry :
                    { b : β // ¬s ((f : (a : α) → β) a) b }))
                a') :
            β)
          b}
  (WellFounded.min (r := s) sorry
    {b : β |
      ∀ (a_1 : α) (h : r a_1 a),
        s
          (↑(IsWellFounded.fix r (motive := fun (a : α) ↦ { b : β // ¬s ((f : (a : α) → β) a) b })
                (fun (a : α) (IH : (y : α) → r y a → { b : β // ¬s ((f : (a : α) → β) y) b }) ↦
                  (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                      (WellFounded.min (r := s) sorry {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} sorry) sorry :
                    { b : β // ¬s ((f : (a : α) → β) a) b }))
                a_1) :
            β)
          b}
    sorry)
Tactic: dsimp only