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

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x : 𝒰.I₀
⊢ (pullbackSymmetry (𝒰.f x) (𝒰.f x)).hom =
    𝟙
      (match (x, x) with
      | (x, y) => pullback (𝒰.f x) (𝒰.f y))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom) ≫
      pullback.fst (𝒰.f y) (𝒰.f x)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom) ≫
      pullback.snd (𝒰.f y) (𝒰.f x)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫
      (ulift 𝒰).gluedCover.ι i ≫ Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram Y (fun i ↦ f (idx 𝒰 i)) ⋯ =
    pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x

Tactic:
hf

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫
      (ulift 𝒰).gluedCover.ι i ≫ Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram Y (fun i ↦ f (idx 𝒰 i)) ⋯ =
    pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f (idx 𝒰 i)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ (fst f (𝒰.f i) ≫ f) ≫ 𝟙 Y = snd f (𝒰.f i) ≫ 𝒰.f i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 Y = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))).hom ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯) ≫
      fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) =
    ((pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))).hom ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯) ≫
      snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫
      f ≫ Cover.glueMorphisms 𝒰 (fun i ↦ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i)) ⋯ =
    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i : 𝒰.I₀
⊢ 𝒰.f i ≫ Cover.glueMorphisms 𝒰 (fun i ↦ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i)) ⋯ ≫ f = 𝒰.f i ≫ 𝟙 Y

Tactic:
simp

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
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)
⊢ ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ≫ (V F i j).ι =
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ≫ (V F i k).ι

Tactic:
simp

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 j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (𝟙 (D.V (i, j))).base) '' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
k : Discrete σ
x : ↥((Discrete.functor g).obj k)
⊢ ⟨k.1, ((Discrete.functor g).map { down := { down := ⋯ } }) x⟩ =
    ⟨k.1, ((Discrete.functor g).map { down := { down := ⋯ } }) x⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i : σ
x : ↥(g i)
e : x ≍ x
⊢ ((Discrete.functor g).map (𝟙 { as := i })) x = x ∧ ((Discrete.functor g).map (𝟙 { as := i })) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
simp

Goal state after:
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 : σ ≃ ι
i : ι
⊢ Sigma.ι g (e.symm i) ≫ Sigma.desc α =
    Sigma.ι g (e.symm i) ≫ (Sigma.reindex e.symm g).inv ≫ Sigma.desc fun i ↦ α (e.symm i)

Tactic:
simp

Goal state after:
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:
· simpa [← WalkingPair.equivBool.symm.iSup_comp, iSup_bool_eq, ← codisjoint_iff] using hf.2

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.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))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.inl ≫ coprod.map f g = f ≫ coprod.inl

Tactic:
simp

Goal state after:
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)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ g ≫ (Iso.refl Y').hom = (Iso.refl Y).hom ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.inl ≫ (coprod.braiding Y X).hom = (Iso.refl Y).hom ≫ coprod.inr

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.inl ≫ (coprod.braiding Y' X').hom = (Iso.refl Y').hom ≫ coprod.inr

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.map g f ≫ (coprod.braiding Y' X').hom = (coprod.braiding Y X).hom ≫ coprod.map f g

Tactic:
simp

Goal state after:
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₀
⊢ ∀ (x : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀),
    (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f x ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
          (gluing 𝒰 f g).ι i =
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f x ≫
        pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
intro j

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₀
⊢ (Precoverage.ZeroHypercover.pullback₁ (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 =
    (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f j ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i)
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.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫
      (gluing 𝒰 f g).ι j ≫ Multicoequalizer.desc (gluing 𝒰 f g).diagram Y (fun i ↦ pullback.snd (𝒰.f i ≫ f) g) ⋯ =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
simp

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 : ι → CommRingCat
⊢ IsOpenImmersion (sigmaSpec R)

Tactic:
classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this

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
b✝ : ι
⊢ Sigma.ι (fun i ↦ Spec (R i)) b✝ ≫ sigmaSpec R =
    Sigma.ι (fun i ↦ Spec (R i)) b✝ ≫
      (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:
simp

Goal state after:
ι : 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
b✝ : ι
⊢ Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) b✝)) = Spec.map ((CommRingCat.piFan R).proj b✝)
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
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
pf✝⁵ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝⁴ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝³ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝² : IsOpenImmersion (F.map fi)
pf✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (Scheme.homOfLE_ι _ _).symm

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 ↥X
inst✝ : DiscreteTopology ↥X
this : IsAffineOpen (⨆ x, { carrier := {x}, is_open' := ⋯ })
x✝ : ↥X
⊢ x✝ ∈ ↑⊤ ↔ x✝ ∈ ↑(⨆ x, { carrier := {x}, is_open' := ⋯ })

Tactic:
simp

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ (𝒰.f i ≫ f) ≫ 𝟙 Z = 𝒰.f i ≫ f

Tactic:
simp

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp

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
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
pf✝⁵ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝⁴ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝³ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝² : IsOpenImmersion (F.map fi)
pf✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (Scheme.homOfLE_ι _ _).symm

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
hf : P f
x : ↥X
⊢ ⊤ ≤ f ⁻¹ᵁ ⊤

Tactic:
simp

Goal state after:
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✝
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₀
⊢ (𝒰.f i ≫ f) ≫ 𝟙 Z = 𝒰.f i ≫ f

Tactic:
simp

Goal state after:
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✝
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₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp

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

Goal state before:
pp: case h.hU
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U ⊆ Set.univ

Tactic:
simp

Goal state after: