-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem ι_eq_iff (i j : D.J) (x : (D.U i).carrier) (y : (D.U j).carrier) :
    (𝖣.ι i).base x = (𝖣.ι j).base y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Proof state:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j ≫
            D.isoCarrier.inv))
        y ↔
    (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j))
          y)

Tactic:
rfl

Result:
no goals

Proof state:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom (D.ι i).base) x = (ConcreteCategory.hom (D.ι j).base) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
          y)

Tactic:
simp_rw [← D.ι_isoCarrier_inv]

Result:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j ≫
            D.isoCarrier.inv))
        y ↔
    (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j))
          y)

Proof state:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom (D.ι i).base) x = (ConcreteCategory.hom (D.ι j).base) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i))
        x =
      (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
        y

Tactic:
rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff, ← ConcreteCategory.comp_apply]

Result:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom (D.ι i).base) x = (ConcreteCategory.hom (D.ι j).base) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
          y)

D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ Mono D.isoCarrier.inv

Proof state:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom (D.ι i).base) x = (ConcreteCategory.hom (D.ι j).base) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
refine Iff.trans ?_
  (TopCat.GlueData.ι_eq_iff_rel
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
    i j x y)

Result:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ (ConcreteCategory.hom (D.ι i).base) x = (ConcreteCategory.hom (D.ι j).base) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i))
        x =
      (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
        y

Proof state:
D : GlueData
i j : D.J
x : ↑↑(D.U i).toPresheafedSpace
y : ↑↑(D.U j).toPresheafedSpace
⊢ Mono D.isoCarrier.inv

Tactic:
infer_instance

Result:
no goals