mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (a : RingQuot r), a + 0 = a

Tactic:
rintro ⟨⟨⟩⟩
    simp only [add_quot, ← zero_quot, add_zero]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Algebra S R
r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) ((algebraMap S R) 1) } = 1

Tactic:
simp [← one_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) 1 } = 1

Tactic:
simp [← one_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : NonAssocSemiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : RingQuot r
⊢ f x = g x

Tactic:
rcases mkRingHom_surjective r x with ⟨x, rfl⟩

Goal state after:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : NonAssocSemiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : R
⊢ f ((mkRingHom r) x) = g ((mkRingHom r) x)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case e_g
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
a : α
b : β
c : α₂
⊢ (y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)).coeff c =
    (y.sum fun a_1 m ↦ single (f a * f a_1) (b * f a • m)).coeff c

Tactic:
simp_rw [hf]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

Tactic:
rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫
      Hom.stalkMap α ((ConcreteCategory.hom (α ≫ β).base) x) ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X).c.app U = X.presheaf.map (𝟙 U)

Tactic:
rw [id_c, map_id]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X.presheaf).app U = 𝟙 (X.presheaf.obj U)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
⊢ (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x) =
    (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y)

Tactic:
apply section_ext X.sheaf (V x ⊓ V y)

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
⊢ ∀ (x_1 : ↑↑X.toPresheafedSpace) (hx : x_1 ∈ V x ⊓ V y),
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x)) =
      (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) =
    eqToHom ⋯
eq₂ :
  eqToHom ⋯ ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯)
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
        ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
reassoc_of% eq₁

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) =
    eqToHom ⋯
eq₂ :
  eqToHom ⋯ ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯)
⊢ eqToHom ⋯ ≫ ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (X.restrict ⋯).presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
by
  dsimp
  rw [Opens.inclusion'_top_functor X.carrier]
  rfl

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

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

Tactic:
rw [this]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsOpen ↑(X.basicOpen i)

Tactic:
exact Opens.isOpen (X.basicOpen i)

Goal state after:
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ᵒᵖ) →
    ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).obj
        X ≅
      (componentwiseDiagram F U).obj X

Tactic:
intro X
    refine (F.obj (unop X)).presheaf.mapIso (eqToIso ?_)
    simp only [Functor.op_obj, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
      Set.preimage_preimage]
    refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
    simp only [colimitCocone, colimit, ← TopCat.comp_app]
    congr
    exact ι_preservesColimitIso_inv (forget C) F (unop X)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = appLE f U (f ⁻¹ᵁ U) ⋯

Tactic:
simp [Hom.appLE]

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

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

Tactic:
rw [this]

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 : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base = s.fst.base

Tactic:
change pullback.lift _ _ _ ≫ pullback.fst _ _ = _

Goal state after:
case refine_1
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
⊢ pullback.lift s.fst.base s.snd.base ⋯ ≫ pullback.fst f.base g.base = s.fst.base
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.snd.c.app x

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

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((pullbackConeOfLeft f g).snd.c.app x ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x
Module: Mathlib.AlgebraicGeometry.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:
simp [Set.range_comp_subset_range]

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

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

Tactic:
rw [this]

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

Goal state before:
pp: X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
⊢ X.OpenCover

Tactic:
by
  have :=
    @CompactSpace.elim_nhds_subcover _ _ H (fun x : X => Set.range (𝒰.f (𝒰.idx x)))
      fun x => (IsOpenImmersion.isOpen_range (𝒰.f (𝒰.idx x))).mem_nhds (𝒰.covers x)
  let t := this.choose
  have h : ∀ x : X, ∃ y : t, x ∈ Set.range (𝒰.f (𝒰.idx y)) := by
    intro x
    have h' : x ∈ (⊤ : Set X) := trivial
    rw [← Classical.choose_spec this, Set.mem_iUnion] at h'
    rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩
    exact ⟨⟨y, hy⟩, hy'⟩
  exact
    { I₀ := t
      X := fun x => 𝒰.X (𝒰.idx x.1)
      f := fun x => 𝒰.f (𝒰.idx x.1)
      mem₀ := by
        rw [presieve₀_mem_precoverage_iff]
        exact ⟨h, inferInstance⟩ }

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

Goal state before:
pp: case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    inv
        (f.stalkMap
          ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x)) ≫
      eqToHom ⋯ ≫
        g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))

Tactic:
rw [this]

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

Tactic:
rw [this]

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 ⋯))
      x =
    inv
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
          ((ConcreteCategory.hom
              (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                  (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)).base)
            x)) ≫
      eqToHom ⋯ ≫ s.snd.stalkMap x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (inv
          (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
            ((ConcreteCategory.hom
                (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                    (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)).base)
              x)) ≫
        eqToHom ⋯ ≫ s.snd.stalkMap x))
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 V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯) =
    ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)

Tactic:
F.map_comp

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) ⋯) =
    ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)
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
U : Opens ↑(PrimeSpectrum.Top R)
x✝¹ : R
x✝ : M
⊢ const (x✝¹ • x✝) 1 U ⋯ = (RingHom.id R) x✝¹ • const x✝ 1 U ⋯

Tactic:
simp [smul_const]

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

Goal state before:
pp: X : TopCat
F : Sheaf CommRingCat X
U V W UW VW : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
h₁ : UW = U ⊓ W
h₂ : VW = V ⊓ W
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y ↔
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y ∧
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y

Tactic:
by
  subst h₁ h₂
  constructor
  · rintro rfl
    rw [← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]
    simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
      homOfLE_comp, and_self]
  · rintro ⟨e₁, e₂⟩
    refine F.eq_of_locally_eq₂
      (homOfLE (inf_le_right : U ⊓ W ≤ W)) (homOfLE (inf_le_right : V ⊓ W ≤ W)) ?_ _ _ ?_ ?_
    · rw [← inf_sup_right]
      exact le_inf e le_rfl
    · rw [← e₁, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst]
      simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
        homOfLE_comp]
    · rw [← e₂, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]
      simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
        homOfLE_comp]

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) + (n ↑i ↑j + 1)) • g ↑j • f ↑i =
    (g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1) + (n ↑i ↑j + 1)) • g ↑i • f ↑j

Tactic:
pow_add,

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.Restrict

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = ↑(𝒰.f i ⁻¹ᵁ U)

Tactic:
exact Subtype.range_val

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op (basicOpen 1)))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen 1)) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj (basicOpen 1)).leTop.op
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤) =
    𝟙 (Γ.obj (op X))

Tactic:
rw! [basicOpen_one] at this

Goal state after:
X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op ⊤) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤) =
    𝟙 (Γ.obj (op X))