case h.e'_3
α : Type ?u.292293
β : Type ?u.292296
γ : Type ?u.292299
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
s : Set Ordinal
hs : Small ↑s
a : Ordinal
ha : a ∈ s
⊢ a = ↑(↑(equivShrink ↑s).symm (↑(equivShrink ↑s) { val := a, property := ha }))
α : Type ?u.292293
β : Type ?u.292296
γ : Type ?u.292299
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
s : Set Ordinal
hs : Small ↑s
a : Ordinal
ha : a ∈ s
⊢ a ≤ sup fun x => ↑(↑(equivShrink ↑s).symm x)
convert le_sup.{u, u} (fun x => ((@equivShrink s hs).symm x).val) ((@equivShrink s hs) ⟨a, ha⟩)
no goals
case h.e'_3
α : Type ?u.292293
β : Type ?u.292296
γ : Type ?u.292299
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
s : Set Ordinal
hs : Small ↑s
a : Ordinal
ha : a ∈ s
⊢ a = ↑(↑(equivShrink ↑s).symm (↑(equivShrink ↑s) { val := a, property := ha }))
rw [symm_apply_apply]