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

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (f.hom ≫ f.inv).hom = 𝟙 X.toPresheafedSpace

Tactic:
f.hom_inv_id,

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (𝟙 X.toSheafedSpace).hom = 𝟙 X.toPresheafedSpace
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  X.presheaf.map (⋯.adjunction.counit.app (unop (op (hf.functor.obj V)))).op ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    X.presheaf.map (⋯.adjunction.counit.app (unop (op (hf.functor.obj V)))).op ≫
      g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
cancel_epi

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : X.basicOpen f = unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
this

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : X.basicOpen f = unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) ≤
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        (pushforwardToOfIso
              ((forget C).mapIso
                  (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).symm
              (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.inv.c).app
          (op U)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
pushforwardToOfIso_app,

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.inv.c.app
            (op
              ((Opens.map
                    ((forget C).mapIso
                          (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).symm.inv).obj
                (unop (op U)))) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom

Tactic:
Spec.sheafedSpaceMap_comp

Goal state after:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ X.basicOpen f ⊔ X.basicOpen g

Tactic:
[

Goal state after:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ X.basicOpen f ⊔ X.basicOpen g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_5.e_8.e_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ (⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U) =
    (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))

Tactic:
this

Goal state after:
case e'_5.e_8.e_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ (⋯.functor.obj U ⟶ hf.functor.obj U) = (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ jointlySurjectivePrecoverage.coverings S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ jointlySurjectivePrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ jointlySurjectivePrecoverage.coverings S

Tactic:
[

Goal state after:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ jointlySurjectivePrecoverage.coverings S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ jointlySurjectivePrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ jointlySurjectivePrecoverage.coverings S
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ jointlySurjectivePrecoverage.coverings S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ jointlySurjectivePrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ jointlySurjectivePrecoverage.coverings S

Tactic:
ofArrows_mem_jointlySurjectivePrecoverage_iff

Goal state after:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
⊢ ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (g i.fst i.snd ≫ f i.fst))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ jointlySurjectivePrecoverage.coverings S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ jointlySurjectivePrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ jointlySurjectivePrecoverage.coverings S

Tactic:
simp_rw [ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf hg ⊢

Goal state after:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
⊢ ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (g i.fst i.snd ≫ f i.fst))
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
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      (op x) =
    s.fst.c.app (op x)

Tactic:
change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _

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
⊢ ((invApp f (unop (op x)) ≫ g.c.app (op (⋯.functor.obj (unop (op x)))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app (op x) =
    s.fst.c.app (op x)
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
⊢ ((invApp f x ≫ g.c.app (op (⋯.functor.obj x)) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).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
⊢ ((invApp f x ≫ g.c.app (op (⋯.functor.obj x)) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app (op x) =
    s.fst.c.app (op x)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
⊢ (E.restrictIndex i).presieve₀ ∈ jointlySurjectivePrecoverage.coverings X

Tactic:
ofArrows_mem_jointlySurjectivePrecoverage_iff

Goal state after:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
⊢ ∀ (x : (fun X ↦ X) X), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom ((E.restrictIndex i).f i_1))
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)ᵒᵖ
⊢ ((pullbackConeOfLeft f g).snd.c.app x ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
          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)ᵒᵖ
⊢ ((pullbackConeOfLeft f g).snd.c.app x ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
          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: P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)

Tactic:
[

Goal state after:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w
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
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      𝟙 (((Functor.const WalkingCospan).obj (limit.cone (cospan f.base g.base)).pt).obj j) ≫
        ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j

Tactic:
[

Goal state after:
case w
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
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      𝟙 (((Functor.const WalkingCospan).obj (limit.cone (cospan f.base g.base)).pt).obj j) ≫
        ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ j y, (map j) y = x
map_prop : ∀ (j : J), P (map j)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
[

Goal state after:
K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ j y, (map j) y = x
map_prop : ∀ (j : J), P (map j)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
TopCat.pullback_fst_image_snd_preimage

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : J), P (map i)

Tactic:
[

Goal state after:
case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : J), P (map i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv))

Tactic:
this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
[

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False

Tactic:
[

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False