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

Goal state before:
pp: case e'_5.e'_5.e'_5.e'_9.e'_5.e'_3.e'_3
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := ⋯
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover := ⋯
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover := ⋯
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) := ⋯
this✝ : Set.range L ⊆ ↑(iSup U)
𝓤 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f g) := ⋯
i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀
this :
  IsEmbedding
    (L ∘
      ⇑(pullback.map ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst) f g
          ((𝒱 i.fst).f i.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f i.fst) (𝒰.f i.fst) ⋯ ⋯))
e_1✝³ :
  ↥(𝓤.X i) =
    ↥(pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
        ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst))
e_1✝² :
  (fun X Y ↦ C(↑X, ↑Y)) ↑(𝓤.X i).toPresheafedSpace ↑(pullback f g).toPresheafedSpace =
    (fun X Y ↦ C(↑X, ↑Y))
      ↑(pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
            ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toPresheafedSpace
      ↑(pullback f g).toPresheafedSpace
e_7✝ :
  ↑(𝓤.X i).toPresheafedSpace =
    ↑(pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toPresheafedSpace
e_3✝ :
  (𝓤.X i).toPresheafedSpace =
    (pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
        ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toPresheafedSpace
e_1✝¹ :
  (𝓤.X i).toLocallyRingedSpace =
    (pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
        ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toLocallyRingedSpace
e_1✝ :
  𝓤.X i =
    pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
      ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)
⊢ 𝓤.f i =
    pullback.map ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
      ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst) f g
      ((𝒱 i.fst).f i.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
      ((𝒲 i.fst).f i.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f i.fst) (𝒰.f i.fst) ⋯ ⋯

Tactic:
apply pullback.hom_ext <;>
      simp [𝓤, Scheme.Cover.pullbackHom]

Goal state after:
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
i : ↑Us
⊢ U ⊓ ↑i = ↑i

Tactic:
simp [heq, le_sSup i.property]

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

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
⊢ I * (J ⊔ K) = I * J ⊔ I * K

Tactic:
by ext U : 2; exact mul_add _ _ _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
U : ↥X → Scheme
i : (x : ↥X) → U x ⟶ X
x✝ : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ { I₀ := ↥X, X := U, f := i }.presieve₀ ∈ IsOpenImmersion.precoverage.coverings X

Tactic:
by simpa

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

Goal state before:
pp: case e'_2
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ IsIso (Scheme.Hom.appTop f) ↔ AffineTargetMorphismProperty.of (isomorphisms Scheme) f

Tactic:
exact ⟨fun ⟨_, _⟩ ↦ (arrow_mk_iso_iff (isomorphisms _) (arrowIsoSpecΓOfIsAffine f)).mpr
    (inferInstanceAs (IsIso (Spec.map (f.appTop)))),
    fun (_ : IsIso f) ↦ ⟨.of_isIso f, inferInstance⟩⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ ↑U ≤ ↑U ⊓ ↑V

Tactic:
by simpa

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ ↑U ≤ ↑U ⊓ ↑V

Tactic:
by simpa

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

Goal state before:
pp: X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine Z
h : IsPullback fst snd f g
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)

Tactic:
by
  have : IsAffine P := .of_isPullback h
  have : IsPullback (AffineScheme.ofHom fst) (AffineScheme.ofHom snd) (AffineScheme.ofHom f)
      (AffineScheme.ofHom g) :=
    IsPullback.of_map_of_faithful AffineScheme.forgetToScheme.{u} h
  exact (IsPullback.map AffineScheme.Γ.rightOp this).unop.flip

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' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
⊢ ⇑g '' ↑(finsetIntegerMultiple M s) ⊆ ↑(Subalgebra.map g A)

Tactic:
exact Set.image_mono hA₁

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

Goal state before:
pp: case right
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
X Y : Scheme
f : X ⟶ Y
hf✝¹ : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine ↑(f ⁻¹ᵁ ↑⟨U, hU⟩)
hf✝ : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rwa [Scheme.Opens.ι_image_top] at hf

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 := ⋯
x : S
⊢ ∀ (i : ↑↑s), l i ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
intro i
    by_cases h : l i = 0; · rw [h]; exact zero_mem _
    apply Algebra.subset_adjoin
    rw [Finset.coe_union, Finset.coe_image]
    exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))

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

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

Tactic:
by simpa

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

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (Localization.awayMap f ↑r).Finite
this✝ : Algebra R S := f.toAlgebra
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
r : ↥s
⊢ IsLocalization (Submonoid.powers ((algebraMap R S) ↑r)) (Localization.Away (f ↑r))

Tactic:
exact Localization.isLocalization

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

Goal state before:
pp: case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.map (f ≫ g) ≤ (I.map f).map g

Tactic:
rw [le_map_iff_comap_le, le_map_iff_comap_le, ← comap_comp]; exact comap_map_le _ _

Goal state after:
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:
ext1
  rw [map, Scheme.Hom.support_ker, Scheme.Hom.comp_base, TopCat.coe_comp,
    Set.range_comp, range_subschemeι, TopologicalSpace.Closeds.coe_closure]

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
⊢ x ∈ U.carrier ∧ f x = f x

Tactic:
by simpa

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
by simpa

Goal state after:
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
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq } ∉ zeroLocus {f}

Tactic:
by simpa

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

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

Tactic:
intro x
  refine ⟨comap (eval₂Hom (.id _) 0) x, ?_⟩
  rw [← comap_comp_apply, (show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),
    comap_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyNoetherian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)

Tactic:
exact (isLocallyNoetherian_iff_openCover X.affineCover).mpr
      fun i ↦ this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩

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

Goal state before:
pp: case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ (s ∩ Set.range ⇑f).Nonempty

Tactic:
Set.range_eq_univ.mpr f.surjective,

Goal state after:
case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ (s ∩ Set.univ).Nonempty
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
this : ∃ i, fT z ∈ Ti i ∧ p z ∈ U i
⊢ z ∈ ↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i)

Tactic:
by simpa

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
h : t' ∉ ⇑fT '' Z
⊢ ⋃ i ∈ σ, (U i).carrier = Set.univ

Tactic:
Set.iUnion₂_eq_univ_iff

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
h : t' ∉ ⇑fT '' Z
⊢ ∀ (a : ↥X), ∃ i, ∃ (_ : i ∈ σ), a ∈ (U i).carrier
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
this : ∃ n_1 i, (e.val i).degree = ↑n_1 ∧ e.val i ≠ 0
⊢ ∃ i, e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree

Tactic:
let m := Nat.find this

Goal state after:
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
this : ∃ n_1 i, (e.val i).degree = ↑n_1 ∧ e.val i ≠ 0
m : ℕ := Nat.find this
⊢ ∃ i, e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))).hom =
    e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ

Tactic:
simp only [Iso.symm_hom, Iso.eq_inv_comp]

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ e.hom ≫ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))).hom =
    (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst✝¹ : X.IsGermInjectiveAt x
inst✝ : IsOpenImmersion f
⊢ Y.IsGermInjectiveAt (f x)

Tactic:
obtain ⟨U, hxU, hU, H⟩ := X.exists_germ_injective x

Goal state after:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst✝¹ : X.IsGermInjectiveAt x
inst✝ : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ Y.IsGermInjectiveAt (f x)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ sX x = (X.fromSpecStalk x ≫ sX) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

Tactic:
Scheme.Hom.comp_apply,

Goal state after:
case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ sX x = sX ((X.fromSpecStalk x) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X.PartialMap Y
inst✝ : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense ↑U
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ IsOver S (f.restrict U hU hUr)

Tactic:
rw [IsOver, ← e]

Goal state after:
X Y S : Scheme
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X.PartialMap Y
inst✝ : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense ↑U
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ Hom.IsOver (f'.restrict U hU hUl).hom S
Module: Mathlib.AlgebraicGeometry.Birational.Dominant

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
this : IsDominant (X.homOfLE hU')
⊢ IsDominant (X.homOfLE hU' ≫ f.hom)

Tactic:
rwa [IsDominant.comp_iff]

Goal state after: