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

Goal state before:
pp: D : GlueData
U : Set ↥D.glued
⊢ ∀ (a : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
    IsOpen
        (⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι a)) ⁻¹'
          ⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U) ↔
      IsOpen (⇑(D.ι a) ⁻¹' U)

Tactic:
intro i

Goal state after:
D : GlueData
U : Set ↥D.glued
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        ⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U) ↔
    IsOpen (⇑(D.ι i) ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
apply pullback.hom_ext <;> simp_rw [Category.id_comp, Category.assoc]

Goal state after:
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 (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
H : ∀ (x : ↥X), ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
⊢ f = g

Tactic:
choose U hxU hU using H
  let 𝒰 : X.OpenCover := {
    I₀ := X, X i := (U i), f i := (U i).ι,
    mem₀ := by
      rw [presieve₀_mem_precoverage_iff]
      refine ⟨fun x ↦ ⟨x, by simpa using hxU x⟩, inferInstance⟩ }
  exact 𝒰.hom_ext _ _ hU

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
⊢ {i j : σ} → i ≠ j → IsInitial (pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt

Tactic:
intro i

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
i : σ
⊢ {j : σ} → i ≠ j → IsInitial (pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ ∀ (x y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        (pullbackSymmetry s.fst (𝒰.f x)).hom ≫
          pullback.map (𝒰.f x) s.fst (𝒰.f x ≫ f) g (𝟙 (𝒰.X x)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι x =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        (pullbackSymmetry s.fst (𝒰.f y)).hom ≫
          pullback.map (𝒰.f y) s.fst (𝒰.f y ≫ f) g (𝟙 (𝒰.X y)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι y

Tactic:
intro i

Goal state after:
case hf
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ∀ (y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
          pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι i =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        (pullbackSymmetry s.fst (𝒰.f y)).hom ≫
          pullback.map (𝒰.f y) s.fst (𝒰.f y ≫ f) g (𝟙 (𝒰.X y)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι y
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
intro i

Goal state after:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
i : ι
⊢ IsOpenMap fun a ↦ (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨i, a⟩
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 : σ ≃ ι
⊢ _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α (e.symm x)))

Tactic:
intro i

Goal state after:
σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
i : ι
⊢ ∀ ⦃j : ι⦄, i ≠ j → (Disjoint on fun x ↦ Set.range ⇑(α (e.symm x))) i j
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 k : D.J
U : Opens ↑↑(D.U i)
X' : C
f' :
  ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).obj
      (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ⟶
    X'
⊢ D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ≫ f' =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ f'

Tactic:
by
  simpa only [Category.assoc] using congr_arg (· ≫ f') (opensImagePreimageMap_app D i j k U)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1
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 := ⋯
i : BinaryCofan.mk f g ≅ c' := ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := ⋯
⊢ ∀ (i : WalkingPair), IsOpenImmersion (fi i)

Tactic:
intro i

Goal state after:
case convert_1
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 : WalkingPair
⊢ IsOpenImmersion (fi i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
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:
intro i

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
i : WalkingPair
⊢ ∀ ⦃j : WalkingPair⦄, i ≠ j → Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) i j
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
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:
intro i j hij
    match i, j with
    | .left, .right => simpa [fi] using hf.1
    | .right, .left => simpa [fi] using hf.1.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✝ 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
⊢ ∀ (x : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x ≫ m =
      (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x ≫ gluedLift 𝒰 f g s

Tactic:
intro i

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₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ gluedLift 𝒰 f g s
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 σ
inst✝ : ∀ (i : σ), IsAffine (g i)
⊢ IsAffine (∐ g)

Tactic:
obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)

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 σ
inst✝ : ∀ (i : σ), IsAffine (g i)
ι : Type u
e : σ ≃ ι
⊢ IsAffine (∐ g)
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)
⊢ IsAffineOpen (iSup U)

Tactic:
obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)

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 : σ ≃ ι
⊢ IsAffineOpen (iSup U)
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)

Tactic:
intro i

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)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀), P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)

Tactic:
intro i

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inj
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.ι i).base)

Tactic:
· have := D.ι_gluedIso_inv (PresheafedSpace.forget _) i
      dsimp at this
      rw [← this, TopCat.coe_comp]
      refine Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)
      rw [← TopCat.mono_iff_injective]
      infer_instance

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₀),
    pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ =
      (pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
        (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).f ((Equiv.refl 𝒰.I₀) i)

Tactic:
intro i

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✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
      (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).f ((Equiv.refl 𝒰.I₀) 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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀) →
    (precoverage IsOpenImmersion).ZeroHypercover ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)

Tactic:
intro i

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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
⊢ (precoverage IsOpenImmersion).ZeroHypercover ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X 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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (i : 𝒰.I₀),
    pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
        (𝒰.f i) ⋯ ⋯ =
      (Iso.refl (pullback (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)))).hom ≫
        (openCoverOfBase' 𝒰 f g).f
          (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i)

Tactic:
intro i

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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (Iso.refl (pullback (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)))).hom ≫
      (openCoverOfBase' 𝒰 f g).f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case basicOpen
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))
this✝ : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
this : Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ((ConcreteCategory.hom (↑U).topIso.inv) r))
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))

Tactic:
exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this

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), Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)

Tactic:
intro i

Goal state after:
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
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)
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)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.gluedCover.isoLocallyRingedSpace.inv

Goal state after:
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)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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₀),
    P (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))

Tactic:
intro i

Goal state after:
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₀
⊢ P (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).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
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)) ≫
        (𝒱 i).f ⟨i, (j, j)⟩.snd.2) ≫
      pullback.fst f (𝒰.f i) =
    ((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)) ≫
        (𝒱 i).f ⟨i, (j, j)⟩.snd.2) ≫
      pullback.fst f (𝒰.f i)

Tactic:
trans pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        (diagonalCover f 𝒰 𝒱).f _ ≫ pullback.snd _ _

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
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)) ≫
        (𝒱 i).f ⟨i, (j, j)⟩.snd.2) ≫
      pullback.fst f (𝒰.f i) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.snd f f

X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
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)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.snd f f =
    ((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)) ≫
        (𝒱 i).f ⟨i, (j, j)⟩.snd.2) ≫
      pullback.fst f (𝒰.f i)
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:
rintro ⟨i, j⟩
      dsimp [glueData, GlueData.diagram]
      simp only [t, IsOpenImmersion.lift_fac, ← Scheme.Hom.comp_toLRSHom]
      rw [← cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.fromGlued.toLRSHom,
        ← cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.gluedCover.isoLocallyRingedSpace.inv]
      refine Multicoequalizer.hom_ext _ _ _ fun ⟨k, hk⟩ ↦ ?_
      rw [← CategoryTheory.GlueData.ι, reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        ← cancel_epi (Hom.isoOpensRange (F.map _)).hom.toLRSHom]
      simp +instances only [Opens.iSupOpenCover, Cover.ulift, V, ← Hom.comp_toLRSHom_assoc,
        Cover.ι_fromGlued_assoc, homOfLE_ι, Hom.isoOpensRange_hom_ι, Cover.idx]
      generalize_proofs _ _ h
      rw [homOfLE_tAux F ↓i ↓j h.choose.2.1 h.choose.2.2, Iso.hom_inv_id_assoc]
      exact (s.w h.choose.2.1).trans (s.w h.choose.2.2).symm

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
  use D.ιInvAppπEqMap U ≫ D.ιInvApp U
  constructor
  · apply π_ιInvApp_eq_id
  · rw [Category.assoc, (D.ιInvApp_π _).choose_spec]
    exact Iso.inv_hom_id ((D.U i).presheaf.mapIso (eqToIso _))

Goal state after: