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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ IsOpenCover (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift)

Tactic:
IsOpenCover,

Goal state after:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ iSup (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → Opens X),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (f ∘ Subtype.val))
X Y : Type u
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
U : Opens X
hs : P f
⊢ IsOpenCover (![⊤, U] ∘ ⇑Equiv.ulift)

Tactic:
IsOpenCover,

Goal state after:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → Opens X),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (f ∘ Subtype.val))
X Y : Type u
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
U : Opens X
hs : P f
⊢ iSup (![⊤, U] ∘ ⇑Equiv.ulift) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r

Tactic:
rw [hBss', hBrr']

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.primeHeight = 0 ↔ I ∈ minimalPrimes R

Tactic:
rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_zero_iff]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
⊢ I.IsMaximal

Tactic:
rcases lt_or_eq_of_le hM' with (hM' | hM')

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I < M
⊢ I.IsMaximal

case inr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I = M
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsMaximal), I.height) = ringKrullDim R

Tactic:
Ideal.sup_isMaximal_height_eq_ringKrullDim

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim (Rₚ P) ≤ ↑n
a✝ : Nontrivial R
P : Ideal R
hP : P.IsMaximal
⊢ P.height ≤ ↑n

Tactic:
rw [← WithBot.coe_le_coe, ← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim (Rₚ P) ≤ ↑n
a✝ : Nontrivial R
P : Ideal R
hP : P.IsMaximal
⊢ ringKrullDim (Rₚ P) ≤ ↑↑n
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
⊢ s = 0

Tactic:
apply TopCat.Presheaf.section_ext X.sheaf U
  intro x hx
  change (X.sheaf.presheaf.germ U x hx) s = (X.sheaf.presheaf.germ U x hx) 0
  rw [map_zero]
  induction U using reduce_to_affine_global generalizing hX with
  | h₁ X U H =>
    obtain ⟨V, hx, i, H⟩ := H ⟨x, hx⟩
    specialize H (X.presheaf.map i.op s)
    rw [Scheme.basicOpen_res, hs] at H
    specialize H (inf_bot_eq _) x hx
    rw [← X.sheaf.presheaf.germ_res_apply i x hx s]
    exact H
  | h₂ X Y f =>
    refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by simp, rfl, ?_⟩
    rintro H hX s hs _ ⟨x, rfl⟩
    have := isReduced_of_isOpenImmersion f
    specialize H (f.app _ s) _ x ⟨x, rfl⟩
    · rw [← Scheme.preimage_basicOpen, hs]; ext1; simp [Opens.map]
    · have H : (X.presheaf.germ _ x _).hom _ = 0 := H
      rw [← Scheme.Hom.germ_stalkMap_apply f ⟨_, _⟩ x] at H
      apply_fun inv <| f.stalkMap x at H
      rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] at H
      exact H
  | h₃ R =>
    rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs
    replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero
    rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs
    rw [hs, map_zero]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
this :
  IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f)
    (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f))
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)

Tactic:
exact IsOpenImmersion.of_isLocalization (Ideal.Quotient.mk _ f)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ (↑U).fromSpecStalk ⟨x, hxU⟩ ≫ U.ι = Spec.map (Hom.stalkMap U.ι ⟨x, hxU⟩) ≫ X.fromSpecStalk x

Tactic:
exact (Scheme.SpecMap_stalkMap_fromSpecStalk U.ι (x := ⟨x, hxU⟩)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x

Tactic:
simp only [Opens.fromSpecStalkOfMem, Spec.map_inv, Category.assoc, IsIso.inv_comp_eq]
  exact (Scheme.SpecMap_stalkMap_fromSpecStalk U.ι (x := ⟨x, hxU⟩)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial = X.presheaf.germ U x hxU ≫ Hom.stalkMap U.ι ⟨x, hxU⟩

Tactic:
Iso.inv_comp_eq

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial = U.topIso.hom ≫ X.presheaf.germ U x hxU ≫ Hom.stalkMap U.ι ⟨x, hxU⟩
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯) ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V

Tactic:
by rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
          exact fun x _ ↦ by simpa using (F x).2.2

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

Tactic:
simp only [Scheme.preimage_basicOpen, Opens.map_top]

Goal state after:
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 ↑(X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ Function.Injective ⇑I.gluedTo

Tactic:
intro a b e

Goal state after:
X : Scheme
I : X.IdealSheafData
a b : ↥I.glueData.glued
e : I.gluedTo a = I.gluedTo b
⊢ a = b
Module: Mathlib.RingTheory.RingHom.EssFiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
hf : f.EssFiniteType
⊢ ((IsLocalRing.ResidueField.map f).comp (IsLocalRing.residue R)).EssFiniteType

Tactic:
IsLocalRing.ResidueField.map_comp_residue

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
hf : f.EssFiniteType
⊢ ((IsLocalRing.residue S).comp f).EssFiniteType
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:
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.RingTheory.Finiteness.FiniteTypeLocal

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

Tactic:
exact fun _ => by simp [Submonoid.mem_powers_iff]

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
q : ↑V ⟶ ↑W := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
⊢ f' ≫ W.ι = U.ι ≫ f

Tactic:
simp [f']

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
this : Epi (app (ker f).subschemeι ↑U)
⊢ app f ↑U =
    CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯) ≫
        X.presheaf.map (eqToHom ⋯)

Tactic:
← reassoc_of% CommRingCat.ofHom_comp,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
this : Epi (app (ker f).subschemeι ↑U)
⊢ app f ↑U =
    CommRingCat.ofHom
        ((Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯).comp
          (Ideal.Quotient.mk ((ker f).ideal U))) ≫
      X.presheaf.map (eqToHom ⋯)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ (map f s).toSet = comap f ⁻¹' s.toSet

Tactic:
by
  unfold toSet map
  rw [set_biUnion_finset_image]
  simp

Goal state after:
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)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
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

Goal state after:
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)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
⊢ IsSeparated f

Tactic:
by
  constructor
  let 𝒰 := Y.affineCover
  let 𝒱 (i) := (pullback f (𝒰.f i)).affineCover
  refine IsZariskiLocalAtTarget.of_iSup_eq_top (fun i : PUnit.{0} ↦ ⊤) (by simp) fun _ ↦ ?_
  rw [← diagonalCoverDiagonalRange_eq_top_of_injective f 𝒰 𝒱 hf]
  exact isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱

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

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

Tactic:
refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_
    have inst : LocallyOfFinitePresentation (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    have inst : QuasiCompact (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    convert!
      (this (Y.affineCover.pullbackHom f i)
            (hs.preimage_of_isOpenEmbedding ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding)
            ⟨_, rfl⟩).preimage_of_isOpenEmbedding
        (Y.affineCover.f i).isoOpensRange.inv.isOpenEmbedding
    refine .trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)
    apply Set.image_injective.mpr Subtype.val_injective
    rw [Set.image_preimage_eq_inter_range, ← Set.image_comp, ← Set.image_comp,
      Subtype.range_coe_subtype, Set.ofPred_mem_eq]
    change _ = (Y.affineCover.pullbackHom f i ≫
      (Y.affineCover.f i).isoOpensRange.hom ≫ Opens.ι _).base.hom '' _
    rw [Scheme.Hom.isoOpensRange_hom_ι, Cover.pullbackHom_map, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range]
    simp [IsOpenImmersion.range_pullbackFst, Set.image_inter_preimage]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsNoetherianRing ↑Γ(X, U)

Tactic:
apply IsLocallyNoetherian.component_noetherian ⟨U, hU⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
⊢ IsLocallyArtinian X

Tactic:
wlog hX : Subsingleton X generalizing X

Goal state after:
case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
⊢ IsLocallyArtinian X

X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
⊢ IsLocallyArtinian X
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
h : IsPullback fst snd f y
⊢ P Z

Tactic:
obtain ⟨⟨y, φ⟩, rfl⟩ := (Scheme.SpecToEquivOfField _ _).symm.surjective y

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f ((Scheme.SpecToEquivOfField K Y).symm ⟨y, φ⟩)
⊢ P Z
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
⊢ ∀ (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → topologically (@IsOpenMap) f'

Tactic:
i₂

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
⊢ ∀ (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → topologically (@IsOpenMap) f'
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
⊢ ∀ (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → topologically (@IsClosedMap) f'

Tactic:
i₂

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
⊢ ∀ (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → topologically (@IsClosedMap) f'
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
⊢ ∀ (i₂ : Y' ⟶ Z) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ g → topologically (@IsClosedMap) f'

Tactic:
i₂

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
⊢ ∀ (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ g → topologically (@IsClosedMap) f'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C

Tactic:
Iso.inv_comp_eq

Goal state after:
n : Type u
R : CommRingCat
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f) (𝔸(n; S) ↘ S) (𝔸(n; T) ↘ T) f

Tactic:
refine (IsPullback.paste_horiz_iff (.flip <| .of_hasPullback _ _) (map_over f)).mp ?_

Goal state after:
n : Type u
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n]))) (𝔸(n; S) ↘ S)
    (terminal.from (Spec ℤ[n])) (f ≫ terminal.from T)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (i ≫ j))) S =
    reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S

Tactic:
ext k <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ geometrically (fun x ↦ IrreducibleSpace ↥x) (𝔸(n; S) ↘ S)

Tactic:
introv K h

Goal state after:
n : Type u
S : Scheme
K : Type u
inst✝ : Field K
y : Spec (CommRingCat.of K) ⟶ S
Z : Scheme
fst : Z ⟶ 𝔸(n; S)
snd : Z ⟶ Spec (CommRingCat.of K)
h : IsPullback fst snd (𝔸(n; S) ↘ S) y
⊢ IrreducibleSpace ↥Z