mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
hr : ↑r ≤ I.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height

Tactic:
by
  induction r with
  | zero => simp
  | succ r ih =>
    obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)
    let S := { K | K ∈ J.minimalPrimes ∧ Ideal.height K = r }
    have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing
      (fun _ h => h.1)
    have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) := by
      refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
      · rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime
      · push Not
        intro K hK e
        have := hr.trans (Ideal.height_mono e)
        rw [Set.Finite.mem_toFinset] at hK
        rw [hK.2, ← not_lt] at this
        norm_cast at this
        exact this r.lt_succ_self
    simp_rw [Set.not_subset, Set.mem_iUnion, not_exists, Set.Finite.mem_toFinset] at this
    obtain ⟨x, hx₁, hx₂⟩ := this
    refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
    · rwa [Ideal.span_le, Set.singleton_subset_iff]
    · apply Submodule.spanRank_sup_le_sum_spanRank.trans
      push_cast
      exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))
    · refine le_iInf₂ (fun p hp ↦ ?_)
      have := hp.isPrime
      rw [← p.height_eq_primeHeight]
      by_cases h : p.height = ⊤
      · exact le_of_le_of_eq le_top h.symm
      have : p.FiniteHeight := ⟨Or.inr h⟩
      have := Ideal.height_mono (le_sup_left.trans hp.le)
      suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
      intro e
      apply hx₂ p
      · refine ⟨mem_minimalPrimes_of_height_le (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩
      · apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x

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

Goal state before:
pp: P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P) fun {x S} {x_1} {x_2} φ ↦
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Tactic:
have := stalkwiseIsZariskiLocalAtTarget_of_respectsIso hP
  have := stalkwise_isZariskiLocalAtSource_of_respectsIso hP
  convert!
    of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget (P := AlgebraicGeometry.stalkwise P) with R
    S _ _ φ
  exact (stalkwise_SpecMap_iff hP (CommRingCat.ofHom φ)).symm

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

Goal state before:
pp: case h.refine_1
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this✝ : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
this :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂)
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op))
      (↑⟨((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁,
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂),
            this⟩).1 =
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁ + n₂) * x)

Tactic:
change (X.presheaf.map _) _ = (X.presheaf.map _) _
      rw [add_assoc, add_comm n₁]
      simp only [pow_add, map_pow, map_mul, hy₁, ← CommRingCat.comp_apply, ← mul_assoc,
        ← Functor.map_comp, ← op_comp, homOfLE_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ¬Set.univ ⊆ S
h₃ : ¬Set.univ ⊆ T
⊢ False

Tactic:
rw [Set.not_univ_subset] at h₂ h₃

Goal state after:
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
⊢ False
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
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : (𝒰.f i) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv 0

Tactic:
map_zero,

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
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : (𝒰.f i) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case left
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

pp: case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))

Tactic:
· simp only [Scheme.preimage_basicOpen, Opens.map_top]
      exact (isAffineOpen_top X).basicOpen _

Goal state after:
case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

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

Tactic:
rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullback₁ f)).jacobsonSpace_iff]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Surjective ⇑f).RespectsIso

Tactic:
rw [← RingHom.toMorphismProperty_respectsIso_iff]

Goal state after:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ closure (⇑f ⁻¹' ↑I.support) = ↑(I.support.preimage ⋯)

Tactic:
TopologicalSpace.Closeds.coe_preimage,

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ closure (⇑f ⁻¹' ↑I.support) = ⇑f ⁻¹' ↑I.support
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' ↑R).toRingHom))

Tactic:
exact .spec_of_surjective _ fun x ↦ ⟨.tmul R 1 x,
    (Algebra.TensorProduct.lmul'_apply_tmul (R := R) (S := S) 1 x).trans (one_mul x)⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| TopologicalSpace.Opens.map f.base

Tactic:
← f.liftCoborder_ι

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| TopologicalSpace.Opens.map (liftCoborder f ≫ (coborderRange f).ι).base
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType f

Tactic:
← f.liftCoborder_ι

Goal state after:
X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
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
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ f ((∑ g ∈ s.attach, g' g * h' g - 1) * q) = 0

Tactic:
simp only [map_mul, map_sub, map_sum, map_one, hg', hh']

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}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0
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
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.f i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s ^ n) *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0

Tactic:
map_pow

Goal state after:
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
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.f i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0
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
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ fn i * g)) = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s ^ Finset.univ.sup fn) *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0

Tactic:
map_pow

Goal state after:
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
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ fn i * g)) = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ Finset.univ.sup fn *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
let U : (Σ i, (𝒱 i).I₀) → (diagonalCoverDiagonalRange f 𝒰 𝒱).toScheme.Opens := fun i ↦
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange
  have hU (i) : (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i =
      ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange := by
    rw [Scheme.Hom.image_preimage_eq_opensRange_inf, inf_eq_right, Opens.opensRange_ι]
    exact le_iSup (fun i : Σ i, (𝒱 i).I₀ ↦ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange) i
  have hf : iSup U = ⊤ := (TopologicalSpace.Opens.map_iSup _ _).symm.trans
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι_preimage_self
  rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsClosedImmersion) _ hf]
  intro i
  rw [MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictRestrict _ _ _),
    MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictEq _ (hU i)),
    MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (diagonalRestrictIsoDiagonal ..)]
  infer_instance

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

Goal state before:
pp: X : Scheme
⊢ autoParam (IsClosedImmersion (pullback.diagonal (terminal.from X)))
      IsSeparated.isClosedImmersion_diagonal._autoParam ↔
    IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
iff_iff_eq,

Goal state after:
X : Scheme
⊢ autoParam (IsClosedImmersion (pullback.diagonal (terminal.from X)))
      IsSeparated.isClosedImmersion_diagonal._autoParam =
    IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))
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))
⊢ pullback.snd f g ⁻¹ᵁ V = pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V

Tactic:
grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]

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}
⊢ IsIrreducible (⇑f ⁻¹' s)

Tactic:
refine hs.preimage_of_isPreirreducible_fiber _ hf
      (fun x ↦ (this isIrreducible_singleton ⟨_, rfl⟩).isPreirreducible) ?_
    rw [Set.range_eq_univ.mpr f.surjective, Set.inter_univ]
    exact hs.nonempty

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ UniversallyClosed f

Tactic:
rw [universallyClosed_eq]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ (topologically @IsClosedMap).universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyClosed

Tactic:
rw [universallyClosed_eq]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsClosedMap).universally.IsStableUnderComposition
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

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

Tactic:
rw [universallyClosed_eq]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget (topologically @IsClosedMap).universally
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed

Tactic:
rw [universallyClosed_eq]

Goal state after:
case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally
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

pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' 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:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
hY : ∃ R, Y = Spec R
⊢ IsOpen s