α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(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)
α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b ↑(collapseF f a)
unfold collapseF
α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(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))) })
α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(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)
rw [WellFounded.fix_eq]
α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (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}))
α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(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))) })
dsimp only
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.71243
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (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}))
exact WellFounded.not_lt_min _ _ _ h