α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ∀ (a_1 : α), r a_1 a → s ↑(collapseF f a_1) ↑(collapseF f a)
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a✝ a : α
⊢ r a a✝ → s ↑(collapseF f a) ↑(collapseF f a✝)
revert a
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ∀ (a_1 : α), r a_1 a → s ↑(collapseF f a_1) ↑(collapseF f a)
show (collapseF f a).1 ∈ { b | ∀ (a') (_ : r a' a), s (collapseF f a').1 b }
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(WellFounded.fix (_ : WellFounded r)
        (fun a IH =>
          let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
          let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
          { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
            property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
        a) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                  let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                  { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                    property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                a'))
            b}
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}
unfold collapseF
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(let S :=
        {b |
          ∀ (a_1 : α) (h : r a_1 a),
            s
              (↑((fun y x =>
                    WellFounded.fix (_ : WellFounded r)
                      (fun a IH =>
                        let S := {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b};
                        let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                        { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                          property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                      y)
                  a_1 h))
              b};
      let_fun this :=
        (_ :
          ∀ (a' : α),
            r a' a →
              s
                (↑(WellFounded.fix (_ : WellFounded r)
                    (fun a IH =>
                      let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                      let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                      { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                        property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                    a'))
                (↑f a));
      { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
        property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) }) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                  let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                  { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                    property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                a'))
            b}
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(WellFounded.fix (_ : WellFounded r)
        (fun a IH =>
          let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
          let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
          { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
            property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
        a) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                  let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                  { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                    property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                a'))
            b}
rw [WellFounded.fix_eq]
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ WellFounded.min (_ : WellFounded s)
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s
              (↑(WellFounded.fix (_ : WellFounded r)
                  (fun a IH =>
                    {
                      val :=
                        WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                          (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                      property :=
                        (_ :
                          ¬s (↑f a)
                              (WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                  a_1))
              b}
      (_ :
        ∃ x,
          x ∈
            {b |
              ∀ (a_1 : α),
                r a_1 a →
                  s
                    (↑(WellFounded.fix (_ : WellFounded r)
                        (fun a IH =>
                          {
                            val :=
                              WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                            property :=
                              (_ :
                                ¬s (↑f a)
                                    (WellFounded.min (_ : WellFounded s)
                                      {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                      (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                        a_1))
                    b}) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  {
                    val :=
                      WellFounded.min (_ : WellFounded s) {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
                        (_ : ∃ x, x ∈ {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}),
                    property :=
                      (_ :
                        ¬s (↑f a)
                            (WellFounded.min (_ : WellFounded s) {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
                              (_ : ∃ x, x ∈ {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}))) })
                a'))
            b}
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(let S :=
        {b |
          ∀ (a_1 : α) (h : r a_1 a),
            s
              (↑((fun y x =>
                    WellFounded.fix (_ : WellFounded r)
                      (fun a IH =>
                        let S := {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b};
                        let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                        { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                          property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                      y)
                  a_1 h))
              b};
      let_fun this :=
        (_ :
          ∀ (a' : α),
            r a' a →
              s
                (↑(WellFounded.fix (_ : WellFounded r)
                    (fun a IH =>
                      let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                      let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                      { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                        property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                    a'))
                (↑f a));
      { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
        property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) }) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                  let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                  { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                    property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                a'))
            b}
dsimp only
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.70675
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ WellFounded.min (_ : WellFounded s)
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s
              (↑(WellFounded.fix (_ : WellFounded r)
                  (fun a IH =>
                    {
                      val :=
                        WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                          (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                      property :=
                        (_ :
                          ¬s (↑f a)
                              (WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                  a_1))
              b}
      (_ :
        ∃ x,
          x ∈
            {b |
              ∀ (a_1 : α),
                r a_1 a →
                  s
                    (↑(WellFounded.fix (_ : WellFounded r)
                        (fun a IH =>
                          {
                            val :=
                              WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                            property :=
                              (_ :
                                ¬s (↑f a)
                                    (WellFounded.min (_ : WellFounded s)
                                      {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                      (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                        a_1))
                    b}) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  {
                    val :=
                      WellFounded.min (_ : WellFounded s) {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
                        (_ : ∃ x, x ∈ {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}),
                    property :=
                      (_ :
                        ¬s (↑f a)
                            (WellFounded.min (_ : WellFounded s) {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
                              (_ : ∃ x, x ∈ {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}))) })
                a'))
            b}
apply WellFounded.min_mem _ _