mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
]

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
inst✝ : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffineOpen (⨆ x, U (e.symm x))

Tactic:
]

Goal state after:
σ : Type v
X : Scheme
inst✝ : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffineOpen (⨆ x, U (e.symm x))
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✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
        pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram 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
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
        pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ IsAffineOpen (⨆ i, U ↑i)

Tactic:
]

Goal state after:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ IsAffineOpen (⨆ i, U ↑i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingPair
⊢ Function.Injective ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i)))

Tactic:
]

Goal state after:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingPair
⊢ Function.Injective ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
]

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ U i)

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
⊢ Set.range ⇑f ⊆ Set.range ⇑(⨆ i, U i).ι

Tactic:
simpa using H

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ Set.range ⇑f ⊆ Set.range ⇑(⨆ i, U i).ι

Tactic:
simpa using H

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

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
          ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
]

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
          ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ≫ (⨆ i, U i).ι)

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ≫ (⨆ i, U i).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ∀ (i : ι), P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i = ⊤

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ∀ (i : ι), P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i = ⊤
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map
        ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
          (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
]

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map
        ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
          (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) := Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (f ∣_ U i)

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) := Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (f ∣_ U i)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map
      ((homOfLE ⋯).op ≫
        (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
          (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
]

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map
      ((homOfLE ⋯).op ≫
        (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
          (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = ⨆ i, U i

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = ⨆ i, U i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case inl
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit))

Tactic:
]

Goal state after:
case inl
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit))
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✝
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))

Tactic:
]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))

Tactic:
]

Goal state after:
case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))
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₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
        f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings (pullback f g)

Tactic:
ofArrows_mem_precoverage_iff

Goal state after:
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,
        x ∈
          Set.range
            ⇑({ 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) ⋯ ⋯ }.f
                i)) ∧
    ∀
      (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₀),
      IsOpenImmersion
        ({ 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) ⋯ ⋯ }.f
          i)
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,
        x ∈
          Set.range
            ⇑({ 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) ⋯ ⋯ }.f
                i)) ∧
    ∀
      (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₀),
      IsOpenImmersion
        ({ 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) ⋯ ⋯ }.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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (∀ (x : ↥(pullback f g)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ 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) ⋯ ⋯ }.f
                i)) ∧
    ∀
      (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₀),
      IsOpenImmersion
        ({ 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) ⋯ ⋯ }.f
          i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)

Tactic:
]

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : (Scheme.Cover.ulift 𝒰).I₀
⊢ P (𝒰.f (Scheme.Cover.idx 𝒰 i) ≫ f)

Tactic:
]

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : (Scheme.Cover.ulift 𝒰).I₀
⊢ P (𝒰.f (Scheme.Cover.idx 𝒰 i) ≫ f)