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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (Z.presheaf.stalkCongr ⋯).hom ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose)

Tactic:
← cancel_mono (f.hom.stalkMap (h₁ y).choose),

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose =
    ((Z.presheaf.stalkCongr ⋯).hom ≫
        PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom
          ((ConcreteCategory.hom f.hom.base) ⋯.choose)) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
⊢ (ConcreteCategory.hom (X.presheaf.germ W x hxW)) ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ W x hxW)) ((ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    1

Tactic:
X.presheaf.germ_res_apply (Opens.infLELeft U V) x hxW f,

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
⊢ (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) f *
      (ConcreteCategory.hom (X.presheaf.germ W x hxW)) ((ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    1
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) →
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
rintro ⟨hxU, hx⟩

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)) →
    x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))

Tactic:
rintro ⟨hxU, hx⟩

Goal state after:
case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha✝ : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
x : ↥U
Va : Opens ↑X
ma : ↑x ∈ Va
ia : Va ⟶ U
ha : P₁.pred fun x ↦ a (ia x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P₃.pred fun x ↦ (fun x ↦ op (a x) (b x)) (i x)

Tactic:
rcases hb x with ⟨Vb, mb, ib, hb⟩

Goal state after:
X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha✝ : P₁.sheafify.pred a
hb✝ : P₂.sheafify.pred b
x : ↥U
Va : Opens ↑X
ma : ↑x ∈ Va
ia : Va ⟶ U
ha : P₁.pred fun x ↦ a (ia x)
Vb : Opens ↑X
mb : ↑x ∈ Vb
ib : Vb ⟶ U
hb : P₂.pred fun x ↦ b (ib x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P₃.pred fun x ↦ (fun x ↦ op (a x) (b x)) (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case w
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥↑U) → T ↑y
h : P.pred f
⊢ (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)

Tactic:
exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝

Tactic:
rw [NatTrans.comp_app, sheafedSpaceMap_hom_c_app, Functor.whiskerRight_app, eqToHom_refl]

Goal state after:
case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          (sheafedSpaceObj T).presheaf.map
            ((𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op).app (op U✝))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ map (inv f) = inv (map f)

Tactic:
by
  change Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
  rw [op_inv, ← Scheme.Spec.map_inv]

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
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H

Tactic:
rw [← cancel_mono f, hl, lift_fac]

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
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H

Tactic:
by rw [← cancel_mono f, hl, lift_fac]

Goal state after:
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
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))

Tactic:
change HasLimit (cospan ((forget).map g) ((forget).map f))

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.fst f g ≫ f) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
f.image_preimage_eq_opensRange_inf,

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Hom.opensRange f ⊓ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PullbackCone f g

Tactic:
by
  refine PullbackCone.mk ?_
      (Y.ofRestrict (TopCat.snd_isOpenEmbedding_of_left H.base_open g.base)) ?_
  · use PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.1 g.1
    intro x
    have := PresheafedSpace.stalkMap.congr_hom _ _
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition f.1 g.1) x
    rw [PresheafedSpace.stalkMap.comp, PresheafedSpace.stalkMap.comp] at this
    rw [← IsIso.eq_inv_comp] at this
    rw [this]
    dsimp
    apply RingHom.isLocalHom_comp
  · exact LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition _ _)

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))

Tactic:
have :=
        PresheafedSpace.stalkMap.congr_hom _ _
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1
            (PullbackCone.mk s.fst.1 s.snd.1
              (congr_arg LocallyRingedSpace.Hom.toHom s.condition)))
          x

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)
      x =
    eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).snd x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))
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)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H'

Tactic:
rw [← cancel_mono f, hl, lift_fac]

Goal state after:
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)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H'

Tactic:
by rw [← cancel_mono f, hl, lift_fac]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
⊢ V.ι ∣_ U ≫ (Iso.refl ↑U).hom = (Scheme.Hom.isoImage V.ι (V.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
by simp [← cancel_mono U.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1
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 j : ↥t
this : n ↑i ↑j + 1 ≤ N
⊢ ((g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) * (g ↑i * g ↑j) ^ (n ↑i ↑j + 1)) • g ↑j • f ↑i =
    ((g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) * (g ↑i * g ↑j) ^ (n ↑i ↑j + 1)) • g ↑i • f ↑j

Tactic:
mul_smul,

Goal state after:
case refine_1
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 j : ↥t
this : n ↑i ↑j + 1 ≤ N
⊢ (g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) • (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑j • f ↑i =
    ((g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) * (g ↑i * g ↑j) ^ (n ↑i ↑j + 1)) • g ↑i • f ↑j
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Tactic:
unfold toSpecΓ
  have := X.toΓSpecSheafedSpace_app_spec 1
  unfold toToΓSpecMapBasicOpen toΓSpecMapBasicOpen at this
  rw! [basicOpen_one] at this
  convert! this
  exact (X.presheaf.map_id ..).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.fst s v ≫ f = lhs ≫ pullback.fst t v

Tactic:
simp [lhs]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen (f ''ᵁ f ⁻¹ᵁ U)

Tactic:
f.image_preimage_eq_opensRange_inf,

Goal state after:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen (Scheme.Hom.opensRange f ⊓ U)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f) = ↑(X.basicOpen f)

Tactic:
change hU.fromSpec '' hU.fromSpec ⁻¹' (X.basicOpen f : Set X) = _

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ⇑hU.fromSpec '' ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen f) = ↑(X.basicOpen f)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ IsLocalizedModule x.asIdeal.primeCompl (ModuleCat.Hom.hom (toStalkₗ' R M x))

Tactic:
by
  convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) (stalkIsoₗ R M x).toLinearEquiv.symm
  ext m
  refine .trans ?_ (localizationtoStalkₗ_mk ..).symm
  dsimp +instances [toStalkₗ', toOpenₗ]
  rw! [PrimeSpectrum.basicOpen_one]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
y : Y
hy : y ∈ U
e' :
  (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) y) =
    (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) x✝)
e'' : Function.Injective ⇑(hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
⊢ Quot.mk (Function.Coequalizer.Rel ⇑(hom f) ⇑(hom g)) y = Quot.mk (Function.Coequalizer.Rel ⇑(hom f) ⇑(hom g)) x✝

Tactic:
apply e''

Goal state after:
case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
y : Y
hy : y ∈ U
e' :
  (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) y) =
    (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) x✝)
e'' : Function.Injective ⇑(hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
⊢ (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      (Quot.mk (Function.Coequalizer.Rel ⇑(hom f) ⇑(hom g)) y) =
    (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      (Quot.mk (Function.Coequalizer.Rel ⇑(hom f) ⇑(hom g)) x✝)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
let e := D.gluedIso F
  obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)
  replace eq := congr_arg e.inv eq
  change ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq
  rw [e.hom_inv_id, D.ι_gluedIso_inv] at eq
  exact ⟨i, y, eq⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
· rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, t_snd, Category.assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case e'_3
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
e_1✝ : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ ⇑(𝒰.f (idx 𝒰 x)) ⁻¹' ⇑(fromGlued 𝒰) '' U = ⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U

Tactic:
simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]

Goal state after:
case e'_3
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
e_1✝ : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ ⇑(TopCat.Hom.hom ((gluedCover 𝒰).ι (idx 𝒰 x)).base) ⁻¹'
      ⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' (fun a ↦ (fromGlued 𝒰) a) '' U =
    ⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ Epi (fromGlued 𝒰).base

Tactic:
rw [TopCat.epi_iff_surjective]

Goal state after:
X : Scheme
𝒰 : X.OpenCover
⊢ Function.Surjective ⇑(fromGlued 𝒰)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
cocycle_fst_snd 𝒰 f g i j k

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ Epi f.base

Tactic:
rw [TopCat.epi_iff_surjective]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
inst✝ : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffineOpen (iSup U)

Tactic:
← e.symm.iSup_congr fun _ ↦ rfl

Goal state after:
σ : Type v
X : Scheme
inst✝ : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffineOpen (⨆ x, U (e.symm x))