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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
⊢ (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
by
  classical
  let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
  calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : ↥U) → T ↑x
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
x : ↥V
⊢ ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)

Tactic:
specialize w (i x)

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : ↥U) → T ↑x
x : ↥V
w : ∃ V_1, ∃ (_ : ↑(i x) ∈ V_1), ∃ i, P.pred fun x ↦ f (i x)
⊢ ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: 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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) (op j) =
    (colimit.ι F j).c.app (op U)

Tactic:
rw [← Iso.eq_inv_comp, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app]

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

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ Y.presheaf.map (⋯.functor.map i.unop).op ≫ f.c.app (op ((opensFunctor f).obj (unop V))) ≫ X.presheaf.map (eqToHom ⋯) =
    (f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯)) ≫
      X.presheaf.map ((Opens.map (𝟙 ↑X)).map i.unop).op

Tactic:
simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj,
        TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op, Category.assoc]

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ f.c.app (op (⋯.functor.obj (unop U))) ≫
      X.presheaf.map ((Opens.map f.base).map (⋯.functor.map i.unop)).op ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op ((opensFunctor f).obj (unop U))) ≫
      X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map ((Opens.map (𝟙 ↑X)).map i.unop).op
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
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso (Hom.stalkMap f x)

Tactic:
rw [← H.isoRestrict_hom_ofRestrict, PresheafedSpace.stalkMap.comp]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f.hom x)
U : Opens ↑↑X.toPresheafedSpace
⊢ IsIso (f.hom.c.app (op (hf.functor.obj U)))

Tactic:
apply +allowSynthFailures TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
          (show Y.sheaf ⟶ (TopCat.Sheaf.pushforward _ f.hom.base).obj X.sheaf from ⟨f.hom.c⟩)

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f.hom x)
U : Opens ↑↑X.toPresheafedSpace
⊢ ∀ (x : ↥(hf.functor.obj U)),
    IsIso
      ((TopCat.Presheaf.stalkFunctor C ↑x).map
        (have this := { hom := f.hom.c };
          this).hom)
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
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop U) ↑x ⋯)) (S ↑x) ≤
    Submonoid.comap (CommRingCat.Hom.hom (F.map i))
      (⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) (S ↑x))

Tactic:
intro s hs
    simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢
    intro x
    change (F.map i.unop.op ≫ F.germ V.unop x.1 x.2) s ∈ _
    rw [F.germ_res]
    exact hs ⟨_, i.unop.le x.2⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (X.homOfLE e).base = (Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e)

Tactic:
by
  ext a; refine Subtype.ext ?_ -- Porting note: `ext` did not pick up `Subtype.ext`
  exact congr($(X.homOfLE_ι e) a)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case mpr
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
y : ↥↑V
hyW : y ∈ ↑W
hyU : (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base) y ∈ ↑U
⊢ (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base) y ∈ ↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W)

Tactic:
exact ⟨⟨y.1, hyU⟩, by simpa [homOfLE_apply'] using hyW, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (asIso t ≪≫ pullbackRestrictIsoRestrict f V).hom ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (pullback.snd f g)).hom ≫ e.hom

Tactic:
Iso.trans_hom,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ ((asIso t).hom ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (pullback.snd f g)).hom ≫ e.hom
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Tactic:
refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
    (Spec.basicOpen_hom_ext w ?_)

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
⊢ ∀ (r : ↑R),
    let U := basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
          (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op U)) ≫
        (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
        (forgetToSheafedSpace.map β).hom.c.app (op U)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y : C
f : X ⟶ Y
𝒰 : PreZeroHypercover Y
hR : 𝒰.presieve₀ ∈ K.coverings Y
⊢ (∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀),
      P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))) ↔
    ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)

Tactic:
have _ (i) : HasPullback (𝒰.f i) f := (Precoverage.hasPullbacks_of_mem _ hR).hasPullback ⟨i⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y : C
f : X ⟶ Y
𝒰 : PreZeroHypercover Y
hR : 𝒰.presieve₀ ∈ K.coverings Y
x✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i) f
⊢ (∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀),
      P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))) ↔
    ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
⊢ P snd

Tactic:
have : HasPullback f (𝒰.f i) := h.hasPullback
  rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
  exact pullbackSnd 𝒰.mem₀ ⟨i⟩ hf

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

Tactic:
let := Module.compHom N σ

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 σ
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
let := Module.compHom N σ

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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this : Module R N := Module.compHom N σ
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom
        ((forget TopCat).map (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      x =
    (ConcreteCategory.hom
        ((forget TopCat).map (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      y

Tactic:
ConcreteCategory.forget_map_eq_ofHom,

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom
        (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      x =
    (ConcreteCategory.hom
        (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
⊢ f = g

Tactic:
have : Mono φ := ConcreteCategory.mono_of_injective _ hφ

Goal state after:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ f = g
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(X.isoSpec.inv ≫ X.toSpecΓ) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
X.isoSpec_inv_toSpecΓ

Goal state after:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(𝟙 (Spec Γ(X, ⊤))) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑U.toSpecΓ ⁻¹' PrimeSpectrum.zeroLocus s = U.carrier ↓∩ X.zeroLocus s

Tactic:
ext x
  refine .trans (forall₂_congr fun y hy ↦ ?_) Set.mem_iInter₂.symm
  exact iff_not_comm.mp congr(x ∈ $(Opens.toSpecΓ_preimage_basicOpen U y)).to_iff.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom) =
    (D.ι i).base

Tactic:
PresheafedSpace.forget_map,

Goal state after:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i).base ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom) =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i).base ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom) =
    (D.ι i).base

Tactic:
PresheafedSpace.forget_map,

Goal state after:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i).base ≫
      (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) = (fromGlued 𝒰) (((gluedCover 𝒰).ι j) y)
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply] at h

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h :
  (ConcreteCategory.hom (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base)) x =
    (ConcreteCategory.hom (((gluedCover 𝒰).ι j).base ≫ (fromGlued 𝒰).base)) y
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: 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 ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
by
  simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
    pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
    pullbackRightPullbackFstIso_hom_fst_assoc]

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)
⊢ ⇑(ConcreteCategory.hom (D.t i j ≫ D.t j i).base) '' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
rw [𝖣.t_inv]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (𝟙 (D.V (i, j))).base) '' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m ≪≫ pullback.congrHom h₁ ⋯).hom ≫ pullback.fst s.fst (𝒰.f i) ≫ m =
    (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m ≪≫ pullback.congrHom h₁ ⋯).hom ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i

Tactic:
Iso.trans_hom,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫ (pullback.congrHom h₁ ⋯).hom) ≫
      pullback.fst s.fst (𝒰.f i) ≫ m =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫ (pullback.congrHom h₁ ⋯).hom) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
inst✝ : IsAffine Z✝
⊢ of P f✝ → of P (e✝.hom ≫ f✝)

Tactic:
apply MorphismProperty.RespectsIso.precomp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case restrict
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), targetAffineLocally Q f → targetAffineLocally Q (f ∣_ U)

Tactic:
intro X Y f U H V

Goal state after:
case restrict
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : targetAffineLocally Q f
V : ↑(↑U).affineOpens
⊢ Q (f ∣_ U ∣_ ↑V)
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 : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))

Tactic:
ext j
  induction j with | op j => ?_
  rcases j with (⟨j, k⟩ | ⟨j⟩)
  · rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),
      ← Category.assoc, Category.id_comp]
    congr 1
    simp_rw [Category.assoc]
    apply π_ιInvApp_π
  · simp_rw [Category.assoc]
    rw [Category.id_comp]
    apply π_ιInvApp_π

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

Goal state before:
pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ ∀ {m : s.pt ⟶ (D.vPullbackCone i j).pt},
    m ≫ (D.vPullbackCone i j).fst = s.fst → m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯

Tactic:
· intro m e₁ _
      rw [← cancel_mono (D.f i j)]
      simp only [lift_fac]
      tauto

Goal state after: