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

Goal state before:
pp: case H
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) = Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)

Tactic:
rw [← cancel_mono (Y.fromSpecStalk _)]

Goal state after:
case H
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) =
    Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x) ≫ Y.fromSpecStalk (f x)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ IsOver S f

Tactic:
rw [isOver_iff]

Goal state after:
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : { f // f ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX }
⊢ (((fun x ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY ↑f ⋯)).restrict
        ((fun x ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY ↑f ⋯)).domain ⋯ ⋯).hom =
    ((Hom.toPartialMap sX).restrict ((fun x ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY ↑f ⋯)).domain ⋯ ⋯).hom

Tactic:
by simp [PartialMap.ofFromSpecStalk_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X.PartialIso Y
hf : IsOver sX sY f
⊢ IsOver sY sX f.symm

Tactic:
by
  simpa [IsOver, ← cancel_epi f.iso.hom] using Eq.symm hf

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
i : ↑I
⊢ ↑↑i ≤ ⨆ i ∈ I, ↑i

Tactic:
intro i

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
i✝ : ↑I
i : ↥X
⊢ i ∈ ↑↑i✝ → i ∈ ⨆ i ∈ I, ↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i : ↑I
⊢ ↑↑i ≤ ⨆ i ∈ I, ↑i

Tactic:
intro i

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i✝ : ↑I
i : ↥T
⊢ i ∈ ↑↑i✝ → i ∈ ⨆ i ∈ I, ↑i
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ ((opensDiagram D i U).map f) x ∈ V ↔
    x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V)

Tactic:
refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩

Goal state after:
case e'_2.refine_1
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ (D.map (Over.Hom.left f)) ↑x ∈ D.map k.hom ⁻¹ᵁ U

case e'_2.refine_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ ⟨(D.map (Over.Hom.left f)) ↑x, ?e'_2.refine_1⟩ ∈ ↑V

case e'_2.refine_3
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) →
    ((opensDiagram D i U).map f) x ∈ V
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X✝ : Scheme
𝒰✝ : X✝.OpenCover
inst✝³ : Category.{v_1, ?u.14} 𝒰✝.I₀
inst✝² : Cover.LocallyDirected 𝒰✝
S : Scheme
X : Over S
𝒰 : X.left.OpenCover
inst✝¹ : Category.{v_2, ?u.91} 𝒰.I₀
inst✝ : Cover.LocallyDirected 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
⊢ ∀ (x : 𝒰.I₀), 𝒰.f x ≫ 𝒰.glueMorphismsOfLocallyDirected g ⋯ ≫ Y.hom = 𝒰.f x ≫ X.hom

Tactic:
intro i

Goal state after:
P : MorphismProperty Scheme
X✝ : Scheme
𝒰✝ : X✝.OpenCover
inst✝³ : Category.{v_1, ?u.14} 𝒰✝.I₀
inst✝² : Cover.LocallyDirected 𝒰✝
S : Scheme
X : Over S
𝒰 : X.left.OpenCover
inst✝¹ : Category.{v_2, ?u.91} 𝒰.I₀
inst✝ : Cover.LocallyDirected 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
i : 𝒰.I₀
⊢ 𝒰.f i ≫ 𝒰.glueMorphismsOfLocallyDirected g ⋯ ≫ Y.hom = 𝒰.f i ≫ X.hom
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝² : Category.{u_2, u_1} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝ : Quiver.IsThin 𝒰.I₀
⊢ ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Function.Injective ⇑(d.functor.map hij)

Tactic:
intro i

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝² : Category.{u_2, u_1} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ ∀ {j : 𝒰.I₀} (hij : i ⟶ j), Function.Injective ⇑(d.functor.map hij)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_2
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
⊢ s.snd ≫ d.toBase = s.fst ≫ 𝒰.f i

Tactic:
s.condition

Goal state after:
case refine_2
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
⊢ s.snd ≫ d.toBase = s.snd ≫ d.toBase
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)

Tactic:
intro i

Goal state after:
case refine_1.refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
i : ι
⊢ IsOpen (Sigma.mk i ⁻¹' s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU : IsCompactOpenCovered f U
h :
  ∃ κ,
    ∃ (_ : Finite κ),
      ∃ a V, (∀ (i : κ), V i ∈ B (a i)) ∧ (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ i, f (a i) '' ↑(V i) = U
⊢ ∃ n a V, (∀ (i : Fin n), V i ∈ B (a i)) ∧ ⋃ i, f (a i) '' ↑(V i) = U

Tactic:
obtain ⟨κ, _, a, V, hB, hc, hU⟩ := h

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB✝ : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU✝ : IsCompactOpenCovered f U
κ : Type ?u.68
w✝ : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), V i ∈ B (a i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ i, f (a i) '' ↑(V i) = U
⊢ ∃ n a V, (∀ (i : Fin n), V i ∈ B (a i)) ∧ ⋃ i, f (a i) '' ↑(V i) = U
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : TopologicalSpace S
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
hfc : ∀ (i : ι), Continuous (f i)
h : ∀ (i : ι), IsOpenMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ i, x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
x : S
hx : x ∈ U
⊢ x ∈ Set.range fun p ↦ f p.fst p.snd

Tactic:
simpa using hs x hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.71} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.71} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
⊢ ∀ (i : 𝒰.toPreZeroHypercover.1), P (pullbackHom 𝒰 d.relativeGluingData.toBase i)

Tactic:
intro i

Goal state after:
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.71} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.71} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
i : 𝒰.toPreZeroHypercover.1
⊢ P (pullbackHom 𝒰 d.relativeGluingData.toBase i)
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ (i : (𝒱 a).I₀) → (𝒱 a).X i ⟶ Over.left (((Functor.const J).obj d.glued).obj a).toComma

Tactic:
intro i

Goal state after:
case refine_1.refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i : (𝒱 a).I₀
⊢ (𝒱 a).X i ⟶ Over.left (((Functor.const J).obj d.glued).obj a).toComma
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ {i j : (𝒱 a).I₀} (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
intro i

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i : (𝒱 a).I₀
⊢ ∀ {j : (𝒱 a).I₀} (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU✝ : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U

Tactic:
have (i) (hi) : IsCompactOpenCovered ((f i).f ·) (V i hi) :=
      isCompactOpenCovered_of_isCompact (f i) (hcV i hi)

Goal state after:
S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU✝ : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
this : ∀ (i : 𝒰.I₀) (hi : i ∈ s), IsCompactOpenCovered (fun x ↦ ⇑((f i).f x)) ↑(V i hi)
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.221} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.221} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := ⋯
a b : J
f : a ⟶ b
⊢ ∀ (x : (𝒱 a).I₀),
    (𝒱 a).f x ≫
        (D.map f ≫
            {
              toCommaMorphism :=
                (𝒱 b).glueMorphismsOverOfLocallyDirected
                  (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
              prop_hom_left := trivial, prop_hom_right := trivial }).left =
      (𝒱 a).f x ≫
        ({
              toCommaMorphism :=
                (𝒱 a).glueMorphismsOverOfLocallyDirected
                  (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
              prop_hom_left := trivial, prop_hom_right := trivial } ≫
            ((Functor.const J).obj d.glued).map f).left

Tactic:
intro i

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.221} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.221} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
⊢ (𝒱 a).f i ≫
      (D.map f ≫
          {
            toCommaMorphism :=
              (𝒱 b).glueMorphismsOverOfLocallyDirected
                (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial }).left =
    (𝒱 a).f i ≫
      ({
            toCommaMorphism :=
              (𝒱 a).glueMorphismsOverOfLocallyDirected
                (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial } ≫
          ((Functor.const J).obj d.glued).map f).left
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
S : Scheme
𝒰 : Cover (precoverage P) S
⊢ ∀ (i : 𝒰.sigma.I₀), Presieve.singleton (Sigma.desc 𝒰.f) (𝒰.sigma.f i)

Tactic:
intro i

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
S : Scheme
𝒰 : Cover (precoverage P) S
i : 𝒰.sigma.I₀
⊢ Presieve.singleton (Sigma.desc 𝒰.f) (𝒰.sigma.f i)
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.117} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
⊢ (i : 𝒱.I₀) → 𝒱.X i ⟶ Over.left s.pt.toComma

Tactic:
intro i

Goal state after:
case refine_1.refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.117} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i : 𝒱.I₀
⊢ 𝒱.X i ⟶ Over.left s.pt.toComma
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.117} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
⊢ ∀ {i j : 𝒱.I₀} (hij : i ⟶ j),
    Cover.trans 𝒱 hij ≫
        ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
          pullback.fst s.pt.hom (𝒰.f j) =
      ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f i)

Tactic:
intro i

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.117} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i : 𝒱.I₀
⊢ ∀ {j : 𝒱.I₀} (hij : i ⟶ j),
    Cover.trans 𝒱 hij ≫
        ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
          pullback.fst s.pt.hom (𝒰.f j) =
      ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f i)