-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
rw :
  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}
            ⋯)
          ⋯) :
      β)
⊢ Membership.mem (γ := Set β) {b : β | ∀ (a' : α), r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) b}
    (↑(collapseF (r := r) (s := s) f a) : β)

Tactic:
rw [collapseF, IsWellFounded.fix_eq]

Premises used: IsWellFounded.fix_eq, _private.0.collapseF