α : 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))
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x y z : α
s : Set α
⊢ ordConnectedSection (↑ofDual ⁻¹' s) = ↑ofDual ⁻¹' ordConnectedSection s
simp_rw [ordConnectedSection, ordConnectedProj]
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))
α : 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))
ext x
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
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))
simp [dual_ordConnectedComponent]
no goals
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
tauto