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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ↑(Hom.ker (pullback.fst f I.subschemeι)).support = ↑(I.support.preimage ⋯)

Tactic:
Scheme.Hom.support_ker,

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ closure (Set.range ⇑(pullback.fst f I.subschemeι)) = ↑(I.support.preimage ⋯)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ J ≤ I.map f

Tactic:
map,

Goal state after:
case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ J ≤ Hom.ker (I.subschemeι ≫ f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

Tactic:
map,

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ Hom.ker ((vanishingIdeal Z).subschemeι ≫ f) ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ ↑(I.map f).support = ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))

Tactic:
map,

Goal state after:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ ↑(Hom.ker (I.subschemeι ≫ f)).support = ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ ↑(Hom.ker (I.subschemeι ≫ f)).support = ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))

Tactic:
Scheme.Hom.support_ker,

Goal state after:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑(I.subschemeι ≫ f)) = ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @IsImmersion

Tactic:
by
  suffices IsZariskiLocalAtTarget
      (topologically fun {X Y} _ _ f ↦ IsLocallyClosed (Set.range f)) from
    isImmersion_eq_inf ▸ inferInstance
  apply +allowSynthFailures topologically_isZariskiLocalAtTarget'
  · refine { precomp := ?_, postcomp := ?_ }
    · intro X Y Z i hi f hf
      change IsIso i at hi
      change IsLocallyClosed _
      simpa only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
        Set.range_eq_univ.mpr i.surjective, Set.image_univ]
    · intro X Y Z i hi f hf
      change IsIso i at hi
      change IsLocallyClosed _
      simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]
      refine hf.image i.homeomorph.isInducing ?_
      rw [Set.range_eq_univ.mpr i.surjective]
      exact isOpen_univ.isLocallyClosed
  · simp_rw [Set.range_restrictPreimage]
    exact fun _ _ _ hU _ ↦ hU.isLocallyClosed_iff_coe_preimage

Goal state after:
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
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
⊢ g' ≫ f = (f' ≫ Scheme.Hom.liftCoborder g) ≫ (Scheme.Hom.coborderRange g).ι

Tactic:
by simpa using H.w.symm

Goal state after:
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
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ g' ≫ f = (f' ≫ Scheme.Hom.liftCoborder g) ≫ (Scheme.Hom.coborderRange g).ι

Tactic:
by simpa using H.w.symm

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
φ : S →+* T
ψ : R →+* S
C : BasicConstructibleSetData R
⊢ map (φ.comp ψ) C = map φ (map ψ C)

Tactic:
simp [map, Function.comp_def]

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
refine ⟨isAffine_of_isAffineHom f, ?_⟩
  simp only [← f.toImage_imageι, Scheme.Hom.comp_appTop, CommRingCat.hom_comp, RingHom.coe_comp,
    Scheme.Hom.image, Scheme.Hom.imageι]
  rw [Scheme.Hom.appTop, Scheme.Hom.appTop, f.ker.subschemeι_app ⟨⊤, isAffineOpen_top Y⟩,
    CommRingCat.hom_comp, RingHom.coe_comp]
  exact (ConcreteCategory.bijective_of_isIso _).2.comp
    ((ConcreteCategory.bijective_of_isIso _).2.comp Ideal.Quotient.mk_surjective)

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_1) [inst_1 : CommRing S] (T : Type u_2) [inst_2 : CommRing T]
    (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)

Tactic:
· intro R _ S _ f hf hf' s hs
    refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_
    rw [range_comap_of_surjective _ f hf]
    exact isRetrocompact_zeroLocus_compl_of_fg hf'

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_1) [inst_1 : CommRing S] (T : Type u_2) [inst_2 : CommRing T]
    (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) ↔
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
by
  constructor
  · rintro ⟨q, ⟨hqg, hqf⟩, rfl⟩ H
    simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf
    have hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField) := by
      rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]
    let F : (A ⧸ Ideal.span s) ⊗[R] (q.asIdeal.comap (algebraMap R A)).ResidueField →ₐ[A]
        q.asIdeal.ResidueField :=
      Algebra.TensorProduct.lift
        (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A _) hs)
        (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
        fun _ _ ↦ .all _ _
    have := H.map F
    rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker,
      Ideal.ker_algebraMap_residueField] at this
    exact hqf this
  · intro H
    rw [← mem_nilradical, nilradical_eq_sInf, Ideal.mem_sInf] at H
    simp only [Set.mem_ofPred_eq, Algebra.TensorProduct.algebraMap_apply,
      Ideal.Quotient.algebraMap_eq, not_forall] at H
    obtain ⟨q, hq, hfq⟩ := H
    have : ∀ a ∈ s, Ideal.Quotient.mk (Ideal.span s) a ⊗ₜ[R] 1 ∈ q := fun a ha ↦ by
      simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span ha)]
    refine ⟨comap (algebraMap A _) ⟨q, hq⟩, ⟨by simpa [Set.subset_def], by simpa⟩, ?_⟩
    rw [← comap_comp_apply, ← IsScalarTower.algebraMap_eq,
      ← Algebra.TensorProduct.includeRight.comp_algebraMap, comap_comp_apply,
      Subsingleton.elim (α := PrimeSpectrum x.asIdeal.ResidueField) (comap _ _) ⊥]
    ext a
    exact congr(a ∈ $(Ideal.ker_algebraMap_residueField _))

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap (comap C)

Tactic:
intro U hU
  obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU
  rw [Set.image_sUnion]
  apply isOpen_sUnion
  rintro _ ⟨t, ht, rfl⟩
  obtain ⟨r, rfl⟩ := hS ht
  simp only [image_comap_C_basicOpen]
  exact (isClosed_zeroLocus _).isOpen_compl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
⊢ DiscreteTopology ↥X

Tactic:
by
  apply discreteTopology_iff_isOpen_singleton.mpr
  intro x
  obtain ⟨W, hW1, hW2, _⟩ := exists_isAffineOpen_mem_and_subset (TopologicalSpace.Opens.mem_top x)
  have : IsArtinianRing Γ(X, W) := IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hW1⟩
  have : DiscreteTopology (Spec Γ(X, W)) := inferInstanceAs (DiscreteTopology (PrimeSpectrum _))
  have : DiscreteTopology W := hW1.isoSpec.hom.homeomorph.symm.discreteTopology
  simpa using (isOpen_discrete ({⟨x, hW2⟩} : Set W)).trans W.2

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ IsOpenMap (comap C)

Tactic:
intro U hU
  obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU
  rw [Set.image_sUnion]
  apply isOpen_sUnion
  rintro _ ⟨t, ht, rfl⟩
  obtain ⟨r, rfl⟩ := hS ht
  simp only [image_comap_C_basicOpen]
  exact (isClosed_zeroLocus _).isOpen_compl

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

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝² : IsIntegral Y
x✝¹ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
z : ↥Y
x✝ : z ∈ ⊤
⊢ z ∈ U i

Tactic:
rwa [Subsingleton.elim z y]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
⊢ f = g

Tactic:
by
    ext x
    · obtain ⟨x⟩ := x
      simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (C x)
    · simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (X x)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.app
            (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
            ⊤)).comp
      (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) =
    CommRingCat.Hom.hom (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv)

Tactic:
← CommRingCat.hom_comp,

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ CommRingCat.Hom.hom
      (Scheme.Hom.appTop (𝔸(n; S) ↘ S) ≫
        Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
          ⊤) =
    CommRingCat.Hom.hom (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (Scheme.Hom.appTop (𝔸(n; S) ↘ S) ≫
        Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
          ⊤) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom =
    (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom

Tactic:
← Scheme.Hom.comp_appTop,

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ Scheme.Hom.appTop
        (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X) ≫
          𝔸(n; S) ↘ S) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom =
    (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsIntegralHom (Spec.map (CommRingCat.ofHom C))
h✝ : Nonempty ↥(Spec R)
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ False

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↥(Spec R)
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ False
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑R
⊢ e ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a) =
    e
      (e.symm
        (((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) (φRA.hom' a)))

Tactic:
RingEquiv.apply_symm_apply

Goal state after:
case refine_2
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑R
⊢ e ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a) =
    ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) (φRA.hom' a)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX

Tactic:
rw [← IsAffineOpen.SpecMap_appLE_fromSpec sY hU hV iVU, ← Spec.map_comp_assoc, ← h₂,
      ← Scheme.Hom.appLE, ← hW.isoSpec_hom, IsAffineOpen.SpecMap_appLE_fromSpec sX hU hW i,
      ← Iso.eq_inv_comp, IsAffineOpen.isoSpec_inv_ι_assoc]

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

Goal state before:
pp: case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    Hom.stalkMap U.ι ⟨x, hx⟩

Tactic:
Hom.stalkMap_congr_hom _ _ (X.homOfLE_ι hU').symm

Goal state after:
case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ X.homOfLE ⋯ ≫ (X.isoOfEq ⋯).inv ≫ (g x).hom = X.homOfLE ⋯ ≫ (X.isoOfEq ⋯).inv ≫ (g y).hom

Tactic:
← cancel_epi (X.isoOfEq congr($(hg₂ x) ⊓ $(hg₂ y))).hom,

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ (X.isoOfEq ⋯).inv ≫ (g x).hom =
    (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ (X.isoOfEq ⋯).inv ≫ (g y).hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝⁵ : IsReduced X
inst✝⁴ : Y.IsSeparated
inst✝³ : S.IsSeparated
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X ⤏ Y
inst✝ : RationalMap.IsOver S f
⊢ RationalMap.IsOver S f.toPartialMap.toRationalMap

Tactic:
f.toRationalMap_toPartialMap

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝⁵ : IsReduced X
inst✝⁴ : Y.IsSeparated
inst✝³ : S.IsSeparated
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X ⤏ Y
inst✝ : RationalMap.IsOver S f
⊢ RationalMap.IsOver S f
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U = ⊤

Tactic:
by_contra! H
  obtain ⟨s, hs⟩ := exists_mem_of_isClosed_of_nonempty' D c hc (fun j f ↦ (D.map f ⁻¹ᵁ U)ᶜ)
    (fun j f ↦ (D.map f ⁻¹ᵁ U).2.isClosed_compl) (fun j f ↦ by
      simp only [TopologicalSpace.Opens.map_coe, Set.nonempty_compl, ne_eq]
      exact SetLike.coe_injective.ne (H j f))
    (fun j f ↦ (D.map f ⁻¹ᵁ U).2.isClosed_compl.isCompact)
    (fun j k fkj fji x (hx : _ ∉ U) ↦ by rwa [Functor.map_comp] at hx)
  exact absurd (hU.ge (Set.mem_univ s)) (by simpa using hs i (𝟙 i))

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

Goal state before:
pp: case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ 𝟙 X ''ᵁ f.domain = f.domain

Tactic:
Hom.id_image

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

Goal state before:
pp: case e'_3.f.a
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := ⋯
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (R ⧸ Ideal.span {c})
hxT₂ : x ∈ ↑T₂
⊢ comap q₂.toRingHom ⁻¹' { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }.toSet =
    comap q₂.toRingHom ⁻¹' comap q₂.toRingHom '' x.toSet

Tactic:
simp only [AlgHom.toLinearMap_apply] at hq₂g₂
          have : q₂ c = 0 := by simp [q₂]
          simp only [BasicConstructibleSetData.toSet, Set.preimage_sdiff, preimage_comap_zeroLocus,
            preimage_comap_zeroLocus,
            Set.preimage_image_eq _ (comap_injective_of_surjective _ q₂_surjective)]
          simp only [Fin.range_cons, Set.image_singleton, Set.image_insert_eq,
            ← Set.range_comp, comp_def]
          simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, hq₂g₂ _ hxT₂, hf₂]
          rw [← Set.union_singleton, zeroLocus_union,
            this, zeroLocus_singleton_zero, Set.inter_univ]

Goal state after: