awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
inst_1 : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ Eq.{u_3 + 1} (α := γ)
    ((PrincipalSeg.toRelEmbedding (r := r) (s := t)
            (match (motive := (r ≺i s) ⊕ (r ≃r s) → r ≺i t) Sum.inr f' with
            | Sum.inl f' => f'.trans (r := r) (s := s) (t := t) g
            | Sum.inr f' => PrincipalSeg.relIsoTrans (r := r) (s := s) (t := t) f' g) :
          (a : α) → γ)
        a :
      γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
have inr : Eq.{u_3 + 1} (α := γ) ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f' : (a : α) → β) a : β) : γ)
  ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
Tactic: rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
inst_1 : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
inr :
  Eq.{u_3 + 1} (α := γ) ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f' : (a : α) → β) a : β) : γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ)
    ((PrincipalSeg.toRelEmbedding (r := r) (s := t)
            (match (motive := (r ≺i s) ⊕ (r ≃r s) → r ≺i t) Sum.inr f' with
            | Sum.inl f' => f'.trans (r := r) (s := s) (t := t) g
            | Sum.inr f' => PrincipalSeg.relIsoTrans (r := r) (s := s) (t := t) f' g) :
          (a : α) → γ)
        a :
      γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
have inr₁ : Eq.{u_3 + 1} (α := γ) ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
  ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
Tactic: rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
have inl : ∀ (f : r ≺i s), ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
Tactic: obtain f | f := f.principalSumRelIso
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
inl : ∀ (f : r ≺i s), ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
have inr : ∀ (f : r ≃r s), ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
Tactic: obtain f | f := f.principalSumRelIso
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
have inl : ∀ (f : r ≺i s), ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
Tactic: classical
  obtain f | f := f.principalSumRelIso
  · exact ⟨_, _, inferInstance,
      ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩
  · exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
inl : ∀ (f : r ≺i s), ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
have inr : ∀ (f : r ≃r s), ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
Tactic: classical
  obtain f | f := f.principalSumRelIso
  · exact ⟨_, _, inferInstance,
      ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩
  · exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
⊢ ∀ {a' : α}, r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) (↑(collapseF (r := r) (s := s) f a) : β)
have change : 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: change _ ∈ { b | ∀ a', r a' a → s (collapseF f a') b }
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
⊢ Membership.mem (γ := Set β) {b : β | ∀ (a' : α), r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) b}
    (↑(collapseF (r := r) (s := s) f a) : β)
have 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 := sorry;
                  (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                      (WellFounded.min (r := s) sorry {b : β | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h) : β) b} sorry) sorry :
                    { 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 := sorry;
                              (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                                  (WellFounded.min (r := s) sorry {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b}
                                    sorry)
                                  sorry :
                                { b : β // ¬s ((f : (a : α) → β) a) b }))
                            y :
                          { b : β // ¬s ((f : (a : α) → β) y) b }))
                      a_1 h) :
                  β)
                b}
          ((f : (a : α) → β) a : β) :=
        sorry;
      Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
        (WellFounded.min (r := s) sorry
          {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 := sorry;
                              (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                                  (WellFounded.min (r := s) sorry {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b}
                                    sorry)
                                  sorry :
                                { b : β // ¬s ((f : (a : α) → β) a) b }))
                            y :
                          { b : β // ¬s ((f : (a : α) → β) y) b }))
                      a_1 h) :
                  β)
                b}
          sorry)
        sorry) :
    β)
Tactic: rw [collapseF, IsWellFounded.fix_eq]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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 (↑(collapseF (r := r) (s := s) f a) : β)
have rw : ¬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 := sorry;
                                (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                                    (WellFounded.min (r := s) sorry
                                      {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} sorry)
                                    sorry :
                                  { b : β // ¬s ((f : (a : α) → β) a) b }))
                              y :
                            { b : β // ¬s ((f : (a : α) → β) y) b }))
                        a_1 h) :
                    β)
                  b}
            ((f : (a : α) → β) a : β) :=
          sorry;
        Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
          (WellFounded.min (r := s) sorry
            {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 := sorry;
                                (Subtype.mk (p := fun (b : β) ↦ ¬s ((f : (a : α) → β) a) b)
                                    (WellFounded.min (r := s) sorry
                                      {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} sorry)
                                    sorry :
                                  { b : β // ¬s ((f : (a : α) → β) a) b }))
                              y :
                            { b : β // ¬s ((f : (a : α) → β) y) b }))
                        a_1 h) :
                    β)
                  b}
            sorry)
          sorry) :
      β)
Tactic: rw [collapseF, IsWellFounded.fix_eq]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
      (↑(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}
              ⋯)
            ⋯) :
        β)
have dsimp : ¬s b
    (WellFounded.min (r := s) sorry
      {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) sorry {b : β | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h) : β) b} sorry) sorry :
                      { b : β // ¬s ((f : (a : α) → β) a) b }))
                  a_1) :
              β)
            b}
      sorry)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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)
⊢ 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
have obtain : ∀ (m : α)
  (hm :
    Membership.mem (γ := Set α)
      {a : α |
        ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) sorry : (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) : β)) sorry : (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) : β)) sorry) : (a : α) → β))
    b
Tactic: obtain ⟨m, hm, hm'⟩ := H.wf.has_min { a | ¬s _ b } ⟨_, asymm h⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ 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
have h₁ : (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) sorry : (a : α) → β) m = b
Tactic: use m
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b
have 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) : β)) sorry : (a : α) → β) m = b
Tactic: obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b
have h₂ : ∀
  (h :
    s (↑(collapseF (r := r) (s := s) f m) : β)
      ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) sorry : (a : α) → β) a))
  (hm :
    Membership.mem (γ := Set α)
      {a : α |
        ¬s ((ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) sorry : (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) : β)) sorry : (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) : β)) sorry : (a : α) → β) m =
    (↑(collapseF (r := r) (s := s) f m) : β)
Tactic: obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)
Cleared hypotheses: b, h, hm, hm'
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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) : β)
⊢ (ofMonotone (r := r) (s := s) (fun (a : α) ↦ (↑(collapseF (r := r) (s := s) f a) : β)) ⋯ : (a : α) → β) m = b
have 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) : β)) sorry : (a : α) → β) m = b
Tactic: obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
have h₁ : ∀ (c : α) (h : r c m), s (↑(collapseF (r := r) (s := s) f c) : β) b
Tactic: refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ s (↑(collapseF (r := r) (s := s) f c) : β) b
have h₁ : ∀ (hn : ¬s (↑(collapseF (r := r) (s := s) f c) : β) b), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
have 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))
Tactic: obtain h | h | h := trichotomous_of (Sum.Lex r s) f.top g.top