[GOAL]
α : 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 }
[PROOFSTEP]
cases' x with x hx
[GOAL]
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 }
[PROOFSTEP]
exact hf _ _ _ _ _
[GOAL]
α : Type u_1
ι : Sort u_3
β : Type 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
t : Set β
⊢ iUnionLift S f hf T hT ⁻¹' t = inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : S i ⊆ ⋃ (i : ι), S i) '' (f i ⁻¹' t)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
ι : Sort u_3
β : Type 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
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)
[PROOFSTEP]
simp only [mem_preimage, mem_iUnion, mem_image]
[GOAL]
case h
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
[GOAL]
case h.mp.intro
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
[GOAL]
case h.mp.intro
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
rwa [iUnionLift_of_mem x hi] at h 
[GOAL]
case h.mpr
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
[GOAL]
case h.mpr.intro.intro.mk.intro
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
obtain rfl : y = x := congr_arg Subtype.val hxy
[GOAL]
case h.mpr.intro.intro.mk.intro
α : Type u_1
ι : Sort u_3
β : Type 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
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
[PROOFSTEP]
rwa [iUnionLift_of_mem x hi]
[GOAL]
α : 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
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
⊢ iUnionLift S f hf T hT c = cβ
[PROOFSTEP]
let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)
[GOAL]
α : 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
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
⊢ iUnionLift S f hf T hT c = cβ
[PROOFSTEP]
have : ci i = ⟨c, hi⟩ := Subtype.ext (hci i)
[GOAL]
α : 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
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
this : ci i = { val := ↑c, property := hi }
⊢ iUnionLift S f hf T hT c = cβ
[PROOFSTEP]
rw [iUnionLift_of_mem _ hi, ← this, h]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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
u : ↑T → ↑T
ui : (i : ι) → ↑(S i) → ↑(S i)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ T) x) = inclusion (_ : S i ⊆ T) (ui i x)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
x : ↑T
⊢ iUnionLift S f hf T (_ : T ≤ iUnion S) (u x) = uβ (iUnionLift S f hf T (_ : T ≤ iUnion S) x)
[PROOFSTEP]
subst hT'
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x) =
    uβ (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) x)
[PROOFSTEP]
cases' Set.mem_iUnion.1 x.prop with i hi
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x) =
    uβ (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) x)
[PROOFSTEP]
rw [iUnionLift_of_mem x hi, ← h i]
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x) = f i (ui i { val := ↑x, property := hi })
[PROOFSTEP]
have : x = Set.inclusion (Set.subset_iUnion S i) ⟨x, hi⟩ :=
  by
  cases x
  rfl
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ x = inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi }
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
i : ι
val✝ : α
property✝ : val✝ ∈ iUnion S
hi : ↑{ val := val✝, property := property✝ } ∈ S i
⊢ { val := val✝, property := property✝ } =
    inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑{ val := val✝, property := property✝ }, property := hi }
[PROOFSTEP]
rfl
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi }
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x) = f i (ui i { val := ↑x, property := hi })
[PROOFSTEP]
conv_lhs => rw [this, hui, iUnionLift_inclusion]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi }
| iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x)
[PROOFSTEP]
rw [this, hui, iUnionLift_inclusion]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi }
| iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x)
[PROOFSTEP]
rw [this, hui, iUnionLift_inclusion]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
hT : iUnion S ⊆ iUnion S
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion (_ : S i ⊆ iUnion S) x) = inclusion (_ : S i ⊆ iUnion S) (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion (_ : S i ⊆ ⋃ (i : ι), S i) { val := ↑x, property := hi }
| iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (u x)
[PROOFSTEP]
rw [this, hui, iUnionLift_inclusion]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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
dir : Directed (fun x x_1 => x ≤ x_1) S
op : ↑T → ↑T → ↑T
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ T) (opi i x y) = op (inclusion (_ : S i ⊆ T) x) (inclusion (_ : S i ⊆ T) y)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
x y : ↑T
⊢ iUnionLift S f hf T (_ : T ≤ iUnion S) (op x y) =
    opβ (iUnionLift S f hf T (_ : T ≤ iUnion S) x) (iUnionLift S f hf T (_ : T ≤ iUnion S) y)
[PROOFSTEP]
subst hT'
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    opβ (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) x)
      (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) y)
[PROOFSTEP]
cases' Set.mem_iUnion.1 x.prop with i hi
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    opβ (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) x)
      (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) y)
[PROOFSTEP]
cases' Set.mem_iUnion.1 y.prop with j hj
[GOAL]
case intro.intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    opβ (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) x)
      (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) y)
[PROOFSTEP]
rcases dir i j with ⟨k, hik, hjk⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    opβ (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) x)
      (iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) y)
[PROOFSTEP]
rw [iUnionLift_of_mem x (hik hi), iUnionLift_of_mem y (hjk hj), ← h k]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    f k (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })
[PROOFSTEP]
have hx : x = Set.inclusion (Set.subset_iUnion S k) ⟨x, hik hi⟩ :=
  by
  cases x
  rfl
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
y : ↑(iUnion S)
i j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
val✝ : α
property✝ : val✝ ∈ iUnion S
hi : ↑{ val := val✝, property := property✝ } ∈ S i
⊢ { val := val✝, property := property✝ } =
    inclusion (_ : S k ⊆ ⋃ (i : ι), S i)
      { val := ↑{ val := val✝, property := property✝ },
        property := (_ : ↑{ val := val✝, property := property✝ } ∈ S k) }
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    f k (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })
[PROOFSTEP]
have hy : y = Set.inclusion (Set.subset_iUnion S k) ⟨y, hjk hj⟩ :=
  by
  cases y
  rfl
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
⊢ y = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑y, property := (_ : ↑y ∈ S k) }
[PROOFSTEP]
cases y
[GOAL]
case mk
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
val✝ : α
property✝ : val✝ ∈ iUnion S
hj : ↑{ val := val✝, property := property✝ } ∈ S j
⊢ { val := val✝, property := property✝ } =
    inclusion (_ : S k ⊆ ⋃ (i : ι), S i)
      { val := ↑{ val := val✝, property := property✝ },
        property := (_ : ↑{ val := val✝, property := property✝ } ∈ S k) }
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
hy : y = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑y, property := (_ : ↑y ∈ S k) }
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    f k (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })
[PROOFSTEP]
have hxy : (Set.inclusion (Set.subset_iUnion S k) (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩) : α) ∈ S k :=
  (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩).prop
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
hy : y = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑y, property := (_ : ↑y ∈ S k) }
hxy :
  ↑(inclusion (_ : S k ⊆ ⋃ (i : ι), S i)
        (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })) ∈
    S k
⊢ iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y) =
    f k (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })
[PROOFSTEP]
conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
hy : y = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑y, property := (_ : ↑y ∈ S k) }
hxy :
  ↑(inclusion (_ : S k ⊆ ⋃ (i : ι), S i)
        (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })) ∈
    S k
| iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y)
[PROOFSTEP]
rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
hy : y = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑y, property := (_ : ↑y ∈ S k) }
hxy :
  ↑(inclusion (_ : S k ⊆ ⋃ (i : ι), S i)
        (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })) ∈
    S k
| iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y)
[PROOFSTEP]
rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
[GOAL]
α : Type u_1
ι : Sort u_2
β : Sort u_3
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 }
dir : Directed (fun x x_1 => x ≤ x_1) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
hT : iUnion S ⊆ iUnion S
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi :
  ∀ (i : ι) (x y : ↑(S i)),
    inclusion (_ : S i ⊆ iUnion S) (opi i x y) =
      op (inclusion (_ : S i ⊆ iUnion S) x) (inclusion (_ : S i ⊆ iUnion S) y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑x, property := (_ : ↑x ∈ S k) }
hy : y = inclusion (_ : S k ⊆ ⋃ (i : ι), S i) { val := ↑y, property := (_ : ↑y ∈ S k) }
hxy :
  ↑(inclusion (_ : S k ⊆ ⋃ (i : ι), S i)
        (opi k { val := ↑x, property := (_ : ↑x ∈ S k) } { val := ↑y, property := (_ : ↑y ∈ S k) })) ∈
    S k
| iUnionLift S f hf (iUnion S) (_ : iUnion S ≤ iUnion S) (op x y)
[PROOFSTEP]
rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
[GOAL]
α : Type u_1
ι : Sort u_3
β : Type 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 }
hS : iUnion S = univ
t : Set β
⊢ liftCover S f hf hS ⁻¹' t = ⋃ (i : ι), Subtype.val '' (f i ⁻¹' t)
[PROOFSTEP]
change (iUnionLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _
[GOAL]
α : Type u_1
ι : Sort u_3
β : Type 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 }
hS : iUnion S = univ
t : Set β
⊢ (iUnionLift S f hf univ (_ : univ ⊆ iUnion S) ∘ fun a => { val := a, property := (_ : a ∈ univ) }) ⁻¹' t =
    ⋃ (i : ι), Subtype.val '' (f i ⁻¹' t)
[PROOFSTEP]
rw [preimage_comp, preimage_iUnionLift]
[GOAL]
α : Type u_1
ι : Sort u_3
β : Type 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 }
hS : iUnion S = univ
t : Set β
⊢ (fun a => { val := a, property := (_ : a ∈ univ) }) ⁻¹'
      (inclusion (_ : univ ⊆ iUnion S) ⁻¹' ⋃ (i : ι), inclusion (_ : S i ⊆ ⋃ (i : ι), S i) '' (f i ⁻¹' t)) =
    ⋃ (i : ι), Subtype.val '' (f i ⁻¹' t)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
ι : Sort u_3
β : Type 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 }
hS : iUnion S = univ
t : Set β
x✝ : α
⊢ x✝ ∈
      (fun a => { val := a, property := (_ : a ∈ univ) }) ⁻¹'
        (inclusion (_ : univ ⊆ iUnion S) ⁻¹' ⋃ (i : ι), inclusion (_ : S i ⊆ ⋃ (i : ι), S i) '' (f i ⁻¹' t)) ↔
    x✝ ∈ ⋃ (i : ι), Subtype.val '' (f i ⁻¹' t)
[PROOFSTEP]
simp
