awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
this : IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
x : ↥X
⊢ x ∈ (↑⊤ : Set ↥X) ↔ x ∈ (↑(⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ : Opens ↥X }) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingPair
rw :
  Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
⊢ Mono ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))

Tactic:
rw [mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingPair
left :
  Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.left))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
right :
  Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.right)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.right)))
⊢ Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))

Tactic:
cases i
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.left))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))

Tactic:
simpa using f.isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.right)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.right)))

Tactic:
simpa using g.isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i j : WalkingSpan
t : i ⟶ j
id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))
init : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))
init₁ : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))
⊢ IsOpenImmersion ((span f g).map t)

Tactic:
obtain (a | (a | a)) := t
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingSpan
id : IsOpenImmersion (𝟙 ((span f g).obj i))
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))

Tactic:
simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Limits.WidePushoutShape.hom_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingSpan
⊢ IsOpenImmersion (𝟙 ((span f g).obj i))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ HasPushout f g

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
⊢ ∀ (i : I), IsIso (α.app i)

Tactic:
have (i : _) : IsIso (α.app i) := IsAffine.affine
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this : ∀ (i : I), IsIso (α.app i)
⊢ IsIso α

Tactic:
have : IsIso α := NatIso.isIso_of_isIso_app α
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this : IsIso α
have : ∀ (this : c.pt ≅ Spec Γ(c.pt, ⊤)), IsAffine.{u} c.pt
⊢ IsAffine.{u} c.pt

Tactic:
have : c.pt ≅ Spec Γ(c.pt, ⊤) := hc.conePointUniqueUpToIso ((IsLimit.postcomposeHomEquiv
    (asIso α).symm _).symm (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc))
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this_2 : IsIso α
this : c.pt ≅ Spec Γ(c.pt, ⊤)
⊢ IsAffine.{u} c.pt

Tactic:
.of_isIso this.hom

Premises used: AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this_2 : IsIso α
this : c.pt ≅ Spec Γ(c.pt, ⊤)
⊢ IsAffine.{u} c.pt

Tactic:
exact .of_isIso this.hom
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
S : Scheme
J : Type u_1
inst : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (Over S)
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (Over.Hom.left (F.map f))
inst_2 : (F ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, v_1} J
inst_4 : Small.{u, u_1} J
⊢ HasColimit F

Tactic:
have {i j} (f : i ⟶ j) : IsOpenImmersion ((F ⋙ Over.forget S).map f) :=
    inferInstanceAs <| IsOpenImmersion (F.map f).left
  have : ((F ⋙ Over.forget S) ⋙ Scheme.forget).IsLocallyDirected := ‹_›
  hasColimit_of_created _ (Over.forget S)

Premises used: _private.0.AlgebraicGeometry.instHasColimitOverScheme._proof_1, CategoryTheory.Over.forget, CategoryTheory.hasColimit_of_created
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingPair
rw :
  Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init i))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
⊢ Mono
    ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))

Tactic:
rw [mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingPair
left :
  Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init WalkingPair.left))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
right :
  Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.right)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init WalkingPair.right))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj
            (some WalkingPair.right)))
⊢ Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init i))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))

Tactic:
cases i
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init WalkingPair.left))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.left)))

Tactic:
simpa using f.left.isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.CommaMorphism.left, Topology.IsEmbedding.injective, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ Function.Injective (α :=
    (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
    (β :=
    (fun (X : Type u) ↦ X)
      ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some WalkingPair.right)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
            (WidePushoutShape.Hom.init WalkingPair.right))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj
            (some WalkingPair.right)))

Tactic:
simpa using g.left.isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.CommaMorphism.left, Topology.IsEmbedding.injective, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i j : WalkingSpan
t : i ⟶ j
id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
init :
  IsOpenImmersion
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
init₁ :
  IsOpenImmersion
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ IsOpenImmersion ((span f g).map t).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
obtain (a | (a | a)) := t
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingSpan
id : IsOpenImmersion (MorphismProperty.Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤) (𝟙 ((span f g).obj i))).left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Limits.WidePushoutShape.hom_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingSpan
⊢ IsOpenImmersion (MorphismProperty.Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤) (𝟙 ((span f g).obj i))).left

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ IsOpenImmersion
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ IsOpenImmersion
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
i j : J
f : i ⟶ j
⊢ IsOpenImmersion (((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S).map f)

Tactic:
inferInstanceAs <| IsOpenImmersion (F.map f).left

Premises used: _private.0.AlgebraicGeometry.instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget._proof_1
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
⊢ HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)

Tactic:
have : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S) :=
    hasColimit_of_created _ (Over.forget S)
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
refine : P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom
⊢ CreatesColimit F (MorphismProperty.Over.forget P ⊤ S)

Tactic:
refine createsColimitOfFullyFaithfulOfIso
      { toComma := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
        prop := ?_ } (Iso.refl _)

Premises used: CategoryTheory.createsColimitOfFullyFaithfulOfIso
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
let : P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom

Tactic:
let e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
      colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
    preservesColimitIso (Over.forget S) _
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : Scheme.OpenCover.{u_1, u} (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion)
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
rw : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) 𝒰]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover