mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : ⟨↑r ^ n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
Submonoid.smul_def,

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : ↑⟨↑r ^ n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
Submonoid.smul_def,

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion f

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff @IsClosedImmersion (arrowIsoSpecΓOfIsAffine f)]
  apply spec_of_surjective
  exact h

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

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝¹ : IsClosedImmersion (Scheme.Hom.toImage f)
this✝ : IsHomeomorph ⇑(Scheme.Hom.toImage f)
x : ↥X
this : IsIso (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x)
⊢ Function.Injective
    ⇑(CommRingCat.Hom.hom (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x))

Tactic:
exact ((ConcreteCategory.isIso_iff_bijective _).mp this).1

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0

Tactic:
let W (i : 𝒰.I₀) : TopologicalSpace.Opens (𝒰.X i) := (𝒰.X i).basicOpen ((res i) (φ s))

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: case e'_5
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FinitePresentation R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
r✝ : R
x✝ : OreLocalization (Submonoid.powers r) S
⊢ (have I := OreLocalization.instAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
simp_rw [Algebra.smul_def]

Goal state after:
case e'_5
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FinitePresentation R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
r✝ : R
x✝ : OreLocalization (Submonoid.powers r) S
⊢ (algebraMap R (OreLocalization (Submonoid.powers r) S)) r✝ * x✝ = r✝ • x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case e'_3.h₀
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.fst Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.fst Y.hom Y.hom

Tactic:
simp [← Over.comp_left]

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

Goal state before:
pp: case h₁
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.snd Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.snd Y.hom Y.hom

Tactic:
simp [← Over.comp_left]

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsSeparated (f ≫ terminal.from Y)

Tactic:
terminal.comp_from

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsSeparated (terminal.from X)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m

Tactic:
let suitableN s :=
    { n : ℕ | ∀ m : ℕ, n ≤ m → (Ideal.map (floc s) (I n)) = (Ideal.map (floc s) (I m)) }

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ NoetherianSpace ↑?m.59

pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ?m.59

pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ Set ↥X

Tactic:
· convert! noetherianSpace_of_isAffineOpen U.1 U.2
        apply IsLocallyNoetherian.component_noetherian

Goal state after:
case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ↑↑U
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ ((algebraMap S (Localization.Away (f t))).comp (algebraMap R S))
      (⟨(fun x ↦ t ^ x) n, ⋯⟩ • (algebraMap S (Localization.Away (f t))) r) p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
Submonoid.smul_def,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ ((algebraMap S (Localization.Away (f t))).comp (algebraMap R S))
      (↑⟨(fun x ↦ t ^ x) n, ⋯⟩ • (algebraMap S (Localization.Away (f t))) r) p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
⊢ Continuous ⇑f ∧ IsClosedMap ⇑f ∧ ∀ (y : ↥Y), IsCompact (⇑f ⁻¹' {y})

Tactic:
refine ⟨f.continuous, f.isClosedMap, fun y ↦ ?_⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
y : ↥Y
⊢ IsCompact (⇑f ⁻¹' {y})
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
⊢ f = g

Tactic:
ext x
    · obtain ⟨x⟩ := x
      simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (C x)
    · simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (X x)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) ((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) v) i = v i

Tactic:
simp [-TopologicalSpace.Opens.map_top, homOfVector_appTop_coord]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j✝ : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂

Tactic:
rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]

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✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ ¬D x = 0 → x ∈ U

Tactic:
exact (support_subset_iff.1 D.supportWithinDomain) x

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✝¹ : 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:
by
      intro z hz
      obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
      obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
      use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
      apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
      intro a ha
      simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
      by_contra! hCon
      simp_all

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✝¹ : 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:
by
      intro z hz
      obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
      obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
      use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
      apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
      intro a ha
      simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
      by_contra! hCon
      simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: case refl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↥X
hW : x ∈ W
iU : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iU.op)) 0
⊢ y = 0

Tactic:
have : Nonempty W := ⟨⟨_, hW⟩⟩

Goal state after:
case refl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↥X
hW : x ∈ W
iU : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iU.op)) 0
this : Nonempty ↥↑W
⊢ y = 0
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↥↑U
⊢ hU.primeIdealOf ⟨genericPoint ↥X, ⋯⟩ = genericPoint ↥(Spec Γ(X, U))

Tactic:
delta IsAffineOpen.primeIdealOf
  convert!
    genericPoint_eq_of_isOpenImmersion
      (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))
        -- Porting note: this was `ext1`

  -- Porting note: this was `ext1`
  apply Subtype.ext
  exact (genericPoint_eq_of_isOpenImmersion U.ι).symm

Goal state after:
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)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
Ug : X.Opens
dense_domain✝ : Dense ↑Ug
g : ↑Ug ⟶ Y
inst✝ : IsOver S { domain := Ug, dense_domain := dense_domain✝, hom := g }
hfg :
  { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain =
    { domain := Ug, dense_domain := dense_domain✝, hom := g }.domain
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Ug, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Ug, dense_domain := dense_domain✝, hom := g }

Tactic:
obtain rfl : Uf = Ug := hfg

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
dense_domain✝ : Dense ↑Uf
g : ↑Uf ⟶ Y
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := g }
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Uf, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Uf, dense_domain := dense_domain✝, hom := g }
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.trans fi ≫ 𝒰.f k) xi = (𝒰.trans fj ≫ 𝒰.f k) xj

Tactic:
Hom.comp_base,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi = (𝒰.trans fj ≫ 𝒰.f k) xj
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi = (𝒰.trans fj ≫ 𝒰.f k) xj

Tactic:
Hom.comp_base,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi =
    (ConcreteCategory.hom ((𝒰.trans fj).base ≫ (𝒰.f k).base)) xj
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.trans fi ≫ 𝒰.f k) xi = (𝒰.trans fj ≫ 𝒰.f k) xj

Tactic:
Hom.comp_base,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi = (𝒰.trans fj ≫ 𝒰.f k) xj
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi = (𝒰.trans fj ≫ 𝒰.f k) xj

Tactic:
Hom.comp_base,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi =
    (ConcreteCategory.hom ((𝒰.trans fj).base ≫ (𝒰.f k).base)) xj