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

Goal state before:
pp: case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : ↥s) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
this :
  P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen ↑r) ↑⟨X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r), ⋯⟩ ⋯))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom,
      ← h₁.isLocalization_away_iff] at this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.germ U y hyU ≫ X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpec hU =
    Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU

Tactic:
TopCat.Presheaf.germ_stalkSpecializes

Goal state after:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.germ U x ⋯) ≫ IsAffineOpen.fromSpec hU =
    Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑I.support) = (I.ideal U).radical

Tactic:
rw [← vanishingIdeal_zeroLocus_eq_radical]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑I.support) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(I.ideal U))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ stalkClosedPointTo (f ≫ g) = Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
by
  rw [stalkClosedPointTo, Scheme.Hom.stalkMap_comp]
  exact Category.assoc _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ (∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd) → f₁ = f₂

Tactic:
obtain ⟨f, _⟩ := f₁

Goal state after:
case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
f : ↥X
snd✝ : X.residueField f ⟶ CommRingCat.of K
⊢ (∃ (e : ⟨f, snd✝⟩.fst = f₂.fst), ⟨f, snd✝⟩.snd = (residueFieldCongr e).hom ≫ f₂.snd) → ⟨f, snd✝⟩ = f₂
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↥(pullback f' g')
x : ↥X
hx : i₁ x = (pullback.fst f' g') z
y : ↥Y
hy : i₂ y = (pullback.snd f' g') z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
⊢ (pullback.fst (pullback.fst f' g') i₁) w₁ = (pullback.fst (pullback.snd f' g') i₂) w₂

Tactic:
simp [hw₁.left, hw₂.left, T₁, T₂]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
he : Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
← he

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
he : Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
⊢ (Hom.ker f).ideal U ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑U ≫ e.hom))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
x✝² x✝¹ : (Over Y)ᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x✝ ≫
        (Over.homMk (Hom.toImage (Opposite.unop x✝¹).hom) ⋯).op).unop =
    ((Over.homMk (Hom.toImage (Opposite.unop x✝²).hom) ⋯).op ≫ (𝟭 (Over Y)ᵒᵖ).map x✝).unop

Tactic:
by ext1; simp [← cancel_mono (subschemeι _)]

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

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ ((subschemeFunctor Y).rightOp.map ({ app := fun I ↦ eqToHom ⋯, naturality := ⋯ }.app I) ≫
        { app := fun f ↦ (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯).op, naturality := ⋯ }.app
          ((subschemeFunctor Y).rightOp.obj I)).unop =
    (𝟙 ((subschemeFunctor Y).rightOp.obj I)).unop

Tactic:
by ext1; simp [← cancel_mono (subschemeι _)]

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)⟩)
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ Hom.opensRange (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⊓
      Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩) =
    Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)

Tactic:
inf_eq_right,

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)⟩)
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩) ≤ Hom.opensRange (diagonalCoverDiagonalRange f 𝒰 𝒱).ι
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    (↑C).toSet

Tactic:
let I := Ideal.span (Set.range C.1.g)

Goal state after:
case e'_3
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    (↑C).toSet
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
⊢ Module.finrank I.ResidueField I.ResidueField * Module.finrank R A = Module.finrank R A

Tactic:
Module.finrank_self,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
⊢ 1 * Module.finrank R A = Module.finrank R A
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case inr
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
⊢ IsClosedImmersion g

pp: X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
hX : ∃ R, X = Spec R
⊢ IsClosedImmersion g

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) X.affineCover]
    intro i
    by_cases hxU : Set.range g ⊆ (X.affineCover.f i).opensRange
    · rw [Scheme.Cover.pullbackHom,
        ← (IsOpenImmersion.isPullback_lift_id _ _ hxU).flip.isoPullback_inv_snd,
        MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion]
      refine this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩
      rw [IsOpenImmersion.lift_fac_assoc, hg]
    · have : IsEmpty ((X.affineCover.pullback₁ g).X i) := by
        apply Scheme.isEmpty_pullback
        rw [← Set.subset_compl_iff_disjoint_left]
        rintro _ hx ⟨x, rfl⟩
        apply hxU
        rintro _ ⟨y, rfl⟩
        exact Subsingleton.elim x y ▸ hx
      infer_instance

Goal state after:
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
hX : ∃ R, X = Spec R
⊢ IsClosedImmersion g
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ ∃ t, comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ

Tactic:
by
  apply +allowSynthFailures exists_image_comap_of_finite_of_free
  · exact .of_basis (AdjoinRoot.powerBasis' hg).basis
  · exact .of_basis (AdjoinRoot.powerBasis' hg).basis

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X

Tactic:
· refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    simpa using (𝒰.f i).isOpenEmbedding.isOpenMap _ (isOpen_discrete {x})

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝ : X.IsQuasiAffine
x : ↥X
x✝ : x ∈ ⊤
⊢ x ∈ ⨆ i, X.basicOpen ↑i

Tactic:
obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ :=
    (IsQuasiAffine.isBasis_basicOpen X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Goal state after:
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝ : X.IsQuasiAffine
x : ↥X
x✝ : x ∈ ⊤
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ ↑(X.basicOpen r)
⊢ x ∈ ⨆ i, X.basicOpen ↑i
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (Spec.map (CommRingCat.ofHom C))

pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))

Tactic:
· rw [HasAffineProperty.iff_of_isAffine (P := isomorphisms _), ← isomorphisms,
      ← arrow_mk_iso_iff (isomorphisms _) (arrowIsoΓSpecOfIsAffine _)]
    exact ⟨inferInstance, (ConcreteCategory.isIso_iff_bijective _).mpr
      ⟨C_injective n _, C_surjective _⟩⟩

Goal state after:
case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
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 : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
⊢ t₁ ∩ t₂ ∩ Function.support (f + g) ⊆ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g

Tactic:
intro a ha

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₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support (f + g)
⊢ a ∈ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g
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✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z) ⊆ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support

Tactic:
intro a ha

Goal state after:
case right
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₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z
⊢ a ∈ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support
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✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z) ⊆ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support

Tactic:
intro a ha

Goal state after:
case right
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₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z
⊢ a ∈ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support
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
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊔ D₂).restrict h = D₁.restrict h ⊔ D₂.restrict h

Tactic:
ext x
    by_cases hx : x ∈ V
    <;> simp [locallyFinsuppWithin.restrict_apply, hx]

Goal state after:
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
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊓ D₂).restrict h = D₁.restrict h ⊓ D₂.restrict h

Tactic:
ext x
    by_cases hx : x ∈ V
    <;> simp [locallyFinsuppWithin.restrict_apply, hx]

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

Goal state before:
pp: 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₂
⊢ Set.range (comap (mapRingHom q₁.toRingHom)) ∪ Set.range (comap (mapRingHom q₂.toRingHom)) = Set.univ

Tactic:
by rw [Ideal.Quotient.mkₐ_toRingHom,
            ← range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk,
            RingHom.algebraMap_toAlgebra]; exact Set.union_compl_self _

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

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
g : Y.PartialMap Z
W : X.Opens
hW : Dense ↑W
hW₁ : W ≤ f₁.domain
hW₂ : W ≤ f₂.domain
e :
  (f₁.comp g).restrict (f₁.domain.ι ''ᵁ f₁.hom ⁻¹ᵁ g.domain ⊓ W) ⋯ ⋯ =
    (f₂.comp g).restrict (f₂.domain.ι ''ᵁ f₂.hom ⁻¹ᵁ g.domain ⊓ W) ⋯ ⋯
⊢ (f₁.comp g).equiv (f₂.comp g)

Tactic:
exact equiv_of_restrict_eq _ _ e

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

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : (f.comp g₁).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ W) ⋯ ⋯ = (f.comp g₂).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ W) ⋯ ⋯
⊢ (f.comp g₁).equiv (f.comp g₂)

Tactic:
exact equiv_of_restrict_eq _ _ e

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)
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 : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (((D.obj i).isoOfEq ⋯).hom ≫ U.ι) ⁻¹ᵁ V = ⊤
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V

Tactic:
replace hj : (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map fji.left ⁻¹ᵁ V = ⊤ := by
    simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base] using hj

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 : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left fji) ⁻¹ᵁ V = ⊤
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_4
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₀
s : PullbackCone (𝒰.f i) d.toBase
m : s.pt ⟶ d.functor.obj i
h1 : m ≫ d.natTrans.app i = s.fst
h2 : m ≫ colimit.ι d.functor i = s.snd
⊢ m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯

Tactic:
simpa [← cancel_mono (colimit.ι d.functor i)]

Goal state after:
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)
U : Set S
⊢ IsCompactOpenCovered f U ↔ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

Tactic:
refine ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩

Goal state after:
case refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
⊢ IsCompactOpenCovered f U
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (t i)
⊢ ⋃ i ∈ s, f i '' t i = U

Tactic:
← heq,

Goal state after:
case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (t i)
⊢ ⋃ i ∈ s, f i '' t i = (fun p ↦ f p.fst p.snd) '' V.carrier