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

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
i : (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWX ≫ fXZ =
    (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY ≫ fYZ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
this : IsIso (pullback.lift fWX fWY h)
⊢ (asIso (pullback.lift fWX fWY h)).hom ≫ pullback.fst fXZ fYZ = fWX

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
this : IsIso (pullback.lift fWX fWY h)
⊢ (asIso (pullback.lift fWX fWY h)).hom ≫ pullback.snd fXZ fYZ = fWY

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
⊢ P f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ (𝒰.f i ≫ fXZ) ≫ 𝟙 Z = 𝒰.f i ≫ fXZ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ fYZ ≫ 𝟙 Z = 𝟙 Y ≫ fYZ

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ P f ↔ ∀ (i : 𝒰.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ pullback.snd fWX (𝒰.f i) ≫ 𝒰.f i ≫ fXZ = (pullback.fst fWX (𝒰.f i) ≫ fWY) ≫ fYZ

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ P f ↔ Q f

Tactic:
by

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)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          (((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
            (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
        (D.U i).presheaf.map (eqToHom ⋯).op ≫
          (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
            (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
← Functor.map_comp_assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
              (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
            (eqToHom ⋯).op) ≫
        (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h =
    pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f

Tactic:
by

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 : Shrink.{u, w} J
f : ↓i ⟶ ↓j
⊢ F.map f ≫ (glueData F).ι j = (glueData F).ι i

Tactic:
by

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
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
⊢ P (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
by

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 : J
f : i ⟶ j
⊢ F.map f ≫ F.map (eqToHom ⋯) ≫ (glueData F).ι ((equivShrink J) j) =
    (F.map (eqToHom ⋯) ≫ (glueData F).ι ((equivShrink J) i)) ≫ ((Functor.const J).obj (glueData F).glued).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsPullback (pullback.fst fWX (𝒰.f i)) (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯)
    (pullback.lift fWX fWY h) f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ IsIso (Cover.pullbackHom (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i)

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget P

Tactic:
by

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
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
⊢ IsPullback fWX fWY fXZ fYZ

Tactic:
by

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
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ ((𝒱 I.fst).f I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst) ≫ 𝒰.f I.fst =
    ((𝒱 I.fst).f I.snd.1 ≫ pullback.fst f (𝒰.f I.fst)) ≫ f

Tactic:
by

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
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ ((𝒱 I.fst).f I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst) ≫ 𝒰.f I.fst =
    ((𝒱 I.fst).f I.snd.2 ≫ pullback.fst f (𝒰.f I.fst)) ≫ f

Tactic:
by

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
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.toPreZeroHypercover.1
e : pullback (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
⊢ e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i

Tactic:
by

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
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : J), (cocone F).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).J).R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ (diagonalCover f 𝒰 𝒱).f I =
    pullback.map ((𝒱 I.fst).f I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst) ((𝒱 I.fst).f I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst)
      f f ((𝒱 I.fst).f I.snd.1 ≫ pullback.fst f (𝒰.f I.fst)) ((𝒱 I.fst).f I.snd.2 ≫ pullback.fst f (𝒰.f I.fst))
      (𝒰.f I.fst) ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
⊢ P (pullback.fst f g)

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) ≫ 𝟙 S =
    𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i) ≫
      pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅ ?m.62

Tactic:
by

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)
⊢ IsIso (D.t i j).c

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
⊢ e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)

Tactic:
by

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)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j = D.diagramOverOpenπ U j

Tactic:
by

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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.snd ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
        ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.fst ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
        ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)

Tactic:
by

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 : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))

Tactic:
by

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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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
x✝ : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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
⊢ colimit.ι F i =
    (F.mapIso (eqToIso ⋯)).hom ≫
      (Precoverage.ZeroHypercover.bind (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
            fun i ↦ (glueData F).openCover).f
        (((equivShrink J).trans (Equiv.uniqueSigma fun x ↦ Shrink.{u, w} J).symm) i)

Tactic:
by

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 : D.J
U : Opens ↑↑(D.U i)
⊢ IsIso (D.diagramOverOpenπ U i)

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
⊢ P (pullback.fst f g)

Tactic:
by

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 : D.J
U : Opens ↑↑(D.U i)
⊢ IsIso ((D.ι i).c.app (op (⋯.functor.obj U)))

Tactic:
by

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
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
⊢ (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ Set.range ⇑(Scheme.Hom.opensRange g).ι = Set.range ⇑g

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ f =
    X.topIso.inv ≫
      (X.isoOfEq this).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
⊢ P f

Tactic:
by

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ P.diagonal.toProperty.RespectsIso

Tactic:
by

Goal state after: