α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
this : ↑f.top = a
⊢ r a b
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
⊢ r a b
have : f.top.1 = a := by
  let f' := PrincipalSeg.ofElement r a
  let g' := f.trans (PrincipalSeg.ofElement r b)
  have : g'.top = f'.top := by rw [Subsingleton.elim f' g']
  exact this
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
this : ↑f.top = a
⊢ r (↑f.top) b
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
this : ↑f.top = a
⊢ r a b
rw [← this]
no goals
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
this : ↑f.top = a
⊢ r (↑f.top) b
exact f.top.2
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
⊢ ↑f.top = a
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
⊢ ↑f.top = a
let f' := PrincipalSeg.ofElement r a
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
⊢ ↑f.top = a
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
⊢ ↑f.top = a
let g' := f.trans (PrincipalSeg.ofElement r b)
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
this : g'.top = f'.top
⊢ ↑f.top = a
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
⊢ ↑f.top = a
have : g'.top = f'.top := by rw [Subsingleton.elim f' g']
no goals
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
this : g'.top = f'.top
⊢ ↑f.top = a
exact this
no goals
α : Type u_1
β : Type ?u.83243
γ : Type ?u.83246
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
⊢ g'.top = f'.top
rw [Subsingleton.elim f' g']