mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case neg
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
h✝ : ¬i = j
⊢ Mono (eqToHom ⋯ ≫ D.f i j h✝)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i : D.J
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : i = k
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
hij : ¬i = j
⊢ IsIso (pullback.snd (D.f' j i) (D.f' j i))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

Goal state after:
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 (inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y))).comp
      ((CommRingCat.Hom.hom ((s.ι.app i).stalkMap y)).comp (CommRingCat.Hom.hom (eqToHom ⋯))))

Tactic:
infer_instance

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

Goal state before:
pp: X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f.hom x))

Tactic:
infer_instance

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
y : ↑↑Y.toPresheafedSpace
h : ↑(s.pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.desc (Hom.toShHom s.π) e).hom.base)
        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))) →+*
  ↑((coequalizerCofork f g).pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y)) :=
  CommRingCat.Hom.hom
    (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))
⊢ IsLocalHom (CommRingCat.Hom.hom (Hom.stalkMap s.π y))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case right
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ LocallyRingedSpace.IsOpenImmersion (Hom.toLRSHom ((D.U i).affineCover.f j) ≫ D.toLocallyRingedSpaceGlueData.ι i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ D.glued.toLocallyRingedSpace ≅ D.toLocallyRingedSpaceGlueData.glued

Tactic:
exact Scheme.GlueData.isoLocallyRingedSpace _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl

Tactic:
by
  dsimp [pushoutZeroZeroIso]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr

Tactic:
by
  dsimp [pushoutZeroZeroIso]
  simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ Epi (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ Mono D.isoCarrier.inv

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
    ((X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)
⊢ IsIso (((X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono (D.gluedIso (forget C)).inv

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ⊢ IsEmpty PEmpty.{u + 1}

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: A : Scheme
f : A ⟶ ⊥_ Scheme
⊢ IsIso f

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : IsEmpty ↥X
⊢ Subsingleton ↑Γ(X, ⊥)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
X : Scheme
inst✝ : Subsingleton ↥X
h : IsEmpty ↥X
⊢ IsAffine X

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case inst
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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
⊢ IsOpenImmersion ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.left } ≫ (coprodIsoSigma X Y).inv)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.right } ≫ (coprodIsoSigma X Y).inv)

Tactic:
infer_instance

Goal state after:
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
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
⊢ IsOpenImmersion (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion f

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion g

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this✝¹ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
this✝ : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this✝¹ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
this✝ : Algebra (R × S) S := (RingHom.snd R S).toAlgebra
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S)))
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsIso
    (TopCat.isoOfHomeo
        (PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
this :
  coprodComparison Scheme.Spec (op R) (op S) ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprodSpec ↑R ↑S
⊢ IsIso
    (coprodSpec ↑R ↑S ≫
      inv
        (Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv)))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
this :
  sigmaSpec R =
    (colimit.isoColimitCocone
        {
          cocone :=
            (Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)).symm
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }).hom
⊢ IsIso
    (colimit.isoColimitCocone
        {
          cocone :=
            (Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)).symm
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }).hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι✝ : Type u
f : ι✝ → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite σ
inst✝ : ∀ (i : σ), IsAffine (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
i : ι
⊢ IsAffine (g (e.symm i))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this✝ : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
this : ∀ (i : ι), IsAffine ↑(U i)
⊢ IsAffine (∐ fun i ↦ ↑(U i))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case id
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingSpan
⊢ IsOpenImmersion (𝟙 ((span f g).obj i))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inj
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
this : (D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv = (D.ι i).base
⊢ Mono (D.gluedIso (forget C)).inv

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
this :
  pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry (𝒰.f i ≫ f) g).hom ≫
      (pullbackLeftPullbackSndIso g f (𝒰.f i)).inv ≫
        pullback.fst (pullback.snd g f) (𝒰.f i) ≫ (pullbackSymmetry g f).hom
⊢ IsOpenImmersion
    ((pullbackSymmetry (𝒰.f i ≫ f) g).hom ≫
      (pullbackLeftPullbackSndIso g f (𝒰.f i)).inv ≫
        pullback.fst (pullback.snd g f) (𝒰.f i) ≫ (pullbackSymmetry g f).hom)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ Epi (D.f i i).base

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
⊢ ∀ {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'

Tactic:
g'

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
⊢ IsPullback g' f' f g → P g → P g'
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ (targetAffineLocally Q).RespectsIso

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
this : IsIso (D.t i j).c
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ IsIso
    ((colimitPresheafObjIsoComponentwiseLimit D.diagram.multispan (⋯.functor.obj U)).hom ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)) (op (WalkingMultispan.right i)))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
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
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ (colimit.ι F ↓i) xi = (colimit.ι F ↓j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
rw [← ((isColimit F).coconePointUniqueUpToIso
    (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff]

Goal state after:
case mp
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
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓i) xi) =
      ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓j) xj) →
    ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).fst = s.fst

Tactic:
apply IsOpenImmersion.lift_fac

Goal state after:
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
x : ↥(Limits.colimit F)
⊢ ∃ i xi, (colimit.ι F i) xi = x

Tactic:
obtain ⟨i, xi, h⟩ :=
    (IsLocallyDirected.glueData F).ι_jointly_surjective
      (((IsLocallyDirected.isColimit F).coconePointUniqueUpToIso (colimit.isColimit _)).inv x)

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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
⊢ ∃ i xi, (colimit.ι F i) xi = x
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
⊢ IsAffine
    (pullback ((𝒰' i.fst).f i.snd.1 ≫ pullback.snd f (𝒰.f i.fst)) ((𝒰' i.fst).f i.snd.2 ≫ pullback.snd f (𝒰.f i.fst)))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
this : PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i)
⊢ PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i ≫ D.isoPresheafedSpace.inv)

Tactic:
infer_instance

Goal state after: