α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b b' : β
hb' : s b' b
⊢ Acc s b'
α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
⊢ WellFounded s ↔ ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
refine'
  ⟨fun wf b => ⟨fun b' => ((PrincipalSeg.ofElement _ b).acc b').mpr (wf.apply b')⟩, fun wf =>
    ⟨fun b => Acc.intro _ fun b' hb' => _⟩⟩
α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b b' : β
hb' : s b' b
f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b
⊢ Acc s b'
α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b b' : β
hb' : s b' b
⊢ Acc s b'
let f := PrincipalSeg.ofElement s b
case intro
α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b : β
f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b
b' : ↑{b_1 | s b_1 b}
hb' : s (↑f.toRelEmbedding b') b
⊢ Acc s (↑f.toRelEmbedding b')
α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b b' : β
hb' : s b' b
f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b
⊢ Acc s b'
obtain ⟨b', rfl⟩ := f.down.mp ((PrincipalSeg.ofElement_top s b).symm ▸ hb' : s b' f.top)
no goals
case intro
α : Type ?u.65547
β✝ : Type ?u.65550
γ : Type ?u.65553
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_1
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b : β
f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b
b' : ↑{b_1 | s b_1 b}
hb' : s (↑f.toRelEmbedding b') b
⊢ Acc s (↑f.toRelEmbedding b')
exact (f.acc b').mp ((wf b).apply b')