awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) b
dsimp :
  ¬s b
      (WellFounded.min (r := s) ⋯
        {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) ⋯ {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} ⋯) ⋯ :
                        { b : β // ¬s ((f : (a : α) → β) a) b }))
                    a_1) :
                β)
              b}
        ⋯)
⊢ ¬s 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}
              ⋯)
            ⋯) :
        β)

Tactic:
dsimp only
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) b
⊢ ¬s b
      (WellFounded.min (r := s) ⋯
        {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) ⋯ {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} ⋯) ⋯ :
                        { b : β // ¬s ((f : (a : α) → β) a) b }))
                    a_1) :
                β)
              b}
        ⋯)

Tactic:
WellFounded.not_lt_min _ {b | ∀ a', r a' a → s (collapseF f a') b} h

Premises used: setOf, WellFounded.not_lt_min
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) b
⊢ ¬s b
      (WellFounded.min (r := s) ⋯
        {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) ⋯ {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} ⋯) ⋯ :
                        { b : β // ¬s ((f : (a : α) → β) a) b }))
                    a_1) :
                β)
              b}
        ⋯)

Tactic:
exact WellFounded.not_lt_min _ {b | ∀ a', r a' a → s (collapseF f a') b} h

Premises used: setOf, WellFounded.not_lt_min
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
obtain :
  ∀ (m : α)
    (hm :
      Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        m)
    (hm' :
      ∀ (x : α),
        Membership.mem (γ := Set α)
            {a : α |
              ¬s
                  ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ :
                      (a : α) → β)
                    a)
                  b}
            x →
          ¬r x m),
    Membership.mem (γ := Set β)
      (Set.range.{u_2, u_1 + 1} (ι := α)
        (⇑(ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯) : (a : α) → β))
      b
⊢ Membership.mem (γ := Set β)
    (Set.range.{u_2, u_1 + 1} (ι := α)
      (⇑(ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯) : (a : α) → β))
    b

Tactic:
obtain ⟨m, hm, hm'⟩ := H.wf.has_min { a | ¬s _ b } ⟨_, asymm h⟩

Premises used: asymm, setOf, IsWellFounded.wf, Exists.intro, WellFounded.has_min, Not
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
h₁ : (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b
⊢ Membership.mem (γ := Set β)
    (Set.range.{u_2, u_1 + 1} (ι := α)
      (⇑(ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯) : (a : α) → β))
    b

Tactic:
use m
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
h₁ :
  ∀ (lt : s b (↑(collapseF (r := r) (s := s) f m) : β)),
    (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b
h₂ :
  ∀
    (h :
      s (↑(collapseF (r := r) (s := s) f m) : β)
        ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a))
    (hm :
      Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              (↑(collapseF (r := r) (s := s) f m) : β)}
        m)
    (hm' :
      ∀ (x : α),
        Membership.mem (γ := Set α)
            {a : α |
              ¬s
                  ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ :
                      (a : α) → β)
                    a)
                  (↑(collapseF (r := r) (s := s) f m) : β)}
            x →
          ¬r x m),
    (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m =
      (↑(collapseF (r := r) (s := s) f m) : β)
h₃ :
  ∀ (gt : s (↑(collapseF (r := r) (s := s) f m) : β) b),
    (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b

Tactic:
obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)

Premises used: _private.0.collapseF, Subtype.val, trichotomous_of, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
lt : s b (↑(collapseF (r := r) (s := s) f m) : β)
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b

Tactic:
(collapseF_not_lt f m (fun c h ↦ ?_) lt).elim

Premises used: False.elim, _private.0.collapseF_not_lt
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
lt : s b (↑(collapseF (r := r) (s := s) f m) : β)
h₁ : ∀ (c : α) (h : r c m), s (↑(collapseF (r := r) (s := s) f c) : β) b
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b

Tactic:
refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim

Premises used: False.elim, _private.0.collapseF_not_lt
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h_1 : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
lt : s b (↑(collapseF (r := r) (s := s) f m) : β)
c : α
h : r c m
h₁ : ∀ (hn : ¬s (↑(collapseF (r := r) (s := s) f c) : β) b), False
⊢ s (↑(collapseF (r := r) (s := s) f c) : β) b

Tactic:
by_contra hn
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h_1 : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
lt : s b (↑(collapseF (r := r) (s := s) f m) : β)
c : α
h : r c m
hn : ¬s (↑(collapseF (r := r) (s := s) f c) : β) b
⊢ False

Tactic:
hm' _ hn h
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h_1 : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
lt : s b (↑(collapseF (r := r) (s := s) f m) : β)
c : α
h : r c m
hn : ¬s (↑(collapseF (r := r) (s := s) f c) : β) b
⊢ False

Tactic:
exact hm' _ hn h
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a m : α
h :
  s (↑(collapseF (r := r) (s := s) f m) : β)
    ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
          (↑(collapseF (r := r) (s := s) f m) : β)}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              (↑(collapseF (r := r) (s := s) f m) : β)}
        x →
      ¬r x m
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m =
    (↑(collapseF (r := r) (s := s) f m) : β)

Tactic:
rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
gt : s (↑(collapseF (r := r) (s := s) f m) : β) b
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b

Tactic:
(hm gt).elim

Premises used: False.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
m : α
hm :
  Membership.mem (γ := Set α)
    {a : α |
      ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a) b}
    m
hm' :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {a : α |
          ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) a)
              b}
        x →
      ¬r x m
gt : s (↑(collapseF (r := r) (s := s) f m) : β) b
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b

Tactic:
exact (hm gt).elim

Premises used: False.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
inl :
  ∀ (h : Sum.Lex r s (f.top (r := r) (s := Sum.Lex r s)) (g.top (r := s) (s := Sum.Lex r s))),
    Nonempty ((r ≼i s) ⊕ (s ≼i r))
inr : ∀ (h : f.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)), Nonempty ((r ≼i s) ⊕ (s ≼i r))
inr₁ :
  ∀ (h : Sum.Lex r s (g.top (r := s) (s := Sum.Lex r s)) (f.top (r := r) (s := Sum.Lex r s))),
    Nonempty ((r ≼i s) ⊕ (s ≼i r))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
obtain h | h | h := trichotomous_of (Sum.Lex r s) f.top g.top

Premises used: trichotomous_of, PrincipalSeg.top, Sum.Lex
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s (f.top (r := r) (s := Sum.Lex r s)) (g.top (r := s) (s := Sum.Lex r s))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
⟨Sum.inl <| (f.codRestrict {x | Sum.Lex r s x g.top}
          (fun a => _root_.trans (f.lt_top a) h) h).transRelIso g.subrelIso⟩

Premises used: PrincipalSeg.subrelIso, trans, setOf, PrincipalSeg.toRelEmbedding, PrincipalSeg.transRelIso, PrincipalSeg.lt_top, PrincipalSeg.mem_range_of_rel, Sum.inl, Nonempty.intro, InitialSeg.mk, PrincipalSeg.top, Sum.Lex, PrincipalSeg.codRestrict
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s (f.top (r := r) (s := Sum.Lex r s)) (g.top (r := s) (s := Sum.Lex r s))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
exact ⟨Sum.inl <| (f.codRestrict {x | Sum.Lex r s x g.top}
          (fun a => _root_.trans (f.lt_top a) h) h).transRelIso g.subrelIso⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f_1 : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f_1.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)
f : RelIso (α := { x : α ⊕ β // Sum.Lex r s x (f_1.top (r := r) (s := Sum.Lex r s)) })
  (Subrel (Sum.Lex r s) fun (x : α ⊕ β) ↦ Sum.Lex r s x (f_1.top (r := r) (s := Sum.Lex r s))) r :=
  f_1.subrelIso (r := r) (s := Sum.Lex r s)
inr :
  ∀
    (f :
      RelIso (α := { x : α ⊕ β // Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s)) })
        (Subrel (Sum.Lex r s) fun (x : α ⊕ β) ↦ Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s))) r),
    Nonempty ((r ≼i s) ⊕ (s ≼i r))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
rw [h] at f
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f_1 : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f_1.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)
f :
  RelIso (α := { x : α ⊕ β // Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s)) })
    (Subrel (Sum.Lex r s) fun (x : α ⊕ β) ↦ Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s))) r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩

Premises used: PrincipalSeg.subrelIso, RelIso.symm, Sum.inl, Nonempty.intro, RelIso.trans, RelIso.toInitialSeg
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f_1 : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f_1.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)
f :
  RelIso (α := { x : α ⊕ β // Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s)) })
    (Subrel (Sum.Lex r s) fun (x : α ⊕ β) ↦ Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s))) r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
exact ⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s (g.top (r := s) (s := Sum.Lex r s)) (f.top (r := r) (s := Sum.Lex r s))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
⟨Sum.inr <| (g.codRestrict {x | Sum.Lex r s x f.top}
          (fun a => _root_.trans (g.lt_top a) h) h).transRelIso f.subrelIso⟩

Premises used: PrincipalSeg.subrelIso, trans, setOf, PrincipalSeg.toRelEmbedding, PrincipalSeg.transRelIso, PrincipalSeg.lt_top, PrincipalSeg.mem_range_of_rel, Nonempty.intro, Sum.inr, InitialSeg.mk, PrincipalSeg.top, Sum.Lex, PrincipalSeg.codRestrict
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s (g.top (r := s) (s := Sum.Lex r s)) (f.top (r := r) (s := Sum.Lex r s))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
exact ⟨Sum.inr <| (g.codRestrict {x | Sum.Lex r s x f.top}
          (fun a => _root_.trans (g.lt_top a) h) h).transRelIso f.subrelIso⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
inl :
  ∀ (h : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)),
    Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) a : β)
inr :
  ∀ (hb : b < (f : (a : α) → β) a), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b

Tactic:
obtain rfl | hb := h.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) a : β)

Tactic:
⟨a, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl