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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))

Tactic:
Scheme.Hom.stalkMap_comp

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (e x) ≫ Scheme.Hom.stalkMap e x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Tactic:
Scheme.Hom.stalkMap_comp

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e (f x) ≫ Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↥X
this : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
Scheme.Hom.stalkMap_comp

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↥X
this : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
Scheme.Hom.stalkMap_comp

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ Finite 𝒰.I₀

Tactic:
dsimp [𝒰]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ Finite Y.affineCover.finiteSubcover.I₀
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace ↥(𝒰.X i)

Tactic:
dsimp [𝒰]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace ↥(pullback f (Y.affineCover.f (Scheme.Cover.idx Y.affineCover ↑i) ≫ g))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
i : 𝒰.I₀
⊢ IsAffine (𝒰.X i)

Tactic:
dsimp [𝒰]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
i : 𝒰.I₀
⊢ IsAffine ((pullback g (Z.affineCover.f i.fst)).affineCover.X i.snd)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R S _ _ f r R' S' _ _ _ _ _ _ H

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁹ : IsZariskiLocalAtTarget P
inst✝⁸ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom (IsLocalization.Away.map R' S' f r)))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ Submodule.spanRank (J ⊔ span {x}) ≤ ↑(r + 1)

Tactic:
apply Submodule.spanRank_sup_le_sum_spanRank.trans
      push_cast
      exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))

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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
⊢ P (f ≫ g)

pp: 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
⊢ P (f ≫ g)

Tactic:
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Y.affineCover.pullback₁ f)]
      intro i
      rw [← Scheme.Cover.pullbackHom_map_assoc]
      exact this _ _ (IsZariskiLocalAtTarget.of_isPullback (.of_hasPullback _ _) hf)
        (comp_of_isOpenImmersion _ _ _ hg) inferInstance

Goal state after:
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
⊢ P (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
this : p.FiniteHeight
hne : p ≠ span {x}
⊢ (span {x}).height < 1

Tactic:
← h1

Goal state after:
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}).height < p.height
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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
⊢ Set.range ⇑((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) = Set.range ⇑(↑s).ι

Tactic:
by simpa only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Scheme.Opens.range_ι,
          Opens.map_coe, Set.image_preimage_eq_iff, heq, Opens.coe_sSup] using! le_sSup s.2

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
this : x ∈ ⨆ i ∈ s, X.basicOpen i
r : ↑Γ(X, ↑⟨V, hV⟩)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ↑⟨U, hU⟩ ↑⟨X.basicOpen r, ⋯⟩ ⋯))

Tactic:
← f.appLE_map e (homOfLE (X.basicOpen_le r)).op

Goal state after:
case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
this : x ∈ ⨆ i ∈ s, X.basicOpen i
r : ↑Γ(X, ↑⟨V, hV⟩)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Tactic:
obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ :=
    Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens (show x ∈ U ⊓ V from ⟨hxU, hxV⟩)
  transitivity fromSpecStalk h₁ h₂
  · delta fromSpecStalk
    rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
  · delta fromSpecStalk
    rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ Hom.stalkMap (f ≫ g) (closedPoint ↑R) ≫ (stalkClosedPointIso R).hom =
    Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
Scheme.Hom.stalkMap_comp

Goal state after:
X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ (Hom.stalkMap g (f (closedPoint ↑R)) ≫ Hom.stalkMap f (closedPoint ↑R)) ≫ (stalkClosedPointIso R).hom =
    Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.germ ⊤ (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom = φ

Tactic:
germ_stalkClosedPointIso_hom,

Goal state after:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫ (ΓSpecIso S).inv ≫ (ΓSpecIso S).hom = φ
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
⊢ X.presheaf.germ U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
by
  have : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint R) = x := by
    rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
  have : x ∈ U := this ▸ hU
  simp only [germ_stalkClosedPointTo, Hom.comp_app,
    fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom, Functor.mapIso_hom,
      (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]
  simp_rw [← Opens.map_top (Spec.map f).base]
  rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Y.residue (f x) ≫ Hom.residueFieldMap f x = Hom.stalkMap f x ≫ X.residue x

Tactic:
by
  simp [Hom.residueFieldMap]
  rfl

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ IsAffine X

Tactic:
by
    constructor
    · apply AffineTargetMorphismProperty.respectsIso_mk
      · rintro X Y Z e _ _ H
        have : IsAffine _ := H
        exact .of_isIso e.hom
      · exact fun _ _ _ ↦ id
    · intro X Y _ f r H
      have : IsAffine X := H
      change IsAffineOpen _
      rw [Scheme.preimage_basicOpen]
      exact (isAffineOpen_top X).basicOpen _
    · intro X Y _ f S hS hS'
      apply_fun Ideal.map (f.appTop).hom at hS
      rw [Ideal.map_span, Ideal.map_top] at hS
      apply isAffine_of_isAffineOpen_basicOpen _ hS
      have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'
      simpa [Scheme.preimage_basicOpen] using! this

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.subschemeCover.f U ≫ I.subschemeι = I.glueDataObjι U ≫ (↑U).ι

Tactic:
simp [subschemeCover, subschemeι_def]

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

Goal state before:
pp: R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e✝ : R✝ ≃+* S✝
⊢ e✝.toRingHom.Finite

Tactic:
exact Finite.of_surjective _ (RingEquiv.toEquiv _).surjective

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

Goal state before:
pp: ⊢ OfLocalizationSpan @Finite

Tactic:
RingHom.ofLocalizationSpan_iff_finite

Goal state after:
⊢ OfLocalizationFiniteSpan @Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↥(Spec R)
i : X.affineCover.I₀
this : JacobsonSpace ↥(X.affineCover.X i)
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.f i))

Tactic:
let e := (X.affineCover.f i).isOpenEmbedding.isEmbedding.toHomeomorph

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↥(Spec R)
i : X.affineCover.I₀
this : JacobsonSpace ↥(X.affineCover.X i)
e : ↥(X.affineCover.X i) ≃ₜ ↑(Set.range ⇑(X.affineCover.f i)) := ⋯.toHomeomorph
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
Scheme.Hom.stalkMap_comp

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ Set.range ⇑((vanishingIdeal Z).subschemeι ≫ f)

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]

Goal state after:
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))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯))
        ((ConcreteCategory.hom (X.presheaf.map w.op)) ((ConcreteCategory.hom φ) g))) =
    0

Tactic:
hg

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))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯)) 0) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
⊢ IsImmersion g → IsImmersion g'

Tactic:
hg

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
⊢ IsImmersion g'
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
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : ↥t), FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := ⋯
this : ∀ (g : ↥t), FinitePresentation R (Localization.Away ↑g)
⊢ Function.Surjective ⇑f'

Tactic:
exact IsLocalization.Away.mapₐ_surjective_of_surjective _ hf

Goal state after: