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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)
      ((Spec.map ((↑U).presheaf.germ ⊤ x True.intro)) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
rw [← Scheme.Hom.comp_apply, ← Spec.map_comp,
    (Iso.eq_comp_inv _).mpr (Scheme.Opens.germ_stalkIso_hom U (V := ⊤) x trivial),
    X.presheaf.germ_res_assoc, Spec.map_comp, Scheme.Hom.comp_apply]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.germ U ↑x ⋯)) ((Spec.map (U.stalkIso x).inv) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))

Tactic:
by
    let p : PrimeSpectrum (Γ.obj (op X)) := X.toΓSpecFun x
    constructor
    -- show stalk map is local hom ↓
    let S := (structureSheaf _).presheaf.stalk p
    rintro (t : S) ht
    obtain ⟨⟨r, s⟩, he⟩ := IsLocalization.surj p.asIdeal.primeCompl t
    dsimp at he
    set t' := _
    change t * t' = _ at he
    apply isUnit_of_mul_isUnit_left (y := t')
    rw [he]
    refine IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)
    apply (notMem_prime_iff_unit_in_stalk _ _ _).mpr
    rw [← toStalk_stalkMap_toΓSpec, CommRingCat.comp_apply]
    erw [← he]
    rw [map_mul]
    exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
this : (Hom.appTop X.toSpecΓ).op = inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ (inv (ΓSpecIso Γ(X, ⊤)).inv).op = (ΓSpecIso Γ(X, ⊤)).hom.op

Tactic:
IsIso.Iso.inv_inv

Goal state after:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ (ΓSpecIso Γ(X, ⊤)).hom.op = (ΓSpecIso Γ(X, ⊤)).hom.op
Module: Mathlib.Topology.Gluing

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

Tactic:
dsimp +instances only at *

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 j)) x = a
e₂ : (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) x) = b
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f j k)) y = b
e₄ : (ConcreteCategory.hom (D.f k j)) ((ConcreteCategory.hom (D.t j k)) y) = c
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 k))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      a ∧
    (ConcreteCategory.hom (D.f k i))
        ((ConcreteCategory.hom (D.t i k))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      c
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ Ideal.span s = ⊤

Tactic:
by
  rw [← hU.iSup_basicOpen_eq_self_iff, @comm _ Eq]
  refine ⟨fun h => le_antisymm h ?_, le_of_eq⟩
  simp only [iSup_le_iff, SetCoe.forall]
  intro x _
  exact X.basicOpen_le x

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨i, x⟩)
    ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨j, y⟩)

Tactic:
change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ InvImage D.Rel (⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((sigmaIsoSigma D.U).inv.hom' ⟨i, x⟩)
    ((sigmaIsoSigma D.U).inv.hom' ⟨j, y⟩)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ x ∈ ⨆ f_1, X.basicOpen ↑f_1

Tactic:
rw [iSup_range', Opens.mem_iSup]

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ ∃ i, x ∈ X.basicOpen (f i)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ Hom.left (OplaxMonoidal.η (pullback f)) ≫ Hom.left (LaxMonoidal.ε (pullback f)) =
    𝟙 ((pullback f).obj (𝟙_ (Over X))).left

Tactic:
← Over.comp_left,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ Hom.left (OplaxMonoidal.η (pullback f) ≫ LaxMonoidal.ε (pullback f)) = 𝟙 ((pullback f).obj (𝟙_ (Over X))).left
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc,
    IsOpenImmersion.inv_invApp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    ((D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯)) ≫
      (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (fV 𝒰 f g j k) (fV 𝒰 f g j i)

Tactic:
by
  refine (pullbackRightPullbackFstIso ..).hom ≫ ?_
  refine ?_ ≫ (pullbackSymmetry _ _).hom
  refine ?_ ≫ (pullbackRightPullbackFstIso ..).inv
  refine pullback.map _ _ _ _ (t 𝒰 f g i j) (𝟙 _) (𝟙 _) ?_ ?_
  · simp_rw [Category.comp_id, t_fst_fst_assoc, ← pullback.condition]
  · rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ (gluing 𝒰 f g).glued ⟶ X

Tactic:
apply Multicoequalizer.desc (gluing 𝒰 f g).diagram _ fun i ↦ pullback.fst _ _ ≫ 𝒰.f i
  simp [t_fst_fst_assoc, ← pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_1
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
                f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
            i)

Tactic:
let 𝒱 := ((gluing 𝒰.ulift f g).openCover.pushforwardIso
              (limit.isoLimitCone ⟨_, gluedIsLimit 𝒰.ulift f g⟩).inv).copy
          𝒰.ulift.I₀ (fun i => pullback (𝒰.ulift.f i ≫ f) g)
          (fun i => pullback.map _ _ _ _ (𝒰.ulift.f i) (𝟙 _) (𝟙 _) (Category.comp_id _) (by simp))
          (Equiv.refl 𝒰.ulift.I₀) (fun _ => Iso.refl _) fun i ↦ by
        simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]
        exact pullback.hom_ext (by simp [p1]) (by simp [p2])

Goal state after:
case refine_1
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
𝒱 : Cover (precoverage IsOpenImmersion) (limit (cospan f g)) :=
  (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).copy
    (Cover.ulift 𝒰).I₀ (fun i ↦ pullback ((Cover.ulift 𝒰).f i ≫ f) g)
    (fun i ↦ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
    (Equiv.refl (Cover.ulift 𝒰).I₀) (fun x ↦ Iso.refl (pullback ((Cover.ulift 𝒰).f x ≫ f) g)) ⋯
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
                f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
            i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ P.toProperty f ↔ P f

Tactic:
by
  delta AffineTargetMorphismProperty.toProperty; simp [*]

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

Goal state before:
pp: case hP₁
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), SpecializingMap ⇑f

Tactic:
introv

Goal state after:
case hP₁
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ SpecializingMap ⇑f
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mpr
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
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
· intro ⟨s, hsone, hs⟩
    use s, hsone, hs

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

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) x *
      (algebraMap S (Localization.Away (f ↑r))) ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩ =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
Subtype.coe_mk,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) x *
      (algebraMap S (Localization.Away (f ↑r))) ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩ =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
f' : Spec A ⟶ Spec R
g' : Spec B ⟶ Spec R
⊢ ∀ (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y) (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))

Tactic:
iX

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
f' : Spec A ⟶ Spec R
g' : Spec B ⟶ Spec R
iX : Spec A ⟶ X
⊢ ∀ (iY : Spec B ⟶ Y) (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↥X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
have h := (f ≫ g).stalkMap_surjective x

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
⊢ IsClosed (⇑f '' Z)

Tactic:
have inst : QuasiCompact (g ≫ f) := HasAffineProperty.iff_of_isAffine.mpr (by infer_instance)

Goal state after:
case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
inst : QuasiCompact (g ≫ f)
⊢ IsClosed (⇑f '' Z)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I✝ I : Ideal R
inst✝ : FiniteRingKrullDim R
⊢ ¬I = ⊤ → ↑I.height < ↑⊤

Tactic:
exact fun h ↦ lt_of_le_of_lt (Ideal.height_le_ringKrullDim_of_ne_top h) ringKrullDim_lt_top

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
e : R ≃+* S
p : Ideal S
inst✝ : p.IsPrime
⊢ (comap e p).height = p.height

Tactic:
rw [height_eq_primeHeight, height_eq_primeHeight, primeHeight, primeHeight,
    ← Order.height_orderIso (PrimeSpectrum.comapEquiv e.symm) ⟨p, ‹_›⟩]

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
e : R ≃+* S
p : Ideal S
inst✝ : p.IsPrime
⊢ Order.height { asIdeal := comap e p, isPrime := ⋯ } =
    Order.height ((PrimeSpectrum.comapEquiv e.symm) { asIdeal := p, isPrime := inst✝ })
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.refine_1.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ ↑p.length ≤ ⨆ (_ : RelSeries.last p ≤ RelSeries.last p), ↑p.length

pp: case a.refine_1.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ ⨆ (_ : RelSeries.last p ≤ RelSeries.last p), ↑p.length ≤ (RelSeries.last p).asIdeal.primeHeight

Tactic:
· exact le_iSup (fun _ => (↑p.length : ℕ∞)) le_rfl

Goal state after:
case a.refine_1.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ ⨆ (_ : RelSeries.last p ≤ RelSeries.last p), ↑p.length ≤ (RelSeries.last p).asIdeal.primeHeight
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case hS'
X : Scheme
⊢ (⋃₀ Set.range fun x ↦ Set.range ⇑(X.affineCover.f x)) = ⊤

Tactic:
· rw [Set.top_eq_univ, Set.sUnion_range, Set.eq_univ_iff_forall]
    intro x; exact ⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ IrreducibleSpace ↥X

Tactic:
by_contra H
  replace H : ¬IsPreirreducible .univ := fun h =>
    H { toPreirreducibleSpace := ⟨h⟩
        toNonempty := inferInstance }
  simp_rw [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at H
  rcases H with ⟨S, T, hS, hT, h₁, h₂, h₃⟩
  rw [Set.not_univ_subset] at h₂ h₃
  have : Nonempty (⟨Sᶜ, hS.1⟩ : X.Opens) := ⟨⟨_, h₂.choose_spec⟩⟩
  have : Nonempty (⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, h₃.choose_spec⟩⟩
  have : Nonempty (⟨Sᶜ, hS.1⟩ ⊔ ⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, Or.inl h₂.choose_spec⟩⟩
  let e : Γ(X, _) ≅ CommRingCat.of _ :=
    (X.sheaf.isProductOfDisjoint ⟨_, hS.1⟩ ⟨_, hT.1⟩ ?_).conePointUniqueUpToIso
      (CommRingCat.prodFanIsLimit _ _)
  · have : IsDomain (Γ(X, ⟨Sᶜ, hS.1⟩) × Γ(X, ⟨Tᶜ, hT.1⟩)) :=
      e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
    exact false_of_nontrivial_of_product_domain Γ(X, ⟨Sᶜ, hS.1⟩) Γ(X, ⟨Tᶜ, hT.1⟩)
  · ext x
    constructor
    · rintro ⟨hS, hT⟩
      rcases h₁ (show x ∈ ⊤ by trivial) with h | h
      exacts [hS h, hT h]
    · simp

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)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) n, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) n, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

Tactic:
cases n <;>
    simpa [RingHom.algebraMap_toAlgebra, ← hfg, hxf, hxs, Scheme.basicOpen_pow] using hs'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
x y : ↥X
hy : y ⤳ x
this : (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk y)) = y
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
exact ⟨_, this⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑U))

Tactic:
simp only [ofIdealTop_ideal, homOfLE_leOfHom, Ideal.map_le_iff_le_comap, RingHom.comap_ker,
    ← CommRingCat.hom_comp, f.naturality]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) ≤
    RingHom.ker (CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.I₀), I ≤ ker (𝒰.f i ≫ f)
U : ↑Y.affineOpens
⊢ I.ideal U ≤ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U

Tactic:
le_iInf_iff

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.I₀), I ≤ ker (𝒰.f i ≫ f)
U : ↑Y.affineOpens
⊢ ∀ (i : 𝒰.I₀), I.ideal U ≤ (ker (𝒰.f i ≫ f)).ideal U
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)
⊢ (fun f ↦ ⟨f (closedPoint ↑(CommRingCat.of K)), descResidueField (stalkClosedPointTo f)⟩)
      ((fun xf ↦ Spec.map xf.snd ≫ X.fromSpecResidueField xf.fst) f) =
    f

Tactic:
by
    rw [SpecToEquivOfField_eq_iff]
    simp only [CommRingCat.coe_of, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply,
      Scheme.fromSpecResidueField_apply, exists_true_left]
    rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)]
    grind [Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField,
      Scheme.fromSpecResidueField_apply,
      Scheme.residueFieldCongr_fromSpecResidueField]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.RightInverse (fun T ↦ T.fst.SpecTensorTo T.snd) fun t ↦ ⟨Triplet.ofPoint t, SpecOfPoint t⟩

Tactic:
by
    intro ⟨T, p⟩
    apply carrierEquiv_eq_iff.mpr
    use T.ofPoint_SpecTensorTo p
    have : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) (⊥ : PrimeSpectrum _) =
        (⊥ : PrimeSpectrum _) :=
      (PrimeSpectrum.instUnique).uniq _
    simp only [SpecOfPoint, Triplet.tensorCongr_inv, ← this, ← Scheme.Hom.comp_apply,
      ← Scheme.Hom.comp_apply]
    simp [Triplet.Spec_ofPointTensor_SpecTensorTo]

Goal state after: