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

Goal state before:
pp: case refine_1
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ 0 1 = 1

pp: case refine_2
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ { toFun := 0, map_one' := ?refine_1 }.toFun (x✝ * y✝) =
    { toFun := 0, map_one' := ?refine_1 }.toFun x✝ * { toFun := 0, map_one' := ?refine_1 }.toFun y✝

pp: case refine_3
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun 0 = 0

pp: case refine_4
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun (x✝ + y✝) =
    (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun x✝ +
      (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun y✝

Tactic:
<;>

Goal state after:
case refine_1
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ 0 1 = 1

case refine_2
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ { toFun := 0, map_one' := ?refine_1 }.toFun (x✝ * y✝) =
    { toFun := 0, map_one' := ?refine_1 }.toFun x✝ * { toFun := 0, map_one' := ?refine_1 }.toFun y✝

case refine_3
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun 0 = 0

case refine_4
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun (x✝ + y✝) =
    (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun x✝ +
      (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun y✝
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
by
  change (e.inv.base ≫ e.hom.base) y = 𝟙 Y.toPresheafedSpace y
  simp

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

Goal state before:
pp: case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f) → x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Tactic:
rintro ⟨hxV, _, hx⟩

Goal state after:
case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ x ∈ ↑(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
⊢ colimit.cocone (F ⋙ forget C) ≅ (forget C).mapCocone (colimitCocone F)

Tactic:
fapply Cocone.ext

Goal state after:
case φ
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
⊢ (colimit.cocone (F ⋙ forget C)).pt ≅ ((forget C).mapCocone (colimitCocone F)).pt

case w
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
⊢ autoParam
    (∀ (j : J), (colimit.cocone (F ⋙ forget C)).ι.app j ≫ Iso.hom ?φ = ((forget C).mapCocone (colimitCocone F)).ι.app j)
    Cocone.ext._auto_1
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
x✝ : ↑↑{ carrier := ↑X, presheaf := X.presheaf ⋙ F }
⊢ (ConcreteCategory.hom { base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F }.base) x✝ =
    (ConcreteCategory.hom (𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }).base) x✝

pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
U✝ : Opens ↑↑{ carrier := ↑X, presheaf := X.presheaf ⋙ F }
⊢ ({ base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F }.c ≫
          whiskerRight (eqToHom ⋯) { carrier := ↑X, presheaf := X.presheaf ⋙ F }.presheaf).app
      (op U✝) =
    (𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }).c.app (op U✝)

Tactic:
<;>

Goal state after:
case w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
x✝ : ↑↑{ carrier := ↑X, presheaf := X.presheaf ⋙ F }
⊢ (ConcreteCategory.hom { base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F }.base) x✝ =
    (ConcreteCategory.hom (𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }).base) x✝

case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
U✝ : Opens ↑↑{ carrier := ↑X, presheaf := X.presheaf ⋙ F }
⊢ ({ base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F }.c ≫
          whiskerRight (eqToHom ⋯) { carrier := ↑X, presheaf := X.presheaf ⋙ F }.presheaf).app
      (op U✝) =
    (𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑↑{ carrier := ↑X✝, presheaf := X✝.presheaf ⋙ F }
⊢ (ConcreteCategory.hom { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.base) x✝ =
    (ConcreteCategory.hom
        ({ base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }).base)
      x✝

pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
U✝ : Opens ↑↑{ carrier := ↑Z✝, presheaf := Z✝.presheaf ⋙ F }
⊢ ({ base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.c ≫
          whiskerRight (eqToHom ⋯) { carrier := ↑X✝, presheaf := X✝.presheaf ⋙ F }.presheaf).app
      (op U✝) =
    ({ base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }).c.app (op U✝)

Tactic:
<;>

Goal state after:
case w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑↑{ carrier := ↑X✝, presheaf := X✝.presheaf ⋙ F }
⊢ (ConcreteCategory.hom { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.base) x✝ =
    (ConcreteCategory.hom
        ({ base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }).base)
      x✝

case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
U✝ : Opens ↑↑{ carrier := ↑Z✝, presheaf := Z✝.presheaf ⋙ F }
⊢ ({ base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.c ≫
          whiskerRight (eqToHom ⋯) { carrier := ↑X✝, presheaf := X✝.presheaf ⋙ F }.presheaf).app
      (op U✝) =
    ({ base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }).c.app (op U✝)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

pp: case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)

Tactic:
<;>

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)
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
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯) ≫ (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
NatTrans.naturality,

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
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (colimit.ι F j).c.app
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj
                  ((Opens.map
                        (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                    U))) ≫
            ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)
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
⊢ IsIso f

Tactic:
apply +allowSynthFailures isIso_of_components

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
⊢ IsIso f.base
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
hx : x ∈ X.basicOpen f
hn : f ^ 0 ∈ I
⊢ f ∈ I

Tactic:
by simpa using I.mul_mem_left f hn

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y) = y

Tactic:
by
  change (e.inv ≫ e.hom) y = 𝟙 Y.toPresheafedSpace y
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ IsLocalizedModule p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).toLinearMap

Tactic:
apply IsLocalizedModule.mkOfAlgebra
  · intro x hx; rw [algebraMap_pushforward_stalk, toPushforwardStalk_comp]
    change IsUnit ((TopCat.Presheaf.stalkFunctor CommRingCat p).map
      (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c _)
    exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _
  · apply isLocalizedModule_toPushforwardStalkAlgHom_aux
  · intro x hx
    rw [toPushforwardStalkAlgHom_apply,
      ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
      toPushforwardStalk] at hx
    rw [CommRingCat.comp_apply, map_zero] at hx
    obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq (C := CommRingCat) _ _ _ _ _ _ hx
    obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
      PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU)
        U.2
    apply_fun (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
        (homOfLE hrU).op at e
    have : algebraMap S ((structureSheaf S).presheaf.obj _) x = 0 := e
    have :=
      (@IsLocalization.mk'_one _ _ _ _ _ _
            (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans
        this
    obtain ⟨⟨_, n, rfl⟩, e⟩ := (IsLocalization.mk'_eq_zero_iff _ _).mp this
    refine ⟨⟨r, hpr⟩ ^ n, ?_⟩
    rw [Submonoid.smul_def, Algebra.smul_def, SubmonoidClass.coe_pow, map_pow]
    exact e

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

Goal state before:
pp: case w.none
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
⊢ (limit.cone (cospan f.base g.base)).π.app none =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app none ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none

pp: case w.some.left
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
⊢ (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left)

pp: case w.some.right
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
⊢ (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case w.none
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
⊢ (limit.cone (cospan f.base g.base)).π.app none =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app none ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none

case w.some.left
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
⊢ (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left)

case w.some.right
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
⊢ (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

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

Tactic:
Set.eq_univ_iff_forall

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

Goal state before:
pp: case none
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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ P ((𝒰.add f).f none)

pp: case some
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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
i : 𝒰.I₀
⊢ P ((𝒰.add f).f (some i))

Tactic:
<;>

Goal state after:
case none
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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ P ((𝒰.add f).f none)

case some
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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
i : 𝒰.I₀
⊢ P ((𝒰.add f).f (some i))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mpr
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
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (H.isoPullback.inv ≫ iU) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
cases hx ⟨_, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.OverClass

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ autoParam (X ↘ S ≫ S ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam

Tactic:
comp_over

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ autoParam (X ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_1
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩)

pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩) ⊆ U

Tactic:
<;>

Goal state after:
case h_nhds.refine_1
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩)

case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩) ⊆ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤

Tactic:
exact U.ι.image_mono le_top

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (F.map (𝟙 U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
F.map_id

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
        (toOpenₗ R M (basicOpen s)) ⋯)
      (LocalizedModule.mk (s ^ n • f) ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯

Tactic:
← Submonoid.mk_smul (S := .powers s) _ ⟨n, rfl⟩,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
        (toOpenₗ R M (basicOpen s)) ⋯)
      (LocalizedModule.mk (⟨(fun x ↦ s ^ x) n, ⋯⟩ • f) ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case H
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι

pp: case H'
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι

Tactic:
<;>

Goal state after:
case H
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι

case H'
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι