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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
f : SkewMonoidAlgebra k G
⊢ ((lift k G A) F) f = f.sum fun a b ↦ b • F a

Tactic:
by simp [lift_apply', Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

Tactic:
intro h
    induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
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✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
hy✝ : b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
ha : (mkRingHom r) a = 0
⊢ (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0

Tactic:
hb

Goal state after:
case refine_3
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✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
hy✝ : b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
ha : (mkRingHom r) a = 0
hb : (mkRingHom r) b = 0
⊢ (mkRingHom r) (a + b) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (((monomial 1) 1).sum fun a₁ b₁ ↦ p.sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)) =
    (p.sum fun a b ↦ (monomial a) (φ b)).sum fun a₁ b₁ ↦
      ((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)

Tactic:
rw [sum_monomial_index (by simp), sum_sum_index (by simp) (by simp)]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (p.sum fun a₂ b₂ ↦ (monomial (1 + a₂)) (1 * (⇑φ)^[1] b₂)) =
    p.sum fun a b ↦
      ((monomial a) (φ b)).sum fun a₁ b₁ ↦ ((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
r : k
x a : G
⊢ a * 1 = x ↔ a = x

Tactic:
by rw [mul_one]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ r • (of k G) g = single g r

Tactic:
by
  rw [of_apply, smul_single, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
r : k
f : SkewMonoidAlgebra A G
⊢ (singleOneRingHom.comp (algebraMap k A)) r * f = f * (singleOneRingHom.comp (algebraMap k A)) r

Tactic:
ext
    simp only [singleOneRingHom, singleAddHom, ZeroHom.toFun_eq_coe, ZeroHom.coe_mk, RingHom.coe_mk,
      MonoidHom.coe_mk, OneHom.coe_mk, coeff_single_one_mul, Algebra.commutes, coeff_mul_single_one,
      smul_algebraMap, RingHom.coe_comp, comp_apply]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base, c := c' }.c
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
dsimp at h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case inst
X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (f.stalkMap x).hom'

pp: case inst
X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (g.stalkMap ((ConcreteCategory.hom f.base) x)).hom'

Tactic:
all_goals apply isLocalHomValStalkMap

Goal state after:
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₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ 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 ⋯).op
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
rw [eqToHom_op, eqToHom_map] at 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 ⋯)
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op 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
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) (g x) =
    (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) (g y)

Tactic:
← map_mul,

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
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x) =
    (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) (g y)
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
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) 1 =
    (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) ((ConcreteCategory.hom (X.presheaf.map (iVU y).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) (g y)

Tactic:
← map_mul,

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
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) 1 =
    (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) ((ConcreteCategory.hom (X.presheaf.map (iVU y).op)) f * g y)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsOpen {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ x ∈ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)},
    ∃ t ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}, IsOpen t ∧ x ∈ t
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

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

Tactic:
rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C ((Opens.inclusionTopIso ↑X).inv ≫ (X.ofRestrict ⋯).base)).obj X.presheaf
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

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ᵒᵖ
⊢ ((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
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case naturality
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)
⊢ autoParam
    (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y),
      ((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))).map
            f ≫
          (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =
        (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f)
    NatIso.ofComponents._auto_1

Tactic:
intro X

Goal state after:
case naturality
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ᵒᵖ
⊢ ∀ {Y : Jᵒᵖ} (f : X ⟶ Y),
    ((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))).map
          f ≫
        (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =
      (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom g.base) ⁻¹' ⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base) '' ↑U =
    ⇑(ConcreteCategory.hom f.base) '' ↑U

Tactic:
rw [Set.image_comp, Set.preimage_image_eq _ hg.base_open.injective]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n) * (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
← map_mul,

Goal state after:
X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n * f) = 0
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s) ↔
    (Spec R).zeroLocus
        (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s) =
      PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

Tactic:
Set.image_preimage_eq

Goal state after:
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s) ↔
    (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

case h
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
x : X
⊢ ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom ((E.restrictIndex i).f i_1))

Tactic:
use x, y x, hy x

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ ∀ {X Y S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : Type u_2
⊢ ∀ {Y S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))
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
⊢ IsOpenImmersion (pullback.snd f g)

Tactic:
by
  delta pullback.snd
  rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (X Y S : Scheme) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)

Tactic:
intro X

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

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

Tactic:
by
  delta pullback.snd
  rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
  infer_instance

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

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
  · rintro _ ⟨a, rfl⟩
    exact IsOpenImmersion.isOpen_range (X.affineBasisCover.f a)
  · rintro a U haU hU
    rcases X.affineCover.covers a with ⟨x, e⟩
    let U' := (X.affineCover.f (X.affineCover.idx a)) ⁻¹' U
    have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
    rcases PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU'
        ((X.affineCover.f (X.affineCover.idx a)).continuous.isOpen_preimage _
          hU) with
      ⟨_, ⟨_, ⟨s, rfl⟩, rfl⟩, hxV, hVU⟩
    refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩ <;> rw [affineBasisCover_map_range]
    · exact ⟨x, hxV, e⟩
    · rw [Set.image_subset_iff]; exact hVU

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
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := ⋯
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
x : ↑X
hx : x ∈ unop U
⊢ (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) t *
      (CommRingCat.Hom.hom (F.presheaf.germ (unop U) ↑⟨x, hx⟩ ⋯)) s =
    0

Tactic:
← map_mul,

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
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
x : ↑X
hx : x ∈ unop U
⊢ (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) (t * s) = 0
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have e₁ := Scheme.Hom.congr_app (X.homOfLE_ι e) (V.ι ''ᵁ W)

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mp
X : TopCat
F : Sheaf CommRingCat X
U V W : 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))))))
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) ∧
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))

Tactic:
← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd

Goal state after:
case mp
X : TopCat
F : Sheaf CommRingCat X
U V W : 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))))))
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) ∧
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))