-- Mathlib/Topology/Gluing.lean
theorem preimage_image_eq_image (i j : D.J) (U : Set (𝖣.U i)) :
    𝖣.ι j ⁻¹' (𝖣.ι i '' U) = D.f _ _ '' ((D.t j i ≫ D.f _ _) ⁻¹' U)

Proof state:
case a
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ⊆
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i))

Tactic:
exact Set.preimage_mono (Set.image_subset_range _ _)

Result:
no goals

Proof state:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
ext x

Result:
case h
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
⊢ x ∈
      ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹'
        (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) ↔
    x ∈ ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Proof state:
case a
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ⊆
    Set.range ⇑(ConcreteCategory.hom (D.f j i))

Tactic:
rw [← D.preimage_range i j]

Result:
case a
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ⊆
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i))

Proof state:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ∩
      Set.range ⇑(ConcreteCategory.hom (D.f j i)) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)

Tactic:
apply Set.inter_eq_self_of_subset_left

Result:
case a
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ⊆
    Set.range ⇑(ConcreteCategory.hom (D.f j i))

Proof state:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) =
    ⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U)

Tactic:
have : D.f _ _ ⁻¹' (𝖣.ι j ⁻¹' (𝖣.ι i '' U)) = (D.t j i ≫ D.f _ _) ⁻¹' U := by
  ext x
  conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]
  simp

Result:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) =
    ⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U)

Proof state:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ∩
      Set.range ⇑(ConcreteCategory.hom (D.f j i))

Tactic:
symm

Result:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ∩
      Set.range ⇑(ConcreteCategory.hom (D.f j i)) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)

Proof state:
case h
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
⊢ x ∈
      ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹'
        (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) ↔
    x ∈
      ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹'
        (⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U))

Tactic:
simp

Result:
no goals

Proof state:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) =
    ⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U)

Tactic:
rw [← this, Set.image_preimage_eq_inter_range]

Result:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U) ∩
      Set.range ⇑(ConcreteCategory.hom (D.f j i))

Proof state:
case h
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
⊢ x ∈
      ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹'
        (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) ↔
    x ∈ ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]

Result:
case h
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
⊢ x ∈
      ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹'
        (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U)) ↔
    x ∈
      ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹'
        (⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' U))