mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
⊢ ∀ {i j k : WidePushoutShape J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
    (ConcreteCategory.hom (F.map fi)) xi = (ConcreteCategory.hom (F.map fj)) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
rintro i j k (_ | i) (_ | j)

Goal state after:
case id.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : WidePushoutShape J
⊢ ∀ (xi xj : F.obj i),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

case id.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
⊢ ∀ (xi : F.obj (some j)) (xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some j)))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

case init.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none) (xj : F.obj (some i)),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some i)))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
⊢ P snd

Tactic:
by
  have : HasPullback f (𝒰.f i) := h.hasPullback
  rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
  exact pullbackSnd 𝒰.mem₀ ⟨i⟩ hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: ⊢ IsIso adjunction.counit

Tactic:
by
  apply +allowSynthFailures NatIso.isIso_of_isIso_app
  intro R
  rw [adjunction_counit_app]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec y))) y.asIdeal

Tactic:
apply
    (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U))
      (S := X.presheaf.stalk (hU.fromSpec y)) _ y.asIdeal.primeCompl _
      (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec y, hy⟩) _ _
      (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ CommRingCat.Hom.hom ((structureSheaf R).obj.map (eqToHom ⋯).op) = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
eqToHom_op,

Goal state after:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ CommRingCat.Hom.hom ((structureSheaf R).obj.map (eqToHom ⋯)) = CommRingCat.Hom.hom (eqToHom ⋯)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k))
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
use (pullback.fst _ _ : _ ⟶ D.V (i, k)) (D.t' _ _ _ z)

Goal state after:
case h
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k))
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨k, c⟩.fst))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      ⟨i, a⟩.snd ∧
    (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨i, a⟩.fst))
        ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨k, c⟩.fst))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      ⟨k, c⟩.snd
Module: Mathlib.Topology.Gluing

Goal state before:
pp: h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
have := h.cocycle j i j x ?_
  · rw [h.t_id] at this
    · convert! Subtype.ext this
  rw [h.V_id]
  trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ Nonempty (IsInitial (pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt)

Tactic:
isInitial_iff_isEmpty

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ IsEmpty ↥(pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
            ((Opens.map (D.t j i).base).1 ((Opens.map (D.f i j).base).obj U))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).op) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
eqToHom_op,

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
            ((Opens.map (D.t j i).base).1 ((Opens.map (D.f i j).base).obj U))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i j : WalkingSpan
t : i ⟶ j
⊢ IsOpenImmersion ((span f g).map t)

Tactic:
obtain (a | (a | a)) := t

Goal state after:
case id
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingSpan
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))

case init.left
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

case init.right
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x ∈ ↑(Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p)))

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x ∈ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case h
X : Scheme
ι : Type v
inst✝ : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
H : ∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(f i)
i : ι
x : ↥(Y i)
⊢ (Limits.Sigma.desc f) ((Limits.Sigma.ι Y i) x) = (f i) x

Tactic:
rw [← Scheme.Hom.comp_apply, Limits.Sigma.ι_desc]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Ideal.span (Set.range s) = ⊤
Sₜ : ι → Type u
inst✝² : (i : ι) → CommRing (Sₜ i)
inst✝¹ : (i : ι) → Algebra S (Sₜ i)
inst✝ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
use Set.range s, hsone
  rintro - ⟨i, rfl⟩
  let e : Localization.Away (s i) ≃+* Sₜ i :=
    (IsLocalization.algEquiv (Submonoid.powers (s i)) _ _).toRingEquiv
  have : algebraMap S (Localization.Away (s i)) = e.symm.toRingHom.comp (algebraMap S (Sₜ i)) :=
    RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _).symm _).symm)
  rw [this, RingHom.comp_assoc]
  exact hP.left _ _ (hf i)

Goal state after:
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] (algebraMap R T) y

Tactic:
TensorProduct.smul_tmul,

Goal state after:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ x ⊗ₜ[R] (y • 1) = x ⊗ₜ[R] (algebraMap R T) y
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
⊢ SurjectiveOnStalks (f ≫ g)

Tactic:
refine ⟨fun x ↦ ?_⟩
    rw [Scheme.Hom.stalkMap_comp]
    exact (f.stalkMap_surjective x).comp (g.stalkMap_surjective (f x))

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

Goal state before:
pp: case hb
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis (Set.range fun U ↦ ↑U)

Tactic:
Subtype.range_coe

Goal state after:
case hb
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis X.affineOpens
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case e'_1
X : Scheme
U : X.Opens
⊢ IsCompact ↑U ↔ IsCompact U.carrier ∧ IsOpen U.carrier

Tactic:
simp [U.isOpen]

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = (⨆ i, ⨆ (h : i ∈ s), ↑↑⟨i, h⟩) ⊓ X.basicOpen f

Tactic:
← e,

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = U ⊓ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparatedSpace ↥X
⊢ QuasiCompact (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rwa [← quasiSeparatedSpace_iff_quasiCompact_prod_lift]

Goal state after:
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 Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H : P g
⊢ P (f ≫ g)

Tactic:
by
  rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H ⊢
  intro U V e
  have : IsIso (f.appLE (f ''ᵁ V) V.1 (f.preimage_image_eq _).ge) :=
    inferInstanceAs (IsIso (f.app _ ≫
      X.presheaf.map (eqToHom (f.preimage_image_eq _).symm).op))
  rw [← Scheme.Hom.appLE_comp_appLE _ _ _ (f ''ᵁ V) V.1
    (Set.image_subset_iff.mpr e) (f.preimage_image_eq _).ge,
    CommRingCat.hom_comp,
    (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso]
  exact H _ ⟨_, V.2.image_of_isOpenImmersion _⟩ _

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ False

Tactic:
have := (I.map_ideal (U := X.affineBasicOpen f) (hfg.trans_le (X.basicOpen_le g))).le
    (Ideal.mem_map_of_mem _ hfU)

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈ I.ideal (X.affineBasicOpen f)
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx : (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0
⊢ ((CommRingCat.Hom.hom (f.app ↑U)) x |_ f ⁻¹ᵁ Y.basicOpen s) ⋯ = 0

Tactic:
rwa [f.naturality] at hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

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

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f (closedPoint R))) isOpen_univ

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
obtain ⟨g, _⟩ := f₂

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

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme),
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
⊢ IsAffineHom f

pp: Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
hY : IsAffine Y
⊢ IsAffineHom f

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
    intro U
    exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) U.2

Goal state after:
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
hY : IsAffine Y
⊢ IsAffineHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
⊢ JacobsonSpace ↥X

Tactic:
rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullback₁ f)).jacobsonSpace_iff]
    intro i
    have inst : LocallyOfFiniteType (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    have inst : JacobsonSpace Y := ‹_› -- TC gets stuck on the WLOG hypothesis without it.
    have inst : JacobsonSpace (Y.affineCover.X i) :=
      .of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
    let e := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.isEmbedding.toHomeomorph
    have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩
    exact .of_isClosedEmbedding e.symm.isClosedEmbedding

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
this : Scheme.Hom.ker f = ⊥
⊢ DenseRange ⇑f

Tactic:
by simpa only [Scheme.Hom.support_ker, Scheme.IdealSheafData.support_bot,
    Closeds.coe_top, ← dense_iff_closure_eq] using! (congr((↑($this).support : Set Y)) :)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
⊢ IsIrreducible (⇑f ⁻¹' s)

Tactic:
by
  wlog H : ∃ x, s = {x} generalizing s
  · refine hs.preimage_of_isPreirreducible_fiber _ hf
      (fun x ↦ (this isIrreducible_singleton ⟨_, rfl⟩).isPreirreducible) ?_
    rw [Set.range_eq_univ.mpr f.surjective, Set.inter_univ]
    exact hs.nonempty
  obtain ⟨s, rfl⟩ := H
  rw [← f.range_fiberι, ← Set.image_univ]
  exact (IrreducibleSpace.isIrreducible_univ _).image _ (f.fiberι _).continuous.continuousOn

Goal state after:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: case pos
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
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
hp' : 1 ≤ p.natDegree
⊢ eval₂ (algebraMap R S) (↑⟨t, ht⟩ ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0

Tactic:
have := p.scaleRoots_eval₂_mul (algebraMap R S) (t ^ n • r) (t ^ m)

Goal state after:
case pos
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
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
hp' : 1 ≤ p.natDegree
this :
  eval₂ (algebraMap R S) ((algebraMap R S) (t ^ m) * t ^ n • r) (p.scaleRoots (t ^ m)) =
    (algebraMap R S) (t ^ m) ^ p.natDegree * eval₂ (algebraMap R S) (t ^ n • r) p
⊢ eval₂ (algebraMap R S) (↑⟨t, ht⟩ ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
x✝ : UniversallyClosed f ∧ IsAffineHom f
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝¹ : Nonempty ↥S
inst✝ : Nonempty n
⊢ ¬IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
by
  simp [isIntegralHom_over_iff_isEmpty]

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
⊢ ⇑D =ᶠ[codiscreteWithin U] 0

Tactic:
apply codiscreteWithin_iff_locallyFiniteComplementWithin.2

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x | (fun x ↦ D x = 0 x) x})).Finite