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

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(U x).ι) i j ↔ (Disjoint on U) i j

Tactic:
;

Goal state after:
ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(U x).ι) i j ↔ (Disjoint on U) i j
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.fst (p1 𝒰 f g) (𝒰.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✝ 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.fst (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite ↥X
inst✝ : DiscreteTopology ↥X
this : IsAffineOpen (⨆ x, { carrier := {x}, is_open' := ⋯ })
⊢ ⊤ = ⨆ x, { carrier := {x}, is_open' := ⋯ }

Tactic:
;

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 ↥X
inst✝ : DiscreteTopology ↥X
this : IsAffineOpen (⨆ x, { carrier := {x}, is_open' := ⋯ })
⊢ ⊤ = ⨆ x, { carrier := {x}, is_open' := ⋯ }
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite ↥X
inst✝ : DiscreteTopology ↥X
this : IsAffineOpen (⨆ x, { carrier := {x}, is_open' := ⋯ })
x✝ : ↥X
⊢ x✝ ∈ ↑⊤ ↔ x✝ ∈ ↑(⨆ x, { carrier := {x}, is_open' := ⋯ })

Tactic:
;

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

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)
x✝ : ↥Y
⊢ x✝ ∈ ↑(iSup Subtype.val) ↔ x✝ ∈ ↑⊤
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:
apply MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance

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) := ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯)
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:
Scheme.Hom.image_top_eq_opensRange,

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 = Scheme.Hom.opensRange (⨆ i, U i).ι
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
hX : ∀ (x : ↥X), ∃ U, f x ∈ U ∧ P ((f ⁻¹ᵁ U).ι ≫ f)
⊢ P f

Tactic:
choose U h₁ h₂ using hX

Goal state after:
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
⊢ P f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ U = (Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U)

Tactic:
;

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ U = (Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U = ↑((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))

Tactic:
;

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U = ↑((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base) ⁻¹'
      ⇑(ConcreteCategory.hom (D.ι i).base) '' ↑U

Tactic:
;

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base) ⁻¹'
      ⇑(ConcreteCategory.hom (D.ι i).base) '' ↑U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x : ↑↑(D.U i)
⊢ x ∈ ↑U ↔
    x ∈
      ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base) ⁻¹'
        ⇑(ConcreteCategory.hom (D.ι i).base) '' ↑U

Tactic:
simp only [SetLike.mem_coe, unop_op, Set.mem_preimage, Set.mem_image]

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x : ↑↑(D.U i)
⊢ x ∈ U ↔
    ∃ x_1 ∈ U,
      (ConcreteCategory.hom (D.ι i).base) x_1 =
        (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
x✝ : ↥X
⊢ x✝ ∈ ↑(iSup Subtype.val) ↔ x✝ ∈ ↑⊤

Tactic:
;

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
x✝ : ↥X
⊢ x✝ ∈ ↑(iSup Subtype.val) ↔ x✝ ∈ ↑⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q

Tactic:
;

Goal state after:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ P x✝¹ ↔ Q x✝¹

Tactic:
;

Goal state after:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ P x✝¹ ↔ Q x✝¹
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ (∃ (h : IsAffine Y), P f) ↔ P f

Tactic:
;

Goal state after:
P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ (∃ (h : IsAffine Y), P f) ↔ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hprecomp
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
a : IsAffine Z
h : P f
⊢ P.toProperty (e.hom ≫ f)

Tactic:
;

Goal state after:
case hprecomp
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
a : IsAffine Z
h : P f
⊢ P.toProperty (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
a : IsAffine Y
h : P f
⊢ P.toProperty (f ≫ e.hom)

Tactic:
;

Goal state after:
case hpostcomp
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
a : IsAffine Y
h : P f
⊢ P.toProperty (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
inst✝ : IsAffine Z✝
⊢ of P f✝ → of P (e✝.hom ≫ f✝)

Tactic:
;

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
inst✝ : IsAffine Z✝
⊢ of P f✝ → of P (e✝.hom ≫ f✝)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ of P f✝ → of P (f✝ ≫ e✝.hom)

Tactic:
;

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ of P f✝ → of P (f✝ ≫ e✝.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
⊢ P ((f ≫ e.hom) ∣_ ↑⟨U, hU⟩)

Tactic:
;

Goal state after:
case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
⊢ P ((f ≫ e.hom) ∣_ ↑⟨U, hU⟩)
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
⊢ IsIso (V F (↓i) ↓j).ι

Tactic:
have : V F ↓i ↓j = ⊤ :=
      top_le_iff.mp (le_iSup_of_le ⟨_, 𝟙 _, f⟩ (by simp [Scheme.Hom.opensRange_of_isIso]))

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
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this : V F (↓i) ↓j = ⊤
⊢ IsIso (V F (↓i) ↓j).ι
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:
;

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
j : J
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
    ((colimitPresheafObjIsoComponentwiseLimit D.diagram.multispan (⋯.functor.obj U)).hom ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)) (op (WalkingMultispan.right i)))

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ IsIso
    ((colimitPresheafObjIsoComponentwiseLimit D.diagram.multispan (⋯.functor.obj U)).hom ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)) (op (WalkingMultispan.right i)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
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
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

pp: case mpr
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
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj) → (colimit.ι F i) xi = (colimit.ι F j) xj

Tactic:
;

Goal state after:
case mp
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
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

case mpr
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
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj) → (colimit.ι F i) xi = (colimit.ι F j) xj
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mpr
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : J
fi : k ⟶ i
fj : k ⟶ j
x : ↥(F.obj k)
⊢ (colimit.ι F i) ((F.map fi) x) = (colimit.ι F j) ((F.map fj) x)

Tactic:
;

Goal state after:
case mpr
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : J
fi : k ⟶ i
fj : k ⟶ j
x : ↥(F.obj k)
⊢ (colimit.ι F i) ((F.map fi) x) = (colimit.ι F j) ((F.map fj) x)
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
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : ↓k ⟶ ↓(i, j).1
kj : ↓k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨↓k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ ((glueData F).ι j) ((F.map kj) y) = (TopCat.Hom.hom ((glueData F).ι j).base) ((TopCat.Hom.hom (F.map kj).base) y)

Tactic:
;

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
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : ↓k ⟶ ↓(i, j).1
kj : ↓k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨↓k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ ((glueData F).ι j) ((F.map kj) y) = (TopCat.Hom.hom ((glueData F).ι j).base) ((TopCat.Hom.hom (F.map kj).base) y)
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
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : ↓k ⟶ ↓(i, j).1
kj : ↓k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨↓k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ (TopCat.Hom.hom ((glueData F).ι i).base) ((TopCat.Hom.hom (F.map ki).base) y) =
    (TopCat.Hom.hom ((glueData F).ι i).base) ((F.map ki) y)

Tactic:
;

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
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : ↓k ⟶ ↓(i, j).1
kj : ↓k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨↓k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ (TopCat.Hom.hom ((glueData F).ι i).base) ((TopCat.Hom.hom (F.map ki).base) y) =
    (TopCat.Hom.hom ((glueData F).ι i).base) ((F.map ki) y)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

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)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
⊢ IsAffine
    (pullback ((𝒰' i.fst).f i.snd.1 ≫ pullback.snd f (𝒰.f i.fst)) ((𝒰' i.fst).f i.snd.2 ≫ pullback.snd f (𝒰.f i.fst)))

Tactic:
;

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
⊢ IsAffine
    (pullback ((𝒰' i.fst).f i.snd.1 ≫ pullback.snd f (𝒰.f i.fst)) ((𝒰' i.fst).f i.snd.2 ≫ pullback.snd f (𝒰.f i.fst)))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x✝

Tactic:
;

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsDominant x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x✝

Tactic:
;

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsDominant x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x✝
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R)

Tactic:
;

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))) x

Tactic:
;

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))) x
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (x ⊗ₜ[R] 1)

Tactic:
;

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (x ⊗ₜ[R] 1)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom ↑includeRight ≫ ofHom ↑(lmul' R)

Tactic:
;

Goal state after:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom ↑includeRight ≫ ofHom ↑(lmul' R)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))) x

Tactic:
;

Goal state after:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))) x
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (1 ⊗ₜ[R] x)

Tactic:
;

Goal state after:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (1 ⊗ₜ[R] x)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : MonObj (Over.mk (M ↘ S))
⊢ MonObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
;

Goal state after:
M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : MonObj (Over.mk (M ↘ S))
⊢ MonObj (Over.mk (pullback (M ↘ S) f ↘ T))