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 ≼i s
b : β
h_1 :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
z : α
hs : ¬s ((f : (a : α) → β) z) x
h : s x ((f : (a : α) → β) z)
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
f.mem_range_of_rel h

Premises used: Set.Mem, setOf, InitialSeg.mem_range_of_rel, Set.range
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h_1 :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
z : α
hs : ¬s ((f : (a : α) → β) z) x
h : s x ((f : (a : α) → β) z)
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
exact f.mem_range_of_rel h

Premises used: InitialSeg.mem_range_of_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
y : β
hy : y ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hs : s y x
inr :
  ∀ (z : α) (hy : ((f : (a : α) → β) z : β) ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (hs : s ((f : (a : α) → β) z) x), ∃ (a : α), (f : (a : α) → β) a = x
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
obtain ⟨z, rfl⟩ := IH y hs

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
z : α
hy : ((f : (a : α) → β) z : β) ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hs : s ((f : (a : α) → β) z) x
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
cases hy (Set.mem_range_self z)

Premises used: Set.mem_range_self
-- 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 : (a : α) → β) a : β)
a : α
x : { x : β // x ∈ p }
b : β
m : b ∈ p
h :
  Subrel s (fun (x : β) ↦ x ∈ p) (Subtype.mk (p := fun (x : β) ↦ x ∈ p) b m)
    ((RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H :
        (a : α) → { x : β // x ∈ p })
      a)
a' : α
e : (f : (a : α) → β) a' = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ p) b m) : β)
subst :
  ∀ (m : Membership.mem (α := β) p ((f : (a : α) → β) a' : β))
    (h :
      Subrel s (fun (x : β) ↦ x ∈ p) (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a') m)
        ((RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H :
            (a : α) → { x : β // x ∈ p })
          a)),
    Eq.{u_2 + 1} (α := { x : β // x ∈ p })
      ((RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H :
            (a : α) → { x : β // x ∈ p })
          a' :
        { x : β // x ∈ p })
      (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a') m : { x : β // x ∈ p })
⊢ (RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H : (a : α) → { x : β // x ∈ p })
      a' =
    Subtype.mk (p := fun (x : β) ↦ x ∈ p) b m

Tactic:
subst e
-- 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 : (a : α) → β) a : β)
a : α
x : { x : β // x ∈ p }
a' : α
m : Membership.mem (α := β) p ((f : (a : α) → β) a' : β)
h :
  Subrel s (fun (x : β) ↦ x ∈ p) (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a') m)
    ((RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H :
        (a : α) → { x : β // x ∈ p })
      a)
⊢ Eq.{u_2 + 1} (α := { x : β // x ∈ p })
    ((RelEmbedding.codRestrict (r := r) (s := s) p (f.toRelEmbedding (r := r) (s := s)) H :
          (a : α) → { x : β // x ∈ p })
        a' :
      { x : β // x ∈ p })
    (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a') m : { x : β // x ∈ p })

Tactic:
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 : (a : α) → β) a : β)
a : α
⊢ Eq.{u_2 + 1} (α := { x : β // x ∈ p })
    ((codRestrict (r := r) (s := s) p f H : (a : α) → { x : β // x ∈ p }) a : { x : β // x ∈ p })
    (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a) ⋯ : { x : β // x ∈ p })

Tactic:
rfl

Premises used: rfl
-- 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
a : α
b : α ⊕ β
inl :
  ∀ (val : α),
    Sum.Lex r s (Sum.inl val)
        ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
      Membership.mem (γ := Set (α ⊕ β))
        (Set.range (ι := α)
          (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
        (Sum.inl val)
inr :
  ∀ (val : β),
    Sum.Lex r s (Sum.inr val)
        ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
      Membership.mem (γ := Set (α ⊕ β))
        (Set.range (ι := α)
          (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
        (Sum.inr val)
⊢ Sum.Lex r s b ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
      b

Tactic:
cases b
-- 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
a val : α
⊢ Sum.Lex r s (Sum.inl val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
      (Sum.inl val)

Tactic:
fun _ => ⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- 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
a val : α
⊢ Sum.Lex r s (Sum.inl val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
      (Sum.inl val)

Tactic:
exact fun _ => ⟨_, rfl⟩
-- 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
a : α
val : β
⊢ Sum.Lex r s (Sum.inr val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
      (Sum.inr val)

Tactic:
False.elim ∘ Sum.lex_inr_inl

Premises used: Sum.lex_inr_inl, False.elim, Function.comp
-- 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
a : α
val : β
⊢ Sum.Lex r s (Sum.inr val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
      (Sum.inr val)

Tactic:
exact False.elim ∘ Sum.lex_inr_inl

Premises used: Sum.lex_inr_inl, 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
a : α
b : α ⊕ β
inl :
  ∀ (val : α),
    Sum.Lex r s (Sum.inl val)
        ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
      Membership.mem (γ := Set (α ⊕ β))
        (Set.range (ι := α)
          (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
        (Sum.inl val)
inr :
  ∀ (val : β),
    Sum.Lex r s (Sum.inr val)
        ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
      Membership.mem (γ := Set (α ⊕ β))
        (Set.range (ι := α)
          (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
        (Sum.inr val)
inl₁ :
  ∀ (val : α),
    Sum.Lex r s (Sum.inl val)
        ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
      Membership.mem (γ := Set (α ⊕ β))
        (Set.range (ι := α)
          (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
        (Sum.inl val)
inr₁ :
  ∀ (val : β),
    Sum.Lex r s (Sum.inr val)
        ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
      Membership.mem (γ := Set (α ⊕ β))
        (Set.range (ι := α)
          (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
        (Sum.inr val)
⊢ Sum.Lex r s b ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯ : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := ⋯ } ⋯) : (a : α) → α ⊕ β))
      b

Tactic:
cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]

Premises used: Sum.lex_inr_inl, False.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
a : α
⊢ Eq (α := α ⊕ β) ((leAdd r s : (a : α) → α ⊕ β) a : α ⊕ β) (Sum.inl a : α ⊕ β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
⊢ Acc r a → Acc s ((f : (a : α) → β) a)

Tactic:
fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_

Premises used: Acc.recOn
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
refine :
  ∀ (h : Acc r a) (a : α),
    (∀ (y : α), r y a → Acc r y) →
      ∀ (ha : ∀ (y : α), r y a → Acc s ((f : (a : α) → β) y)) (b : β) (hb : s b ((f : (a : α) → β) a)), Acc s b
⊢ Acc r a → Acc s ((f : (a : α) → β) a)

Tactic:
refine fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a_1 : α
h : Acc r a_1
a : α
h_1 : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s ((f : (a : α) → β) y)
b : β
hb : s b ((f : (a : α) → β) a)
obtain : ∀ (a' : α) (hb : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)), Acc s ((f : (a : α) → β) a')
⊢ Acc s b

Tactic:
obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb

Premises used: InitialSeg.mem_range_of_rel, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a_1 : α
h : Acc r a_1
a : α
h_1 : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s ((f : (a : α) → β) y)
a' : α
hb : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)
⊢ Acc s ((f : (a : α) → β) a')

Tactic:
ha _ (f.map_rel_iff.mp hb)

Premises used: InitialSeg.map_rel_iff, Iff.mp
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a_1 : α
h : Acc r a_1
a : α
h_1 : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s ((f : (a : α) → β) y)
a' : α
hb : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)
⊢ Acc s ((f : (a : α) → β) a')

Tactic:
exact ha _ (f.map_rel_iff.mp hb)

Premises used: InitialSeg.map_rel_iff, Iff.mp
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b ↔ s b a
b : β
hg :
  ∀ (b_1 : β),
    Membership.mem (γ := Set β)
        (Set.range.{u_2, u_1 + 1} (ι := α)
          (⇑((mk (r := r) (s := s) f a hf).toRelEmbedding (r := r) (s := s)) : (a : α) → β))
        b_1 ↔
      s b_1 b
e_top : a = b
⊢ mk (r := r) (s := s) f a hf =
    mk (r := r) (s := s) ((mk (r := r) (s := s) f a hf).toRelEmbedding (r := r) (s := s)) b hg

Tactic:
congr
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b ↔ s b a
b : β
hg :
  ∀ (b_1 : β),
    Membership.mem (γ := Set β)
        (Set.range.{u_2, u_1 + 1} (ι := α)
          (⇑((mk (r := r) (s := s) f a hf).toRelEmbedding (r := r) (s := s)) : (a : α) → β))
        b_1 ↔
      s b_1 b
⊢ a = b

Tactic:
extensional_of_trichotomous_of_irrefl s fun x ↦ ?_

Premises used: extensional_of_trichotomous_of_irrefl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b ↔ s b a
b : β
hg :
  ∀ (b_1 : β),
    Membership.mem (γ := Set β)
        (Set.range.{u_2, u_1 + 1} (ι := α)
          (⇑((mk (r := r) (s := s) f a hf).toRelEmbedding (r := r) (s := s)) : (a : α) → β))
        b_1 ↔
      s b_1 b
e_top : ∀ (x : β), s x a ↔ s x b
⊢ a = b

Tactic:
refine extensional_of_trichotomous_of_irrefl s fun x ↦ ?_

Premises used: extensional_of_trichotomous_of_irrefl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b ↔ s b a
b : β
hg :
  ∀ (b_1 : β),
    Membership.mem (γ := Set β)
        (Set.range.{u_2, u_1 + 1} (ι := α)
          (⇑((mk (r := r) (s := s) f a hf).toRelEmbedding (r := r) (s := s)) : (a : α) → β))
        b_1 ↔
      s b_1 b
x : β
e_top : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b
e_top₁ e_top₂ : s x b ↔ s x b
⊢ s x a ↔ s x b

Tactic:
rw [← hf, hg]
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f g : r ≺i s
⊢ f.toRelEmbedding (r := r) (s := s) = g.toRelEmbedding (r := r) (s := s) ↔ f = g

Tactic:
toRelEmbedding_injective.eq_iff

Premises used: Function.Injective.eq_iff, PrincipalSeg.toRelEmbedding_injective
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f g : r ≺i s
h :
  ∀ (x : α),
    Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
      ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
rw : f.toRelEmbedding (r := r) (s := s) = g.toRelEmbedding (r := r) (s := s)
⊢ f = g

Tactic:
rw [← toRelEmbedding_inj]

Premises used: PrincipalSeg.toRelEmbedding_inj
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f g : r ≺i s
h h₁ :
  ∀ (x : α),
    Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
      ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
⊢ f.toRelEmbedding (r := r) (s := s) = g.toRelEmbedding (r := r) (s := s)

Tactic:
ext
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f g : r ≺i s
h :
  ∀ (x : α),
    Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
      ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
    ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)

Tactic:
h _
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl s
inst_1 : Std.Trichotomous s
f g : r ≺i s
h :
  ∀ (x : α),
    Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
      ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
    ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)

Tactic:
exact h _
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
t : β
o : ∀ (b : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b ↔ s b t
⊢ Eq (α := (a : α) → β) (⇑((mk (r := r) (s := s) f t o).toRelEmbedding (r := r) (s := s)) : (a : α) → β)
    (⇑f : (a : α) → β)

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 : β
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β))
      b ↔
    s b (f.top (r := r) (s := s))

Tactic:
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
f : r ≺i s
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β))
    {b : β | s b (f.top (r := r) (s := s))}

Tactic:
Set.ext_iff.2 fun _ ↦ mem_range_iff_rel f

Premises used: Iff.mpr, PrincipalSeg.mem_range_iff_rel, Set.ext_iff
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
a : α
⊢ s ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a) (f.top (r := r) (s := s))

Tactic:
f.mem_range_iff_rel.1 ⟨_, rfl⟩

Premises used: PrincipalSeg.mem_range_iff_rel, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : s b (f.top (r := r) (s := s))
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β))
    b

Tactic:
f.mem_range_iff_rel.2 h

Premises used: Iff.mpr, PrincipalSeg.mem_range_iff_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsTrans β s
f : r ≺i s
a : α
b : β
h : s b ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a)
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β))
    b

Tactic:
f.mem_range_of_rel_top <| _root_.trans h <| f.lt_top _

Premises used: trans, PrincipalSeg.mem_range_of_rel_top, PrincipalSeg.lt_top
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : Membership.mem (γ := Set β) {b : β | s b (f.top (r := r) (s := s))} b
⊢ Membership.mem (γ := Set β)
    (Set.image.{u_1, u_2} (α := α) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) Set.univ) b

Tactic:
simpa using mem_range_of_rel_top _ h

Premises used: PrincipalSeg.mem_range_of_rel_top
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsTrans β s
f : r ≺i s
⊢ Eq (α := (a : α) → β) (⇑(InitialSeg.mk (r := r) (s := s) (f.toRelEmbedding (r := r) (s := s)) ⋯) : (a : α) → β)
    (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β)

Tactic:
rfl

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

Tactic:
InitialSeg.eq g f a

Premises used: InitialSeg.eq
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsTrans β s
f : r ≺i s
a : α
b : β
⊢ s b ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a) ↔
    ∃ (a' : α), (f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' = b ∧ r a' a

Tactic:
@InitialSeg.exists_eq_iff_rel α β r s f a b

Premises used: InitialSeg.exists_eq_iff_rel, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
hf : ¬Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
x : α
⊢ Eq.{u_2 + 1} (α := β) (((f.toPrincipalSeg (r := r) (s := s) hf).toRelEmbedding (r := r) (s := s) : (a : α) → β) x : β)
    ((f : (a : α) → β) x : β)

Tactic:
rfl

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

Tactic:
have h := f.lt_top f.top
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
f : r ≺i r
h : r ((f.toRelEmbedding (r := r) (s := r) : (a : α) → α) (f.top (r := r) (s := r))) (f.top (r := r) (s := r))
⊢ r (f.top (r := r) (s := r)) (f.top (r := r) (s := r))

Tactic:
rw [show f f.top = f.top from InitialSeg.eq f (InitialSeg.refl r) f.top] at h
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
f : r ≺i r
h : r (f.top (r := r) (s := r)) (f.top (r := r) (s := r))
⊢ False

Tactic:
_root_.irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
f : r ≺i r
h : r (f.top (r := r) (s := r)) (f.top (r := r) (s := r))
⊢ False

Tactic:
exact _root_.irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
⊢ IsEmpty.{u_1 + 1} (r ≺i r)

Tactic:
⟨fun f => f.irrefl⟩

Premises used: PrincipalSeg.irrefl, IsEmpty.mk
-- 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 : γ
⊢ 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 : α) → γ))
      a ↔
    t a ((g : (a : β) → γ) (f.top (r := r) (s := s)))

Tactic:
simp [g.exists_eq_iff_rel, ← PrincipalSeg.mem_range_iff_rel, exists_comm, ← exists_and_left]

Premises used: PrincipalSeg.mem_range_iff_rel, InitialSeg.exists_eq_iff_rel, exists_and_left, exists_comm