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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i : J
⊢ colimit.ι F i =
    (F.mapIso (eqToIso ⋯)).hom ≫
      (Precoverage.ZeroHypercover.bind (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
            fun i ↦ (glueData F).openCover).f
        (((equivShrink J).trans (Equiv.uniqueSigma fun x ↦ Shrink.{u, w} J).symm) i)

Tactic:
change colimit.ι F i = _ ≫ (glueData F).ι (equivShrink J i) ≫ _
  simp [← Category.assoc, ← Iso.comp_inv_eq, cocone]

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 : D.J
U : Opens ↑↑(D.U i)
⊢ IsIso ((D.ι i).c.app (op (⋯.functor.obj U)))

Tactic:
by erw [← colimitPresheafObjIsoComponentwiseLimit_hom_π]; infer_instance

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

Goal state before:
pp: case add
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 y : S ⊗[R] T
ex : ∃ a, (algebraMap S (S ⊗[R] T)) a = x
ey : ∃ a, (algebraMap S (S ⊗[R] T)) a = y
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = x + y

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey

Goal state after:
case add
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 y : S
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = (algebraMap S (S ⊗[R] T)) x + (algebraMap S (S ⊗[R] T)) y
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))

Tactic:
← RingHom.comp_assoc,

Goal state after:
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (((algebraMap T (Localization.Away (e a))).comp e.toRingHom).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun f ↦ Y.basicOpen ↑f) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : 𝒰.toPreZeroHypercover.1
⊢ Y.basicOpen ↑i = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
by simp [𝒰]

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)
x : ↥X
⊢ f x ∈ ⊤

Tactic:
trivial

Goal state after:
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 : CommRingCat
⊢ ∀ (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:
B

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.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
⊢ x ∈ ⊤

Tactic:
trivial

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparatedSpace ↥Y
inst✝ : QuasiSeparated f
⊢ QuasiSeparatedSpace ↥X

Tactic:
by
  rw [quasiSeparatedSpace_iff_quasiSeparated] at hY ⊢
  rw [← terminalIsTerminal.hom_ext (f ≫ terminal.from Y) (terminal.from X)]
  infer_instance

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

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ IsQuasiSeparated ⊥.carrier →
    ∀ (f : ↑Γ(X, ⊥)) (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

Tactic:
intro _ f x
    use 0, f
    refine @Subsingleton.elim _
      (CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty ?_)) _ _
    rw [eq_bot_iff]
    exact X.basicOpen_le f

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS✝ : IsClosed S
hT✝ : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
hS : x ∈ ↑{ carrier := Sᶜ, is_open' := ⋯ }
hT : x ∈ ↑{ carrier := Tᶜ, is_open' := ⋯ }
⊢ x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
z : ↥X
n : ℕ
hz : coheight z ≤ ↑n
⊢ Ring.KrullDimLE n ↑(X.presheaf.stalk z)

Tactic:
by
  rw [Ring.krullDimLE_iff, ringKrullDim_stalk_eq_coheight z]
  exact_mod_cast hz

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsClosed I.supportSet

Tactic:
TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage (iSup_affineOpens_eq_top X)

Goal state after:
X : Scheme
I : X.IdealSheafData
⊢ ∀ (i : ↑X.affineOpens), IsClosed (Subtype.val ⁻¹' I.supportSet)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ hU.fromSpecStalk hxU = fromSpecStalk h₁ h₂

pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ fromSpecStalk h₁ h₂ = hV.fromSpecStalk hxV

Tactic:
· delta fromSpecStalk
    rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]

Goal state after:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ fromSpecStalk h₁ h₂ = hV.fromSpecStalk hxV
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
⊢ ↑Z ∩ ↑↑U ⊆ ↑I.support ∩ ↑↑U ↔ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
rw [coe_support_inter, ← Set.image_subset_image_iff U.2.fromSpec.isOpenEmbedding.injective,
    Set.image_preimage_eq_inter_range, IsAffineOpen.fromSpec_image_zeroLocus,
    IsAffineOpen.range_fromSpec]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
f : ↑(X.presheaf.obj (op ⊤))
⊢ x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
this : Nonempty ↥S
⊢ ¬Disjoint (Set.range ⇑f) (Set.range ⇑g)

Tactic:
Set.not_disjoint_iff

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
this : Nonempty ↥S
⊢ ∃ x ∈ Set.range ⇑f, x ∈ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
⊢ (Hom.ker X.toSpecΓ).ideal ⟨⊤, ⋯⟩ = ⊥.ideal ⟨⊤, ⋯⟩

Tactic:
simpa using! RingHom.ker_coe_equiv (ΓSpecIso Γ(X, ⊤)).commRingCatIsoToRingEquiv

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ inv (X.homOfLE ⋯) = X.homOfLE ⋯

Tactic:
rw [eq_comm, ← hom_comp_eq_id]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑U ⊓ ↑V)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ix))) x) ∈ ↑I.support

Tactic:
change (I.glueData.ι _ ≫ I.gluedTo) x ∈ I.support

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ (I.glueData.ι ix ≫ I.gluedTo) x ∈ I.support
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 ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case refine_3
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) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r ⊗[R] S)) x ∈ ⊤

Tactic:
trivial

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

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away (f ↑r))) x ∈ ⊤

Tactic:
trivial

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

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), ((algebraMap S (Localization.Away ↑r)).comp f).FiniteType
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FiniteType

Tactic:
replace H : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FiniteType] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
algInst✝ : Algebra R S := f.toAlgebra
H : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away r)
⊢ f.FiniteType
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ Hom.ker ((vanishingIdeal Z).subschemeι ≫ f) ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

Tactic:
← le_support_iff_le_vanishingIdeal,

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ TopologicalSpace.Closeds.closure (⇑f '' ↑Z) ≤ (Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0

Tactic:
obtain ⟨_, ⟨s, rfl⟩, hyv, bsle⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_basicOpen Y)
    (show f x ∈ ⟨f '' U.carrier, hfopen U.carrier U.is_open'⟩ from ⟨x, by simpa⟩)

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
⊢ IsImmersion g'

Tactic:
let e : Y' ⟶ Z := Limits.pullback.lift g' (f' ≫ g.liftCoborder) (by simpa using H.w.symm)

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsImmersion g'
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 ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderSpecialization s
hs' : IsConstructible s
⊢ IsClosed s

Tactic:
by
  obtain ⟨S, _, f, rfl⟩ := exists_range_eq_of_isConstructible hs'
  exact isClosed_range_of_stableUnderSpecialization _ hs

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

Goal state before:
pp: R : Type u_3
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 : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) ((toMatrix b b) f).charpoly

Tactic:
← (f.baseChange A).charpoly_toMatrix (b.baseChange A),

Goal state after:
R : Type u_3
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 : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
⊢ ((toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b)) (baseChange A f)).charpoly =
    Polynomial.map (algebraMap R A) ((toMatrix b b) f).charpoly
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
⊢ (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x = (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) y

Tactic:
coeq_condition

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
⊢ (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x = (ConcreteCategory.hom (F.map (f' ≫ coeqHom f f'))) y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
x x' : F.obj j
eq✝ : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ (ConcreteCategory.hom (F.map (f' ≫ coeqHom f f'))) x' = (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x'

Tactic:
coeq_condition

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
x x' : F.obj j
eq✝ : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ (ConcreteCategory.hom (F.map (f' ≫ coeqHom f f'))) x' = (ConcreteCategory.hom (F.map (f' ≫ coeqHom f f'))) x'
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
f : locallyFinsupp X Y
x✝ : X
⊢ x✝ ∈ univ

Tactic:
trivial

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ 0 ≤ single x y ↔ 0 ≤ y

Tactic:
simp only [le_def, coe_single]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ ⇑0 ≤ Pi.single x y ↔ 0 ≤ y
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inl
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : IsEmpty I
⊢ Nonempty ↥c.pt

pp: case inr
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
⊢ Nonempty ↥c.pt

Tactic:
· have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
    exact Nonempty.map e.inv inferInstance

Goal state after:
case inr
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
⊢ Nonempty ↥c.pt
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j : Over i
⊢ c.π.app i ⁻¹ᵁ U ≤ (c.π.app j.left ≫ D.map j.hom) ⁻¹ᵁ U

Tactic:
c.w

Goal state after:
I : Type u
inst✝ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j : Over i
⊢ c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ U