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

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
⊢ (Function.support fun g' ↦ A ((coeff B g') u)) ⊆ Function.support ((of R).symm (B u)).coeff

Tactic:
simp only [coeff_apply_apply, Function.support_subset_iff, ne_eq, Function.mem_support]

Goal state after:
Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
⊢ ∀ (x : Γ'), ¬A (((of R).symm (B u)).coeff x) = 0 → ¬((of R).symm (B u)).coeff x = 0
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ (A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝ =
    (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ + (A (((of R).symm (B v)).coeff x✝¹)).coeff x✝

Tactic:
← HahnSeries.coeff_add

Goal state after:
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ (A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝ =
    (A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝
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 g : X ⟶ Y
h : f.hom.base = g.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap f.hom x = (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g.hom x
⊢ f = g

Tactic:
by
  obtain ⟨f, fc⟩ := f
  obtain ⟨g, gc⟩ := g
  obtain rfl : f = g := h
  congr
  ext U s
  refine section_ext X.sheaf _ _ _ fun x hx ↦
    show X.presheaf.germ _ x _ _ = X.presheaf.germ _ x _ _ from ?_
  erw [← PresheafedSpace.stalkMap_germ_apply ⟨f, fc⟩, ← PresheafedSpace.stalkMap_germ_apply ⟨f, gc⟩]
  simp [h']

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.inv.base ≫ e.hom.base = 𝟙 ↑Y.toPresheafedSpace

Tactic:
simp only [← comp_base, Iso.inv_hom_id, id_toHom, PresheafedSpace.id_base]

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

Goal state before:
pp: case h
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
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
⊢ m.c ≫ whiskerRight (eqToHom ⋯) (colimitCocone F).pt.presheaf = (desc F s).c

Tactic:
refine NatTrans.ext (funext fun U => limit_obj_ext fun j => ?_)
      simp [desc, descCApp,
        PresheafedSpace.congr_app (w (unop j)).symm U,
        NatTrans.congr (limit.π (pushforwardDiagramToColimit F).leftOp j)
        (congr_arg op (Functor.congr_obj (congr_arg Opens.map t) (unop U)))]

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
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.ofRestrict ⋯ ≫ X.toRestrictTop).c ≫ whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
· erw [comp_c, toRestrictTop_c, whiskerRight_id',
        comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans, eqToHom_refl]
      rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ sheafedSpaceMap (𝟙 R) = 𝟙 (sheafedSpaceObj R)

Tactic:
ext : 1
  · exact Spec.topMap_id R
  · ext
    dsimp
    rw [comap_id (by simp)]
    simp
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha :
  IsUnit
    (↑(stalkIso (↑S) p)
      ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯)
        ((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm a)))
⊢ IsUnit a

Tactic:
have : IsLocalHom (stalkIso S p) := isLocalHom_equiv _

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha :
  IsUnit
    (↑(stalkIso (↑S) p)
      ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯)
        ((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm a)))
this : IsLocalHom (stalkIso (↑S) p)
⊢ IsUnit a
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ f = (isoRestrict f).hom ≫ Y.ofRestrict ⋯

Tactic:
isoRestrict_hom_ofRestrict

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ f = 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)
⊢ IsIso (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

Tactic:
apply c_iso' f U

Goal state after:
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)
⊢ (Opens.map g.base).obj (h.functor.obj U) = (opensFunctor f).obj U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
h : toLRSHom f = toLRSHom g
⊢ f = g

Tactic:
by
  cases f; cases g; congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ app (eqToHom e) U = eqToHom ⋯

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
⊢ (∃ x_1, x ∈ X.basicOpen x_1) ↔ x ∈ U

Tactic:
exact ⟨fun ⟨f, hf⟩ ↦ X.basicOpen_le f hf, fun _ ↦ ⟨1, by rwa [X.basicOpen_of_isUnit isUnit_one]⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f).base) ⁻¹' Set.range ⇑i

Tactic:
exact h₁

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

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

Tactic:
delta pullback.snd

Goal state after:
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 (limit.π (cospan f g) WalkingCospan.right)
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)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso (pullback.snd f g).base

Tactic:
delta pullback.snd

Goal state after:
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)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso (limit.π (cospan f g) WalkingCospan.right).base
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:
delta pullback.snd

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.right)
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
R : CommRingCat
⊢ (∀ (x : ↥(Spec R)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
                    f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
                i)) ∧
    ∀
      (i :
        { I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.I₀),
      IsOpenImmersion
        ({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
          i)

Tactic:
refine ⟨fun x ↦ ⟨1, ?_⟩, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway⟩

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ x ∈
    Set.range
      ⇑({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
          1)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, TopCat.coe_comp, Set.range_comp,
      Set.range_eq_univ.mpr, Set.image_univ]

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

X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Function.Surjective
    ⇑(ConcreteCategory.hom
        ((inv (pullback.snd f g)).base ≫
          (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom))
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)
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
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ 1 • ⟨g j, ⋯⟩ • g i • f j = 1 • ⟨g i * g j, ⋯⟩ • f j

Tactic:
simp [Submonoid.smul_def, ← smul_assoc]; ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ∣_ U ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
delta morphismRestrict
  rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ∣_ U ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
by
  delta morphismRestrict
  rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]

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 V : Y.Opens
e : U = V
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ V)

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    (CommRingCat.ofHom
          (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        X.toΓSpecCApp (unop r)) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
rw [show algebraMap (Γ.obj (op X)) ((structureSheaf (Γ.obj (op X))).obj.obj _) = algebraMap _
      ((structureSheafInType (Γ.obj (op X)) (Γ.obj (op X))).obj.obj _) from rfl,
      X.toΓSpecCApp_spec r.unop]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    X.toToΓSpecMapBasicOpen (unop r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: ⊢ HasLimits AffineScheme

Tactic:
by
  have := Adjunction.has_colimits_of_equivalence Γ.{u}
  have : HasLimits AffineScheme.{u}ᵒᵖᵒᵖ := Limits.hasLimits_op_of_hasColimits
  exact Adjunction.has_limits_of_equivalence (opOpEquivalence AffineScheme.{u}).inverse

Goal state after:
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
f : R
x : M
⊢ (toOpenₗ R M (basicOpen f)) x =
    (↑(LinearEquiv.ofBijective (toBasicOpenₗ R M f) ⋯) ∘ₗ LocalizedModule.mkLinearMap (Submonoid.powers f) M) x

Tactic:
simp [toOpenₗ]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case id.init
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))
j : J
⊢ ∀ (xi : F.obj (some j)) (xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some j)))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

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

pp: case init.init
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 xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init 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_comm, forall_eq]
    exact fun x ↦ ⟨_, .init _, 𝟙 _, x, by simp⟩

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) (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

case init.init
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 xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ (equalizer.ι f g ≫ prod.lift f g) ≫ prod.fst = ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) ≫ prod.fst

Tactic:
simp [equalizer.condition f g]

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

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ (equalizer.ι f g ≫ prod.lift f g) ≫ prod.snd = ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) ≫ prod.snd

Tactic:
simp [equalizer.condition f g]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsLocalization (Submonoid.powers f) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
convert! StructureSheaf.IsLocalization.to_basicOpen _ f using 1

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
⊢ ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f))).toAlgebra =
    StructureSheaf.openAlgebra (↑Γ(X, U)) (op (PrimeSpectrum.basicOpen f))
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: 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
⊢ ⇑(hom π) ⁻¹' ⇑(hom π) '' U = U

Tactic:
by
  have lem : ∀ x y, Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U) := by
    rintro _ _ ⟨x⟩
    change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
    rw [H]
  have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U := by
    aesop (add safe constructors _root_.Equivalence)
  ext
  constructor
  · rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]
    rintro ⟨y, hy, e'⟩
    dsimp at e'
    have e'' :=
      (mono_iff_injective
            (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
        inferInstance
    refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem y _ (Quot.eqvGen_exact ?_))).mp hy
    apply e''
    convert! e'
  · exact fun hx => ⟨_, hx, rfl⟩

Goal state after:
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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (Localizations.comapFun f ↑x✝) (r • ↑m ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    σ r • (Localizations.comapFun f ↑x✝) (↑m ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)

Tactic:
rw [map_smulₛₗ, ← IsScalarTower.algebraMap_smul S]

Goal state after: