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

Goal state before:
pp: case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝¹ }.toLRSHom = { toLRSHom' := toLRSHom'✝ }.toLRSHom
⊢ { toLRSHom' := toLRSHom'✝¹ } = { toLRSHom' := toLRSHom'✝ }

Tactic:
;

Goal state after:
case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝¹ }.toLRSHom = { toLRSHom' := toLRSHom'✝ }.toLRSHom
⊢ { toLRSHom' := toLRSHom'✝¹ } = { toLRSHom' := toLRSHom'✝ }
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
rw [IsIso.comp_inv_eq]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
simp only [invApp, ← Category.assoc]
  rw [IsIso.comp_inv_eq]
  simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
    NatTrans.naturality, Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc,
    TopCat.Presheaf.pushforward_obj_map]
  congr 1

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ IsIso (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ IsIso (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = app f U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = app f U ≫ X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ app (eqToHom ⋯) U = eqToHom ⋯

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
⊢ app (eqToHom ⋯) U = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
⊢ f.base = ofHom { toFun := ⇑f, continuous_toFun := ⋯ }

Tactic:
;

Goal state after:
X Y : Scheme
f : X.Hom Y
⊢ f.base = ofHom { toFun := ⇑f, continuous_toFun := ⋯ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ ⊥

Tactic:
;

Goal state after:
case refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ ⊥
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
x✝ : ↥X
⊢ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) ↔ x✝ ∈ X.zeroLocus s

Tactic:
;

Goal state after:
X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
x✝ : ↥X
⊢ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) ↔ x✝ ∈ X.zeroLocus s
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit
    ((algebraMap ↑R
        ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).stalk
            p))
      x)

Tactic:
;

Goal state after:
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit
    ((algebraMap ↑R
        ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).stalk
            p))
      x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit
    ((ConcreteCategory.hom
        ((TopCat.Presheaf.stalkFunctor CommRingCat p).map
          (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c))
      ((toStalk (↑R) p).hom' x))

Tactic:
exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom ⋯).op) ⁻¹ᵁ W)

Tactic:
;

Goal state after:
case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom ⋯).op) ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ f ''ᵁ ⊤ = opensRange f

Tactic:
apply Opens.ext

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ ↑(f ''ᵁ ⊤) = ↑(opensRange f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f ⁻¹ᵁ f ''ᵁ U = U

Tactic:
apply Opens.ext

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ ↑(f ⁻¹ᵁ f ''ᵁ U) = ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ f ''ᵁ f ⁻¹ᵁ U = opensRange f ⊓ U

Tactic:
apply Opens.ext

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ ↑(f ''ᵁ f ⁻¹ᵁ U) = ↑(opensRange f ⊓ U)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (𝟙 (op U))

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (𝟙 (op U))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ↑Γ(X, 𝟙 X ''ᵁ U)
⊢ (CommRingCat.Hom.hom (appIso (𝟙 X) U).hom) x✝ =
    (CommRingCat.Hom.hom (Functor.mapIso X.presheaf (eqToIso ⋯).op).hom) x✝

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
x✝ : ↑Γ(X, 𝟙 X ''ᵁ U)
⊢ (CommRingCat.Hom.hom (appIso (𝟙 X) U).hom) x✝ =
    (CommRingCat.Hom.hom (Functor.mapIso X.presheaf (eqToIso ⋯).op).hom) x✝
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opens
⊢ (appIso (f ≫ g) U).hom = (Functor.mapIso Z.presheaf (eqToIso ⋯).op ≪≫ appIso g (f ''ᵁ U) ≪≫ appIso f U).hom

Tactic:
;

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opens
⊢ (appIso (f ≫ g) U).hom = (Functor.mapIso Z.presheaf (eqToIso ⋯).op ≪≫ appIso g (f ''ᵁ U) ≪≫ appIso f U).hom
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.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_2
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' := ⋯ }
⊢ LocallyRingedSpace.IsOpenImmersion
    (have this := ⋯;
    inv (pullback.snd (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom') ≫
      pullback.fst (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom')

Tactic:
;

Goal state after:
case refine_2
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' := ⋯ }
⊢ LocallyRingedSpace.IsOpenImmersion
    (have this := ⋯;
    inv (pullback.snd (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom') ≫
      pullback.fst (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom')
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: 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
⊢ ∃ a, (pullback.snd f g) a = y

Tactic:
have : HasPullback g f := hasPullback_symmetry f g

Goal state after:
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.snd f g) a = y
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case mk
Y : Scheme
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ } = Y

Tactic:
;

Goal state after:
case mk
Y : Scheme
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ } = Y
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case mk.mk
toLocallyRingedSpace✝¹ : LocallyRingedSpace
local_affine✝¹ :
  ∀ (x : ↑toLocallyRingedSpace✝¹.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝¹.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ }.toLocallyRingedSpace =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ } =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }

Tactic:
;

Goal state after:
case mk.mk
toLocallyRingedSpace✝¹ : LocallyRingedSpace
local_affine✝¹ :
  ∀ (x : ↑toLocallyRingedSpace✝¹.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝¹.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ }.toLocallyRingedSpace =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ } =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝ : P.IsStableUnderComposition
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).IsStableUnderComposition

Tactic:
;

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝ : P.IsStableUnderComposition
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).IsStableUnderComposition
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).HasIsos

Tactic:
;

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).HasIsos
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
H : IsIso f.base
⊢ Epi f.base ∧ IsOpenEmbedding ⇑f

Tactic:
;

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
H : IsIso f.base
⊢ Epi f.base ∧ IsOpenEmbedding ⇑f
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
⊢ PreservesLimit (cospan f g) (Scheme.forgetToTop ⋙ «forget» TopCat)

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
⊢ PreservesLimit (cospan f g) (Scheme.forgetToTop ⋙ «forget» TopCat)
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
⊢ PreservesLimit (cospan g f) (Scheme.forgetToTop ⋙ «forget» TopCat)

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
⊢ PreservesLimit (cospan g f) (Scheme.forgetToTop ⋙ «forget» TopCat)
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
;

Goal state after:
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 : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
;

Goal state after:
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 : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mk
C : Type u
inst✝¹ : Category.{v, u} C
Y : SheafedSpace C
toPresheafedSpace✝ : PresheafedSpace C
IsSheaf✝ : toPresheafedSpace✝.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ } ⟶ Y
inst✝ : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ }

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
Y : SheafedSpace C
toPresheafedSpace✝ : PresheafedSpace C
IsSheaf✝ : toPresheafedSpace✝.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ } ⟶ Y
inst✝ : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ }
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
hx✝ : x ∈ ↑(f' ⁻¹ᵁ W)
hx : (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base) x ∉ Set.range ⇑iU
⊢ (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
;

Goal state after:
case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
hx✝ : x ∈ ↑(f' ⁻¹ᵁ W)
hx : (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base) x ∉ Set.range ⇑iU
⊢ (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)
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
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

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
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
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
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ 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
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ 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
inst✝ : HasPullback f g
H : IsOpenImmersion g
⊢ IsOpenImmersion (pullback.fst f g)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
H : IsOpenImmersion g
⊢ IsOpenImmersion (pullback.fst f g)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X.toPresheafedSpace
⊢ IsIso (PresheafedSpace.IsOpenImmersion.invApp f.hom U)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X.toPresheafedSpace
⊢ IsIso (PresheafedSpace.IsOpenImmersion.invApp f.hom U)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (snd ≫ g) p = g (snd p)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (snd ≫ g) p = g (snd p)