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

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) = ⊥

Tactic:
rw [← Scheme.preimage_basicOpen, hs]; ext1; simp [Opens.map]

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

Goal state before:
pp: case inr.refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
⊢ ∃ a, ↑s = Y.basicOpen a

Tactic:
obtain ⟨a, ha⟩ := hUs s.2

Goal state after:
case inr.refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
a : ↑Γ(Y, ⊤)
ha : Y.basicOpen a = ↑s
⊢ ∃ a, ↑s = Y.basicOpen a
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) a * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ IsUnit 0

Tactic:
convert! hx₁.mul hx₂

Goal state after:
case e'_3
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) a * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ 0 =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a *
      (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]

Goal state after:
case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this✝ : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
this : f = φ ≫ i.inv
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f

Tactic:
have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
hS : Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S) = ⊤
⊢ ∀ i ∈ ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S, IsAffineOpen (X.basicOpen i)

Tactic:
have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
hS : Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S) = ⊤
this : ∀ (i : ↥S), IsAffineOpen (f ⁻¹ᵁ Y.basicOpen ↑i)
⊢ ∀ i ∈ ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S, IsAffineOpen (X.basicOpen i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤

Tactic:
exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

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

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj ⟨U, hU⟩)
hx : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑I.support
hxU : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑U
⊢ (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ Set.range ⇑I.gluedTo

Tactic:
rw [← ι_gluedTo]

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj ⟨U, hU⟩)
hx : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑I.support
hxU : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑U
⊢ (I.glueData.ι ⟨U, hU⟩ ≫ I.gluedTo) y ∈ Set.range ⇑I.gluedTo
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Submonoid R
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
⊢ ∃ m, m • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
obtain ⟨⟨_, a, ha, rfl⟩, e⟩ :=
    IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _)
      Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Submonoid R
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e : ⟨(algebraMap R S) a, ⋯⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ∃ m, m • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ n, ↑r ^ n • x ∈ adjoin R (↑(s.attach.biUnion sf) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))

Tactic:
Finset.coe_biUnion

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ n, ↑r ^ n • x ∈ adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_2.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.hom)

Tactic:
exact (P.cancel_left_of_respectsIso _ _).mpr S.prop

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
⊢ FiniteType R S

Tactic:
apply Algebra.FiniteType.of_span_eq_top_target s hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
⊢ ∀ x ∈ ↑s, FiniteType R (Localization.Away x)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
by
  rw [← MorphismProperty.cancel_right_of_respectsIso @IsImmersion _ (prodIsoPullback X X).hom]
  convert! (inferInstance : IsImmersion (pullback.diagonal (terminal.from X)))
  ext : 1 <;> simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
⊢ FinitePresentation R S

Tactic:
let t : Finset A := Finset.image (fun g ↦ g' g) Finset.univ

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ FinitePresentation R S
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case inr
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))),
    IsOpen U → (∃ f, U = ↑(basicOpen f)) → IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ f, U = ↑(basicOpen f)
⊢ IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)

Tactic:
eq_biUnion_of_isOpen hU,

Goal state after:
case inr
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))),
    IsOpen U → (∃ f, U = ↑(basicOpen f)) → IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ f, U = ↑(basicOpen f)
⊢ IsOpen (comap (algebraMap A (A ⊗[K] B)) '' ⋃ r, ⋃ (_ : ↑(basicOpen r) ⊆ U), ↑(basicOpen r))
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
wlog hY : ∃ R, Y = Spec R
  · refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_
    have inst : LocallyOfFinitePresentation (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    have inst : QuasiCompact (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    convert!
      (this (Y.affineCover.pullbackHom f i)
            (hs.preimage_of_isOpenEmbedding ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding)
            ⟨_, rfl⟩).preimage_of_isOpenEmbedding
        (Y.affineCover.f i).isoOpensRange.inv.isOpenEmbedding
    refine .trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)
    apply Set.image_injective.mpr Subtype.val_injective
    rw [Set.image_preimage_eq_inter_range, ← Set.image_comp, ← Set.image_comp,
      Subtype.range_coe_subtype, Set.ofPred_mem_eq]
    change _ = (Y.affineCover.pullbackHom f i ≫
      (Y.affineCover.f i).isoOpensRange.hom ≫ Opens.ι _).base.hom '' _
    rw [Scheme.Hom.isoOpensRange_hom_ι, Cover.pullbackHom_map, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range]
    simp [IsOpenImmersion.range_pullbackFst, Set.image_inter_preimage]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
    let 𝒰 := X.affineCover.finiteSubcover
    rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]
    refine .iUnion fun i ↦ ?_
    have inst : QuasiCompact (𝒰.f i ≫ f) :=
      HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
    convert! this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩
    rw [Scheme.Hom.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp,
      ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, coe_opensRange]
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)] at hf
  exact (PrimeSpectrum.isConstructible_comap_image hf hs.isConstructible).isLocallyConstructible

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

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝¹ : IrreducibleSpace ↥(Spec R)
this✝ : IsDomain ↑R
φ : S ⟶ R
this : IsField ↑R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
let := this.toField

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝² : IrreducibleSpace ↥(Spec R)
this✝¹ : IsDomain ↑R
φ : S ⟶ R
this✝ : IsField ↑R
this : Field ↑R := this✝.toField
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case mpr
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
hx : x ∈ {x | D x = 0}ᶜ ∩ U
⊢ x ∈ D.support

Tactic:
mem_inter_iff,

Goal state after:
case mpr
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
hx : x ∈ {x | D x = 0}ᶜ ∧ x ∈ U
⊢ x ∈ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
⊢ ⇑(∑ᶠ (i : ι), F i) = ∑ᶠ (i : ι), ⇑(F i)

Tactic:
have : F.support = (fun i ↦ (F i : X → ℤ)).support := by
    simp [Set.ext_iff, DFunLike.ext_iff, funext_iff]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support fun i ↦ ⇑(F i)
⊢ ⇑(∑ᶠ (i : ι), F i) = ∑ᶠ (i : ι), ⇑(F i)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst✝¹ : X.IsGermInjectiveAt x
inst✝ : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ Y.IsGermInjectiveAt (f x)

Tactic:
refine ⟨⟨f ''ᵁ U, ⟨x, hxU, rfl⟩, hU.image_of_isOpenImmersion f, ?_⟩⟩

Goal state after:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst✝¹ : X.IsGermInjectiveAt x
inst✝ : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯))
Module: Mathlib.AlgebraicGeometry.Birational.Dominant

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
h : f.equiv g
⊢ IsDominant f.hom ↔ IsDominant g.hom

Tactic:
obtain ⟨W, hW, hWl, hWr, h⟩ := h

Goal state after:
X Y : Scheme
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
h : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ IsDominant f.hom ↔ IsDominant g.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✝¹ : 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
i : I
⊢ (m ≫ (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι) ≫ c.π.app i =
    (IsClosedImmersion.lift (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι
          (hc.lift ((Cone.postcompose ι).obj s)) ⋯ ≫
        (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι) ≫
      c.π.app i

Tactic:
simp [ι, c', ← hm]

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 := ⋯ }
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:
by
      rw [← cancel_mono (subschemeι _)]
      refine hc.hom_ext fun i ↦ ?_
      simp [ι, c', ← hm]

Goal state after: