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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
⊢ IsPullback (Cover.pullbackHom Y.openCoverBasicOpenTop f r)
    ((Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ)
    (Y.openCoverBasicOpenTop.f r ≫ Y.toSpecΓ) (Spec.map (Hom.appTop f))

Tactic:
let e : pullback f (Y.basicOpen r.1).ι ≅ Spec Γ(X, X.basicOpen (f.appTop r.1)) :=
    pullbackRestrictIsoRestrict _ _ ≪≫ X.isoOfEq (Scheme.preimage_basicOpen_top f r.1) ≪≫
    IsAffineOpen.isoSpec (by rw [← Scheme.preimage_basicOpen_top]; exact r.2.preimage f)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ IsPullback (Cover.pullbackHom Y.openCoverBasicOpenTop f r)
    ((Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ)
    (Y.openCoverBasicOpenTop.f r ≫ Y.toSpecΓ) (Spec.map (Hom.appTop f))
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

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

Tactic:
exact .rel _ _ ⟨f, by rw [← h]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
h : IsReduced S
⊢ IsReduced 𝔸(n; S)

Tactic:
wlog hS : ∃ R, S = Spec R
  · rw [IsReduced.iff_of_openCover _ (S.affineCover.pullback₁ (𝔸(n; S) ↘ S))]
    intro i
    have : IsReduced 𝔸(n; S.affineCover.X i) := this _ ⟨_, rfl⟩
    exact isReduced_of_isOpenImmersion ((isPullback_map _).isoPullback.inv)
  obtain ⟨R, rfl⟩ := hS
  rw [affine_isReduced_iff] at h
  exact isReduced_of_isOpenImmersion (SpecIso n R).hom

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

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ ⟨↑((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p),
      (residueFieldIsoBase f ↑((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p) ⋯).1⟩ =
    (Scheme.SpecToEquivOfField K X) ↑p

Tactic:
rw [Scheme.SpecToEquivOfField_eq_iff]

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ ∃ (e :
    ⟨↑((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p),
          (residueFieldIsoBase f ↑((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p) ⋯).1⟩.fst =
      ((Scheme.SpecToEquivOfField K X) ↑p).fst),
    ⟨↑((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p),
          (residueFieldIsoBase f ↑((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p) ⋯).1⟩.snd =
      (Scheme.residueFieldCongr e).hom ≫ ((Scheme.SpecToEquivOfField K X) ↑p).snd
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ IsDiscrete D.support

Tactic:
by
  have : D.support = {x | D x = 0}ᶜ ∩ U := by
    ext x
    constructor
    · exact fun hx ↦ ⟨by tauto, D.supportWithinDomain hx⟩
    · intro hx
      rw [mem_inter_iff, mem_compl_iff, mem_ofPred_eq] at hx
      tauto
  rw [this]
  apply isDiscrete_of_codiscreteWithin
  rw [compl_compl]
  apply (supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
  exact D.supportLocallyFiniteWithinDomain

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
intro z hz

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
Module: Mathlib.Topology.LocallyFinsupp

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

Tactic:
intro z hz

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

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

Tactic:
intro z hz

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ ∀ z ∈ V, ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0).Finite

Tactic:
intro z hz

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0).Finite
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst✝ : IsLocallyNoetherian X
⊢ X.IsGermInjective

Tactic:
by
  suffices ∀ (R : CommRingCat.{u}) (_ : IsNoetherianRing R), (Spec R).IsGermInjective by
    refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
    exact isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))
  refine fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_
  let J := RingHom.ker <| algebraMap R (Localization.AtPrime I)
  have hJ (x) : x ∈ J ↔ ∃ y : I.primeCompl, y * x = 0 :=
    IsLocalization.map_eq_zero_iff I.primeCompl _ x
  choose f hf using fun x ↦ (hJ x).mp
  obtain ⟨s, hs⟩ := (isNoetherianRing_iff_ideal_fg R).mp ‹_› J
  have hs' : (s : Set R) ⊆ J := hs ▸ Ideal.subset_span
  refine ⟨_, (s.attach.prod fun x ↦ f x (hs' x.2)).2, fun x y e hy ↦ ⟨1, ?_⟩⟩
  rw [pow_one, mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton]
  refine SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)
  rw [← hs, Ideal.span_le]
  intro i hi
  rw [SetLike.mem_coe, Submodule.mem_annihilator_span_singleton, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton, Submonoid.coe_finsetProd]
  refine Ideal.mem_of_dvd _ (Finset.dvd_prod_of_mem _ (s.mem_attach ⟨i, hi⟩)) ?_
  rw [Submodule.mem_annihilator_span_singleton, smul_eq_mul]
  exact hf i _

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
fapply spread_out_unique_of_isGermInjective
  · simpa using congr($e (IsLocalRing.closedPoint _))
  · apply Spec.map_injective
    rw [← cancel_mono (Y.fromSpecStalk _)]
    simpa [Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

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

Goal state before:
pp: case e'_2.e'_4.e_a
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
⊢ IsUnit (IsLocalization.Away.invSelf c)

Tactic:
exact isUnit_iff_exists_inv'.mpr ⟨_, IsLocalization.Away.mul_invSelf c⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: case convert_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ (Set.univ ∩ Set.range ⇑f).Nonempty

Tactic:
exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ (Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
        (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩)) ≫
      f.hom =
    (Spec.map (((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩)) ≫
      f.hom

Tactic:
congr 3

Goal state after:
case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩) =
    ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

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

Tactic:
· rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
      ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H
    simpa only [fromSpecStalkOfMem, restrict_domain, Opens.fromSpecStalkOfMem, Spec.map_inv,
      restrict_hom, Category.assoc, IsIso.eq_inv_comp, IsIso.hom_inv_id_assoc] using H

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')
X Y : I
f : X ⟶ Y
⊢ vanishingIdeal { carrier := Z Y, isClosed' := ⋯ } ≤ (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).map (D.map f)

Tactic:
rw [map_vanishingIdeal, ← le_support_iff_le_vanishingIdeal]
      simpa [(hZc _).closure_subset_iff] using (hmapsTo f).subset_preimage

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

Goal state before:
pp: case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
x✝ : ↥X
⊢ x✝ ∈ ↑((f.restrict U hU hU').comp g).domain ↔
    x✝ ∈ ↑((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).domain

pp: case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
⊢ ((f.restrict U hU hU').comp g).hom =
    (X.isoOfEq ⋯).hom ≫ ((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).hom

Tactic:
· simp [ι_image_homOfLE_eq_ι_image_inf]

Goal state after:
case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
⊢ ((f.restrict U hU hU').comp g).hom =
    (X.isoOfEq ⋯).hom ≫ ((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
g₁ g₂ : Spec (CommRingCat.of K) ⟶ X
hg : (fun g ↦ g ≫ f) g₁ = (fun g ↦ g ≫ f) g₂
e :
  (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) =
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₂.base) (IsLocalRing.closedPoint K))
h :
  CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f (g₁ (IsLocalRing.closedPoint K)) ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo g₁)) =
    CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) ≫
        (Scheme.residueFieldCongr ⋯).hom ≫ Scheme.descResidueField (Scheme.stalkClosedPointTo g₂))
⊢ (Scheme.SpecToEquivOfField K X) g₁ = (Scheme.SpecToEquivOfField K X) g₂

Tactic:
rw [Scheme.SpecToEquivOfField_eq_iff]

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
g₁ g₂ : Spec (CommRingCat.of K) ⟶ X
hg : (fun g ↦ g ≫ f) g₁ = (fun g ↦ g ≫ f) g₂
e :
  (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) =
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₂.base) (IsLocalRing.closedPoint K))
h :
  CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f (g₁ (IsLocalRing.closedPoint K)) ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo g₁)) =
    CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) ≫
        (Scheme.residueFieldCongr ⋯).hom ≫ Scheme.descResidueField (Scheme.stalkClosedPointTo g₂))
⊢ ∃ (e : ((Scheme.SpecToEquivOfField K X) g₁).fst = ((Scheme.SpecToEquivOfField K X) g₂).fst),
    ((Scheme.SpecToEquivOfField K X) g₁).snd =
      (Scheme.residueFieldCongr e).hom ≫ ((Scheme.SpecToEquivOfField K X) g₂).snd
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case e'_3
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]
⊢ coeff(f) = ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}

Tactic:
trans f.coeff '' (Set.Iio (f.natDegree + 2))

Goal state after:
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]
⊢ coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)

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]
⊢ f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf✝ : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
hcomp : (fun x ↦ f x.fst x.snd) ∘ p = fun x ↦ g x.fst x.snd
hp : Continuous p
hf : Continuous fun p ↦ f p.fst p.snd
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun p ↦ g p.fst p.snd) '' V.carrier = U
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

Tactic:
obtain ⟨K, hK, ho, hVK, hKU⟩ := PrespectralSpace.exists_isCompact_and_isOpen_between
      (hV.image hp) (ho.preimage hf) <| by
    simp [← heq, ← Set.preimage_comp, hcomp, Set.subset_preimage_image]

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf✝ : ∀ (i : ι), Continuous (f i)
U : Set S
ho✝ : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
hcomp : (fun x ↦ f x.fst x.snd) ∘ p = fun x ↦ g x.fst x.snd
hp : Continuous p
hf : Continuous fun p ↦ f p.fst p.snd
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun p ↦ g p.fst p.snd) '' V.carrier = U
K : Set ((i : ι) × X i)
hK : IsCompact K
ho : IsOpen K
hVK : p '' V.carrier ⊆ K
hKU : K ⊆ (fun p ↦ f p.fst p.snd) ⁻¹' U
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰 : PreZeroHypercover S
𝒱 : PreZeroHypercover S
f : 𝒱.Hom 𝒰
inst✝ : QuasiCompactCover 𝒱
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (fun x ↦ ⇑(𝒰.f x)) ↑U

Tactic:
exact .of_comp (a := f.s₀) (𝒱.f ·) (f.h₀ ·)
    (fun _ ↦ Scheme.Hom.continuous _) (fun i ↦ funext <| by simp [← Scheme.Hom.comp_apply])
    (fun _ ↦ Scheme.Hom.continuous _) U.2 (hU.isCompactOpenCovered 𝒱)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
this : forgetToTop.map (fst π π ≫ f) = forgetToTop.map (snd π π ≫ f)
⊢ fst π.base π.base ≫ f.base = snd π.base π.base ≫ f.base

Tactic:
Functor.map_comp,

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
this : forgetToTop.map (fst π π) ≫ forgetToTop.map f = forgetToTop.map (snd π π ≫ f)
⊢ fst π.base π.base ≫ f.base = snd π.base π.base ≫ f.base
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
this : forgetToTop.map (fst π π) ≫ forgetToTop.map f = forgetToTop.map (snd π π ≫ f)
⊢ fst π.base π.base ≫ f.base = snd π.base π.base ≫ f.base

Tactic:
Functor.map_comp,

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
this : forgetToTop.map (fst π π) ≫ forgetToTop.map f = forgetToTop.map (snd π π) ≫ forgetToTop.map f
⊢ fst π.base π.base ≫ f.base = snd π.base π.base ≫ f.base
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this✝ : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
l : I
hl1 : {X : I} → X ∈ O → (l ⟶ X)
hl2 :
  ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
    ⟨X_1, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈
        Finset.image (fun i ↦ ⟨k (Cover.idx A.𝒰D ↑i), ⟨A.i', ⟨⋯, ⟨⋯, hki' (Cover.idx A.𝒰D ↑i)⟩⟩⟩⟩) Finset.univ →
      hl1 mX ≫ f_1 = hl1 mY
this : ∀ (w v : 𝒰Df.I₀), hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D ↑w) = hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D ↑v)
u : (Precoverage.ZeroHypercover.pullback₁ (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o))) 𝒰Df).I₀
⊢ D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o)) ≫ 𝟙 (D.obj A.i') = D.map (hl1 ⋯) ≫ D.map (hki' (Cover.idx A.𝒰D ↑u))

Tactic:
by rw [Category.comp_id, ← D.map_comp, this]

Goal state after: