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

Goal state before:
pp: case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
exact IsSumNonzeroSq.sq_add ne_a (ih ne_s)

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

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ f.support.erase a

Tactic:
Finset.mem_erase

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective ⇑(mkRingHom r)

Tactic:
simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective fun x ↦ { toQuot := Quot.mk (Rel r) x }
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective ⇑(mkRingHom r)

Tactic:
by
  simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
  rintro ⟨⟨⟩⟩
  simp

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
mul_comm : IsMulCommutative (CentroidHom α)
x✝² x✝¹ : CentroidHom α
x✝ : α
⊢ (star (x✝² * x✝¹)) x✝ = (star x✝¹ * star x✝²) x✝

Tactic:
by simp [mul_comm']

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : ↑↑X
hx : (ConcreteCategory.hom α.base) x ∈ U
⊢ Y.presheaf.germ U ((ConcreteCategory.hom α.base) x) hx ≫ Hom.stalkMap α x =
    α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx

Tactic:
rw [Hom.stalkMap, stalkFunctor_map_germ_assoc, stalkPushforward_germ]

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

Goal state before:
pp: case h
X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
carrier✝ : Set ↑↑X.toPresheafedSpace
is_open'✝ : IsOpen carrier✝
x : ↑(X.presheaf.obj (op { carrier := carrier✝, is_open' := is_open'✝ }))
⊢ (CommRingCat.Hom.hom
        ((f.c ≫ whiskerRight (eqToHom ⋯) ∅.presheaf).app (op { carrier := carrier✝, is_open' := is_open'✝ })))
      x =
    (CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier✝, is_open' := is_open'✝ }))) x

Tactic:
cat_disch

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
x✝ : n = 0 ∨ n > 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
cases n.eq_zero_or_pos with

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

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

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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

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

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case e'_7.e'_3.e'_6
X Y : Scheme
f : X.Hom Y
x : ↥X
e_3✝ :
  (↑(Y.presheaf.stalk ((ConcreteCategory.hom (ofHom { toFun := ⇑f, continuous_toFun := ⋯ })) x)) →+*
      ↑(X.presheaf.stalk x)) =
    (↑(Y.presheaf.stalk (f x)) →+* ↑(X.presheaf.stalk x))
e_1✝ :
  Y.presheaf.stalk ((ConcreteCategory.hom (ofHom { toFun := ⇑f, continuous_toFun := ⋯ })) x) = Y.presheaf.stalk (f x)
e_5✝ : ofHom { toFun := ⇑f, continuous_toFun := ⋯ } ≍ f.toLRSHom'.1.base
⊢ f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom = f.toLRSHom'.1.c

Tactic:
cat_disch

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))
⊢ f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom = f₃

Tactic:
cat_disch

Goal state after:
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✝ } ≫
          colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ } ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False

Tactic:
TopCat.sigmaIsoSigma_hom_ι

Goal state after:
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
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
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
x : ↥X
⊢ (ConcreteCategory.hom (((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict ⋯).base)) ⟨x, ⋯⟩ = x

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy✝⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy✝⟩

Tactic:
obtain ⟨hgy, H⟩ := hfg ⟨y, hg'U hy.1⟩

Goal state after:
case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
hgy : g ∉ (↑⟨y, ⋯⟩).asIdeal
H : (fun x ↦ ↑s (iVU x)) ⟨y, ⋯⟩ = LocalizedModule.mk f ⟨g, hgy⟩
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy✝⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy✝⟩
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
⊢ const (f * g) (f * g) U ⋯ = 1

Tactic:
const_self

Goal state after:
R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
⊢ 1 = 1
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R), f.unop ≫ (x * y) = f.unop ≫ x * f.unop ≫ y

Tactic:
cat_disch

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 : R
f : M
n : ℕ
⊢ (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
        (toOpenₗ R M (basicOpen s)) ⋯)
      (LocalizedModule.mk (⟨(fun x ↦ s ^ x) n, ⋯⟩ • f) ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯

Tactic:
LocalizedModule.mk_cancel,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
        (toOpenₗ R M (basicOpen s)) ⋯)
      (LocalizedModule.mk f 1) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R), f.unop ≫ (x + y) = f.unop ≫ x + f.unop ≫ y

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑((X.homOfLE e) x) = ↑x

Tactic:
by
  rw [Scheme.homOfLE_apply']

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
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x = stalkMap (resLE f U V e ≫ U.ι) x

Tactic:
stalkMap_congr_hom _ _ (resLE_comp_ι f e),

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    (Y.presheaf.stalkCongr ⋯).hom ≫ stalkMap (V.ι ≫ f) x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = X.toRingedSpace.zeroLocus s

Tactic:
simp only [RingedSpace.zeroLocus]
  have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
      (SetLike.coe (X.toRingedSpace.basicOpen i))ᶜ =
        X.toΓSpec.base ⁻¹' ((PrimeSpectrum.basicOpen i).carrier)ᶜ := by
    symm
    rw [Set.preimage_compl, Opens.carrier_eq_coe]
    erw [X.toΓSpec_preimage_basicOpen_eq i]
  erw [Set.iInter₂_congr this]
  simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    compl_compl]
  rw [← PrimeSpectrum.zeroLocus_iUnion₂]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case init.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none) (xj : F.obj (some i)),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some i)))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_eq']

Goal state after:
case init.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none),
    ∃ l fli flj x,
      (ConcreteCategory.hom (F.map fli)) x = xi ∧
        (ConcreteCategory.hom (F.map flj)) x = (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi
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:
toStalkₗ',

Goal state after:
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 =
    ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).germ ⊤ x _root_.trivial
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
        (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
      (LocalizedModule.mk (s • f) s) =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
LocalizedModule.mk_cancel,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
        (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
      (LocalizedModule.mk f 1) =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ toStalkₗ' R M x ≫ stalkToLocalizationₗ R M x = ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
toStalkₗ',

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).germ ⊤ x _root_.trivial) ≫
      stalkToLocalizationₗ R M x =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r))

Tactic:
exact hU.basicOpen _

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
⊢ (comapFun f y) (LocalizedModule.mk (b • a) b) = σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
LocalizedModule.mk_cancel,

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.mk a 1) = σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
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
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑(r * s) ⟨PrimeSpectrum.comap f ↑p, ⋯⟩) =
    (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑r ⟨PrimeSpectrum.comap f ↑p, ⋯⟩) *
      (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)

Tactic:
exact (Localization.localRingHom ..).map_mul _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan 0 X), s.snd ≫ 0 = s.fst

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan X 0), s.fst ≫ 0 = s.snd

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan 0 X), 0 ≫ s.inr = s.inl

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan X 0), 0 ≫ s.inl = s.inr

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply glued_cover_cocycle_fst

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))

Tactic:
have := Hom.stalkMap_congr_hom _ _ (𝒰.ι_fromGlued i) x

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this : Hom.stalkMap ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
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.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp_rw [Category.assoc, cocycle_fst_fst_snd 𝒰 f g i j k]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ (Opens.map (D.ι j).base).obj (⋯.functor.obj U) =
    (opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))

Tactic:
ext1
  dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj]
  rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) i, ←
    show _ = (𝖣.ι j).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) j]
  rw [TopCat.coe_comp, TopCat.coe_comp, Set.image_comp, Set.preimage_comp, Set.preimage_image_eq]
  · refine Eq.trans (D.toTopGlueData.preimage_image_eq_image' _ _ _) ?_
    dsimp
    rw [Set.image_comp]
    refine congr_arg (_ '' ·) ?_
    rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]
    swap
    · exact CategoryTheory.ConcreteCategory.bijective_of_isIso (C := TopCat) _
    change (D.t i j ≫ D.t j i).base '' _ = _
    rw [𝖣.t_inv]
    simp
  · rw [← TopCat.mono_iff_injective]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : Subsingleton ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine ↑U
hxU : x ∈ ↑U
y : ↥X
⊢ y ∈ ↑U ↔ y ∈ ↑⊤

Tactic:
simpa [Subsingleton.elim y x]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ IsOpenMap (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

Tactic:
· rw [isOpenMap_sigma]
      intro i
      simpa [← Scheme.Hom.comp_apply] using (α i).isOpenEmbedding.isOpenMap

Goal state after: