-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem ι_isoCarrier_inv (i : D.J) :
    (D_).ι i ≫ D.isoCarrier.inv = (D.ι i).base

Proof state:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base

Tactic:
rw [D.ι_isoLocallyRingedSpace_inv i]

Result:
no goals

Proof state:
D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ D.isoCarrier.inv =
    (D.ι i).base

Tactic:
delta isoCarrier

Result:
D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
      ((PresheafedSpace.forget CommRingCat).mapIso
            (SheafedSpace.forgetToPresheafedSpace.mapIso
                (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                  D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
              D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace) ≪≫
          D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)).inv =
    (D.ι i).base

Proof state:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i ≫
        D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
          (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).base =
    (D.ι i).base

Tactic:
erw [← Category.assoc, D.toLocallyRingedSpaceGlueData.ι_isoSheafedSpace_inv i]

Result:
D : GlueData
i : D.J
⊢ ((D.toLocallyRingedSpaceGlueData.ι i).toHom ≫
        (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).base =
    (D.ι i).base

Proof state:
D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
      ((PresheafedSpace.forget CommRingCat).mapIso
            (SheafedSpace.forgetToPresheafedSpace.mapIso
                (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                  D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
              D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace) ≪≫
          D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)).inv =
    (D.ι i).base

Tactic:
rw [Iso.trans_inv, GlueData.ι_gluedIso_inv_assoc, Functor.mapIso_inv, Iso.trans_inv,
  Functor.mapIso_inv, Iso.trans_inv, SheafedSpace.forgetToPresheafedSpace_map, forget_map,
  forget_map, ← PresheafedSpace.comp_base, ← Category.assoc,
  D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι_isoPresheafedSpace_inv i]

Result:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i ≫
        D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
          (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).base =
    (D.ι i).base

Proof state:
D : GlueData
i : D.J
⊢ ((D.toLocallyRingedSpaceGlueData.ι i).toHom ≫
        (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).base =
    (D.ι i).base

Tactic:
change (_ ≫ D.isoLocallyRingedSpace.inv).base = _

Result:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base