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

Goal state before:
pp: X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
i : ↑s
⊢ ↑↑i ≤ S ⊓ ↑U

Tactic:
rw [hs]

Goal state after:
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
i : ↑s
⊢ ↑↑i ≤ ⨆ i, ↑↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
⊢ P (f ≫ g)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Y.affineCover.pullback₁ f)]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    P ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f ≫ g)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case iUV
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
i : ↑s
⊢ ↑↑i ≤ S ⊓ ↑U

Tactic:
rw [hs]

Goal state after:
case iUV
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
i : ↑s
⊢ ↑↑i ≤ ⨆ i, ↑↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme⦄ (g : Y ⟶ S), P g → IsAffine Y → P (pullback.fst f g)
hX : ¬IsAffine Y
⊢ P (pullback.fst f g)

pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : P g
hX : IsAffine Y
⊢ P (pullback.fst f g)

Tactic:
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
      (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
    intro i
    simp only [Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_π_app,
      Category.comp_id]
    apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance

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
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : P g
hX : IsAffine Y
⊢ P (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

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

Tactic:
rwa [P.cancel_right_of_respectsIso]

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
this :
  ∀ {X Y : Scheme} [IsAffine Y] (a : ↑Γ(Y, ⊤)) (f : X ⟶ ↑(Y.basicOpen a)), P f → IsAffine X → P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
⊢ P (f ≫ (Y.basicOpen a).ι)

pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
hX : IsAffine X
⊢ P (f ≫ (Y.basicOpen a).ι)

Tactic:
· rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
    intro V
    rw [← Category.assoc]
    exact this _ _ (IsZariskiLocalAtSource.comp hf _) V.2

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
hX : IsAffine X
⊢ P (f ≫ (Y.basicOpen a).ι)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ J.ideal U

Tactic:
rw [pow_add, mul_assoc]

Goal state after:
case refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U
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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P (f ≫ e.hom)

Tactic:
rwa [P.cancel_right_of_respectsIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
← hU.fromSpecStalk_eq_fromSpecStalk hyU,

Goal state after:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.app (↑U).ι ↑V ≫
          Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V) ≫
            (I.glueDataObj U).presheaf.map (homOfLE ⋯).op ≫
              Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      x =
    0

Tactic:
simp only [Scheme.Hom.app_eq_appLE, homOfLE_leOfHom, Scheme.Hom.map_appLE,
    Scheme.Hom.appLE_comp_appLE, Category.assoc, glueDataObjMap_glueDataObjι_assoc]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.appLE (I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯ ≫ (↑U).ι) (↑V)
          (I.glueDataObjMap ⋯ ⁻¹ᵁ I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f) ⋯))
      x =
    0
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Spec.map (Hom.appTop (X.fromSpecStalk x) ≫ (ΓSpecIso (X.presheaf.stalk x)).hom) =
    Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
Scheme.fromSpecStalk_appTop

Goal state after:
X : Scheme
x : ↥X
⊢ Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op) ≫
        (ΓSpecIso (X.presheaf.stalk x)).hom) =
    Spec.map (X.presheaf.germ ⊤ x trivial)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((CommRingCat.Hom.hom (Hom.stalkMap f ↑x))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
rw [LocallyRingedSpace.stalkMap_germ_apply]

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ ↑(ker f).support

Tactic:
rw [(support _).isClosed.closure_subset_iff]
    exact f.range_subset_ker_support

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

Goal state before:
pp: case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen ((↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) j))

Tactic:
← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion,

Goal state after:
case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen (U.ι ''ᵁ (↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) j))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case respectsIso.h₂
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], IsAffine X → IsAffine X

Tactic:
exact fun _ _ _ ↦ id

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = I.glueData.ι U

Tactic:
by
  have : IsIso (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) :=
    ⟨X.homOfLE (by simpa), by simp, by simp⟩
  have H : inv (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) = X.homOfLE (by simpa) := by
    rw [eq_comm, ← hom_comp_eq_id]; simp
  have := I.glueData.glue_condition U V
  simp only [glueData_J, glueData_V, glueData_t, glueData_U, glueData_f] at this
  rw [← IsIso.inv_comp_eq] at this
  rw [← Category.id_comp (I.glueData.ι U), ← this]
  simp_rw [← Category.assoc]
  congr 1
  rw [← cancel_mono (glueDataObjι _ _)]
  simp [pullback_inv_fst_snd_of_right_isIso_assoc, H]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x).1
h2 : (pullback.snd f g) z = (↑x).2
⊢ (ConcreteCategory.hom (pullback.snd (forget.map f) (forget.map g)))
      ((ConcreteCategory.hom (pullbackComparison forget f g)) z) =
    (↑x).2

Tactic:
← types_comp_apply (g := pullback.snd _ _),

Goal state after:
case h.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x).1
h2 : (pullback.snd f g) z = (↑x).2
⊢ (ConcreteCategory.hom (pullbackComparison forget f g ≫ pullback.snd (forget.map f) (forget.map g))) z = (↑x).2
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
⊢ 1 ∈ Ideal.span ↑s

Tactic:
rw [hs]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
⊢ 1 ∈ ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x

Tactic:
let i := 𝒰.idx (f (pullback.fst f f x))

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ 1 ∈ Ideal.span ↑s

Tactic:
rw [hs]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ 1 ∈ ⊤
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

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

Tactic:
apply Ideal.subset_span

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.app f U))

Tactic:
HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally
      (fun X x f [IsAffine x] ↦ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))) f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ Y✝ Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion

Goal state after:
X✝ Y✝ Z X Y : Scheme
f : X ⟶ Y
h :
  targetAffineLocally
    (fun X x f [IsAffine x] ↦ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))) f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ IsPullback (p ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)

Tactic:
convert! h
    simp [p]

Goal state after: