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

Goal state before:
pp: X : Scheme
s : Set ↑X.affineOpens
hs : s.Finite
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ i, ↑↑i).carrier
x f : ↑Γ(X, ⨆ i, ↑↑i)
H : (x |_ X.basicOpen f) ⋯ = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ i, ↑↑i
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : ∀ (i : ↑s), (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
i : ↑s
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (Opens.leSupr (fun i ↦ ↑↑i) i).op)) (f ^ Finset.univ.sup n * x) =
    (ConcreteCategory.hom (X.sheaf.obj.map (Opens.leSupr (fun i ↦ ↑↑i) i).op)) 0

Tactic:
rw [map_zero]

Goal state after:
X : Scheme
s : Set ↑X.affineOpens
hs : s.Finite
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ i, ↑↑i).carrier
x f : ↑Γ(X, ⨆ i, ↑↑i)
H : (x |_ X.basicOpen f) ⋯ = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ i, ↑↑i
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : ∀ (i : ↑s), (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
i : ↑s
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (Opens.leSupr (fun i ↦ ↑↑i) i).op)) (f ^ Finset.univ.sup n * x) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE e).op)) 0 = 0

Tactic:
rw [map_zero]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
⊢ ∀ (x : S), IsNilpotent x → x = 0

Tactic:
rintro x ⟨_ | n, e⟩

Goal state after:
case zero
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
e : x ^ 0 = 0
⊢ x = 0

case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
⊢ x = 0
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
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
rw [iff_of_source_openCover (P := P) (Scheme.coverOfIsIso.{u} (𝟙 _))]

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
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 X)).I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((Scheme.coverOfIsIso (𝟙 X)).f i ≫ f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Tactic:
rw [map_zero]

Goal state after:
X : Scheme
inst✝ : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Tactic:
rw [map_zero]

Goal state after:
X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0
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))
e : a * b = 0
⊢ ¬(↑(X.basicOpen a)).Nonempty ∨ ¬(↑(X.basicOpen b)).Nonempty

Tactic:
by_contra! h

Goal state after:
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))
e : a * b = 0
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
⊢ False
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X Y : Scheme
h : IsIntegral X
f : X ⟶ Y
inst✝ : IsIso f
⊢ Nonempty ↥Y

Tactic:
exact Nonempty.map f inferInstance

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
K : Type u
inst✝ : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ descResidueField (stalkClosedPointTo (Spec.map f.snd ≫ X.fromSpecResidueField f.fst)) =
    (residueFieldCongr ⋯).hom ≫ f.snd

Tactic:
rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)]

Goal state after:
X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
K : Type u
inst✝ : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ Spec.map (descResidueField (stalkClosedPointTo (Spec.map f.snd ≫ X.fromSpecResidueField f.fst))) ≫
      X.fromSpecResidueField ((X.fromSpecResidueField f.fst) ((Spec.map f.snd) (closedPoint K))) =
    (Spec.map f.snd ≫ Spec.map (residueFieldCongr ⋯).hom) ≫
      X.fromSpecResidueField ((X.fromSpecResidueField f.fst) ((Spec.map f.snd) (closedPoint K)))
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.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span ↑S) =
    Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤
⊢ IsAffine X

Tactic:
rw [Ideal.map_span, Ideal.map_top] at 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) = ⊤
⊢ IsAffine X
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : f x = g y
e : P ≅ pullback f g := ⋯
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ fst (h.isoPullback.inv z) = x ∧ snd (h.isoPullback.inv z) = y

Tactic:
simp [← Scheme.Hom.comp_apply, hzl, hzr]

Goal state after:
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' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
⊢ ∃ m, m • x ∈ A

Tactic:
obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx''

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ∃ m, m • x ∈ A
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ Set.range ⇑I.subschemeι = ↑I.support

Tactic:
by
  simp [← range_gluedTo, I.subschemeι_def, Set.range_comp]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ↑(Hom.opensRange (I.glueData.ι U ≫ I.subschemeIso.inv)) = ↑(I.subschemeι ⁻¹ᵁ ↑U)

Tactic:
simp [Set.range_comp, I.range_glueData_ι, subschemeι_def, ← coe_homeoOfIso_symm,
    ← homeoOfIso_symm, ← Homeomorph.coe_symm_toEquiv, Equiv.image_symm_eq_preimage]

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' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0

Tactic:
rw [← Scheme.Hom.appLE_map _ ((Opens.map _).map w).le (homOfLE <| hwle i).op,
      ← Scheme.Hom.map_appLE _ le_rfl w.op]

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))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom
        ((X.presheaf.map w.op ≫ Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯) ≫ (𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom φ) g) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType f

Tactic:
rw [← f.liftCoborder_ι]
  infer_instance

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
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
by
  let φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := f.appTop
  let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover
  let res (i : 𝒰.I₀) : Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := (𝒰.f i).appTop
  refine stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) h ↦ ?_)
  rw [TopCat.Presheaf.Γgerm, Scheme.Hom.germ_stalkMap_apply] at h
  obtain ⟨U, w, (hx : x ∈ U), hg⟩ :=
    X.toRingedSpace.exists_res_eq_zero_of_germ_eq_zero ⊤ (φ g) ⟨x, trivial⟩ h
  obtain ⟨_, ⟨s, rfl⟩, hyv, bsle⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_basicOpen Y)
    (show f x ∈ ⟨f '' U.carrier, hfopen U.carrier U.is_open'⟩ from ⟨x, by simpa⟩)
  let W (i : 𝒰.I₀) : TopologicalSpace.Opens (𝒰.X i) := (𝒰.X i).basicOpen ((res i) (φ s))
  have hwle (i : 𝒰.I₀) : W i ≤ (𝒰.f i) ⁻¹ᵁ U := by
    change (𝒰.X i).basicOpen ((𝒰.f i ≫ f).appTop s) ≤ _
    rw [← Scheme.preimage_basicOpen_top, Scheme.Hom.comp_base, Opens.map_comp_obj]
    refine Scheme.Hom.preimage_mono _
      (le_trans (f.preimage_mono bsle) (le_of_eq ?_))
    simp [Set.preimage_image_eq _ hfinj₁]
  have h0 (i : 𝒰.I₀) : (𝒰.f i).appLE _ (W i) (by simp) (φ g) = 0 := by
    rw [← Scheme.Hom.appLE_map _ ((Opens.map _).map w).le (homOfLE <| hwle i).op,
      ← Scheme.Hom.map_appLE _ le_rfl w.op]
    simp only [CommRingCat.comp_apply]
    rw [hg]
    simp only [map_zero]
  have h1 (i : 𝒰.I₀) : ∃ n, (res i) (φ (s ^ n * g)) = 0 := by
    obtain ⟨n, hn⟩ := exists_of_res_zero_of_qcqs_of_top (s := ((res i) (φ s))) (h0 i)
    exact ⟨n, by rwa [map_mul, map_mul, map_pow, map_pow]⟩
  have h2 : ∃ n, ∀ i, (res i) (φ (s ^ n * g)) = 0 := by
    choose fn hfn using h1
    refine ⟨Finset.sup Finset.univ fn, fun i ↦ ?_⟩
    rw [map_mul, map_pow, map_mul, map_pow]
    simp only [map_mul, map_pow, map_mul, map_pow] at hfn
    apply pow_mul_eq_zero_of_le (Finset.le_sup (Finset.mem_univ i)) (hfn i)
  obtain ⟨n, hn⟩ := h2
  apply germ_eq_zero_of_pow_mul_eq_zero (U := ⊤) ⟨f x, trivial⟩ hyv
  rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at hfinj₂
  exact hfinj₂ _ (Scheme.zero_of_zero_cover _ _ hn)

Goal state after:
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:
rw [eq_biUnion_of_isOpen hU, Set.image_iUnion₂]
    exact isOpen_iUnion fun _ ↦ isOpen_iUnion fun _ ↦ this _ (basicOpen _).isOpen ⟨_, rfl⟩

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

Goal state before:
pp: case inr
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible (⇑f '' ⋃ i, s ∩ ↑(opensRange (𝒰.f i)))

Tactic:
Set.image_iUnion

Goal state after:
case inr
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible (⋃ i, ⇑f '' (s ∩ ↑(opensRange (𝒰.f i))))
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)

Tactic:
· simp [Scheme.Hom.fiberToSpecResidueField]

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

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

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically IsOpenMap) Y.affineCover]
    intro i
    dsimp only [Scheme.Cover.pullbackHom]
    refine this _ ?_ ⟨_, rfl⟩
    exact IsZariskiLocalAtTarget.of_isPullback (P := topologically GeneralizingMap)
      (iY := Y.affineCover.f i) (IsPullback.of_hasPullback ..) hf

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

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

Tactic:
obtain ⟨f, h⟩ := h
      exact ⟨y.1, f, 𝟙 _, by simpa using h.symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ Scheme.Hom.appTop (isoOfIsAffine n S).hom =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom ≫
      CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))

Tactic:
by
  simp [isoOfIsAffine_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        ((Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(Spec R, ⊤)))).inv ≫
          Scheme.Hom.app (Spec.map (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
            ⊤))
      (X i) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
← Scheme.ΓSpecIso_inv_naturality,

Goal state after:
n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv ≫
          (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv))
      (X i) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝) =
    (ConcreteCategory.hom
        ((Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv ≫
          Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      (X i✝)

Tactic:
← Scheme.ΓSpecIso_inv_naturality,

Goal state after:
case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝) =
    (ConcreteCategory.hom
        (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)) ≫
          (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv))
      (X i✝)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
a : ↥(Spec (CommRingCat.of K))
⊢ (pointOfClosedPoint f x hx) a = x

Tactic:
by
  simp [pointOfClosedPoint]

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✝ : AddGroup Y
D : locallyFinsuppWithin U Y
⊢ (-D).support = D.support

Tactic:
support,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddGroup Y
D : locallyFinsuppWithin U Y
⊢ Function.support ⇑(-D) = D.support
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
refine ⟨U, hxU, ?_⟩

Goal state after:
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ U.ι ≫ f = U.ι ≫ g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g h : X.PartialMap Y
⊢ f.equiv g → g.equiv h → f.equiv h

Tactic:
intro ⟨W₁, hW₁, hW₁l, hW₁r, e₁⟩ ⟨W₂, hW₂, hW₂l, hW₂r, e₂⟩

Goal state after:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense ↑W₁
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : (f.restrict W₁ hW₁ hW₁l).hom = (g.restrict W₁ hW₁ hW₁r).hom
W₂ : X.Opens
hW₂ : Dense ↑W₂
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : (g.restrict W₂ hW₂ hW₂l).hom = (h.restrict W₂ hW₂ hW₂r).hom
⊢ f.equiv h
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ f.hom =
    ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ g.hom

Tactic:
convert! e using 2 <;> rw [← cancel_mono (Scheme.Opens.ι _)] <;> simp

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

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

Tactic:
by
  rw [ext_iff]
  exact ⟨e, e', H⟩

Goal state after: