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

Proof state:
case h.e'_3.h.e'_4.hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ IsIso ⇑(ConcreteCategory.hom (D.t i j))

Tactic:
apply (forget TopCat).map_isIso

Result:
no goals

Proof state:
case h.e'_3
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f j i)) ''
      (⇑(ConcreteCategory.hom (D.t i j)) '' (⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U)) =
    ⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U)

Tactic:
congr! 1

Result:
case h.e'_3.h.e'_4
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j)) '' (⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U) =
    ⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U

Proof state:
case h.e'_3.h.e'_4
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j)) '' (⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U) =
    ⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U

Tactic:
rw [← Set.eq_preimage_iff_image_eq, Set.preimage_preimage]

Result:
case h.e'_3.h.e'_4
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    (fun x =>
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

case h.e'_3.h.e'_4.hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))

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.t i j ≫ D.f j i)) '' (⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U)

Tactic:
convert D.preimage_image_eq_image i j U using 1

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

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

Tactic:
rw [𝖣.t_inv_assoc]

Result:
no goals

Proof state:
case h.e'_3.h.e'_4
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    (fun x =>
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

Tactic:
change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _

Result:
case h.e'_3.h.e'_4
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U = ⇑(ConcreteCategory.hom (D.t i j ≫ D.t j i ≫ D.f i j)) ⁻¹' U

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

Tactic:
rw [coe_comp, coe_comp, Set.image_comp]

Result:
case h.e'_3
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f j i)) ''
      (⇑(ConcreteCategory.hom (D.t i j)) '' (⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U)) =
    ⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U)

Proof state:
case h.e'_3.h.e'_4.hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))

Tactic:
rw [← isIso_iff_bijective]

Result:
case h.e'_3.h.e'_4.hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ IsIso ⇑(ConcreteCategory.hom (D.t i j))