mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Tactic:
← X.presheaf.map_comp_assoc

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    X.presheaf.map
        ((⋯.adjunction.counit.app
              (unop ((OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op.obj (op V)))).op ≫
          h.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫
      colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
        ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ ∃ t ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨V, i, hxV, hf⟩ := X.isUnit_res_of_isUnit_germ U f x hxU hx

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
⊢ ∃ t ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
⊢ IsIso (CommRingCat.ofHom (↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).toRingHom)

Tactic:
exact inferInstanceAs (IsIso <| (IsLocalization.algEquiv
      (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)

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

Goal state before:
pp: case refine_2.op
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
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ invApp f x ≫
      f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫
          inv (s.pt.presheaf.map (eqToHom ⋯)) ≫
            ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
              s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
hf.invApp_app_assoc,

Goal state after:
case refine_2.op
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
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ X.presheaf.map (eqToHom ⋯) ≫
      s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫
        inv (s.pt.presheaf.map (eqToHom ⋯)) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    Presieve.ofArrows X f ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings S ∧
      ∀ (i : ι), P (f i)

Tactic:
exact ⟨fun hmem ↦ ⟨hmem.1, fun i ↦ hmem.2 ⟨i⟩⟩, fun h ↦ ⟨h.1, fun {Y} g ⟨i⟩ ↦ h.2 i⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW ≫ 𝟙 ((↑U).presheaf.stalk x) =
    (↑U).presheaf.germ W x hxW ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
simp only [Category.comp_id, U.germ_stalkIso_hom_assoc]

Goal state after:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) ↑x ⋯ ≫ Hom.stalkMap U.ι x
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
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
x : ↥(unop V)
⊢ (ConcreteCategory.hom (F.map i.unop.op ≫ F.germ (unop V) ↑x ⋯)) s ∈ S ↑x

Tactic:
F.germ_res

Goal state after:
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
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
x : ↥(unop V)
⊢ (ConcreteCategory.hom (F.germ (unop U) ↑x ⋯)) s ∈ S ↑x
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.ι ⋯
⊢ g = e.hom ≫ V.ι

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac

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.ι ⋯
⊢ g = g
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ (𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec = X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f

Tactic:
by
    symm
    apply LocallyRingedSpace.comp_ring_hom_ext
    · ext1 x
      dsimp
      change PrimeSpectrum.comap (f.c.app (op ⊤)).hom (X.toΓSpecFun x) = Y.toΓSpecFun (f.base x)
      dsimp [toΓSpecFun]
      rw [← IsLocalRing.comap_closedPoint (f.stalkMap x).hom, ←
        PrimeSpectrum.comap_comp_apply, ← PrimeSpectrum.comap_comp_apply,
        ← CommRingCat.hom_comp, ← CommRingCat.hom_comp]
      congr 2
      exact (PresheafedSpace.stalkMap_germ f.1 ⊤ x trivial).symm
    · intro r
      rw [LocallyRingedSpace.comp_c_app, ← Category.assoc]
      erw [Y.toΓSpecSheafedSpace_app_spec, f.c.naturality]
      rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
use f * x

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
      (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: 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
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) s) p =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)

Tactic:
dsimp [comapₗ, comapFun]

Goal state after:
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
⊢ (Localizations.comapFun f.toSemilinearMap ↑p) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩) =
    (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case none
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅ (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none

pp: case some
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
val✝ : WalkingPair
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val✝) ≅
    (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some val✝)

Tactic:
exacts [D.gluedIso F, Iso.refl _]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) =
    Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
by
  ext x
  constructor
  · rintro ⟨⟨x₁, eq₁⟩, ⟨x₂, eq₂⟩⟩
    obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)
    · subst eq₁
      exact ⟨y, by simp [e₁]⟩
  · rintro ⟨x, hx⟩
    refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
    rw [D.glue_condition_apply]
    exact hx

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

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k

Tactic:
IsIso.inv_comp_eq,

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ pullback.fst (D.f k i) (D.f k j) = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : Subsingleton ↥X
x✝ : IsEmpty ↥X ∨ Nonempty ↥X
⊢ IsAffine X

Tactic:
cases isEmpty_or_nonempty X with

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
this : x ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ x ∈ Scheme.Hom.opensRange (Sigma.desc f)

Tactic:
obtain ⟨i, y, rfl⟩ := by simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
i : σ
y : ↥(X i)
hx : (f i) y ∈ ⊤
this : (f i) y ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ (f i) y ∈ Scheme.Hom.opensRange (Sigma.desc f)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal

Tactic:
· change Ideal.comap _ _ = Ideal.prod ⊤ x.asIdeal
    ext; simp [Ideal.prod, CommRingCat.ofHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))

Tactic:
coprodMk_inl,

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
⊢ IsIso (Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case of_sSup_eq_top
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
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
this : P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ Q (Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f ⟨i, j⟩)

Tactic:
rw [← Q.cancel_left_of_respectsIso (𝒰.pullbackCoverAffineRefinementObjIso f _).inv,
      𝒰.pullbackCoverAffineRefinementObjIso_inv_pullbackHom]

Goal state after:
case of_sSup_eq_top
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
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
this : P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ Q (Scheme.Cover.pullbackHom (𝒰.X ⟨i, j⟩.fst).affineCover (Scheme.Cover.pullbackHom 𝒰 f ⟨i, j⟩.fst) ⟨i, j⟩.snd)
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)
⊢ IsIso ((D.ι i).c.app (op (⋯.functor.obj U)))

Tactic:
← colimitPresheafObjIsoComponentwiseLimit_hom_π

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ IsIso
    ((colimitPresheafObjIsoComponentwiseLimit D.diagram.multispan (⋯.functor.obj U)).hom ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)) (op (WalkingMultispan.right i)))
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 : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ Arrow.mk (pullback.diagonal f ∣_ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩)) ≅
    Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))

Tactic:
refine (morphismRestrictOpensRange _ _).trans ?_
  refine Arrow.isoMk ?_ (Iso.refl _) ?_
  · exact pullback.congrHom rfl (diagonalCover_map _ _ _ _) ≪≫
      pullbackDiagonalMapIso _ _ _ _ ≪≫ (asIso (pullback.diagonal _)).symm
  have H : pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.snd _ _ = pullback.snd _ _ ≫ pullback.fst _ _ := by
    rw [← cancel_mono ((𝒱 i).f _)]
    apply pullback.hom_ext
    · trans pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        (diagonalCover f 𝒰 𝒱).f _ ≫ pullback.snd _ _
      · simp [diagonalCover_map]
      symm
      trans pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        (diagonalCover f 𝒰 𝒱).f _ ≫ pullback.fst _ _
      · simp [diagonalCover_map]
      · rw [← pullback.condition_assoc, ← pullback.condition_assoc]
        simp
    · simp [pullback.condition, Cover.pullbackHom]
  dsimp [Cover.pullbackHom] at H ⊢
  apply pullback.hom_ext
  · simp only [Category.assoc, pullback.diagonal_fst, Category.comp_id]
    simp only [← Category.assoc, IsIso.comp_inv_eq]
    apply pullback.hom_ext <;> simp [H]
  · simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
    simp only [← Category.assoc, IsIso.comp_inv_eq]
    apply pullback.hom_ext <;> simp [H]

Goal state after:
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 : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ Arrow.mk (pullback.diagonal f ∣_ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩)) ≅
    Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))

Tactic:
by
  refine (morphismRestrictOpensRange _ _).trans ?_
  refine Arrow.isoMk ?_ (Iso.refl _) ?_
  · exact pullback.congrHom rfl (diagonalCover_map _ _ _ _) ≪≫
      pullbackDiagonalMapIso _ _ _ _ ≪≫ (asIso (pullback.diagonal _)).symm
  have H : pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.snd _ _ = pullback.snd _ _ ≫ pullback.fst _ _ := by
    rw [← cancel_mono ((𝒱 i).f _)]
    apply pullback.hom_ext
    · trans pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        (diagonalCover f 𝒰 𝒱).f _ ≫ pullback.snd _ _
      · simp [diagonalCover_map]
      symm
      trans pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        (diagonalCover f 𝒰 𝒱).f _ ≫ pullback.fst _ _
      · simp [diagonalCover_map]
      · rw [← pullback.condition_assoc, ← pullback.condition_assoc]
        simp
    · simp [pullback.condition, Cover.pullbackHom]
  dsimp [Cover.pullbackHom] at H ⊢
  apply pullback.hom_ext
  · simp only [Category.assoc, pullback.diagonal_fst, Category.comp_id]
    simp only [← Category.assoc, IsIso.comp_inv_eq]
    apply pullback.hom_ext <;> simp [H]
  · simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
    simp only [← Category.assoc, IsIso.comp_inv_eq]
    apply pullback.hom_ext <;> simp [H]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x * x ^ n * y ∈ J
⊢ y ∈ J

Tactic:
mul_assoc

Goal state after:
case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x * (x ^ n * y) ∈ J
⊢ y ∈ J
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ P (⨆ i ∈ insert x s, ↑i)

Tactic:
rw [iSup_insert, sup_comm]

Goal state after:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ P ((⨆ x ∈ s, ↑x) ⊔ ↑x)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
exact H _ _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ (RelSeries.last l).asIdeal.height ≤ m.height

Tactic:
exact height_mono hle

Goal state after: