awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≼i t
a : α
⊢ Eq.{u_3 + 1} (α := γ)
    (((f.transInitial (r := r) (s := s) (t := t) g).toRelEmbedding (r := r) (s := t) : (a : α) → γ) a : γ)
    ((g : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≼i t
⊢ (f.transInitial (r := r) (s := s) (t := t) g).top (r := r) (s := t) = (g : (a : β) → γ) (f.top (r := r) (s := s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsTrans γ t
f : r ≺i s
g : s ≺i t
a : α
⊢ Eq.{u_3 + 1} (α := γ) (((f.trans (r := r) (s := s) (t := t) g).toRelEmbedding (r := r) (s := t) : (a : α) → γ) a : γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsTrans γ t
f : r ≺i s
g : s ≺i t
⊢ (f.trans (r := r) (s := s) (t := t) g).top (r := r) (s := t) =
    (g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) (f.top (r := r) (s := s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
g : s ≺i t
c : γ
⊢ Membership.mem (γ := Set γ)
      (Set.range.{u_3, u_1 + 1} (ι := α)
        (⇑(f.toRelEmbedding (r := r) (s := s).trans (r := r) (s := s) (t := t) (g.toRelEmbedding (r := s) (s := t))) :
          (a : α) → γ))
      c ↔
    t c (g.top (r := s) (s := t))

Tactic:
simp [g.mem_range_iff_rel]

Premises used: PrincipalSeg.mem_range_iff_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
g : s ≺i t
a : α
⊢ Eq.{u_3 + 1} (α := γ)
    (((relIsoTrans (r := r) (s := s) (t := t) f g).toRelEmbedding (r := r) (s := t) : (a : α) → γ) a : γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
g : s ≺i t
⊢ (relIsoTrans (r := r) (s := s) (t := t) f g).top (r := r) (s := t) = g.top (r := s) (s := t)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≃r t
a : α
⊢ Eq.{u_3 + 1} (α := γ)
    (((f.transRelIso (r := r) (s := s) (t := t) g).toRelEmbedding (r := r) (s := t) : (a : α) → γ) a : γ)
    ((g : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≃r t
⊢ (f.transRelIso (r := r) (s := s) (t := t) g).top (r := r) (s := t) = (g : (a : β) → γ) (f.top (r := r) (s := s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f g : r ≺i s
a : α
rw rw₁ :
  Eq.{u_2 + 1} (α := β) ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
    ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
⊢ Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
    ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)

Tactic:
rw [Subsingleton.elim f g]

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
rw : (relIsoTrans (r := r) (s := s) (t := t) e g).top (r := r) (s := t) = g.top (r := s) (s := t)
⊢ f.top (r := r) (s := t) = g.top (r := s) (s := t)

Tactic:
rw [Subsingleton.elim f (PrincipalSeg.relIsoTrans e g)]

Premises used: PrincipalSeg.relIsoTrans, Subsingleton.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans (r := r) (s := s) (t := t) e g).top (r := r) (s := t) = g.top (r := s) (s := t)

Tactic:
rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
rw : t ((f.trans (r := r) (s := s) (t := t) g).top (r := r) (s := t)) (g.top (r := s) (s := t))
⊢ t (h.top (r := r) (s := t)) (g.top (r := s) (s := t))

Tactic:
rw [Subsingleton.elim h (f.trans g)]

Premises used: Subsingleton.elim, PrincipalSeg.trans
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t ((f.trans (r := r) (s := s) (t := t) g).top (r := r) (s := t)) (g.top (r := s) (s := t))

Tactic:
apply PrincipalSeg.lt_top

Premises used: PrincipalSeg.lt_top
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_4
r : α → α → Prop
a : α
b : { x : α // r x a }
⊢ ((ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) : (a : { x : α // r x a }) → α) b =
    (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : { b : β // s b (f.top (r := r) (s := s)) }
⊢ (f.toRelEmbedding (r := r) (s := s) : (a : α) → β)
      ((f.subrelIso (r := r) (s := s) : (a : { x : β // s x f.top }) → α) b : α) =
    (↑b : β)

Tactic:
Equiv.apply_ofInjective_symm f.injective _

Premises used: Function.invFun, Set.Mem, RelEmbedding.injective, setOf, PrincipalSeg.toRelEmbedding, dite, Set.range, Equiv.apply_ofInjective_symm
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
a : α
⊢ (f.subrelIso (r := r) (s := s) : (a : { x : β // s x f.top }) → α)
      (Subtype.mk (p := fun (x : β) ↦ s x (f.top (r := r) (s := s)))
          ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a) ⋯ :
        { x : β // s x (f.top (r := r) (s := s)) }) =
    a

Tactic:
Equiv.ofInjective_symm_apply f.injective _

Premises used: Function.invFun, RelEmbedding.injective, PrincipalSeg.toRelEmbedding, Equiv.ofInjective_symm_apply, dite
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≺i s
H : ∀ (a : α), Membership.mem (α := β) p ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
H₂ : f.top (r := r) (s := s) ∈ p
x : { x : β // x ∈ p }
val : β
property : val ∈ p
⊢ Membership.mem (γ := Set { x : β // x ∈ p })
      (Set.range.{u_2, u_1 + 1} (ι := α)
        (⇑(RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H) :
          (a : α) → { x : β // x ∈ p }))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ p) val property) ↔
    Subrel s (fun (x : β) ↦ x ∈ p) (Subtype.mk (p := fun (x : β) ↦ x ∈ p) val property)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ p) (f.top (r := r) (s := s)) H₂)

Tactic:
simp [← f.mem_range_iff_rel]

Premises used: PrincipalSeg.mem_range_iff_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p : Set β
f : r ≺i s
H : ∀ (a : α), Membership.mem (α := β) p ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
H₂ : f.top (r := r) (s := s) ∈ p
a : α
⊢ Eq.{u_2 + 1} (α := { x : β // x ∈ p })
    (((codRestrict (r := r) (s := s) p f H H₂).toRelEmbedding (r := r) (s := Subrel s fun (x : β) ↦ x ∈ p) :
          (a : α) → { x : β // x ∈ p })
        a :
      { x : β // x ∈ p })
    (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a) ⋯ :
      { x : β // x ∈ p })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p : Set β
f : r ≺i s
H : ∀ (a : α), Membership.mem (α := β) p ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
H₂ : f.top (r := r) (s := s) ∈ p
⊢ (codRestrict (r := r) (s := s) p f H H₂).top (r := r) (s := Subrel s fun (x : β) ↦ x ∈ p) =
    Subtype.mk (p := fun (x : β) ↦ x ∈ p) (f.top (r := r) (s := s)) H₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsEmpty α
b : β
H : ∀ (b' : β), ¬s b' b
⊢ ∀ (b_1 : β),
    Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(RelEmbedding.ofIsEmpty r s) : (a : α) → β)) b_1 ↔
      s b_1 b

Tactic:
simp [H]
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
s : β → β → Prop
r : α → α → Prop
inst : IsEmpty α
b : β
H : ∀ (b' : β), ¬s b' b
⊢ (ofIsEmpty (s := s) r H).top (r := r) (s := s) = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsTrans β s
f : r ≺i s
a : α
⊢ Acc r a ↔ Acc s ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a)

Tactic:
(f : r ≼i s).acc a

Premises used: InitialSeg.acc, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
β : Type u
s : β → β → Prop
inst : IsTrans β s
⊢ WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (x : r ≺i s), WellFounded r

Tactic:
⟨fun wf _ _ f => RelHomClass.wellFounded f.toRelEmbedding wf, fun h =>
    wellFounded_iff_wellFounded_subrel.mpr fun b => h _ _ (PrincipalSeg.ofElement s b)⟩

Premises used: Iff.mpr, RelHomClass.wellFounded, PrincipalSeg.toRelEmbedding, Subtype, Subrel, Iff.intro, wellFounded_iff_wellFounded_subrel, PrincipalSeg.ofElement
-- Module: Mathlib.Order.InitialSeg
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 : α
rw :
  Eq.{u_3 + 1} (α := γ)
    ((PrincipalSeg.toRelEmbedding (r := r) (s := t)
            (match (motive := (r ≺i s) ⊕ (r ≃r s) → r ≺i t) f.principalSumRelIso (r := r) (s := s) 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 : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ)
    (((f.transPrincipal (r := r) (s := s) (t := t) g).toRelEmbedding (r := r) (s := t) : (a : α) → γ) a : γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rw [InitialSeg.transPrincipal]

Premises used: InitialSeg.transPrincipal
-- Module: Mathlib.Order.InitialSeg
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 : α
inl :
  ∀ (f' : r ≺i s),
    Eq.{u_3 + 1} (α := γ)
      ((PrincipalSeg.toRelEmbedding (r := r) (s := t)
              (match (motive := (r ≺i s) ⊕ (r ≃r s) → r ≺i t) Sum.inl 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 : β) : γ)
inr :
  ∀ (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 : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ)
    ((PrincipalSeg.toRelEmbedding (r := r) (s := t)
            (match (motive := (r ≺i s) ⊕ (r ≃r s) → r ≺i t) f.principalSumRelIso (r := r) (s := s) 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 : β) : γ)

Tactic:
obtain f' | f' := f.principalSumRelIso

Premises used: InitialSeg.principalSumRelIso
-- Module: Mathlib.Order.InitialSeg
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 ≺i s
inl :
  Eq.{u_3 + 1} (α := γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f'.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β) : γ)
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)
inl₁ inl₂ :
  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.inl 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 : β) : γ)

Tactic:
rw [PrincipalSeg.trans_apply, f.eq_principalSeg]

Premises used: PrincipalSeg.trans_apply, InitialSeg.eq_principalSeg
-- Module: Mathlib.Order.InitialSeg
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 : β) : γ)
inr₁ 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 : β) : γ)

Tactic:
rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]

Premises used: InitialSeg.eq_relIso, PrincipalSeg.relIsoTrans_apply
-- Module: Mathlib.Order.InitialSeg
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)
inr : ∀ (f : r ≃r 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)

Tactic:
obtain f | f := f.principalSumRelIso

Premises used: InitialSeg.principalSumRelIso
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f_1 : r ≼i s
f : r ≺i s
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
⟨_, _, inferInstance,
      ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩

Premises used: PrincipalSeg.subrelIso, RelIso.refl, inferInstance, RelIso.symm, RelIso.sumLexComplLeft, Nonempty.intro, And.intro, Exists.intro, RelIso.trans, RelIso.sumLexCongr
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f_1 : r ≼i s
f : r ≺i s
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
exact ⟨_, _, inferInstance,
      ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f_1 : r ≼i s
f : r ≃r s
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩

Premises used: _private.0.InitialSeg.exists_sum_relIso.match_1, inferInstance, PEmpty, Nonempty.intro, And.intro, RelIso.sumLexEmpty, Exists.intro, RelIso.trans
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst : IsWellOrder β s
f_1 : r ≼i s
f : r ≃r s
⊢ ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩
-- Module: Mathlib.Order.InitialSeg
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)
inr inr₁ : ∀ (f : r ≃r 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)

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⟩⟩

Premises used: InitialSeg.principalSumRelIso
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ↪r s
a : α
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) : β)
⊢ ∀ {a' : α}, r a' a → s (↑(collapseF (r := r) (s := s) f a') : β) (↑(collapseF (r := r) (s := s) f a) : β)

Tactic:
change _ ∈ { b | ∀ a', r a' a → s (collapseF f a') b }
-- Module: Mathlib.Order.InitialSeg
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
            (↑(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_1 : α) (h : r a_1 a), s (↑(IH a_1 h) : β) b} ⋯) ⋯ :
                      { b : β // ¬s ((f : (a : α) → β) a) b }))
                  a') :
              β)
            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.min_mem _ _ _

Premises used: WellFounded.min_mem
-- Module: Mathlib.Order.InitialSeg
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
            (↑(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_1 : α) (h : r a_1 a), s (↑(IH a_1 h) : β) b} ⋯) ⋯ :
                      { b : β // ¬s ((f : (a : α) → β) a) b }))
                  a') :
              β)
            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.min_mem _ _ _

Premises used: WellFounded.min_mem
-- 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
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 := ⋯;
                                  (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}
              ⋯)
            ⋯) :
        β)
⊢ ¬s b (↑(collapseF (r := r) (s := s) f a) : β)

Tactic:
rw [collapseF, IsWellFounded.fix_eq]

Premises used: IsWellFounded.fix_eq, _private.0.collapseF