case refine'_1
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ brange (type r) (bfamilyOfFamily' r f) → a ∈ range f

case refine'_2
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ brange (type r) (bfamilyOfFamily' r f)
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
⊢ brange (type r) (bfamilyOfFamily' r f) = range f
refine' Set.ext fun a => ⟨_, _⟩
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : Ordinal
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f
case refine'_1
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ brange (type r) (bfamilyOfFamily' r f) → a ∈ range f
rintro ⟨i, hi, rfl⟩
no goals
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : Ordinal
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f
apply mem_range_self
case refine'_2.intro
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ brange (type r) (bfamilyOfFamily' r f)
case refine'_2
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ brange (type r) (bfamilyOfFamily' r f)
rintro ⟨b, rfl⟩
no goals
case refine'_2.intro
α : Type u_1
β : Type ?u.276348
γ : Type ?u.276351
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ brange (type r) (bfamilyOfFamily' r f)
exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩