Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x✝ :
  (MultispanShape.prod
      (Cover.ulift
              (Opens.iSupOpenCover fun i_1 ↦
                Hom.opensRange (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk : k ∈ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
pf✝⁷ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝⁶ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝⁵ : IsOpenImmersion (F.map h.choose.snd.1)
pf✝⁴ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝³ : ∀ (x : ↥↑(⨆ i_1, Hom.opensRange (F.map i_1.snd.1))), IsOpenImmersion (F.map ⋯.choose.snd.1)
pf✝² :
  ∀ (x : ↥↑(⨆ i_1, Hom.opensRange (F.map i_1.snd.1))),
    Hom.opensRange (F.map ⋯.choose.snd.1) ≤ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
pf✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝ : Hom.opensRange (F.map h.choose.snd.1) ≤ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [homOfLE_tAux F ↓i ↓j h.choose.2.1 h.choose.2.2, Iso.hom_inv_id_assoc]

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x✝ :
  (MultispanShape.prod
      (Cover.ulift
              (Opens.iSupOpenCover fun i_1 ↦
                Hom.opensRange (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk : k ∈ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
pf✝⁷ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝⁶ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝⁵ : IsOpenImmersion (F.map h.choose.snd.1)
pf✝⁴ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝³ : ∀ (x : ↥↑(⨆ i_1, Hom.opensRange (F.map i_1.snd.1))), IsOpenImmersion (F.map ⋯.choose.snd.1)
pf✝² :
  ∀ (x : ↥↑(⨆ i_1, Hom.opensRange (F.map i_1.snd.1))),
    Hom.opensRange (F.map ⋯.choose.snd.1) ≤ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
pf✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝ : Hom.opensRange (F.map h.choose.snd.1) ≤ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)