-- Mathlib/Order/InitialSeg.lean
theorem collapseF_lt [IsWellOrder β s] (f : r ↪r s) {a : α} :
    ∀ {a'}, r a' a → s (collapseF f a') (collapseF f a)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}

Tactic:
rw [collapseF, IsWellFounded.fix_eq]

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(let_fun H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x =>
                      IsWellFounded.fix r
                        (fun a IH =>
                          let_fun H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH =>
                  let_fun H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(let_fun H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x =>
                      IsWellFounded.fix r
                        (fun a IH =>
                          let_fun H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH =>
                  let_fun H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}

Tactic:
dsimp only

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ⋯.min
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s (↑(IsWellFounded.fix r (fun a IH => ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩) a_1))
              b}
      ⋯ ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s (↑(IsWellFounded.fix r (fun a IH => ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩) a')) b}

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ∀ {a' : α}, r a' a → s ↑(collapseF f a') ↑(collapseF f a)

Tactic:
show _ ∈ { b | ∀ a', r a' a → s (collapseF f a') b }

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ⋯.min
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s (↑(IsWellFounded.fix r (fun a IH => ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩) a_1))
              b}
      ⋯ ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s (↑(IsWellFounded.fix r (fun a IH => ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩) a')) b}

Tactic:
exact WellFounded.min_mem _ _ _

Result:
no goals