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

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

Tactic:
by
  rw [eq]
  apply universally_isZariskiLocalAtTarget
  intro X Y f ι U hU H
  simp_rw [topologically, morphismRestrict_base] at H
  exact hU.isOpenMap_iff_restrictPreimage.mpr H

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

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)

Tactic:
refine this f _ _ ?_ ⟨_, rfl⟩

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
⊢ GeneralizingMap ⇑(X.affineCover.f i ≫ f)
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: ⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral

Tactic:
introv R hs H r
  let := f.toAlgebra
  change r ∈ (integralClosure R S).toSubmodule
  apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ s hs
  rintro ⟨t, ht⟩
  let := (Localization.awayMap f t).toAlgebra
  have : IsScalarTower R (Localization.Away t) (Localization.Away (f t)) := .of_algebraMap_eq'
    (IsLocalization.lift_comp _).symm
  have : _root_.IsIntegral (Localization.Away t) (algebraMap S (Localization.Away (f t)) r) :=
    H ⟨t, ht⟩ (algebraMap _ _ r)
  obtain ⟨⟨_, n, rfl⟩, p, hp, hp'⟩ := this.exists_multiple_integral_of_isLocalization (.powers t)
  rw [IsScalarTower.algebraMap_eq R S, Submonoid.smul_def, Algebra.smul_def,
    IsScalarTower.algebraMap_apply R S, ← map_mul, ← hom_eval₂,
    IsLocalization.map_eq_zero_iff (.powers (f t))] at hp'
  obtain ⟨⟨x, m, (rfl : algebraMap R S t ^ m = x)⟩, e⟩ := hp'
  by_cases hp' : 1 ≤ p.natDegree; swap
  · obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)
    exact ⟨m, by simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]⟩
  refine ⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩
  have := p.scaleRoots_eval₂_mul (algebraMap R S) (t ^ n • r) (t ^ m)
  simp only [pow_add, ← Algebra.smul_def, mul_smul, ← map_pow] at e this ⊢
  rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]

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

Goal state before:
pp: case h
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
⊢ ¬(e.val j %ₘ e.val i).degree = (ofLex e.degree).1 j

Tactic:
refine ((degree_modByMonic_lt _ hi).trans_le i_min).ne

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ (∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd) →
    Relation.EqvGen F.ColimitTypeRel x y

Tactic:
· rintro ⟨k, f, f', h⟩
    apply Relation.EqvGen.trans (y := ⟨k, F.map f' y.2⟩)
    · exact .rel _ _ ⟨f, by rw [← h]⟩
    · exact .symm _ _ (.rel _ _ ⟨f', rfl⟩)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ map n (Spec.map φ) =
    (SpecIso n S).hom ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv

Tactic:
rw [← Iso.inv_comp_eq]
  ext1
  · simp only [map_over, Category.assoc, SpecIso_inv_over, SpecIso_inv_over_assoc,
      ← Spec.map_comp, ← CommRingCat.ofHom_comp]
    rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]
  · simp only [TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, CommRingCat.comp_apply]
    conv_lhs => enter [2]; tactic => exact map_appTop_coord _ _
    conv_rhs => enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _
    rw [SpecIso_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
        CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, map_X]

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

Goal state after:
case h₁
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (i ≫ j))) S ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S =
    (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S) ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S

case h₂
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
k : (fun X ↦ X) n₁
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom (i ≫ j))) S))) (coord S k) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S)))
      (coord S k)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
⊢ restrict 0 h = 0

Tactic:
by
    ext x
    simp [restrict_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
hx : (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0
⊢ x = 0

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
    (S := ((Spec.structureSheaf R).obj.obj (.op <| PrimeSpectrum.basicOpen f))) (.powers f) x

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ f = g

Tactic:
rw [ext_iff]

Goal state after:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ f.equiv g

Tactic:
have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
    (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_

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

case refine_1
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ f.equiv g ↔ f = g

Tactic:
rw [equiv_iff_of_isSeparated_of_le (S := S) f.dense_domain le_rfl hfg.le]
  obtain ⟨Uf, _, f⟩ := f
  obtain ⟨Ug, _, g⟩ := g
  obtain rfl : Uf = Ug := hfg
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
i j : I
f : i ⟶ j
⊢ IsAffineHom (D'.map f)

Tactic:
suffices IsAffineHom (D'.map f ≫ ι.app j) from .of_comp _ (ι.app j)

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
i j : I
f : i ⟶ j
⊢ IsAffineHom (D'.map f ≫ ι.app j)
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X Y : Scheme
f g : X.PartialIso Y
e : f.source = g.source
e' : g.target = f.target
H : f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'
⊢ f = g

Tactic:
rw [ext_iff]

Goal state after:
X Y : Scheme
f g : X.PartialIso Y
e : f.source = g.source
e' : g.target = f.target
H : f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'
⊢ ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
x✝¹ : ∀ (i : I), Nonempty ↥(D'.obj i)
x✝ : ∀ (i : I), CompactSpace ↥(D'.obj i)
c' : Cone D' :=
  { pt := (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subscheme,
    π :=
      {
        app := fun i ↦
          (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeMap
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
m : s.pt ⟶ c'.pt
hm : ∀ (j : I), m ≫ c'.π.app j = s.π.app j
⊢ m =
    IsClosedImmersion.lift (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι
      (hc.lift ((Cone.postcompose ι).obj s)) ⋯

Tactic:
rw [← cancel_mono (subschemeι _)]
      refine hc.hom_ext fun i ↦ ?_
      simp [ι, c', ← hm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ≫ f.hom ∣_ g.domain ≫ g.hom) ∣_ h.domain ≫ h.hom =
    (X₁.isoOfEq ⋯).hom ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        f.hom ∣_ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain ≫
          (Hom.isoImage g.domain.ι (g.hom ⁻¹ᵁ h.domain)).inv ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
simp_rw [morphismRestrict_comp, morphismRestrict_ι_image_ι_isoImage_inv_assoc,
      Hom.comp_preimage, Category.assoc]

Goal state after:
case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain ≫
        f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom =
    (X₁.isoOfEq ⋯).hom ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        (↑f.domain).homOfLE ⋯ ≫
          (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
            f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V

Tactic:
have H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤ := by
    rw [Scheme.Hom.comp_preimage, ← top_le_iff]
    exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H✝ : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x).universally f

Tactic:
rw [universallyInjective_iff]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : (c.π.app i) x ∈ ↑V
this✝ : ∀ (j : (Over i)ᵒᵖ), IsAffine (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine ((opensDiagram D i V).obj j)
r : ↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
hrU : (((Functor.const I).obj c.pt).obj i).basicOpen r ≤ U
hxr : ↑⟨x, hxU⟩ ∈ (((Functor.const I).obj c.pt).obj i).basicOpen r
j : Over i
s : ↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V)
hs :
  (ConcreteCategory.hom (((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).ι.app (Opposite.op j)))
      ((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv s) =
    (ConcreteCategory.hom (c.π.app i ⁻¹ᵁ V).topIso.inv) r
h : c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V
⊢ r = (ConcreteCategory.hom (Scheme.Hom.appLE (c.π.app j.left) (D.map j.hom ⁻¹ᵁ V) (c.π.app i ⁻¹ᵁ V) ⋯)) s

Tactic:
convert!
      show r = ((topIso _).inv ≫ ((opensCone D c i V).π.app j).appTop ≫ (topIso _).hom) s from
        (c.π.app i ⁻¹ᵁ V).topIso.commRingCatIsoToRingEquiv.symm_apply_eq.mp hs.symm using 3

Goal state after:
case e'_5.e'_9
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : (c.π.app i) x ∈ ↑V
this✝ : ∀ (j : (Over i)ᵒᵖ), IsAffine (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine ((opensDiagram D i V).obj j)
r : ↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
hrU : (((Functor.const I).obj c.pt).obj i).basicOpen r ≤ U
hxr : ↑⟨x, hxU⟩ ∈ (((Functor.const I).obj c.pt).obj i).basicOpen r
j : Over i
s : ↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V)
hs :
  (ConcreteCategory.hom (((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).ι.app (Opposite.op j)))
      ((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv s) =
    (ConcreteCategory.hom (c.π.app i ⁻¹ᵁ V).topIso.inv) r
h : c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V
e_1✝ :
  (fun R S ↦ ↑R →+* ↑S) Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app i ⁻¹ᵁ V) =
    (fun R S ↦ ↑R →+* ↑S) Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
e_8✝ :
  Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app i ⁻¹ᵁ V) = Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
⊢ Scheme.Hom.appLE (c.π.app j.left) (D.map j.hom ⁻¹ᵁ V) (c.π.app i ⁻¹ᵁ V) ⋯ =
    (D.map j.hom ⁻¹ᵁ V).topIso.inv ≫ Scheme.Hom.appTop ((opensCone D c i V).π.app j) ≫ (c.π.app i ⁻¹ᵁ V).topIso.hom
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
ui : ↥(𝒰.X i)
j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
h : (𝒰.f i) ui = d.toBase ((colimit.ι d.functor j) xj)
⊢ (𝒰.f i) ui = (𝒰.f j) ((d.natTrans.app j) xj)

Tactic:
by
      simp only [h, functorOfLocallyDirected_obj, ← Scheme.Hom.comp_apply, ι_toBase]

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

Goal state before:
pp: case e'_2.e_a
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ Set.univ ⊆ zeroLocus (Set.range 0)

Tactic:
rintro x _ _ ⟨_, rfl⟩

Goal state after:
case e'_2.e_a
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
x : PrimeSpectrum R[X]
a✝ : x ∈ Set.univ
w✝ : Fin n
⊢ 0 w✝ ∈ ↑x.asIdeal