awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.InitialSeg (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
h : ¬∃ (b : β), ∀ (x : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b
b : β
⊢ ∃ (a : α), (f : (a : α) → β) a = b
have 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
Tactic: push Not at h
Cleared hypotheses: h
-- 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 ≼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
⊢ ∃ (a : α), (f : (a : α) → β) a = b
have apply : ∀ (x : β), (∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y) → ∃ (a : α), (f : (a : α) → β) a = x
Tactic: apply IsWellFounded.induction s 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 ≼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
⊢ ∃ (a : α), (f : (a : α) → β) a = x
have inl : ∀ (y : β) (hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y) (hs : ¬s y x),
  ∃ (a : α), (f : (a : α) → β) a = x
Tactic: obtain ⟨y, ⟨hy, hs⟩ | ⟨hy, hs⟩⟩ := h x
-- 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 ≼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
inl :
  ∀ (y : β) (hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y) (hs : ¬s y x),
    ∃ (a : α), (f : (a : α) → β) a = x
⊢ ∃ (a : α), (f : (a : α) → β) a = x
have inr : ∀ (y : β) (hy : y ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) (hs : s y x),
  ∃ (a : α), (f : (a : α) → β) a = x
Tactic: obtain ⟨y, ⟨hy, hs⟩ | ⟨hy, hs⟩⟩ := h x
-- 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 ≼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 : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
hs : ¬s y x
⊢ ∃ (a : α), (f : (a : α) → β) a = x
have inl : ∀ (IH : ∀ (y_1 : β), s y_1 y → ∃ (a : α), (f : (a : α) → β) a = y_1) (hs : ¬s y y), ∃ (a : α), (f : (a : α) → β) a = y
Tactic: obtain (rfl | h) := (trichotomous y x).resolve_left hs
Cleared hypotheses: x, IH, hs
-- 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 ≼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 : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
hs : ¬s y x
inl :
  ∀ (IH : ∀ (y_1 : β), s y_1 y → ∃ (a : α), (f : (a : α) → β) a = y_1) (hs : ¬s y y), ∃ (a : α), (f : (a : α) → β) a = y
⊢ ∃ (a : α), (f : (a : α) → β) a = x
have inl₁ : ∀ (h : s x y), ∃ (a : α), (f : (a : α) → β) a = x
Tactic: obtain (rfl | h) := (trichotomous y x).resolve_left hs
-- 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 ≼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
y : β
hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
hs : ¬s y x
h : s x y
⊢ ∃ (a : α), (f : (a : α) → β) a = x
have inl : ∀ (z : α) (hs : ¬s ((f : (a : α) → β) z) x) (h : s x ((f : (a : α) → β) z)), ∃ (a : α), (f : (a : α) → β) a = x
Tactic: obtain ⟨z, rfl⟩ := hy
Cleared hypotheses: y, hy, hs, h
-- 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 ≼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
⊢ ∃ (a : α), (f : (a : α) → β) a = x
have 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
Tactic: obtain ⟨z, rfl⟩ := IH y hs
Cleared hypotheses: y, hy, hs
-- 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
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) : β)
⊢ (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
have 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 })
Tactic: subst e
Cleared hypotheses: b, m, h, e
-- 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
a : α
b : α ⊕ β
⊢ 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
have inl : ∀ (val : α),
  Sum.Lex r s (Sum.inl val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry) : (a : α) → α ⊕ β))
      (Sum.inl val)
Tactic: cases b
Cleared hypotheses: b
-- 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
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)
⊢ 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
have inr : ∀ (val : β),
  Sum.Lex r s (Sum.inr val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry) : (a : α) → α ⊕ β))
      (Sum.inr val)
Tactic: cases b
Cleared hypotheses: b
-- 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
a : α
b : α ⊕ β
⊢ 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
have inl : ∀ (val : α),
  Sum.Lex r s (Sum.inl val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry) : (a : α) → α ⊕ β))
      (Sum.inl val)
Tactic: cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]
Cleared hypotheses: b
-- 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
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)
⊢ 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
have inr : ∀ (val : β),
  Sum.Lex r s (Sum.inr val)
      ((RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry : (a : α) → α ⊕ β) a) →
    Membership.mem (γ := Set (α ⊕ β))
      (Set.range (ι := α)
        (⇑(RelEmbedding.mk (r := r) (s := Sum.Lex r s) { toFun := Sum.inl, inj' := sorry } sorry) : (a : α) → α ⊕ β))
      (Sum.inr val)
Tactic: cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
⊢ Acc r a → Acc s ((f : (a : α) → β) a)
have 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
Tactic: refine fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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)
⊢ Acc s b
have obtain : ∀ (a' : α) (hb : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)), Acc s ((f : (a : α) → β) a')
Tactic: obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ 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
have e_top : a = b
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
have e_top : ∀ (x : β), s x a ↔ s x b
Tactic: refine extensional_of_trichotomous_of_irrefl s fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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 : β
⊢ s x a ↔ s x b
have e_top : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b
Tactic: rw [← hf, hg]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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
⊢ s x a ↔ s x b
have e_top₁ : s x b ↔ s x b
Tactic: rw [← hf, hg]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
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 : β)
⊢ f = g
have rw : f.toRelEmbedding (r := r) (s := s) = g.toRelEmbedding (r := r) (s := s)
Tactic: rw [← toRelEmbedding_inj]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
f : r ≺i r
⊢ False
have h : 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
-- Lean 4 proof step from Mathlib.Order.InitialSeg (hypothesis)
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))
⊢ False
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f g : r ≺i s
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
    ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
have rw : Eq.{u_2 + 1} (α := β) ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
  ((g.toRelEmbedding (r := r) (s := s) : (a : α) → β) a : β)
Tactic: rw [Subsingleton.elim f g]
-- 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 γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ f.top (r := r) (s := t) = g.top (r := s) (s := t)
have rw : (relIsoTrans (r := r) (s := s) (t := t) e g).top (r := r) (s := t) = g.top (r := s) (s := t)
Tactic: rw [Subsingleton.elim f (PrincipalSeg.relIsoTrans e g)]
-- 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 γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (h.top (r := r) (s := t)) (g.top (r := s) (s := t))
have rw : t ((f.trans (r := r) (s := s) (t := t) g).top (r := r) (s := t)) (g.top (r := s) (s := t))
Tactic: rw [Subsingleton.elim h (f.trans g)]
-- 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 : α
⊢ 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 : β) : γ)
have 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 : β) : γ)
Tactic: rw [InitialSeg.transPrincipal]
-- 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 : α
⊢ 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 : β) : γ)
have 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 : β) : γ)
Tactic: obtain f' | f' := f.principalSumRelIso
-- 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 : α
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 : β) : γ)
⊢ 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 : β) : γ)
have 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 : β) : γ)
Tactic: obtain f' | f' := f.principalSumRelIso
-- 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 ≺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 : β) : γ)
have 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 : β) : γ)
Tactic: rw [PrincipalSeg.trans_apply, f.eq_principalSeg]
-- 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 ≺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 : β) : γ)
⊢ 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 : β) : γ)
have 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 : β) : γ)
Tactic: rw [PrincipalSeg.trans_apply, f.eq_principalSeg]