[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


[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑toDual x ∈ ordConnectedComponent (↑ofDual ⁻¹' s) (↑toDual x✝) ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
[PROOFSTEP]
rw [mem_ordConnectedComponent, dual_uIcc]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑ofDual ⁻¹' [[x✝, x]] ⊆ ↑ofDual ⁻¹' s ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ x ∈ ordConnectedComponent s x ↔ x ∈ s
[PROOFSTEP]
rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordConnectedComponent s x = ∅ ↔ ¬x ∈ s
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordConnectedComponent univ x = univ
[PROOFSTEP]
simp [ordConnectedComponent]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s✝ t✝ : Set α
x✝ y z : α
s t : Set α
x : α
⊢ ordConnectedComponent (s ∩ t) x = ordConnectedComponent s x ∩ ordConnectedComponent t x
[PROOFSTEP]
simp [ordConnectedComponent, setOf_and]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ y ∈ ordConnectedComponent s x ↔ x ∈ ordConnectedComponent s y
[PROOFSTEP]
rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ ordConnectedProj s x = ordConnectedProj s y ↔ [[↑x, ↑y]] ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ ordConnectedProj s x = ordConnectedProj s y → [[↑x, ↑y]] ⊆ s
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ [[↑x, ↑y]] ⊆ s → ordConnectedProj s x = ordConnectedProj s y
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
h : ordConnectedProj s x = ordConnectedProj s y
⊢ [[↑x, ↑y]] ⊆ s
[PROOFSTEP]
rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h, ordConnectedComponent_ordConnectedProj,
  self_mem_ordConnectedComponent]
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
h : ordConnectedProj s x = ordConnectedProj s y
⊢ ↑y ∈ s
[PROOFSTEP]
exact y.2
[GOAL]
case mpr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ ordConnectedProj s x = ordConnectedProj s y
[PROOFSTEP]
simp only [ordConnectedProj, ordConnectedComponent_eq h]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x y z : α
s : Set α
⊢ ordConnectedSection (↑ofDual ⁻¹' s) = ↑ofDual ⁻¹' ordConnectedSection s
[PROOFSTEP]
simp_rw [ordConnectedSection, ordConnectedProj]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x y z : α
s : Set α
⊢ (range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent (↑ofDual ⁻¹' s) ↑x))) =
    ↑ofDual ⁻¹' range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent s ↑x))
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x✝ y z : α
s : Set α
x : αᵒᵈ
⊢ (x ∈ range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent (↑ofDual ⁻¹' s) ↑x))) ↔
    x ∈ ↑ofDual ⁻¹' range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent s ↑x))
[PROOFSTEP]
simp [dual_ordConnectedComponent]
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x✝ y z : α
s : Set α
x : αᵒᵈ
⊢ (∃ a h, Nonempty.some (_ : Set.Nonempty (↑ofDual ⁻¹' ordConnectedComponent s a)) = x) ↔
    ∃ a h, Nonempty.some (_ : Set.Nonempty (ordConnectedComponent s ↑{ val := a, property := (_ : a ∈ s) })) = ↑ofDual x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
hx : x ∈ ordConnectedSection s
hy : y ∈ ordConnectedSection s
h : [[x, y]] ⊆ s
⊢ x = y
[PROOFSTEP]
rcases hx with ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
y z : α
hy : y ∈ ordConnectedSection s
x : ↑s
h : [[ordConnectedProj s x, y]] ⊆ s
⊢ ordConnectedProj s x = y
[PROOFSTEP]
rcases hy with ⟨y, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
z : α
x y : ↑s
h : [[ordConnectedProj s x, ordConnectedProj s y]] ⊆ s
⊢ ordConnectedProj s x = ordConnectedProj s y
[PROOFSTEP]
exact
  ordConnectedProj_eq.2
    (mem_ordConnectedComponent_trans
      (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
      (mem_ordConnectedComponent_ordConnectedProj _ _))
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordSeparatingSet (↑ofDual ⁻¹' s) (↑ofDual ⁻¹' t) = ↑ofDual ⁻¹' ordSeparatingSet s t
[PROOFSTEP]
simp only [ordSeparatingSet, mem_preimage, ← toDual.surjective.iUnion_comp, ofDual_toDual, dual_ordConnectedComponent, ←
  preimage_compl, preimage_inter, preimage_iUnion]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ Disjoint (ordT5Nhd s t) (ordT5Nhd t s)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordT5Nhd s t ⊓ ordT5Nhd t s ≤ ⊥
[PROOFSTEP]
rintro x ⟨hx₁, hx₂⟩
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₁ : x ∈ ordT5Nhd s t
hx₂ : x ∈ ordT5Nhd t s
⊢ x ∈ ⊥
[PROOFSTEP]
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₁ : x ∈ ordT5Nhd s t
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ (ordConnectedSection (ordSeparatingSet s t))ᶜ) a
⊢ x ∈ ⊥
[PROOFSTEP]
clear hx₁
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ (ordConnectedSection (ordSeparatingSet s t))ᶜ) a
⊢ x ∈ ⊥
[PROOFSTEP]
rcases mem_iUnion₂.1 hx₂ with ⟨b, hbt, hb⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ (ordConnectedSection (ordSeparatingSet s t))ᶜ) a
b : α
hbt : b ∈ t
hb : x ∈ ordConnectedComponent (sᶜ ∩ (ordConnectedSection (ordSeparatingSet t s))ᶜ) b
⊢ x ∈ ⊥
[PROOFSTEP]
clear hx₂
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ (ordConnectedSection (ordSeparatingSet s t))ᶜ) a
b : α
hbt : b ∈ t
hb : x ∈ ordConnectedComponent (sᶜ ∩ (ordConnectedSection (ordSeparatingSet t s))ᶜ) b
⊢ x ∈ ⊥
[PROOFSTEP]
rw [mem_ordConnectedComponent, subset_inter_iff] at ha hb
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
[PROOFSTEP]
on_goal 2 => swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
[GOAL]
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
[PROOFSTEP]
on_goal 2 => swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
[GOAL]
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
[PROOFSTEP]
swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
[GOAL]
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
[PROOFSTEP]
all_goals
  -- porting note: wlog not implemented yet, the following replaces the three previous lines
  -- wlog (discharger := tactic.skip) hab : a ≤ b := le_total a b using a b s t, b a t s
  cases' ha with ha ha'
  cases' hb with hb hb'
  have hsub : [[a, b]] ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ :=
    by
    rw [ordSeparatingSet_comm, uIcc_comm] at hb'
    calc
      [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
      _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
  clear ha' hb'
  cases' le_total x a with hxa hax
  · exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
  cases' le_total b x with hbx hxb
  · exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
  have h' : x ∈ ordSeparatingSet s t :=
    ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
      -- porting note: lift not implemented yet
          -- lift x to ordSeparatingSet s t using this
  suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
  exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
  rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
  rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
  have sol1 := fun (hya : y < a) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
      (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
  have sol2 := fun (hby : b < y) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
      (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
  exact ⟨sol1, sol2⟩
[GOAL]
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
[PROOFSTEP]
cases' ha with ha ha'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' hb with hb hb'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
have hsub : [[a, b]] ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ :=
  by
  rw [ordSeparatingSet_comm, uIcc_comm] at hb'
  calc
    [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
    _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
⊢ [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
[PROOFSTEP]
rw [ordSeparatingSet_comm, uIcc_comm] at hb'
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
[PROOFSTEP]
calc
  [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
  _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
clear ha' hb'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total x a with hxa hax
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hxa : x ≤ a
⊢ x ∈ ⊥
[PROOFSTEP]
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total b x with hbx hxb
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥
[PROOFSTEP]
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥
[PROOFSTEP]
have h' : x ∈ ordSeparatingSet s t :=
  ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
    -- porting note: lift not implemented yet
        -- lift x to ordSeparatingSet s t using this
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ x ∈ ⊥
[PROOFSTEP]
suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
this : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
⊢ x ∈ ⊥
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[PROOFSTEP]
exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[PROOFSTEP]
rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ y ∈ [[a, b]]
[PROOFSTEP]
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ ¬y < a ∧ ¬b < y
[PROOFSTEP]
have sol1 := fun (hya : y < a) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
    (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y
[PROOFSTEP]
have sol2 := fun (hby : b < y) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
    (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y
[PROOFSTEP]
exact ⟨sol1, sol2⟩
[GOAL]
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
[PROOFSTEP]
cases' ha with ha ha'
[GOAL]
case intro.intro.intro.intro.intro.inr.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' hb with hb hb'
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
have hsub : [[a, b]] ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ :=
  by
  rw [ordSeparatingSet_comm, uIcc_comm] at hb'
  calc
    [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
    _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
⊢ [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
[PROOFSTEP]
rw [ordSeparatingSet_comm, uIcc_comm] at hb'
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
[PROOFSTEP]
calc
  [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
  _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
clear ha' hb'
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total x a with hxa hax
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hxa : x ≤ a
⊢ x ∈ ⊥
[PROOFSTEP]
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total b x with hbx hxb
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥
[PROOFSTEP]
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥
[PROOFSTEP]
have h' : x ∈ ordSeparatingSet s t :=
  ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
    -- porting note: lift not implemented yet
        -- lift x to ordSeparatingSet s t using this
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ x ∈ ⊥
[PROOFSTEP]
suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
this : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
⊢ x ∈ ⊥
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[PROOFSTEP]
exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[PROOFSTEP]
rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ y ∈ [[a, b]]
[PROOFSTEP]
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ ¬y < a ∧ ¬b < y
[PROOFSTEP]
have sol1 := fun (hya : y < a) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
    (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y
[PROOFSTEP]
have sol2 := fun (hby : b < y) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
    (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y
[PROOFSTEP]
exact ⟨sol1, sol2⟩


[GOAL]
k : Type u_1
inst✝ : LinearOrderedField k
⊢ k ≃o ↑(Ioo (-1) 1)
[PROOFSTEP]
refine' StrictMono.orderIsoOfRightInverse _ _ (fun x ↦ x / (1 - |↑x|)) _
[GOAL]
case refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
⊢ k → ↑(Ioo (-1) 1)
[PROOFSTEP]
refine' codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 _
[GOAL]
case refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
x : k
⊢ |(fun x => x / (1 + |x|)) x| < 1
[PROOFSTEP]
have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)
[GOAL]
case refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
x : k
H : 0 < 1 + |x|
⊢ |(fun x => x / (1 + |x|)) x| < 1
[PROOFSTEP]
calc
  |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
  _ < 1 := (div_lt_one H).2 (lt_one_add _)
[GOAL]
k : Type u_1
inst✝ : LinearOrderedField k
x : k
H : 0 < 1 + |x|
⊢ |x / (1 + |x|)| = |x| / (1 + |x|)
[PROOFSTEP]
rw [abs_div, abs_of_pos H]
[GOAL]
case refine'_2
k : Type u_1
inst✝ : LinearOrderedField k
⊢ StrictMono
    (codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
      (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1))
[PROOFSTEP]
refine' (strictMono_of_odd_strictMonoOn_nonneg _ _).codRestrict _
[GOAL]
case refine'_2.refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
⊢ ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))
[PROOFSTEP]
intro x
[GOAL]
case refine'_2.refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
x : k
⊢ -x / (1 + |(-x)|) = -(x / (1 + |x|))
[PROOFSTEP]
simp only [abs_neg, neg_div]
[GOAL]
case refine'_2.refine'_2
k : Type u_1
inst✝ : LinearOrderedField k
⊢ StrictMonoOn (fun x => x / (1 + |x|)) (Ici 0)
[PROOFSTEP]
rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy
[GOAL]
case refine'_2.refine'_2
k : Type u_1
inst✝ : LinearOrderedField k
x : k
hx : 0 ≤ x
y : k
hy : 0 ≤ y
hxy : x < y
⊢ (fun x => x / (1 + |x|)) x < (fun x => x / (1 + |x|)) y
[PROOFSTEP]
simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff, hx.trans_lt (lt_one_add _), hy.trans_lt (lt_one_add _), *]
[GOAL]
case refine'_3
k : Type u_1
inst✝ : LinearOrderedField k
⊢ Function.RightInverse (fun x => ↑x / (1 - |↑x|))
    (codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
      (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1))
[PROOFSTEP]
refine' fun x ↦ Subtype.ext _
[GOAL]
case refine'_3
k : Type u_1
inst✝ : LinearOrderedField k
x : ↑(Ioo (-1) 1)
⊢ ↑(codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
        (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1)
        ((fun x => ↑x / (1 - |↑x|)) x)) =
    ↑x
[PROOFSTEP]
have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)
[GOAL]
case refine'_3
k : Type u_1
inst✝ : LinearOrderedField k
x : ↑(Ioo (-1) 1)
this : 0 < 1 - |↑x|
⊢ ↑(codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
        (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1)
        ((fun x => ↑x / (1 - |↑x|)) x)) =
    ↑x
[PROOFSTEP]
field_simp [abs_div, this.ne', abs_of_pos this]


[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a b c : α
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
[PROOFSTEP]
rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a✝ b c a : α
⊢ ⋃ (b : α), Icc a b = Ici a
[PROOFSTEP]
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a✝ b c a : α
⊢ ⋃ (b : α), Ioc a b = Ioi a
[PROOFSTEP]
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a b✝ c b : α
⊢ ⋃ (a : α), Icc a b = Iic b
[PROOFSTEP]
simp only [← Ici_inter_Iic, ← iUnion_inter, iUnion_Ici, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a b✝ c b : α
⊢ ⋃ (a : α), Ico a b = Iio b
[PROOFSTEP]
simp only [← Ici_inter_Iio, ← iUnion_inter, iUnion_Ici, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a✝ b c : α
inst✝ : NoMaxOrder α
a : α
⊢ ⋃ (b : α), Ico a b = Ici a
[PROOFSTEP]
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a✝ b c : α
inst✝ : NoMaxOrder α
a : α
⊢ ⋃ (b : α), Ioo a b = Ioi a
[PROOFSTEP]
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a b✝ c : α
inst✝ : NoMinOrder α
b : α
⊢ ⋃ (a : α), Ioc a b = Iic b
[PROOFSTEP]
simp only [← Ioi_inter_Iic, ← iUnion_inter, iUnion_Ioi, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a b✝ c : α
inst✝ : NoMinOrder α
b : α
⊢ ⋃ (a : α), Ioo a b = Iio b
[PROOFSTEP]
simp only [← Ioi_inter_Iio, ← iUnion_inter, iUnion_Ioi, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
[PROOFSTEP]
simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, inf_eq_min, sup_eq_max, not_lt]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
[PROOFSTEP]
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (Ico (↑toDual a₂) (↑toDual a₁)) (Ico (↑toDual b₂) (↑toDual b₁)) ↔
    min (↑toDual a₁) (↑toDual b₁) ≤ max (↑toDual a₂) (↑toDual b₂)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
[PROOFSTEP]
simpa only [dual_Ico] using h
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
[PROOFSTEP]
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
[PROOFSTEP]
apply le_antisymm h2.1
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁
[PROOFSTEP]
exact h.elim (fun h => absurd hx (not_lt_of_le h)) id
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
f : ι → α
a : α
⊢ ⋃ (i : ι), Ico (f i) a = Iio a ↔ ∀ (x : α), x < a → ∃ i, f i ≤ x
[PROOFSTEP]
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
f : ι → α
a : α
⊢ ⋃ (i : ι), Ioc a (f i) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ (i : ι) (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ (x : α), x < a → ∃ i hi, f i hi ≤ x
[PROOFSTEP]
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ (i : ι) (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ (x : α), a < x → ∃ i hi, x ≤ f i hi
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
⊢ ⋃ (x : α) (_ : x ∈ s), Ioi x = Ioi a
[PROOFSTEP]
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
[GOAL]
case refine'_1
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a
[PROOFSTEP]
exact Ioi_subset_Ioi (h.1 hx)
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ioi i
[PROOFSTEP]
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ioi i
[PROOFSTEP]
exact mem_biUnion hys hyx
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
⊢ ⋃ (x : α) (_ : x ∈ s), Ici x = Ioi a
[PROOFSTEP]
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
[GOAL]
case refine'_1
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ioi a
[PROOFSTEP]
exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_not_mem) hx)
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ici i
[PROOFSTEP]
rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ici i
[PROOFSTEP]
apply mem_iUnion₂.mpr
[GOAL]
case refine'_2.intro.intro.intro
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ ∃ i j, x ∈ Ici i
[PROOFSTEP]
refine' ⟨y, hys, hyx.le⟩
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
⊢ ⋃ (x : α) (_ : x ∈ s), Ici x = Ici a
[PROOFSTEP]
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
[GOAL]
case refine'_1
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a
[PROOFSTEP]
exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ici i
[PROOFSTEP]
apply mem_iUnion₂.mpr
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ ∃ i j, x ∈ Ici i
[PROOFSTEP]
refine' ⟨a, a_mem, hx⟩
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : LinearOrder α
s : Set α
a : α
f✝ : ι → α
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
no_least_elem : ¬⨅ (i : ι), f i ∈ range f
⊢ ⋃ (i : ι), Ici (f i) = Ioi (⨅ (i : ι), f i)
[PROOFSTEP]
simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range, iUnion_exists, iUnion_iUnion_eq']
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : LinearOrder α
s : Set α
a : α
f✝ : ι → α
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
has_least_elem : ⨅ (i : ι), f i ∈ range f
⊢ ⋃ (i : ι), Ici (f i) = Ici (⨅ (i : ι), f i)
[PROOFSTEP]
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range, iUnion_exists, iUnion_iUnion_eq']