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

Goal state before:
pp: case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
· rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, Category.assoc, t_fst_fst]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion coprod.inr

Tactic:
rw [← ι_right_coprodIsoSigma_inv]

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.right } ≫ (coprodIsoSigma X Y).inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q

Tactic:
by
  delta AffineTargetMorphismProperty; ext; exact H _

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsAffine Z
⊢ P (f ≫ g) ↔ P g

Tactic:
by
  rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_left_of_respectsIso]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app
            (op (WalkingMultispan.left (i, j))) ≫
          𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
rw [Category.comp_id, Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app
          (op (WalkingMultispan.left (i, j))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := ⋯
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).toPreZeroHypercover.1), Q ((Scheme.coverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔
    Q (pullback.snd f (𝟙 Y))

pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := ⋯
⊢ Q (pullback.snd f (𝟙 Y)) ↔ Q f

Tactic:
· exact ⟨fun H => H PUnit.unit, fun H _ => H⟩

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := ⋯
⊢ Q (pullback.snd f (𝟙 Y)) ↔ Q f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
this : P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ Q (Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f ⟨i, j⟩)

Tactic:
← Q.cancel_left_of_respectsIso (𝒰.pullbackCoverAffineRefinementObjIso f _).inv,

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
this : P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ Q
    ((Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 ⟨i, j⟩).inv ≫
      Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f ⟨i, j⟩)
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case h
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 * (algebraMap R (Rₜ ⟨a, ha⟩)) a ^ ((sec a x).2 + 1) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1

Tactic:
← map_pow,

Goal state after:
case h
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 * (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ ((sec a x).2 + 1)) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
⊢ IsUnit ((algebraMap S (Localization.Away ↑a)) ↑a ^ (IsLocalization.Away.sec ↑a ↑b).2)

Tactic:
exact IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)

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 * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f ↑r ^ n' * f (↑r ^ n) * x = f ↑r ^ n' * f b
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
← map_pow,

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 * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ n') * f (↑r ^ n) * x = f (↑r ^ n') * f b
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
⊢ ∀ (i : ↥sf × ↥sg),
    P
      ((algebraMap T
            ((fun x ↦
                match x with
                | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
              i)).comp
        (g.comp f))

Tactic:
intro ⟨a, b⟩
    let g' := (algebraMap T (Localization.Away b.val)).comp g
    let a' := (algebraMap T (Localization.Away b.val)) (g a.val)
    have : (algebraMap T <| Localization.Away a').comp (g.comp f) =
        (Localization.awayMap g' a.val).comp ((algebraMap S (Localization.Away a.val)).comp f) := by
      ext x
      simp only [coe_comp, Function.comp_apply, a']
      change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))
      simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]
      rfl
    simp only [this, a']
    apply hPc _ _ (hsf a.val a.property)
    apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)
    exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val

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

Goal state before:
pp: case of_sSup_eq_top.a.refine_2
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i = ((X'.isoOfEq ⋯).hom ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i

Tactic:
· rw [← cancel_mono (Scheme.Opens.ι _)]
          simp [morphismRestrict_ι_assoc, h.1.1]

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g (𝒰.f i ≫ f)
⊢ P ((pullbackLeftPullbackSndIso g f (𝒰.f i)).hom ≫ pullback.fst g (𝒰.f i ≫ f))

Tactic:
pullbackLeftPullbackSndIso_hom_fst

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g (𝒰.f i ≫ f)
⊢ P (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
let Q := affineLocally (fun f ↦ P (Spec.map (CommRingCat.ofHom f)))

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s ^ n = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
← map_pow,

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case inst.refine_2
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsQuasiSeparated ⊤.carrier

Tactic:
· exact isQuasiSeparated_univ

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊓ ↑↑V ⊆ X.zeroLocus ↑(I.ideal V)

Tactic:
rintro x ⟨⟨hx, hxU⟩, hxV⟩

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hx : x ∈ X.zeroLocus ↑(I.ideal U)
hxU : x ∈ ↑↑U
⊢ x ∈ X.zeroLocus ↑(I.ideal V)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: 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 (f.app (Y.basicOpen s))) (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨s ^ n, ⋯⟩) = 0
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

Tactic:
← IsLocalization.mk'_spec' (M := .powers s),

Goal state after:
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 (f.app (Y.basicOpen s))) (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨s ^ n, ⋯⟩) = 0
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s)))
      ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) ↑?y * IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ?y) =
    0

case y
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 (f.app (Y.basicOpen s))) (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨s ^ n, ⋯⟩) = 0
⊢ ↥(Submonoid.powers s)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
by
  rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
by
  refine (pullback.lift_fst_assoc _ _ _ _).trans ?_
  conv_lhs => enter [2]; rw [glueDataObjι]
  rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : P g
x : ↥X
y : ↥Y
hxy : f x = g y
⊢ ∃ a, (pullback.fst f g) a = x

Tactic:
obtain ⟨a, b, h⟩ := Pullback.exists_preimage_pullback x y hxy

Goal state after:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : P g
x : ↥X
y : ↥Y
hxy : f x = g y
a : ↥(pullback f g)
b : (pullback.fst f g) a = x
h : (pullback.snd f g) a = y
⊢ ∃ a, (pullback.fst f g) a = 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
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : f y = g x
o : ↥P
hl : fst o = y
hr : snd o = x
⊢ o ∈ ⇑fst ⁻¹' s ∧ snd o = x

Tactic:
simpa [hl, hr]

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

Goal state before:
pp: case 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
⊢ ∀ (Y : CommRingCatᵒᵖ), ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ Y)

Tactic:
· intro R
    refine ⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩
    refine fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩
    · simp [← Spec.map_comp_assoc, F]
    · exact (P.cancel_left_of_respectsIso _ _).mpr S.prop

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

Goal state before:
pp: case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤ Hom.ker I.subschemeι

Tactic:
← pullback.lift_fst (f := f) (g := J.subschemeι) I.subschemeι
      ((I.subschemeι ≫ f).toImage ≫ inclusion H) (by simp)

Goal state after:
case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤
    Hom.ker (pullback.lift I.subschemeι (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ⋯ ≫ pullback.fst f J.subschemeι)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.snd f I.subschemeι = (I.comap f).subschemeMap I f ⋯

Tactic:
rw [← cancel_mono I.subschemeι]

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ((I.comapIso f).hom ≫ pullback.snd f I.subschemeι) ≫ I.subschemeι = (I.comap f).subschemeMap I f ⋯ ≫ I.subschemeι
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)
⊢ FinitePresentation R S

Tactic:
have hfintype : Algebra.FiniteType R S := by
    apply Algebra.FiniteType.of_span_eq_top_target s hs
    intro x hx
    have := h ⟨x, hx⟩
    infer_instance

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
⊢ FinitePresentation R S
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ≫ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι)
⊢ IsImmersion (pullback.diagonal f)

Tactic:
morphismRestrict_ι,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion ((pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱).ι ≫ pullback.diagonal f)
⊢ IsImmersion (pullback.diagonal f)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
H : IsConstructible s
⊢ ∃ S, S.toSet = s

Tactic:
induction s, H using IsConstructible.induction_of_isTopologicalBasis
      _ (isTopologicalBasis_basic_opens (R := R)) with
  | isCompact_basis i => exact isCompact_basicOpen _
  | sdiff i s hs =>
    have : Finite s := hs
    refine ⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩
    simp only [ConstructibleSetData.toSet, Finset.mem_singleton, BasicConstructibleSetData.toSet,
      Set.iUnion_iUnion_eq_left, basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂,
        compl_sdiff_compl, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton]
    congr! 2
    ext
    simp [← (Finite.equivFin s).exists_congr_right, -Nat.card_coe_set_eq]
  | union s hs t ht Hs Ht =>
    obtain ⟨S, rfl⟩ := Hs
    obtain ⟨T, rfl⟩ := Ht
    refine ⟨S ∪ T, ?_⟩
    simp only [ConstructibleSetData.toSet, Set.biUnion_union, ← Finset.mem_coe, Finset.coe_union]

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
a✝ : Nontrivial R
⊢ LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Tactic:
rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ HasAffineProperty @IsSeparated fun X x x_1 x_2 ↦ X.IsSeparated

Tactic:
by
  convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated with X Y f hY
  rw [Scheme.isSeparated_iff, ← terminal.comp_from f, IsSeparated.comp_iff]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this : IsArtinianRing ↑Γ(X, W)
⊢ IsOpen {x}

Tactic:
have : DiscreteTopology (Spec Γ(X, W)) := inferInstanceAs (DiscreteTopology (PrimeSpectrum _))

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this✝ : IsArtinianRing ↑Γ(X, W)
this : DiscreteTopology ↥(Spec Γ(X, W))
⊢ IsOpen {x}
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
hf : geometrically P f
⊢ P X

Tactic:
by
  rw [geometrically_eq_universally] at hf
  exact MorphismProperty.universally_le _ _ hf ‹_› ‹_›

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this : IsReduced (Y.affineCover.X i)
⊢ Finite ↑(irreducibleComponents ↥(Y.affineCover.X i))

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId (hygieneInfo `[anonymous]))
   []
   [(Term.typeSpec
     ":"
     (Term.app
      `IsNoetherian
      [(Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.app `Y.affineCover.X [`i]) ")")]))]
   ":="
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this✝ : IsReduced (Y.affineCover.X i)
this : IsNoetherian (Y.affineCover.X i) :=
  { toIsLocallyNoetherian := instIsLocallyNoetherianXScheme i,
    toCompactSpace := Scheme.compactSpace_of_isAffine (Y.affineCover.X i) }
⊢ Finite ↑(irreducibleComponents ↥(Y.affineCover.X i))