mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
have h₂ : colimit.ι F i =
      { hom := (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫
        (preservesColimitIso _ F).inv) } :=
      InducedCategory.hom_ext h₁.symm

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
      refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
      change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x
      cat_disch

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

Goal state before:
pp: X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
by
      rw [presieve₀_mem_precoverage_iff]
      refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
      change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x
      cat_disch

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_2.e'_6.e'_6.e'_5
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
this : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c
j : Discrete ι
hj : op j ≠ op i
e_1✝¹ : Opens ↑↑(F.obj j).toPresheafedSpace = Opens ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
e_1✝ : Opens ↑↑(colimit F).toPresheafedSpace = Opens ↑↑(forgetToPresheafedSpace.obj (colimit F))
e_2✝ :
  Preorder.smallCategory (Opens ↑↑((F ⋙ forgetToPresheafedSpace).obj i)) =
    Preorder.smallCategory (Opens ↑↑(F.obj i).toPresheafedSpace)
e_4✝ :
  Preorder.smallCategory (Opens ↑↑(forgetToPresheafedSpace.obj (colimit F))) =
    Preorder.smallCategory (Opens ↑↑(colimit F).toPresheafedSpace)
⊢ (colimit.ι (F ⋙ forgetToPresheafedSpace) i).base ≫ (preservesColimitIso forgetToPresheafedSpace F).inv.base =
    (colimit.ι F i).hom.base

Tactic:
exact congr_arg PresheafedSpace.Hom.base h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ X.basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r

Tactic:
topIso_inv,

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r) = X.basicOpen r
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(⊥.colon {d • a - b • c}))

Tactic:
PrimeSpectrum.mem_vanishingIdeal

Goal state after:
case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus ↑(⊥.colon {d • a - b • c}), f ∈ x.asIdeal
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
R : TopCommRingCat
X : TopCatᵒᵖ
⊢ continuousFunctions.pullback (𝟙 X) R = 𝟙 (continuousFunctions X R)

Tactic:
by
        ext
        rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (Set.range b))

Tactic:
PrimeSpectrum.mem_vanishingIdeal

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus (Set.range b), f ∈ x.asIdeal
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
by
  rwa [f.isAffineOpen_iff_of_isOpenImmersion]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
⊢ f = g

Tactic:
have : Mono φ := ConcreteCategory.mono_of_injective _ hφ
  rw [← IsOpenImmersion.lift_fac U.ι f (by simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx),
    ← IsOpenImmersion.lift_fac U.ι g (by simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx)]
  congr 1
  rw [← cancel_mono hU.isoSpec.hom, ← Spec.homEquiv.injective.eq_iff,
    ← cancel_mono φ, ← Spec.map_injective.eq_iff]
  simp [← cancel_mono U.ι, H]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case h
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := ⋯
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ s = X.zeroLocus ↑I

Tactic:
simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]

Goal state after:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ s = ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y : ↥(gluedCover 𝒰).glued
h : (fromGlued 𝒰) x = (fromGlued 𝒰) y
⊢ x = y

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x

Goal state after:
X : Scheme
𝒰 : X.OpenCover
y : ↥(gluedCover 𝒰).glued
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
h : (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) = (fromGlued 𝒰) y
⊢ ((gluedCover 𝒰).ι i) x = y
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x : ↥(gluedCover 𝒰).glued
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) x)

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ IsIso f

Tactic:
have : Epi f.base := by
    rw [TopCat.epi_iff_surjective]; rintro (x : Y)
    exact isEmptyElim x

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this✝ : IsEmpty ↥X
this : Epi f.base
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))

Tactic:
· apply isOpenImmersion_sigmaDesc_aux
    intro i j hij
    exact hα (fun h ↦ hij (e.symm.injective h))

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

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P f

Tactic:
exact P.of_zeroHypercover_target Y.affineCover
        fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf

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

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ ∀ {ι : Type u_1} (U : ι → Opens β),
    IsOpenCover U →
      Continuous[inst✝¹, inst✝] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
ι

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
⊢ ∀ (U : ι → Opens β),
    IsOpenCover U →
      Continuous[inst✝¹, inst✝] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy✝ : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy : ⟨y, hi⟩ ∈ closure[instTopologicalSpaceSubtype] {⟨f x, hfx⟩}
a : ↑(f ⁻¹' (U i).carrier)
ha : ↑a ∈ closure[inst✝¹] (Subtype.val '' {⟨x, hfx⟩})
hay : (U i).carrier.restrictPreimage f a = ⟨y, hi⟩
⊢ y ∈ f '' closure[inst✝¹] {x}

Tactic:
simp only [Opens.carrier_eq_coe, Set.image_singleton] at ha

Goal state after:
case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy✝ : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy : ⟨y, hi⟩ ∈ closure[instTopologicalSpaceSubtype] {⟨f x, hfx⟩}
a : ↑(f ⁻¹' (U i).carrier)
hay : (U i).carrier.restrictPreimage f a = ⟨y, hi⟩
ha : ↑a ∈ closure[inst✝¹] {x}
⊢ y ∈ f '' closure[inst✝¹] {x}
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f

Tactic:
ι

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
⊢ ∀ (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
ι

Goal state after:
case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
⊢ ∀ (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
ι

Goal state after:
case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
⊢ ∀ (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
ι

Goal state after:
case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
⊢ ∀ (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case to_basicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : CompactSpace ↥X
⊢ CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen r)

Tactic:
rw [Scheme.preimage_basicOpen f r]

Goal state after:
case to_basicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : CompactSpace ↥X
⊢ CompactSpace ↥↑(X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r))
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')
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
obtain ⟨s, s', hBss', hBx⟩ := exists_basicOpen_le_affine_inter V₁.2 ha x ⟨hx₁, hxa⟩

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
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
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✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.affineRefinement.openCover.I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.affineRefinement.openCover.f i ≫ f)))) ↔
    ∀ (i : 𝒰.I₀) (i_1 : (𝒰.X i).affineCover.I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((𝒰.X i).affineCover.f i_1 ≫ 𝒰.f i ≫ f)))

Tactic:
simp [Scheme.OpenCover.affineRefinement, Sigma.forall]

Goal state after:
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:
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.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal

Tactic:
by
  refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_
  simp only [iInf_insert, e, ideal_inf]

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

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
n : ℕ
e : f ^ n * z = 0
⊢ ↑⟨(fun x ↦ f ^ x) n, ⋯⟩ * z = 0

Tactic:
simpa [mul_comm z] using! e

Goal state after: