mathlib-initiative/mathlib-tactics huggingface dataset:
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:
← H.isoRestrict_hom_ofRestrict,

Goal state after:
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 ((isoRestrict f).hom ≫ Y.ofRestrict ⋯) x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ } ≤
    {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ }

pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ } ≤
    (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ }

Tactic:
· rintro _ ⟨_, h₁, h₂⟩
                    use (TopCat.pullbackIsoProdSubtype _ _).inv ⟨⟨_, _⟩, h₂⟩
                    simpa [(TopCat.pullbackIsoProdSubtype_inv_fst_apply),
                      (TopCat.pullbackIsoProdSubtype_inv_snd_apply)]

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ } ≤
    (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ }
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y✝ : Type u
f : X ⟶ Y✝
hf : ∀ (x : Y✝), ∃ Y g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
x : (fun X ↦ X) Y✝
Y : Type u
hx : x ∈ Set.range ⇑(ConcreteCategory.hom f)
⊢ ∃ a, (ConcreteCategory.hom f) a = x

Tactic:
exact hx

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
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
by
  have := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H
  have : IsIso (pullback.snd f g).base := by
    delta pullback.snd
    rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
    change IsIso (_ ≫ pullback.snd _ _)
    infer_instance
  apply to_iso

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i =
    (Precoverage.ZeroHypercover.pullback₁ (Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst

Tactic:
by
  simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, AffineOpenCover.openCover_X, AffineOpenCover.openCover_f,
    pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv, Iso.symm_inv, Category.assoc,
    PreZeroHypercover.pullback₁_f, pullbackSymmetry_inv_comp_fst, IsIso.inv_comp_eq,
    limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app,
    pullbackSymmetry_hom_comp_fst]
  convert!
    pullbackSymmetry_inv_comp_snd_assoc ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _) _ using 2
  exact pullbackRightPullbackFstIso_hom_snd _ _ _

Goal state after:
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
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ Set.range s ⊆ ↑x.asIdeal

Tactic:
Set.range_subset_iff

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
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ ∀ (y : ι), s y ∈ ↑x.asIdeal
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) 0

Tactic:
by rw [map_zero]; exact h i

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

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ?K₁ ≅ cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace

Tactic:
exact (diagramIsoCospan _).symm

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
g : ↥(Submonoid.powers s)
⊢ (toBasicOpenₗ R M s) (LocalizedModule.mk f g) = const f (↑g) (basicOpen s) ⋯

Tactic:
obtain ⟨_, n, rfl⟩ := g
  apply ((Module.End.isUnit_iff _).mp ((isUnit_basicOpen_end ..).pow n)).1 ?_
  rw [← map_pow]
  dsimp [toBasicOpenₗ]
  rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.mk_smul (S := .powers s) _ ⟨n, rfl⟩,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
    smul_const]
  dsimp [toOpenₗ]
  exact const_eq_const_of_smul_eq_smul (H := by simp) ..

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

Goal state before:
pp: case mpr
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y ∧
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y →
    (ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y

Tactic:
rintro ⟨e₁, e₂⟩
    refine F.eq_of_locally_eq₂
      (homOfLE (inf_le_right : U ⊓ W ≤ W)) (homOfLE (inf_le_right : V ⊓ W ≤ W)) ?_ _ _ ?_ ?_
    · rw [← inf_sup_right]
      exact le_inf e le_rfl
    · rw [← e₁, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst]
      simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
        homOfLE_comp]
    · rw [← e₂, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]
      simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
        homOfLE_comp]

Goal state after:
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))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      X.presheaf.map ((X.toΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r)).leTop.op ≫ eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
exact h r

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map ((Scheme.Hom.appTop (f ∣_ U) ≫ Scheme.Hom.appTop (X.homOfLE i)) ≫ X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι

Tactic:
morphismRestrict_appTop,

Goal state after:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map
        (((Scheme.Hom.app f (U.ι ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom ⋯).op) ≫ Scheme.Hom.appTop (X.homOfLE i)) ≫
          X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
this : (Hom.appTop X.toSpecΓ).op ≫ (ΓSpecIso Γ(X, ⊤)).inv.op = 𝟙 (op Γ(X, ⊤))
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
← IsIso.eq_comp_inv

Goal state after:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
x : (fun X ↦ X) X
⊢ (⇑(hom s.π) ∘ ⇑(hom f)) x = (⇑(hom s.π) ∘ ⇑(hom g)) x

Tactic:
exact ConcreteCategory.congr_hom s.condition x

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s✝ : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
m : R
s : ↥(PrimeSpectrum.comap f ↑p).asIdeal.primeCompl
⊢ (Localizations.comapFun f.toSemilinearMap ↑p) (LocalizedModule.mk m s) =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (LocalizedModule.mk m s)

Tactic:
| h m s =>

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
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
by rwa [hUV, PrimeSpectrum.comap_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ Ideal.span (Set.range f) = ⊤

Tactic:
rw [← V.prop.self_le_iSup_basicOpen_iff]

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ ↑V ≤ ⨆ f_1, X.basicOpen ↑f_1
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ unop ((Opens.map (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.obj (op U)) ≤
    unop ((Opens.map (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.obj (op U))

Tactic:
coequalizer.condition f.toShHom g.toShHom

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ unop ((Opens.map (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.obj (op U)) ≤
    unop ((Opens.map (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.obj (op U))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) x) = x✝

Tactic:
exact hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal

Tactic:
simp_rw [not_not]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ ↑x.asIdeal
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
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (D.ι i).base)

Tactic:
rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _, TopCat.coe_comp]
  exact (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).isOpenEmbedding.comp
      (D.toTopGlueData.ι_isOpenEmbedding i)

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

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

Tactic:
erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
    IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ←
    (D.V (i, k)).presheaf.map_comp, ← (D.V (i, k)).presheaf.map_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, k)).presheaf.map
        ((homOfLE ⋯).op ≫
          (opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map
              (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫
            eqToHom ⋯)
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 : ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = ((gluedCover 𝒰).ι j ≫ fromGlued 𝒰) y
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y

Tactic:
rw [ι_fromGlued, ι_fromGlued] at h

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) ≫ Hom.stalkMap ((gluedCover 𝒰).ι i) x =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))

Tactic:
← IsIso.eq_comp_inv

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
    ((X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
  have := Hom.stalkMap_congr_hom _ _ (𝒰.ι_fromGlued i) x
  rw [Hom.stalkMap_comp, ← IsIso.eq_comp_inv] at this
  rw [this]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) ((ulift 𝒰).f i) ≫ (ulift 𝒰).gluedCover.ι i ≫ (ulift 𝒰).fromGlued ≫ glueMorphisms 𝒰 f hf =
    pullback.fst (𝒰.f x) ((ulift 𝒰).f i) ≫ f x

Tactic:
glueMorphisms,

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) ((ulift 𝒰).f i) ≫
      (ulift 𝒰).gluedCover.ι i ≫
        (ulift 𝒰).fromGlued ≫
          inv (ulift 𝒰).fromGlued ≫ Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram Y (fun i ↦ f (idx 𝒰 i)) ⋯ =
    pullback.fst (𝒰.f x) ((ulift 𝒰).f i) ≫ f x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)

Tactic:
simp only [Sum.elim_inr, coprodMk_inr, exists_apply_eq_apply]

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

Goal state before:
pp: case left
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
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k)))

Tactic:
refine
      D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom ?_)
    rw [Functor.op_obj]
    congr 1; ext1
    dsimp only [Functor.op_obj, Opens.map_coe, unop_op, IsOpenMap.coe_functor_obj]
    rw [Set.preimage_preimage]
    change (D.f j k ≫ 𝖣.ι j).base ⁻¹' _ = _
    congr 4
    exact colimit.w 𝖣.diagram.multispan (WalkingMultispan.Hom.fst (j, k))

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @QuasiCompact = targetAffineLocally fun X x x_1 x_2 ↦ CompactSpace ↥X

Tactic:
ext X Y f
    simp only [quasiCompact_iff_forall_isAffineOpen, isCompact_iff_compactSpace,
      targetAffineLocally, Subtype.forall]
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.height = 0 ↔ I ∈ minimalPrimes R

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_eq_zero,
    minimalPrimes_eq_minimals]
  refine ⟨fun h ↦ ⟨‹_›, ?_⟩, fun ⟨hI, hI'⟩ b hb ↦ hI' b.isPrime hb⟩
  by_contra! ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩
  exact hP₃ (h (b := ⟨P, hP₁⟩) hP₂)

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
this : ∀ {X : Scheme} (f : X ⟶ Y), P f → IsAffine X → P (f ≫ g)
hX : ¬IsAffine X
i : X.affineCover.I₀
⊢ P (X.affineCover.f i ≫ f ≫ g)

Tactic:
rw [← Category.assoc]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
this : ∀ {X : Scheme} (f : X ⟶ Y), P f → IsAffine X → P (f ≫ g)
hX : ¬IsAffine X
i : X.affineCover.I₀
⊢ P ((X.affineCover.f i ≫ f) ≫ g)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
this : (span {x}).IsPrime
⊢ p.FiniteHeight

Tactic:
simp [p.finiteHeight_iff, h1]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
this✝ : (span {x}).IsPrime
this : p.FiniteHeight
hne : p ≠ span {x}
⊢ span {x} ≤ p

Tactic:
simp only [p.span_singleton_le_iff_mem, hx]

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

Goal state before:
pp: X : Scheme
s : Set X.IdealSheafData
⊢ sSup (ideal '' s) = ⨆ i, (↑i).ideal

Tactic:
conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]

Goal state after:
X : Scheme
s : Set X.IdealSheafData
⊢ sSup (Set.range (ideal ∘ Subtype.val)) = ⨆ i, (↑i).ideal
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
hs : (Spec R).basicOpen s = ⊥
x : ↥(Spec R)
hx : x ∈ ⊤
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs

Goal state after:
case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
hs : IsNilpotent ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s)
x : ↥(Spec R)
hx : x ∈ ⊤
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0