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

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsCompact (⋃ i, ((Opens.map f.base).1 (Y.basicOpen ↑i)).carrier)

Tactic:
exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X

Tactic:
by
    constructor
    · apply AffineTargetMorphismProperty.respectsIso_mk <;> rintro X Y Z e _ _ H
      exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.base)), H]
    · introv _ H
      rw [Scheme.preimage_basicOpen f r]
      exact (isCompact_iff_compactSpace.mp (isCompact_basicOpen _ isCompact_univ _))
    · rintro X Y H f S hS hS'
      rw [← (isAffineOpen_top _).iSup_basicOpen_eq_self_iff] at hS
      rw [← isCompact_univ_iff, ← Opens.coe_top, ← f.preimage_top, ← hS, Scheme.Hom.preimage_iSup,
        Opens.iSup_mk, Opens.coe_mk]
      exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)

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

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ (fun a ↦ U.ι a) '' Set.range ⇑(IsOpenImmersion.lift U.ι f ⋯) = ↑U

Tactic:
← Set.range_comp,

Goal state after:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ((fun a ↦ U.ι a) ∘ ⇑(IsOpenImmersion.lift U.ι f ⋯)) = ↑U
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
⊢ QuasiSeparated f

Tactic:
have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance

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
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ QuasiSeparated f
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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
iff_of_source_openCover (P := P) (Scheme.coverOfIsIso.{u} (𝟙 _))

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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 X)).I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((Scheme.coverOfIsIso (𝟙 X)).f i ≫ f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
    intro U
    have : IsAffine (𝟙 X ⁻¹ᵁ U.1) := U.2
    rw [morphismRestrict_id, iff_of_isAffine (P := P), Scheme.Hom.id_appTop]
    apply hP

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : Ideal R
n : ℕ
inst✝ : p.IsPrime
⊢ p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

Tactic:
rw [height_eq_primeHeight, primeHeight, Order.height_le_coe_iff,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall]
  congr!
  rw [height_eq_primeHeight, primeHeight]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_1
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), ↑(Order.height i) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ ↑p.height ≤ n

Tactic:
rw [Ideal.height_eq_primeHeight]
    exact h ⟨p, hp⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⨆ I, ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ I, ⨆ (_ : I.IsMaximal), I.height

Tactic:
refine iSup_mono' fun I => ?_
    obtain rfl | I_top := eq_or_ne I ⊤
    · exact ⟨⊥, by grind [iSup_le_iff, Ideal.IsPrime.ne_top]⟩
    · obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top
      exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, height_mono hIM⟩)⟩

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
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), P ((V i).ι ≫ f ≫ U.ι)

Tactic:
intro s
      let f' : (V s).toScheme ⟶ U.ι ⁻¹ᵁ s := f ∣_ U.ι ⁻¹ᵁ s
      have hf' : P f' := IsZariskiLocalAtTarget.restrict hf _
      let e : (U.ι ⁻¹ᵁ s).toScheme ≅ s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ s).ι ≫ U.ι) s.1.ι
        (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)
      have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
        simp only [V, IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
      rw [heq, ← Category.assoc]
      refine this _ ?_ ?_
      · rwa [P.cancel_right_of_respectsIso]
      · obtain ⟨a, ha⟩ := hUs s.2
        use a, ha.symm

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

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
⊢ sSup (ideal '' Set.range I) = sSup (Set.range fun i ↦ (I i).ideal)

Tactic:
← Set.range_comp,

Goal state after:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
⊢ sSup (Set.range (ideal ∘ I)) = sSup (Set.range fun i ↦ (I i).ideal)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.map i.op))

Tactic:
by
  rw [injective_iff_map_eq_zero]
  intro x hx
  rw [← basicOpen_eq_bot_iff] at hx ⊢
  rw [Scheme.basicOpen_res] at hx
  revert hx
  contrapose!
  simp_rw [Ne, ← Opens.not_nonempty_iff_eq_bot, Classical.not_not]
  apply nonempty_preirreducible_inter U.isOpen (RingedSpace.basicOpen _ _).isOpen
  simpa using H

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
x : ↥X
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)

Tactic:
obtain ⟨R, f, hf, hsub⟩ := Scheme.exists_affine_mem_range_and_range_subset
      (show x ∈ ⊤ from trivial)

Goal state after:
case inr
X : Scheme
x : ↥X
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
hsub : x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑⊤
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
x y : ↥X
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
rintro (hy : y ⤳ x)

Goal state after:
case mpr
X : Scheme
x y : ↥X
hy : y ⤳ x
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
have : QuasiCompact f' := MorphismProperty.of_isPullback H.flip inferInstance

Goal state after:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this : QuasiCompact f'
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this✝¹ : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
this✝ : x ∈ closure (Set.range ⇑(Cover.pullbackHom 𝒰 f i))
this : (𝒰.f i) x ∈ closure (⇑(𝒰.f i) '' Set.range ⇑(Cover.pullbackHom 𝒰 f i))
⊢ (𝒰.f i) x ∈ closure (Set.range ⇑f)

Tactic:
← Set.range_comp,

Goal state after:
case a.inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this✝¹ : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
this✝ : x ∈ closure (Set.range ⇑(Cover.pullbackHom 𝒰 f i))
this : (𝒰.f i) x ∈ closure (Set.range (⇑(𝒰.f i) ∘ ⇑(Cover.pullbackHom 𝒰 f i)))
⊢ (𝒰.f i) x ∈ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

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

Tactic:
rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]

Goal state after:
case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen
    (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) ((ConcreteCategory.hom U.topIso.inv) j)))
Module: Mathlib.RingTheory.RingHom.EssFiniteType

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R T).EssFiniteType
⊢ (algebraMap S (TensorProduct R S T)).EssFiniteType

Tactic:
essFiniteType_algebraMap

Goal state after:
R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : Algebra.EssFiniteType R T
⊢ Algebra.EssFiniteType S (TensorProduct R S T)
Module: Mathlib.RingTheory.RingHom.EssFiniteType

Goal state before:
pp: R S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ (algebraMap R S).EssFiniteType

Tactic:
essFiniteType_algebraMap

Goal state after:
R S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Algebra.EssFiniteType R S
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj ⟨U, hU⟩)
hx : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑I.support
hxU : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑U
⊢ (I.glueData.ι ⟨U, hU⟩ ≫ I.gluedTo) y ∈ Set.range ⇑I.gluedTo

Tactic:
exact ⟨_, rfl⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑I.gluedTo '' Set.range ⇑(I.glueData.ι U) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U

Tactic:
← Set.range_comp,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range (⇑I.gluedTo ∘ ⇑(I.glueData.ι U)) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Tactic:
← Set.range_comp,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ closure (Set.range (⇑(Hom.imageι f) ∘ ⇑(Hom.toImage f)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ ⇑(Scheme.Hom.coborderRange f).ι '' Set.range ⇑(Scheme.Hom.liftCoborder f) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f

Tactic:
← Set.range_comp,

Goal state after:
case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range (⇑(Scheme.Hom.coborderRange f).ι ∘ ⇑(Scheme.Hom.liftCoborder f)) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion (X.topIso.hom ≫ pullback.diagonal f)
⊢ IsImmersion (pullback.diagonal f)

Tactic:
MorphismProperty.cancel_left_of_respectsIso (P := @IsImmersion)

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion (pullback.diagonal f)
⊢ IsImmersion (pullback.diagonal f)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsOpen (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
by
  obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg
  rw [ht]
  exact (isClosed_zeroLocus (R := R) t).isOpen_compl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))

Tactic:
refine .of_right (h₁₂ := pullback.fst _ _) ?_ ?_
      (IsPullback.of_hasPullback f (Z.fromSpecResidueField (g y)))

Goal state after:
case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      pullback.fst f (Z.fromSpecResidueField (g y)))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))

case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝⁴ : GeometricallyIntegral f
inst✝³ : Flat f
inst✝² : UniversallyOpen f
inst✝¹ : IsIntegral S
inst✝ : IsLocallyNoetherian S
⊢ IsIntegral X

Tactic:
rw [isIntegral_iff_irreducibleSpace_and_isReduced]
  exact ⟨GeometricallyIrreducible.irreducibleSpace f f.isOpenMap,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤)) (coord (Spec S) i✝) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

Tactic:
conv_rhs => enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _

Goal state after:
case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤)) (coord (Spec S) i✝) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i✝))
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ (fun x ↦ ⟨pointOfClosedPoint f ↑x ⋯, ⋯⟩) ((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p) = p

Tactic:
by
    ext
    refine ((Scheme.SpecToEquivOfField _ _).symm_apply_eq (x := ⟨_, _⟩)).mpr ?_
    rw [Scheme.SpecToEquivOfField_eq_iff]
    dsimp [Scheme.SpecToEquivOfField]
    simp only [Category.id_comp, exists_const]
    generalize_proofs _ h
    refine (Category.comp_id _).symm.trans (((residueFieldIsoBase f _ h).eq_inv_comp).mp ?_)
    rw [← Spec.map_injective.eq_iff]
    simp only [Spec.map_id, Spec.map_comp, SpecMap_residueFieldIsoBase_inv]
    rw [reassoc_of% Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, p.2]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommMonoid Y
ι : Type u_3
s : Finset ι
F : ι → locallyFinsuppWithin U Y
⊢ ⇑(∑ n ∈ s, F n) = ∑ n ∈ s, ⇑(F n)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case left
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ f₁ x + f₂ x ≤ max (f₁ x) 0 + max (f₂ x) 0

Tactic:
simp [add_le_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
obtain ⟨U, hU, g, hg⟩ := X.presheaf.exists_germ_eq f

Goal state after:
X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
have : Nonempty A := ⟨_, hxA⟩

Goal state after:
X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
this : Nonempty ↥↑A
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g

Tactic:
refine ⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
      ⟨_, ⟨_, hxU, rfl⟩⟩,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩

Goal state after:
case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (ConcreteCategory.hom (↾⇑(F.map fi))) xi = (ConcreteCategory.hom (↾⇑(F.map fj))) xj
⊢ (ConcreteCategory.hom ((G ⋙ forget).map fi)) ((s.app i) xi) =
    (ConcreteCategory.hom ((G ⋙ forget).map fj)) ((s.app j) xj)

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      dsimp at heq
      rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]
      simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := ↑X.affineOpens, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)

Tactic:
use ⟨(isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose,
      (isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose_spec.1⟩

Goal state after:
case h
P : MorphismProperty Scheme
X : Scheme
x : ↥X
⊢ x ∈ Set.range ⇑({ I₀ := ↑X.affineOpens, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f ⟨⋯.choose, ⋯⟩)