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

Goal state before:
pp: case refine_2
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
hf : ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↥X
⊢ ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
obtain ⟨U, V, hxV, e, hf⟩ := hf x

Goal state after:
case refine_2
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
hf✝ : ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↥X
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x✝ : ↑Γ(X, ↑U)
hx : x✝ ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ IsAffineOpen.fromSpec ⋯) x ∈ ↑Z

Tactic:
IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2

Goal state after:
case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x✝ : ↑Γ(X, ↑U)
hx : x✝ ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (IsAffineOpen.fromSpec ⋯) x ∈ ↑Z
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
⊢ ∀ x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U)),
    ∃ V,
      ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
        x ∈ V ∧
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
            (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0

Tactic:
rintro x hxU

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
x : ↥X
hxU : x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
      x ∈ V ∧
        (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f = (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g

Tactic:
by
  simp only [residueFieldCongr_inv, Category.assoc, tensorInl, tensorInr,
    ← Hom.SpecMap_residueFieldMap_fromSpecResidueField]
  rw [← residueFieldCongr_fromSpecResidueField T.hx.symm,
    ← residueFieldCongr_fromSpecResidueField T.hy.symm]
  simp only [← Category.assoc, ← Spec.map_comp, pushout.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x) ≫ Hom.residueFieldMap (pullback.fst f g) t =
    ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫ Hom.residueFieldMap (pullback.snd f g) t

Tactic:
simp [← residueFieldMap_comp, Scheme.Hom.residueFieldMap_congr pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl

Tactic:
rw [← cancel_mono <| X.fromSpecResidueField T.x]

Goal state after:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact ↑(↑U ⊓ X.basicOpen ↑i)

Tactic:
← X.basicOpen_res _ (homOfLE le_top).op

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ↑i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact ↑(↑V ⊓ X.basicOpen ↑i)

Tactic:
← X.basicOpen_res _ (homOfLE le_top).op

Goal state after:
case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ↑i))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝¹ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
x : ↥(Spec S)
hx✝ : x ∈ ↑(ker f).support
inst✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
hx : x ∈ (fun i ↦ ↑(ker (𝒰.f i ≫ f)).support) i
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ x ∈ closure (Set.range ⇑f)

Tactic:
exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)

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

Goal state before:
pp: X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.map φ)
⊢ closure
      (Set.range
        (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) ∘ PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv))) ⊆
    closure (Set.range ⇑(Spec.map φ))

Tactic:
exact closure_mono (Set.range_comp_subset_range _ (Spec.map φ))

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderBaseChange

Tactic:
have : (affineAnd Q).toProperty.RespectsIso := affineAnd_respectsIso hQi
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g ⟨hY, hg⟩
  exact ⟨inferInstance, hQb.pullback_fst_appTop _ hQi f _ hg⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ m, ↑m • x ∈ adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))

Tactic:
refine IsLocalization.exists_smul_mem_of_mem_adjoin
      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r)) ⊆
    ↑(adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)))

case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ Submonoid.powers ↑r ≤ (adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))).toSubmonoid

case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
⊢ P ≤ @IsAffineHom

Tactic:
intro X Y f hf
  wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
    intro U
    exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) U.2
  rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
  rw [HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)]
  exact hf.1

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ Function.Injective ⇑(ConcreteCategory.hom (app (toImage f) (imageι f ⁻¹ᵁ ↑U)))

Tactic:
simp only [f.toImage_app U, CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ Function.Injective
    (⇑(Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯) ∘
      ⇑(CommRingCat.Hom.hom ((ker f).subschemeObjIso U).hom))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (Spec.map f) x))

Tactic:
have : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by
      rw [← RingHom.toMorphismProperty_respectsIso_iff]
      exact RingHom.surjective_respectsIso
    apply (MorphismProperty.arrow_mk_iso_iff
      (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
      (Scheme.arrowStalkMapSpecIso f x)).mpr
    exact RingHom.surjective_localRingHom_of_surjective f.hom h x.asIdeal

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

Goal state before:
pp: case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed (Set.range ⇑(f ≫ i))

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]

Goal state after:
case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed (⇑i '' Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
⊢ IsLocallyClosed (Set.range ⇑(f ≫ g))

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
⊢ IsLocallyClosed (⇑g '' Set.range ⇑f)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
⊢ ⋃ i,
      Set.range
        (comap
          ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
                i).comp
            (algebraMap R
              ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    ⋃ x, (↑x).toSet

Tactic:
congr! with _ _ C

Goal state after:
case e'_3
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    (↑C).toSet
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case pos
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)

pp: case neg
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)

Tactic:
· rw [Scheme.Cover.pullbackHom,
        ← (IsOpenImmersion.isPullback_lift_id _ _ hxU).flip.isoPullback_inv_snd,
        MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion]
      refine this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩
      rw [IsOpenImmersion.lift_fac_assoc, hg]

Goal state after:
case neg
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ x ∈ comap (algebraMap R A) '' (zeroLocus {f})ᶜ

Tactic:
basicOpen_eq_zeroLocus_compl

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus {f})ᶜ ↔ x ∈ comap (algebraMap R A) '' (zeroLocus {f})ᶜ
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case inr
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
⊢ IsLocallyConstructible (⇑f '' s)

pp: X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
hX : ∃ S, X = Spec S
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
· have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
    let 𝒰 := X.affineCover.finiteSubcover
    rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]
    refine .iUnion fun i ↦ ?_
    have inst : QuasiCompact (𝒰.f i ≫ f) :=
      HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
    convert! this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩
    rw [Scheme.Hom.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp,
      ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, coe_opensRange]

Goal state after:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
hX : ∃ S, X = Spec S
⊢ IsLocallyConstructible (⇑f '' s)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (⇑f ⁻¹' (↑U ∩ Set.range ⇑f))

Tactic:
apply f.isOpenEmbedding.isInducing.isCompact_preimage'

Goal state after:
case hK
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (↑U ∩ Set.range ⇑f)

case Kf
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsCompact ↑(⨆ i, ↑(S i))

Tactic:
Opens.iSup_mk

Goal state after:
case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsCompact ↑{ carrier := ⋃ i, (S i).1.carrier, is_open' := ⋯ }
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Function.Injective ⇑(ConcreteCategory.hom (pushoutSection ⋯ hVU ⋯ ⋯))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯))

Tactic:
simpa [Scheme.Hom.appLE] using f.app_injective U

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ X.IsQuasiAffine

Tactic:
have : IsImmersion (X.toSpecΓ ≫ Spec.map f.appTop) := by rw [← toSpecΓ_naturality]; infer_instance
  have : IsImmersion X.toSpecΓ := .of_comp _ (Spec.map f.appTop)
  constructor

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : _root_.IsReduced ↑R
⊢ IsReduced 𝔸(n; Spec R)

Tactic:
exact isReduced_of_isOpenImmersion (SpecIso n R).hom

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

Goal state before:
pp: 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 := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Localization.Away c))) ∘ e.val } →
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
      Statement R₀ R n e

Tactic:
have q₂_surjective : Surjective q₂ := Ideal.Quotient.mk_surjective

Goal state after:
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 := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Localization.Away c))) ∘ e.val } →
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
      Statement R₀ R n e
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite
⊢ (U ∩ support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x).Finite

Tactic:
by
      refine h.subset (inter_subset_inter_right U fun y hy ↦ ?_)
      obtain ⟨x, (hx : f x = y), h'⟩ := exists_ne_zero_of_finsum_mem_ne_zero hy
      use x
      grind [mem_support]

Goal state after: