-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem isOpen_iff (U : Set D.glued.carrier) : IsOpen U ↔ ∀ i, IsOpen ((D.ι i).base ⁻¹' U)

Proof state:
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i).base) ⁻¹' U)

Tactic:
rw [← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage, TopCat.GlueData.isOpen_iff]

Result:
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
⊢ (∀ (i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
      IsOpen
        (⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
          (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U))) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i).base) ⁻¹' U)

Proof state:
case h
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
⊢ ∀ (a : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
    IsOpen
        (⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι a)) ⁻¹'
          (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U)) ↔
      IsOpen (⇑(ConcreteCategory.hom (D.ι a).base) ⁻¹' U)

Tactic:
intro i

Result:
case h
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U)) ↔
    IsOpen (⇑(ConcreteCategory.hom (D.ι i).base) ⁻¹' U)

Proof state:
case h
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U)) ↔
    IsOpen (⇑(ConcreteCategory.hom (D.ι i).base) ⁻¹' U)

Tactic:
rw [← Set.preimage_comp, ← ι_isoCarrier_inv]

Result:
case h
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ∘
          ⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        U) ↔
    IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
              D.isoCarrier.inv)) ⁻¹'
        U)

Proof state:
case h
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ∘
          ⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        U) ↔
    IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
              D.isoCarrier.inv)) ⁻¹'
        U)

Tactic:
rfl

Result:
no goals

Proof state:
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
⊢ (∀ (i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
      IsOpen
        (⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
          (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U))) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i).base) ⁻¹' U)

Tactic:
apply forall_congr'

Result:
case h
D : GlueData
U : Set ↑↑D.glued.toPresheafedSpace
⊢ ∀ (a : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
    IsOpen
        (⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι a)) ⁻¹'
          (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U)) ↔
      IsOpen (⇑(ConcreteCategory.hom (D.ι a).base) ⁻¹' U)