-- Mathlib/Topology/Connected/Clopen.lean
/-- If `u v : Set X` and `u ⊆ v` is clopen in `v`, then `u` is the union of the connected
components of `v` in `X` which intersect `u`. -/
lemma IsClopen.biUnion_connectedComponentIn {X : Type*} [TopologicalSpace X] {u v : Set X}
    (hu : IsClopen (v ↓∩ u)) (huv₁ : u ⊆ v) :
    u = ⋃ x ∈ u, connectedComponentIn v x

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
nth_rw 1 [this]

Result:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩ = ⋃ x ∈ u, connectedComponentIn v x

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩ = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
congr! 2 with x hx

Result:
case h.e'_3.h
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
x : X
⊢ ⋃ (x_1 : x ∈ v), ⋃ (_ : x ∈ u), Subtype.val '' connectedComponent ⟨x, ⋯⟩ = ⋃ (_ : x ∈ u), connectedComponentIn v x

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : Subtype.val '' v ↓∩ u = Subtype.val '' ⋃ x ∈ v ↓∩ u, connectedComponent x
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
  inter_eq_right.mpr huv₁] at this

Result:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
have := congr(((↑) : Set v → Set X) $(hu.biUnion_connectedComponent_eq.symm))

Result:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : Subtype.val '' v ↓∩ u = Subtype.val '' ⋃ x ∈ v ↓∩ u, connectedComponent x
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Proof state:
case h.e'_3.h
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
x : X
⊢ ⋃ (_ : x ∈ v), ⋃ (_ : x ∈ u), connectedComponentIn v x = ⋃ (_ : x ∈ u), connectedComponentIn v x

Tactic:
exact le_antisymm (iUnion_subset fun _ ↦ le_rfl) <|
  iUnion_subset fun hx ↦ subset_iUnion₂_of_subset (huv₁ hx) hx le_rfl

Result:
no goals

Proof state:
case h.e'_3.h
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
x : X
⊢ ⋃ (x_1 : x ∈ v), ⋃ (_ : x ∈ u), Subtype.val '' connectedComponent ⟨x, ⋯⟩ = ⋃ (_ : x ∈ u), connectedComponentIn v x

Tactic:
simp only [← connectedComponentIn_eq_image]

Result:
case h.e'_3.h
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
x : X
⊢ ⋃ (_ : x ∈ v), ⋃ (_ : x ∈ u), connectedComponentIn v x = ⋃ (_ : x ∈ u), connectedComponentIn v x