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

Goal state before:
pp: case app
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
x : ↑((F ⋙ forget C).obj (unop X))
⊢ (ConcreteCategory.hom
        (colimit.ι (F ⋙ forget C) (unop X) ≫
          (colimit.isoColimitCocone
                  {
                    cocone :=
                      {
                        pt :=
                          { carrier := Limits.colimit (F ⋙ forget C),
                            presheaf := limit (pushforwardDiagramToColimit F).leftOp },
                        ι :=
                          {
                            app := fun j ↦
                              { base := colimit.ι (F ⋙ forget C) j,
                                c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) },
                            naturality := ⋯ } },
                    isColimit := colimitCoconeIsColimit F }).symm.hom.base))
      x =
    (ConcreteCategory.hom (colimit.ι F (unop X)).base) x

Tactic:
congr

Goal state after:
case app
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
x : ↑((F ⋙ forget C).obj (unop X))
⊢ colimit.ι (F ⋙ forget C) (unop X) ≫
      (colimit.isoColimitCocone
              {
                cocone :=
                  {
                    pt :=
                      { carrier := Limits.colimit (F ⋙ forget C),
                        presheaf := limit (pushforwardDiagramToColimit F).leftOp },
                    ι :=
                      {
                        app := fun j ↦
                          { base := colimit.ι (F ⋙ forget C) j,
                            c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) },
                        naturality := ⋯ } },
                isColimit := colimitCoconeIsColimit F }).symm.hom.base =
    (colimit.ι F (unop X)).base
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 ↑↑Y
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (homOfLE ⋯).op

Tactic:
congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ : Y.presheaf ⟶ (Presheaf.pushforward CommRingCat { hom' := { toFun := f₁, continuous_toFun := f₂ } }).obj X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
⊢ {
      base :=
        ofHom
          { toFun := ⇑(ConcreteCategory.hom { hom' := { toFun := f₁, continuous_toFun := f₂ } }),
            continuous_toFun := ⋯ },
      c := f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ } =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }

Tactic:
congr

Goal state after:
X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ : Y.presheaf ⟶ (Presheaf.pushforward CommRingCat { hom' := { toFun := f₁, continuous_toFun := f₂ } }).obj X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
⊢ f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom = f₃
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_4
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
⊢ Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))

Tactic:
congr

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

Goal state before:
pp: case 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))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))

Tactic:
congr

Goal state after:
case e'_5.e_8.e_3
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)) = unop (op (hf.functor.obj U))

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))
⊢ ⋯.adjunction.counit.app (hf.functor.obj U) ≍ 𝟙 (unop (op (hf.functor.obj U)))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_5.e_8.e_3
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

Tactic:
congr

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

Goal state before:
pp: case op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op
      ((opensFunctor f).obj
        ((↑(TopCat.Hom.frameHom f.base)).toFunctor.obj { carrier := carrier✝, is_open' := is_open'✝ }))

Tactic:
congr

Goal state after:
case op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ carrier✝ =
    ⇑(ConcreteCategory.hom f.base) ''
      ↑((↑(TopCat.Hom.frameHom f.base)).toFunctor.obj { carrier := carrier✝, is_open' := is_open'✝ })
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0

Tactic:
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.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.grothendieckTopology = P.pretopology.toGrothendieck

Tactic:
by
  rw [grothendieckTopology, coverage_eq_toCoverage_pretopology,
    Pretopology.toGrothendieck_toCoverage]

Goal state after:
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:
congr

Goal state after:
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
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_
  · change pullback.lift _ _ _ ≫ pullback.snd _ _ = _
    simp
  · change (_ ≫ _ ≫ _) ≫ _ = _
    simp_rw [Category.assoc]
    erw [s.snd.c.naturality_assoc]
    erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]
    trans s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 _)
    · congr 1
    · simp

Goal state after:
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 ⋯ = 𝟙 X

Tactic:
rw [← cancel_mono f]

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 : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr

Goal state after:
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
Y' : Scheme
g' : Y' ⟶ Y
H : Set.range ⇑g ⊆ Set.range ⇑f
⊢ Set.range ⇑(g' ≫ g) ⊆ Set.range ⇑g

Tactic:
by simp [Set.range_comp_subset_range]

Goal state after:
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 ⋯ = 𝟙 X

Tactic:
rw [← cancel_mono f]

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.Geometry.RingedSpace.OpenImmersion

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

Tactic:
convert! h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
x : ↥X
r : ↑⋯.choose
⊢ ⇑(TopCat.Hom.hom (X.affineCover.f x).base) ''
      Set.range ⇑(TopCat.Hom.hom ((affineBasisCoverOfAffine (Classical.choose ⋯)).f r).base) =
    (fun a ↦ (X.affineCover.f x) a) '' (PrimeSpectrum.basicOpen r).carrier

Tactic:
congr

Goal state after:
case e_s
X : Scheme
x : ↥X
r : ↑⋯.choose
⊢ Set.range ⇑(TopCat.Hom.hom ((affineBasisCoverOfAffine (Classical.choose ⋯)).f r).base) =
    (PrimeSpectrum.basicOpen r).carrier
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
            ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
rw [TopCat.pullback_fst_range]
    ext
    constructor
    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤))))) r)

Tactic:
congr

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ (Hom.appIso (X.ofRestrict ⋯) ⊤).inv = X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))
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
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
⊢ Function.Injective ⇑(algebraMap (↑(F.presheaf.obj U)) (Localization m))

Tactic:
refine IsLocalization.injective (M := m) (S := Localization m) ?_

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
⊢ m ≤ (↑(F.presheaf.obj U))⁰
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).inv = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [eq_comm, ← Iso.hom_comp_eq_id]
  dsimp
  simp only [appIso_hom, homOfLE_app, homOfLE_leOfHom, eqToHom_op, Opens.toScheme_presheaf_map,
    eqToHom_unop, ← X.presheaf.map_comp, Category.assoc, ← X.presheaf.map_id]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ⇑(TopCat.Hom.hom f.base) '' ↑(f ⁻¹ᵁ U) = ↑U

Tactic:
refine @Set.image_preimage_eq _ _ f U.1 f.homeomorph.surjective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g : ↑R
⊢ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (f * g)))) =
    Spec.map
      (CommRingCat.ofHom ((IsLocalization.Away.awayToAwayRight f g).comp (algebraMap (↑R) (Localization.Away f))))

Tactic:
congr

Goal state after:
R : CommRingCat
f g : ↑R
⊢ algebraMap (↑R) (Localization.Away (f * g)) =
    (IsLocalization.Away.awayToAwayRight f g).comp (algebraMap (↑R) (Localization.Away f))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r

Tactic:
congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e'_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i : ↥t
x : ↥(unop (op (basicOpen ((fun i ↦ g ↑i ^ (N + 1)) i))))
⊢ 1 • ⟨g ↑i, ⋯⟩ • (fun i ↦ g ↑i ^ N • f ↑i) i = 1 • ⟨(fun i ↦ g ↑i ^ (N + 1)) i, ⋯⟩ • f ↑i

Tactic:
simp [Submonoid.smul_def, pow_succ', mul_smul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : IsAffine Y
⊢ IsAffine X

Tactic:
← essImage_Spec

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx = toStalkₗ' R M x

Tactic:
rw [toStalkₗ', ← Presheaf.germ_res _ (homOfLE le_top) _ hx, ← Category.assoc]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P.IsLocalAtTarget K

Tactic:
refine mk_of_iff fun X Y f R hR ↦ ?_
  obtain ⟨𝒰, rfl⟩ := R.exists_eq_preZeroHypercover
  rw [H _ ⟨𝒰, hR⟩]
  have _ (i) : HasPullback (𝒰.f i) f := (Precoverage.hasPullbacks_of_mem _ hR).hasPullback ⟨i⟩
  refine ⟨fun h U g hfg ↦ ?_, fun h i ↦ h _ ⟨i⟩⟩
  rintro ⟨i⟩
  exact h i

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app (op ⊤) ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
← Γ_map_op

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      Γ.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).op ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r)) =
    X.basicOpen r

Tactic:
congr

Goal state after:
X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
exact isLocalization_basicOpen hU f

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ σ ↑b • (comapFun f y) (LocalizedModule.mk a b) = σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
rw [← (comapFun f y).map_smulₛₗ, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply]

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (comapFun f y) ((LocalizedModule.mkLinearMap (Ideal.comap σ y.asIdeal).primeCompl M) a) =
    σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i : D.J
⊢ IsIso (D.f' i i)

Tactic:
simp only [↓reduceDIte, GlueData'.f']

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i : D.J
⊢ IsIso (eqToHom ⋯)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
⊢ ∀ {x y z : (i : D.J) × ↑(D.U i)}, D.Rel x y → D.Rel y z → D.Rel x z

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ ⟨x, e₁, e₂⟩

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
⊢ D.Rel ⟨j, b⟩ ⟨k, c⟩ → D.Rel ⟨i, a⟩ ⟨k, c⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
x : ↑(D.U i)
⊢ ∀ ⦃a₂ : ↑(D.U i)⦄, (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) a₂ → x = a₂

Tactic:
y

Goal state after:
D : GlueData
i : D.J
x y : ↑(D.U i)
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y → x = y