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

Goal state before:
pp: case e_supportSet
X : Scheme
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝¹ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
t : Set ↥X
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
        ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          U) =
      { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal
        (X.affineBasicOpen f)
ht :
  t =
    ⋂ U,
      X.zeroLocus
        ↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs }.ideal
            U)
⊢ s = t

Tactic:
hs,

Goal state after:
case e_supportSet
X : Scheme
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝¹ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
t : Set ↥X
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
        ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          U) =
      { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal
        (X.affineBasicOpen f)
ht :
  t =
    ⋂ U,
      X.zeroLocus
        ↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs }.ideal
            U)
⊢ ⋂ U, X.zeroLocus ↑(i U) = t
Module: Mathlib.AlgebraicGeometry.Properties

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

Tactic:
hs,

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x : ↥X
U : ↑X.affineOpens
h : x ∈ ↑U
⊢ x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U)

Tactic:
by
  simpa [-mem_zeroLocus_iff, h] using congr(x ∈ $(I.supportSet_inter U))

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

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
⊢ X.nilradical = ⊥

Tactic:
ext; simp [nilradical, Ideal.radical_eq_iff.mpr (Ideal.isRadical_bot)]

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

Goal state before:
pp: case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈
    Y.zeroLocus
        (⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv) ''
          ↑(Ideal.comap (CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv) ((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩))) ∩
      Set.range ⇑(𝒰.f i)

pp: case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
Ideal.coe_comap,

Goal state after:
case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈
    Y.zeroLocus
        (⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv) ''
          ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv) ⁻¹' ↑((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩)) ∩
      Set.range ⇑(𝒰.f i)

case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) =
    𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))

Tactic:
· apply pullback.hom_ext
      · rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
        rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]
      · rw [← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_snd_ι, limit.lift_π_assoc, cospan_left, glueDataT'Aux_fst_assoc,
          glueDataT_fst_assoc, Scheme.homOfLE_ι, Category.id_comp]
        rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]

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

Goal state before:
pp: case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ Ideal.map (CommRingCat.Hom.hom U.topIso.inv) (Ideal.span s) = ⊤

Tactic:
hs,

Goal state after:
case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ Ideal.map (CommRingCat.Hom.hom U.topIso.inv) ⊤ = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ Ideal.span (⇑(ConcreteCategory.hom U.topIso.inv) '' s) = ⊤

Tactic:
rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
h : (g.comp f).EssFiniteType
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝ : Algebra.EssFiniteType R T
⊢ g.EssFiniteType

Tactic:
exact Algebra.EssFiniteType.of_comp R S T

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ closure (Set.range ⇑(Hom.toImage f ≫ Hom.imageι f))

Tactic:
f.toImage_imageι

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.comap (f ≫ g) = (I.comap g).comap f

Tactic:
let e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
    asIso (pullback.map _ _ _ _ (𝟙 _) (I.comapIso g).hom (𝟙 _) (by simp) (by simp)) ≪≫
      pullbackRightPullbackFstIso _ _ _

Goal state after:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
  asIso (pullback.map f (I.comap g).subschemeι f (pullback.fst g I.subschemeι) (𝟙 X) (I.comapIso g).hom (𝟙 Y) ⋯ ⋯) ≪≫
    pullbackRightPullbackFstIso g I.subschemeι f
⊢ I.comap (f ≫ g) = (I.comap g).comap f
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝ : IsEmpty ↥X
f : X ⟶ Y
⊢ IsClosed ∅

Tactic:
exact isClosed_empty

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso f'.op

Tactic:
rw [← isIso_iff_of_reflects_iso _ (IsClosedImmersion.overEquivIdealSheafData X).functor]

Goal state after:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso ((overEquivIdealSheafData X).functor.map f'.op)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
let φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := f.appTop

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ W i ≤ 𝒰.f i ⁻¹ᵁ U

Tactic:
change (𝒰.X i).basicOpen ((𝒰.f i ≫ f).appTop s) ≤ _

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (𝒰.X i).basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop (𝒰.f i ≫ f))) s) ≤ 𝒰.f i ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (𝒰.X i).basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop (𝒰.f i ≫ f))) s) ≤ 𝒰.f i ⁻¹ᵁ U

Tactic:
← Scheme.preimage_basicOpen_top,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (𝒰.f i ≫ f) ⁻¹ᵁ Y.basicOpen s ≤ 𝒰.f i ⁻¹ᵁ U
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FinitePresentation

Tactic:
finitePresentation_algebraMap

Goal state after:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FinitePresentation R S
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι : Type u_3
s : ι → S
hs : Ideal.span (Set.range s) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommRing (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (s i) (T i)
inst✝ : ∀ (i : ι), FinitePresentation R (T i)
i : ι
⊢ FinitePresentation R (Localization.Away (s i))

Tactic:
exact .equiv <| (IsLocalization.algEquiv (.powers <| s i) _ (T i)).symm |>.restrictScalars R

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))

Tactic:
· simp [e, scalarRTensorAlgEquiv, coeff, map, X, monomial]

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

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)

Tactic:
by
  refine ⟨fun hf y ↦ (geometrically P).pullback_snd _ _ hf, fun H ↦ ?_⟩
  intro K _ y Z fst snd h
  obtain ⟨⟨y, φ⟩, rfl⟩ := (Scheme.SpecToEquivOfField _ _).symm.surjective y
  let p : Z ⟶ f.fiber y :=
    pullback.lift fst (snd ≫ Spec.map φ) (by simp [h.w, Scheme.SpecToEquivOfField])
  apply H y (Spec.map φ) p snd
  simp only [Scheme.SpecToEquivOfField, Equiv.coe_fn_symm_mk] at h
  refine .flip (.of_bot (.flip ?_) ?_ (IsPullback.of_hasPullback f (Y.fromSpecResidueField y)).flip)
  · convert! h
    simp [p]
  · simp [p, Scheme.Hom.fiberToSpecResidueField]

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

Goal state before:
pp: X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ IsSchemeTheoreticallyDominant (f ≫ g)

Tactic:
by
  rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]

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

Goal state before:
pp: case refine_1
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

pp: case refine_2
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
· exact (surjective_iff (Spec.map φ)).mp inferInstance

Goal state after:
case refine_2
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ support fun x ↦ 0).Finite

Tactic:
simp_rw [support_fun_zero, inter_empty, finite_empty, and_true]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t, t ∈ 𝓝 z
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support fun i ↦ ⇑(F i)
h : (Function.support F).Finite
h₂ : (Function.support fun i ↦ ⇑(F i)).Finite
⊢ ∑ n ∈ h.toFinset, ⇑(F n) = ∑ᶠ (i : ι), ⇑(F i)

Tactic:
simp_all [finsum_eq_sum _ h₂]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType (Y ↘ S)
⊢ (fun f ↦ Hom.IsOver f S) = fun f ↦ f ≫ Y ↘ S = X.fromSpecStalk (genericPoint ↥X) ≫ X ↘ S

Tactic:
by simp only [Hom.isOver_iff]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X Y : Scheme
f g : X.PartialIso Y
e : f.source = g.source
e' : g.target = f.target
H : f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'
⊢ ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'

Tactic:
exact ⟨e, e', H⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
x✝ : ↥X₁
⊢ x✝ ∈ ↑((f.comp g).comp h).domain ↔ x✝ ∈ ↑(f.comp (g.comp h)).domain

Tactic:
comp_domain,

Goal state after:
case e
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
x✝ : ↥X₁
⊢ x✝ ∈ ↑((f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι ''ᵁ (f.comp g).hom ⁻¹ᵁ h.domain) ↔
    x✝ ∈ ↑(f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
hIUX : ∀ (i : ↑I), ↑↑i ≤ UX
this : Finite ↑I
⊢ ⨆ i, ↑↑i = UX

Tactic:
rwa [iSup_subtype,
    eq_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).domain = f.domain

Tactic:
comp_domain,

Goal state after:
case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (PartialMap.id X).domain.ι ''ᵁ (PartialMap.id X).hom ⁻¹ᵁ f.domain = f.domain
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
⊢ IsAffineHom ((opensDiagram D i U).map f)

Tactic:
by
  refine ⟨fun V hV ↦ ?_⟩
  convert!
    ((hV.image_of_isOpenImmersion (D.map k.hom ⁻¹ᵁ U).ι).preimage
          (D.map f.left)).preimage_of_isOpenImmersion
      (D.map j.hom ⁻¹ᵁ U).ι ?_
  · ext x
    change _ ∈ V ↔ _
    refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩
    · change (D.map f.left ≫ D.map k.hom).base x.1 ∈ U
      rw [← D.map_comp, Over.w f]
      exact x.2
    · convert! h
      exact Subtype.ext (by simp)
    · rintro ⟨⟨_, hU⟩, hV, rfl⟩
      convert! hV
      exact Subtype.ext (by simp)
  · simp only [opensDiagram_obj, Scheme.Opens.opensRange_ι]
    rintro x ⟨⟨y, h₁ : (D.map k.hom).base y ∈ U⟩, h₂, e⟩
    obtain rfl : y = (D.map f.left).base x := congr($e)
    dsimp at h₁
    rw [← Scheme.Hom.comp_apply] at h₁
    rwa [← D.map_comp, Over.w f] at h₁

Goal state after: