-- Mathlib/AlgebraicGeometry/Limits.lean
@[reassoc (attr := simp)]
lemma ι_sigmaIsoGlued_inv (i) : (disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv = Sigma.ι f i

Proof state:
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ (disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv = Sigma.ι f i

Tactic:
apply Scheme.forgetToLocallyRingedSpace.map_injective

Result:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ Scheme.forgetToLocallyRingedSpace.map ((disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv) =
    Scheme.forgetToLocallyRingedSpace.map (Sigma.ι f i)

Proof state:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ Scheme.Hom.toLRSHom
      ((disjointGlueData f).ι i ≫
        Scheme.fullyFaithfulForgetToLocallyRingedSpace.preimage
          (((disjointGlueData f).isoLocallyRingedSpace.hom ≫
              (colimit.isoColimitCocone
                  { cocone := toLocallyRingedSpaceCoproductCofan f,
                    isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv) ≫
            sigmaComparison Scheme.forgetToLocallyRingedSpace f)) =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Tactic:
simp only [Category.assoc]

Result:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ Scheme.Hom.toLRSHom
      ((disjointGlueData f).ι i ≫
        Scheme.fullyFaithfulForgetToLocallyRingedSpace.preimage
          ((disjointGlueData f).isoLocallyRingedSpace.hom ≫
            (colimit.isoColimitCocone
                  { cocone := toLocallyRingedSpaceCoproductCofan f,
                    isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv ≫
              sigmaComparison Scheme.forgetToLocallyRingedSpace f)) =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Proof state:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ ((disjointGlueData f).mapGlueData Scheme.forgetToLocallyRingedSpace).ι i ≫
      (colimit.isoColimitCocone
            { cocone := toLocallyRingedSpaceCoproductCofan f,
              isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv ≫
        sigmaComparison Scheme.forgetToLocallyRingedSpace f =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc
  ⟨_, toLocallyRingedSpaceCoproductCofanIsColimit f⟩ ⟨i⟩ _).trans ?_

Result:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ colimit.ι (Discrete.functor (Scheme.toLocallyRingedSpace ∘ f)) { as := i } ≫
      sigmaComparison Scheme.forgetToLocallyRingedSpace f =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Proof state:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ Scheme.Hom.toLRSHom
      ((disjointGlueData f).ι i ≫
        Scheme.fullyFaithfulForgetToLocallyRingedSpace.preimage
          ((disjointGlueData f).isoLocallyRingedSpace.hom ≫
            (colimit.isoColimitCocone
                  { cocone := toLocallyRingedSpaceCoproductCofan f,
                    isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv ≫
              sigmaComparison Scheme.forgetToLocallyRingedSpace f)) =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Tactic:
refine ((disjointGlueData f).ι_gluedIso_hom_assoc Scheme.forgetToLocallyRingedSpace i _).trans ?_

Result:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ ((disjointGlueData f).mapGlueData Scheme.forgetToLocallyRingedSpace).ι i ≫
      (colimit.isoColimitCocone
            { cocone := toLocallyRingedSpaceCoproductCofan f,
              isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv ≫
        sigmaComparison Scheme.forgetToLocallyRingedSpace f =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Proof state:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ colimit.ι (Discrete.functor (Scheme.toLocallyRingedSpace ∘ f)) { as := i } ≫
      sigmaComparison Scheme.forgetToLocallyRingedSpace f =
    Scheme.Hom.toLRSHom (Sigma.ι f i)

Tactic:
exact ι_comp_sigmaComparison Scheme.forgetToLocallyRingedSpace _ _

Result:
no goals

Proof state:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ Scheme.forgetToLocallyRingedSpace.map ((disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv) =
    Scheme.forgetToLocallyRingedSpace.map (Sigma.ι f i)

Tactic:
dsimp [sigmaIsoGlued]

Result:
case a
ι : Type u
f : ι → Scheme
i : (disjointGlueData f).J
⊢ Scheme.Hom.toLRSHom
      ((disjointGlueData f).ι i ≫
        Scheme.fullyFaithfulForgetToLocallyRingedSpace.preimage
          (((disjointGlueData f).isoLocallyRingedSpace.hom ≫
              (colimit.isoColimitCocone
                  { cocone := toLocallyRingedSpaceCoproductCofan f,
                    isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv) ≫
            sigmaComparison Scheme.forgetToLocallyRingedSpace f)) =
    Scheme.Hom.toLRSHom (Sigma.ι f i)