mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ ↑(s, ⟨r, hpr⟩ ^ n).2 • y = (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1

Tactic:
Algebra.smul_def,

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ (algebraMap ↑R
          ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).obj).stalk
              p))
        ↑(s, ⟨r, hpr⟩ ^ n).2 *
      y =
    (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Γ(Spec Γ(X, V), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom h).op) ⁻¹ᵁ W)

Tactic:
by cases h; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
x : ↑X.toTopCat
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
h₂ : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom (X.ofRestrict ⋯).base) = Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
exact Subtype.range_coe_subtype

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

Goal state before:
pp: X : Type u_1
R S : Presieve X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
x✝ : S ∈ jointlySurjectivePrecoverage.coverings X
x : X
Y : Type u_1
f : Y ⟶ X
hf : R f
hx : x ∈ Set.range ⇑(ConcreteCategory.hom f)
⊢ ∃ Y g, (R ⊔ S) g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
use Y, f, .inl hf

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : MorphismProperty C
⊢ P.precoverage.morphismProperty = P

Tactic:
by
  ext X Y f
  exact ⟨fun ⟨R, hR, hf⟩ ↦ hR hf, fun hf ↦ ⟨.singleton f, by simpa⟩⟩

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
f : R
⊢ Function.Injective ⇑(toBasicOpenₗ R M f)

Tactic:
intro s t h_eq

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s t : LocalizedModule.Away f M
h_eq : (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) t
⊢ s = t
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ X.toΓSpecFun ⁻¹' ↑(basicOpen r) = ↑(X.toRingedSpace.basicOpen r)

Tactic:
by
      ext
      dsimp
      simp only [Set.mem_preimage, SetLike.mem_coe]
      rw [X.toRingedSpace.mem_top_basicOpen]
      exact notMem_prime_iff_unit_in_stalk ..

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
        f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r))))
⊢ CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)

Tactic:
exact IsLocalization.ringHom_ext (Submonoid.powers r) h

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t *
      (ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t')

Tactic:
exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _

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
x : ↑(PrimeSpectrum.Top R)
r : R
α : Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R M).presheaf.obj (op U))
this✝ :
  Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
    (forget₂ (ModuleCat R) Ab).map ((structurePresheafInModuleCat R M).germ U x hxU)
this :
  ∀ (m : ↑((moduleStructurePresheaf R M).presheaf.obj (op U))),
    (ConcreteCategory.hom α.hom)
        ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m) =
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) m
⊢ (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) (r • s) =
    r • (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) s

Tactic:
exact ((structurePresheafInModuleCat R M).germ U x hxU).hom.map_smul _ _

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ MorphismProperty.isomorphisms C (equalizer.ι f g)

Tactic:
(MorphismProperty.isomorphisms C).iff_of_zeroHypercover_target (𝒰.pullback₁ s)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀),
    MorphismProperty.isomorphisms C (pullback.snd (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen (f * x) =
    X.basicOpen
      (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩))

Tactic:
Algebra.smul_def,

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen (f * x) =
    X.basicOpen
      ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x *
        ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' U)

Tactic:
by
  delta CategoryTheory.GlueData.ι
  simp_rw [← Multicoequalizer.ι_sigmaπ 𝖣.diagram]
  rw [← (homeoOfIso (Multicoequalizer.isoCoequalizer 𝖣.diagram).symm).isOpen_preimage]
  rw [coequalizer_isOpen_iff, colimit_isOpen_iff.{u}]
  tauto

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
← isoSpec_inv_preimage_zeroLocus,

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

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ (↑U).basicOpen ((hom U.topIso.inv) r) = (↑U).basicOpen ((hom (X.presheaf.map (homOfLE ⋯).op)) r)

Tactic:
← Scheme.basicOpen_res_eq _ _ (eqToHom U.ι_preimage_self.symm).op,

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ (↑U).basicOpen ((hom U.topIso.inv) r) =
    (↑U).basicOpen ((hom ((↑U).presheaf.map (eqToHom ⋯).op)) ((hom (X.presheaf.map (homOfLE ⋯).op)) r))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap g.hom x))

Tactic:
PresheafedSpace.stalkMap.congr_hom _ _ (congr_arg InducedCategory.Hom.hom H.symm) x

Goal state after:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f.hom x))
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
apply pullback.hom_ext
      · simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]
      · 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:
by
  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.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.snd (D.f k i) (D.f k j))
          (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U))))) ≫
        (D.t j k).c.app
            (op
              ((opensFunctor (pullback.snd (D.f k i) (D.f k j))).obj
                (unop
                  (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U))))))) ≫
          ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
snd_invApp_t_app_assoc,

Goal state after:
case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      (D.t' j k i).c.app
          (op (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
        invApp (pullback.fst (D.f j k) (D.f j i))
            ((Opens.map (D.t' j k i).base).1
              (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
            ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ (Hom.opensRange ι₁ ⊔ Hom.opensRange ι₂) ⊓ U = U

Tactic:
(isCompl_opensRange_inl_inr X Y).sup_eq_top,

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ ⊤ ⊓ U = U
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
S : CommRingCatᵒᵖ
R : CommRingCat
⊢ IsIso (coprodComparison Scheme.Spec (op R) S)

Tactic:
obtain ⟨S⟩ := S

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ IsIso (coprodComparison Scheme.Spec (op R) (op S))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
erw [IsOpenImmersion.lift_fac_assoc]

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

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

Tactic:
rw [← cancel_mono (𝖣.ι j), Category.assoc, ← (𝖣.vPullbackCone i j).condition]
      conv_rhs => rw [← s.condition]
      erw [IsOpenImmersion.lift_fac_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
this : (glueData F).ι i ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (glueData F).ι ((equivShrink J) ↓i)
⊢ colimit.ι F ↓i ≫ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv = (glueData F).ι i

Tactic:
simp [cocone, eqToHom_map, ← this]

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

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
s : ↥S
⊢ s ∈ Set.range ⇑f ↔ s ∈ Set.range ⇑g

Tactic:
by
  rw [range_eq_range_of_surjective f g e hge]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom ↑includeRight) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
← pullbackSpecIso_inv_snd,

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫
      (pullbackSpecIso R S T).inv ≫
        pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
⊢ P.universally (𝒰.f i ≫ f)

Tactic:
apply MorphismProperty.universally_mk'
    intro T g _
    rw [← P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso g f _).hom,
      pullbackLeftPullbackSndIso_hom_fst]
    exact IsZariskiLocalAtSource.comp (hf _ _ _ (IsPullback.of_hasPullback ..)) _

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))

Tactic:
let Sₐ (a : s) := Localization (Mₐ a)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
⊢ IsClosedMap ⇑f

Tactic:
change topologically @IsClosedMap f

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
⊢ topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
by
  have := (hU.isLocalization_basicOpen f).1.2
  obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x
  use n, y
  simpa [mul_comm x] using! d.symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
this : q.IsPrime
⊢ 1 ≤ q.height

Tactic:
rw [Order.one_le_iff_ne_zero, Ne, height_eq_zero_iff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
this : q.IsPrime
⊢ q ∉ minimalPrimes R