mathlib-initiative/mathlib-tactics huggingface dataset:
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.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
·

Goal state after:
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.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case x
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ ↥(∐ g)

pp: case a
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ ?x ∈ Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)

Tactic:
·

Goal state after:
case x
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ ↥(∐ g)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_1
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 : 𝒰.I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X i ⟶ pullback (𝒰.f i ≫ f) g

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
i j : 𝒰.I₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) ≫ 𝟙 X = ?refine_1 ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i

pp: case refine_3
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 : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
·

Goal state after:
case refine_1
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 : 𝒰.I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X i ⟶ pullback (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ (a ≫ Sigma.ι g i) z ∈ Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)

Tactic:
·

Goal state after:
case a
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ (a ≫ Sigma.ι g i) z ∈ Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)
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
i j : 𝒰.I₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) ≫ 𝟙 X =
    ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i

pp: case refine_3
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 : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
·

Goal state after:
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
i j : 𝒰.I₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) ≫ 𝟙 X =
    ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_3
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 : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
·

Goal state after:
case refine_3
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 : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j
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.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    (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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
·

Goal state after:
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.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    (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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Topology.IsOpenEmbedding ⇑(Sigma.desc α)

pp: case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
·

Goal state after:
case left
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Topology.IsOpenEmbedding ⇑(Sigma.desc α)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case f
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 : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued

pp: case hf
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 y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        ?f x =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        ?f y

Tactic:
·

Goal state after:
case f
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 : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_1
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Continuous (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

pp: case left.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Function.Injective (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

pp: case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ IsOpenMap (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

Tactic:
·

Goal state after:
case left.refine_1
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Continuous (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Function.Injective (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

pp: case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ IsOpenMap (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

Tactic:
·

Goal state after:
case left.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Function.Injective (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf
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 ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i =
    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 ⋯ ⋯ ≫ (gluing 𝒰 f g).ι j

Tactic:
← (gluing 𝒰 f g).glue_condition i j,

Goal state after:
case hf
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 ≫ (gluing 𝒰 f g).t i j ≫ (gluing 𝒰 f g).f j i ≫ (gluing 𝒰 f g).ι j =
    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 ⋯ ⋯ ≫ (gluing 𝒰 f g).ι j
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ IsOpenMap (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

Tactic:
·

Goal state after:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ IsOpenMap (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
·

Goal state after:
case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)
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)
⊢ ((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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
            ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ≫
      (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    ((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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U)) ≫
      (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
·

Goal state after:
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)
⊢ ((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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
            ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ≫
      (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    ((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))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U)) ≫
      (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right.refine_1
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ (Sigma.desc α)
      (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y) =
    (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

pp: case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

Tactic:
·

Goal state after:
case right.refine_1
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ (Sigma.desc α)
      (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y) =
    (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

Tactic:
·

Goal state after:
case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ Sigma.desc α = (Sigma.reindex e.symm g).inv ≫ Sigma.desc fun i ↦ α (e.symm i)

pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))

Tactic:
·

Goal state after:
σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ Sigma.desc α = (Sigma.reindex e.symm g).inv ≫ Sigma.desc fun i ↦ α (e.symm i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))

Tactic:
·

Goal state after:
σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf.e_a.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.fst (𝒰.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.fst (𝒰.f j ≫ 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
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 hf.e_a.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.fst (𝒰.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.fst (𝒰.f j ≫ f) g