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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
⊢ supportSet = ⋂ U, X.zeroLocus ↑(ideal U)

Tactic:
let I' : X.IdealSheafData := { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen }

Goal state after:
X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
⊢ supportSet = ⋂ U, X.zeroLocus ↑(ideal U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr
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
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

pp: X✝ Y✝ X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hY : ∃ S, Y = Spec S
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

Tactic:
· intro x hx
      let 𝒰 := Y.affineCover
      obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
      have inst : QuasiCompact (𝒰.pullbackHom f i) :=
        MorphismProperty.pullback_snd _ _ inferInstance
      have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
        ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
      · have := image_closure_subset_closure_image (f := 𝒰.f i)
          (𝒰.f i).continuous (Set.mem_image_of_mem _ this)
        rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, 𝒰.pullbackHom_map] at this
        exact closure_mono (Set.range_comp_subset_range _ _) this
      · rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
        · exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
        · exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2
        · exact (IsPullback.of_hasPullback _ _).flip

Goal state after:
X✝ Y✝ X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hY : ∃ S, Y = Spec S
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) =
    𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))

Tactic:
apply pullback.hom_ext
      · rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
        rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]
      · rw [← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_snd_ι, limit.lift_π_assoc, cospan_left, glueDataT'Aux_fst_assoc,
          glueDataT_fst_assoc, Scheme.homOfLE_ι, Category.id_comp]
        rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : P g
x : ↥X
y : ↥Y
hxy : f x = g y
a : ↥(pullback f g)
b : (pullback.fst f g) a = x
h : (pullback.snd f g) a = y
⊢ ∃ a, (pullback.fst f g) a = x

Tactic:
use a

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
h : (g.comp f).EssFiniteType
⊢ g.EssFiniteType

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.EssFiniteType.of_comp R S T

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:
rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]

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

Goal state before:
pp: case a
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := ⋯
⊢ coprod.desc f g ⁻¹ᵁ W ≤ Scheme.Hom.opensRange i

Tactic:
intro x hx
    obtain ⟨(x | x), rfl⟩ := (coprodMk U V).surjective x
    · replace hx : f x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
      exact ⟨coprodMk _ _ (.inl ⟨x, hx⟩), by simp [i, ← Scheme.Hom.comp_apply]⟩
    · replace hx : g x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
      exact ⟨coprodMk _ _ (.inr ⟨x, hx⟩), by simp [i, ← Scheme.Hom.comp_apply]⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.app I.subschemeι ↑U)) = I.ideal U

Tactic:
by
  rw [subschemeι_app]
  let e : CommRingCat.of (Γ(X, U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ U) :=
    (Scheme.ΓSpecIso _).symm ≪≫ ((I.subschemeCover.f U).appIso _).symm ≪≫
      I.subscheme.presheaf.mapIso (eqToIso (by simp)).op
  change RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp
    (Ideal.Quotient.mk (I.ideal U))) = _
  rw [RingHom.ker_equiv_comp, Ideal.mk_ker]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
let e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(Limits.pullback (C := Scheme) f U.1.ι, ⊤) :=
    X.presheaf.mapIso (eqToIso (by simp [Scheme.Hom.opensRange_pullbackFst])).op
      ≪≫ (Limits.pullback.fst (C := Scheme) f U.1.ι).appIso ⊤

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))
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)
⊢ Set.range ⇑(Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f

Tactic:
f.liftCoborder_ι

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 ⇑f = ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

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

Tactic:
change IsLocallyClosed _

Goal state after:
case inst.refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : X ⟶ Y
f : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed (Set.range ⇑(i ≫ f))
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
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)

Tactic:
change IsLocallyClosed _

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 (Set.range ⇑(f ≫ i))
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
⊢ FinitePresentation R S

Tactic:
let I : Ideal (MvPolynomial (Fin n) R) := Ideal.span { ∑ g : s, g' g * h' g - 1 }

Goal state after:
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 = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
⊢ FinitePresentation R S
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
⊢ HasAffineProperty @IsClosedImmersion fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
by
  convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion
  refine ⟨fun ⟨h₁, h₂⟩ ↦ of_surjective_of_isAffine _ h₂, by apply isAffine_surjective_of_isAffine⟩

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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
⊢ f = g

Tactic:
by
  let X' : Over Z := Over.mk (f ≫ s)
  let Y' : Over Z := Over.mk s
  let U' : Over Z := Over.mk (ι ≫ f ≫ s)
  let f' : X' ⟶ Y' := Over.homMk f
  let g' : X' ⟶ Y' := Over.homMk g
  let ι' : U' ⟶ X' := Over.homMk ι
  have : IsSeparated Y'.hom := ‹_›
  have : IsDominant (equalizer.ι f' g').left := by
    apply +allowSynthFailures IsDominant.of_comp (equalizer.lift ι' ?_).left
    · rwa [← Over.comp_left, equalizer.lift_ι]
    · ext1; exact hU
  have : Surjective (equalizer.ι f' g').left :=
    surjective_of_isDominant_of_isClosed_range _ (Scheme.Hom.isClosedEmbedding _).isClosed_range
  have := isIso_of_isClosedImmersion_of_surjective (Y := X) (equalizer.ι f' g').left
  rw [← cancel_epi (equalizer.ι f' g').left]
  exact congr($(equalizer.condition f' g').left)

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

Goal state before:
pp: X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
ha : IsAffine Y
hsurj : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
⊢ IsAffine (Limits.pullback f g) ∧
    Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))

Tactic:
exact ⟨inferInstance, RingHom.surjective_isStableUnderBaseChange.pullback_fst_appTop _
    RingHom.surjective_respectsIso f _ hsurj⟩

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

Goal state before:
pp: case mpr
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
H : ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})

Tactic:
← mem_nilradical,

Goal state after:
case mpr
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
H :
  (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∉
    nilradical ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))

Tactic:
apply isOpen_sUnion

Goal state after:
R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ ∀ t ∈ Set.image (comap C) '' S, IsOpen t
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))

Tactic:
apply isOpen_sUnion

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ ∀ t ∈ Set.image (comap C) '' S, IsOpen t
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: 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))

pp: 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)

Tactic:
· simpa using! (IsPullback.of_hasPullback _ _).paste_horiz h

Goal state after:
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.Morphisms.Flat

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
⊢ IsOpen s

Tactic:
let 𝒰 := Y.affineCover
    rw [𝒰.isOpenCover_opensRange.isOpen_iff_inter]
    intro i
    rw [Scheme.Hom.coe_opensRange, ← Set.image_preimage_eq_inter_range]
    apply (𝒰.f i).isOpenEmbedding.isOpenMap
    refine this (f := pullback.fst (𝒰.f i) f) _ ?_ ⟨_, rfl⟩
    rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, pullback.condition,
      Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]
    exact hs.preimage (Scheme.Hom.continuous _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))

Tactic:
have := isIso_of_isTerminal specULiftZIsTerminal.{u} terminalIsTerminal (terminal.from _)

Goal state after:
n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z).Finite

Tactic:
intro z hz
      obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
      obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
      use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
      apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
      intro a ha
      simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
      by_contra! hCon
      simp_all

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✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite

Tactic:
intro z hz
      obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
      obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
      use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
      apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
      intro a ha
      simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
      by_contra! hCon
      simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
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 : ↑A
⊢ (CommRingCat.Hom.hom φ) a =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (e.symm.toRingHom.comp
              ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯)) ≫
          X.presheaf.germ V' x hxV'))
      a

Tactic:
change φ a = (e (e.symm _)).1

Goal state after:
case refine_1
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 : ↑A
⊢ (ConcreteCategory.hom φ) a =
    ↑(e (e.symm (((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) a)))
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case mpr
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
V : X.Opens
hV : Dense ↑V
g : ↑V ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = { domain := V, dense_domain := hV, hom := g }.domain),
      { domain := U, dense_domain := hU, hom := f }.hom =
        (X.isoOfEq e).hom ≫ { domain := V, dense_domain := hV, hom := g }.hom) →
    { domain := U, dense_domain := hU, hom := f } = { domain := V, dense_domain := hV, hom := g }

Tactic:
rintro ⟨rfl : U = V, e⟩

Goal state after:
case mpr
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
hV : Dense ↑U
g : ↑U ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
⊢ { domain := U, dense_domain := hU, hom := f } = { domain := U, dense_domain := hV, hom := g }