case mk
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ iUnion S
hT' : T = iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑{ val := x, property := hx✝ } ∈ S i
⊢ iUnionLift S f hf T hT { val := x, property := hx✝ } = f i { val := ↑{ val := x, property := hx✝ }, property := hx }
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ iUnion S
hT' : T = iUnion S
x : ↑T
i : ι
hx : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x = f i { val := ↑x, property := hx }
cases' x with x hx
no goals
case mk
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ iUnion S
hT' : T = iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑{ val := x, property := hx✝ } ∈ S i
⊢ iUnionLift S f hf T hT { val := x, property := hx✝ } = f i { val := ↑{ val := x, property := hx✝ }, property := hx }
exact hf _ _ _ _ _