mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
·

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g
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 k : D.J
U : Opens ↑↑(D.U i)
⊢ D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ op
      ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
        (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U)))))) =
    (Opens.map (D.f j k).base).op.obj (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U)))

Tactic:
· delta opensImagePreimageMap
    simp_rw [Category.assoc]
    rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]
    · erw [← (D.V (j, k)).presheaf.map_comp]
      · simp_rw [← Category.assoc]
        erw [← comp_c_app, ← comp_c_app]
        · simp_rw [Category.assoc]
          dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
          rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
          congr

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k)))

pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j))

Tactic:
·

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h.inl
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inl x)))
        y =
      (coprodMk X Y) (Sum.inl x)

pp: case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)

Tactic:
·

Goal state after:
case h.inl
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inl x)))
        y =
      (coprodMk X Y) (Sum.inl x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)

Tactic:
·

Goal state after:
case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j))

Tactic:
·

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1
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 := ⋯
i : BinaryCofan.mk f g ≅ c' := ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := ⋯
⊢ ∀ (i : WalkingPair), IsOpenImmersion (fi i)

pp: case convert_2
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
⊢ ⨆ i, Scheme.Hom.opensRange (fi i) = ⊤

pp: case convert_3
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
⊢ _root_.Pairwise (Function.onFun Disjoint fun x ↦ Scheme.Hom.opensRange (fi x))

Tactic:
·

Goal state after:
case convert_1
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 := ⋯
i : BinaryCofan.mk f g ≅ c' := ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := ⋯
⊢ ∀ (i : WalkingPair), IsOpenImmersion (fi i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_2
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
⊢ ⨆ i, Scheme.Hom.opensRange (fi i) = ⊤

pp: case convert_3
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
⊢ _root_.Pairwise (Function.onFun Disjoint fun x ↦ Scheme.Hom.opensRange (fi x))

Tactic:
·

Goal state after:
case convert_2
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
⊢ ⨆ i, Scheme.Hom.opensRange (fi i) = ⊤
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op.id
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X : WalkingMultispan (MultispanShape.prod D.J)
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.id X)) ≫
      D.ιInvAppπApp U (unop (op X)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.id X))

pp: case op.op.fst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))

pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k)))

Tactic:
·

Goal state after:
case op.op.id
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X : WalkingMultispan (MultispanShape.prod D.J)
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.id X)) ≫
      D.ιInvAppπApp U (unop (op X)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.id X))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_3
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
⊢ _root_.Pairwise (Function.onFun Disjoint fun x ↦ Scheme.Hom.opensRange (fi x))

Tactic:
·

Goal state after:
case convert_3
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
⊢ _root_.Pairwise (Function.onFun Disjoint fun x ↦ Scheme.Hom.opensRange (fi x))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op.fst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))

pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k)))

Tactic:
·

Goal state after:
case op.op.fst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl ≤ Scheme.Hom.opensRange coprod.inl

pp: case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Scheme.Hom.opensRange coprod.inl ≤ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl

Tactic:
·

Goal state after:
case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl ≤ Scheme.Hom.opensRange coprod.inl
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a.inl
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inl x))
⊢ (coprodMk X Y) (Sum.inl x) ∈ Scheme.Hom.opensRange coprod.inl

pp: case a.inr
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inr x))
⊢ (coprodMk X Y) (Sum.inr x) ∈ Scheme.Hom.opensRange coprod.inl

Tactic:
·

Goal state after:
case a.inl
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inl x))
⊢ (coprodMk X Y) (Sum.inl x) ∈ Scheme.Hom.opensRange coprod.inl
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a.inr
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inr x))
⊢ (coprodMk X Y) (Sum.inr x) ∈ Scheme.Hom.opensRange coprod.inl

Tactic:
·

Goal state after:
case a.inr
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inr x))
⊢ (coprodMk X Y) (Sum.inr x) ∈ Scheme.Hom.opensRange coprod.inl
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Scheme.Hom.opensRange coprod.inl ≤ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl

Tactic:
·

Goal state after:
case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Scheme.Hom.opensRange coprod.inl ≤ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ {X' Y' : Scheme} (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

pp: case refine_2
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {Z : Scheme} →
    (f : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inl)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inl) ⋯).fst
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inr)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inr) ⋯).fst)

Tactic:
·

Goal state after:
case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ {X' Y' : Scheme} (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j

pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
·

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.fst (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
·

Goal state after:
case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.fst (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {Z : Scheme} →
    (f : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inl)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inl) ⋯).fst
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inr)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inr) ⋯).fst)

Tactic:
·

Goal state after:
case refine_2
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {Z : Scheme} →
    (f : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inl)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inl) ⋯).fst
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inr)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inr) ⋯).fst)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
·

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g