case h
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ x ∈ iUnionLift S f hf T hT ⁻¹' t ↔ x ∈ inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : S i ⊆ ⋃ (i : ι), S i) '' (f i ⁻¹' t)
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
⊢ iUnionLift S f hf T hT ⁻¹' t = inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : S i ⊆ ⋃ (i : ι), S i) '' (f i ⁻¹' t)
ext x
case h
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ iUnionLift S f hf T hT x ∈ t ↔ ∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x
case h
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ x ∈ iUnionLift S f hf T hT ⁻¹' t ↔ x ∈ inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : S i ⊆ ⋃ (i : ι), S i) '' (f i ⁻¹' t)
simp only [mem_preimage, mem_iUnion, mem_image]
case h.mp
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ iUnionLift S f hf T hT x ∈ t → ∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x

case h.mpr
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ (∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x) → iUnionLift S f hf T hT x ∈ t
case h
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ iUnionLift S f hf T hT x ∈ t ↔ ∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x
constructor
case h.mp.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x ∈ t → ∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x
case h.mp
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ iUnionLift S f hf T hT x ∈ t → ∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x
rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
case h.mp.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : iUnionLift S f hf T hT x ∈ t
⊢ f i { val := ↑x, property := hi } ∈ t
case h.mp.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x ∈ t → ∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x
refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
no goals
case h.mp.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : iUnionLift S f hf T hT x ∈ t
⊢ f i { val := ↑x, property := hi } ∈ t
rwa [iUnionLift_of_mem x hi] at h
case h.mpr.intro.intro.mk.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
y : α
hi : y ∈ S i
h : f i { val := y, property := hi } ∈ t
hxy : inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := y, property := hi } = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t
case h.mpr
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
⊢ (∃ i x_1, f i x_1 ∈ t ∧ inclusion (_ : S i ⊆ ⋃ (i : ι), S i) x_1 = inclusion hT x) → iUnionLift S f hf T hT x ∈ t
rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
case h.mpr.intro.intro.mk.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : f i { val := ↑x, property := hi } ∈ t
hxy : inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi } = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t
case h.mpr.intro.intro.mk.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
y : α
hi : y ∈ S i
h : f i { val := y, property := hi } ∈ t
hxy : inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := y, property := hi } = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t
obtain rfl : y = x := congr_arg Subtype.val hxy
no goals
case h.mpr.intro.intro.mk.intro
α : Type u_2
ι : Sort u_3
β : Type u_1
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
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : f i { val := ↑x, property := hi } ∈ t
hxy : inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi } = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t
rwa [iUnionLift_of_mem x hi]