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

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ s.fst.c.app (op x) ≫
      ((TopCat.Presheaf.pushforward C s.fst.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
        inv (s.pt.presheaf.map (eqToHom ⋯)) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
]

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ s.fst.c.app (op x) ≫
      ((TopCat.Presheaf.pushforward C s.fst.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
        inv (s.pt.presheaf.map (eqToHom ⋯)) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈ ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (F.map (f i)))

Tactic:
]

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈ ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f).base) ⁻¹' Set.range ⇑i

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f).base) ⁻¹' Set.range ⇑i
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : P.IsMultiplicative
⊢ P.pretopology.toGrothendieck = P.pretopology.toGrothendieck

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ (pullback.fst g f) a = y

Tactic:
]

Goal state after:
case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ (pullback.fst g f) a = y
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ ∃ a,
    (ConcreteCategory.hom
          ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
        a =
      x

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ ∃ a,
    (ConcreteCategory.hom
          ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
        a =
      x
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ x ∈ {x | ∃ y, f x = g y}

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ x ∈ {x | ∃ y, f x = g y}
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
this : x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f.base g.base))
⊢ ∃ a,
    (ConcreteCategory.hom
          ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
        a =
      x

Tactic:
obtain ⟨a, ha⟩ := this

Goal state after:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ ∃ a,
    (ConcreteCategory.hom
          ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
        a =
      x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.adjunction.counit.app (unop x)).op ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.adjunction.counit.app (unop x)).op ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: case h
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ (ConcreteCategory.hom (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) a = x

Tactic:
]

Goal state after:
case h
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ (ConcreteCategory.hom (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) a = x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ (Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∈ (precoverage P).coverings S ↔ Function.Surjective ⇑f ∧ P f

Tactic:
ofArrows_mem_precoverage_iff

Goal state after:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ ((∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑f) ∧ ∀ (i : PUnit.{1}), P f) ↔ Function.Surjective ⇑f ∧ P f
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ ((∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑f) ∧ ∀ (i : PUnit.{1}), P f) ↔ Function.Surjective ⇑f ∧ P f

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ ((∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑f) ∧ ∀ (i : PUnit.{1}), P f) ↔ Function.Surjective ⇑f ∧ P f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ((Epi f.base ∧ IsOpenEmbedding ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ ((Epi f.base ∧ IsOpenEmbedding ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ jointlySurjectivePrecoverage ⊓ Q.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (precoverage P).coverings S
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows T p₁ ∈ (precoverage P).coverings Y

Tactic:
ofArrows_mem_precoverage_iff

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ (∀ (x : ↥Y), ∃ i, x ∈ Set.range ⇑(p₁ i)) ∧ ∀ (i : ι), P (p₁ i)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ (∀ (x : ↥Y), ∃ i, x ∈ Set.range ⇑(p₁ i)) ∧ ∀ (i : ι), P (p₁ i)

Tactic:
]

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ (∀ (x : ↥Y), ∃ i, x ∈ Set.range ⇑(p₁ i)) ∧ ∀ (i : ι), P (p₁ i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion (Y.ofRestrict ⋯)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion (Y.ofRestrict ⋯)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g).hom ≫
      pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g) =
    Scheme.Hom.toLRSHom (pullback.snd f g)
⊢ LocallyRingedSpace.IsOpenImmersion
    ((PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g).hom ≫
      pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g).hom ≫
      pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g) =
    Scheme.Hom.toLRSHom (pullback.snd f g)
⊢ LocallyRingedSpace.IsOpenImmersion
    ((PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g).hom ≫
      pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd

Tactic:
]

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion
    ((limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }).hom ≫
      { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }.cone.π.app WalkingCospan.right)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion
    ((limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }).hom ≫
      { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }.cone.π.app WalkingCospan.right)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.left ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.left ≫ f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ''
      ⇑(ConcreteCategory.hom (pullback.fst f.base g.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ''
      ⇑(ConcreteCategory.hom (pullback.fst f.base g.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso
    ((limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }).hom ≫
        { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }.cone.π.app
          WalkingCospan.right).base

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso
    ((limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }).hom ≫
        { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }.cone.π.app
          WalkingCospan.right).base
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ∀ (x : ↥X), x ∈ ⋃ i, Set.range ⇑(𝒰.f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ∀ (x : ↥X), x ∈ ⋃ i, Set.range ⇑(𝒰.f i)