mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i = pullback.fst (D.f k j) (D.f k i) ≫ D.f k j

Tactic:
]

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i = pullback.fst (D.f k j) (D.f k i) ≫ D.f k j
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ Arrow.mk (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))

Tactic:
refine Arrow.isoMk ?_ ?_ ?_

Goal state after:
case refine_1
R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ (Arrow.mk (Spec.map f ∣_ basicOpen r)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).left

case refine_2
R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ (Arrow.mk (Spec.map f ∣_ basicOpen r)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).right

case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ Iso.hom ?refine_1 ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (Spec.map f ∣_ basicOpen r)).hom ≫ Iso.hom ?refine_2
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : Category.{w', w} J
inst✝¹ : Small.{v, w} J
F : J ⥤ SheafedSpace C
inst✝ : HasLimits C
X Y : SheafedSpace C
f g : X ⟶ Y
⊢ Epi (coequalizer.π ((forget C).map f) ((forget C).map g) ≫ (PreservesCoequalizer.iso (forget C) f g).hom)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : Category.{w', w} J
inst✝¹ : Small.{v, w} J
F : J ⥤ SheafedSpace C
inst✝ : HasLimits C
X Y : SheafedSpace C
f g : X ⟶ Y
⊢ Epi (coequalizer.π ((forget C).map f) ((forget C).map g) ≫ (PreservesCoequalizer.iso (forget C) f g).hom)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
hcomp :
  CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) =
    f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r)))
⊢ (((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
        (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) =
    ((Arrow.mk (Spec.map f ∣_ basicOpen r)).hom ≫ (basicOpenIsoSpecAway r).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))

Tactic:
]

Goal state after:
case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
hcomp :
  CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) =
    f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r)))
⊢ (((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
        (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) =
    ((Arrow.mk (Spec.map f ∣_ basicOpen r)).hom ≫ (basicOpenIsoSpecAway r).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom
        (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom)
      ((ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one))))
        x) =
    (ConcreteCategory.hom
        (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      y

Tactic:
]

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom
        (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom)
      ((ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one))))
        x) =
    (ConcreteCategory.hom
        (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ∀ i ∈ s, X.basicOpen i ≤ U

Tactic:
]

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ∀ i ∈ s, X.basicOpen i ≤ U
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
      inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y) =
    PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
        inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y)))

Tactic:
]

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
      inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y) =
    PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
        inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U)))

Tactic:
]

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U)))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
          (op U) ≫
        (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U)))).hom ≫
          limit.π
            (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U))))
            (op WalkingParallelPair.one)))

Tactic:
]

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
          (op U) ≫
        (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U)))).hom ≫
          limit.π
            (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U))))
            (op WalkingParallelPair.one)))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
]

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ i ∈ s, X.basicOpen i)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨i, x⟩) ⟨j, y⟩

Tactic:
]

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨i, x⟩) ⟨j, y⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨i, x⟩)
    ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨j, y⟩)

Tactic:
]

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨i, x⟩)
    ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨j, y⟩)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ ↑V ≤ ⨆ f_1, X.basicOpen ↑f_1

Tactic:
]

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ ↑V ≤ ⨆ f_1, X.basicOpen ↑f_1
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ Relation.EqvGen (InvImage D.Rel ⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((sigmaIsoSigma D.U).inv.hom' ⟨i, x⟩)
    ((sigmaIsoSigma D.U).inv.hom' ⟨j, y⟩)

Tactic:
]

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ Relation.EqvGen (InvImage D.Rel ⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((sigmaIsoSigma D.U).inv.hom' ⟨i, x⟩)
    ((sigmaIsoSigma D.U).inv.hom' ⟨j, y⟩)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ ∃ i, x ∈ X.basicOpen (f i)

Tactic:
]

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ ∃ i, x ∈ X.basicOpen (f i)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))

Tactic:
]

Goal state after:
case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (f.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))

Tactic:
]

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (f.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι

Tactic:
]

Goal state after:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)

Tactic:
]

Goal state after:
case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)