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

Goal state before:
pp: case e'_3.h₀
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.fst Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.fst Y.hom Y.hom

pp: case h₁
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.snd Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.snd Y.hom Y.hom

Tactic:
<;>

Goal state after:
case e'_3.h₀
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.fst Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.fst Y.hom Y.hom

case h₁
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.snd Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.snd Y.hom Y.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case h₀
X : Scheme
⊢ pullback.diagonal (terminal.from X) ≫ pullback.fst (terminal.from X) (terminal.from X) =
    (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.fst (terminal.from X) (terminal.from X)

pp: case h₁
X : Scheme
⊢ pullback.diagonal (terminal.from X) ≫ pullback.snd (terminal.from X) (terminal.from X) =
    (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.snd (terminal.from X) (terminal.from X)

Tactic:
<;>

Goal state after:
case h₀
X : Scheme
⊢ pullback.diagonal (terminal.from X) ≫ pullback.fst (terminal.from X) (terminal.from X) =
    (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.fst (terminal.from X) (terminal.from X)

case h₁
X : Scheme
⊢ pullback.diagonal (terminal.from X) ≫ pullback.snd (terminal.from X) (terminal.from X) =
    (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.snd (terminal.from X) (terminal.from X)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ ¬IsNilpotent
        ((algebraMap (A ⧸ Ideal.span s) ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField))
          ((algebraMap A (A ⧸ Ideal.span s)) f)) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
isNilpotent_tensor_residueField_iff

Goal state after:
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ (¬∀ i < Module.finrank R (A ⧸ Ideal.span s),
        (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((algebraMap A (A ⧸ Ideal.span s)) f))).coeff i ∈
          x.asIdeal) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)

Tactic:
refine ⟨fun _ ↦ inferInstance, ?_⟩
  · rw [isLocallyNoetherian_iff_of_affine_openCover (𝒰 := 𝒰.affineRefinement.openCover)]
    intro h i
    exact @isNoetherianRing_of_ringEquiv _ _ _ _
      (IsOpenImmersion.ΓIsoTop (PreZeroHypercover.f _ i.2)).symm.commRingCatIsoToRingEquiv
      (IsLocallyNoetherian.component_noetherian ⟨_, isAffineOpen_opensRange _⟩)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
⊢ IsArtinianScheme X ↔ IsNoetherian X ∧ DiscreteTopology ↥X

Tactic:
aesop (add simp [isArtinianScheme_iff, isNoetherian_iff,
    IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology])

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

Goal state before:
pp: case refine_1.commfst
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ snd ≫ (Iso.refl X).hom = (Iso.refl Z).hom ≫ snd

pp: case refine_1.commsnd
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ fst ≫ W.isoSpec.hom = (Iso.refl Z).hom ≫ fst ≫ W.isoSpec.hom

pp: case refine_1.commf
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ f ≫ (Iso.refl Y).hom = (Iso.refl X).hom ≫ f

pp: case refine_1.commg
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ q ≫ (Iso.refl Y).hom = W.isoSpec.hom ≫ W.isoSpec.inv ≫ q

Tactic:
<;>

Goal state after:
case refine_1.commfst
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ snd ≫ (Iso.refl X).hom = (Iso.refl Z).hom ≫ snd

case refine_1.commsnd
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ fst ≫ W.isoSpec.hom = (Iso.refl Z).hom ≫ fst ≫ W.isoSpec.hom

case refine_1.commf
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ f ≫ (Iso.refl Y).hom = (Iso.refl X).hom ≫ f

case refine_1.commg
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ q ≫ (Iso.refl Y).hom = W.isoSpec.hom ≫ W.isoSpec.inv ≫ q
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✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ closure (Set.range ⇑g) = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ ∀ (x : ↥Y), x ∈ closure (Set.range ⇑g)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
⊢ IsSchemeTheoreticallyDominant (pullback.snd f g)

Tactic:
rw [isSchemeTheoreticallyDominant_iff]

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
⊢ Scheme.Hom.ker (pullback.snd f g) = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically IsOpenMap) Y.affineCover]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap)
      (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X Y Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsIntegralHom f ↔
      IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral

Tactic:
simp [isIntegralHom_iff]

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case e'_1
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

pp: case e'_3.e'_6
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1✝ : ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) = ↑(X.basicOpen r)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
<;>

Goal state after:
case e'_1
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

case e'_3.e'_6
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1✝ : ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) = ↑(X.basicOpen r)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ f = g

Tactic:
suffices f.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom =
      g.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom by
    ext x
    · obtain ⟨x⟩ := x
      simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (C x)
    · simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (X x)
  ext1
  · exact RingHom.ext_int _ _
  · simpa using! h _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
⊢ (f ≫ homOfVector g v) ≫ 𝔸(n; S) ↘ S =
    homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v) ≫ 𝔸(n; S) ↘ S

pp: case h₂
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (f ≫ homOfVector g v))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v))))
      (coord S i✝)

Tactic:
<;>

Goal state after:
case h₁
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
⊢ (f ≫ homOfVector g v) ≫ 𝔸(n; S) ↘ S =
    homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (f ≫ homOfVector g v))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v))))
      (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
⊢ map n (𝟙 S) ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

pp: case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (𝟙 S)))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
<;>

Goal state after:
case h₁
n : Type u
S : Scheme
⊢ map n (𝟙 S) ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (𝟙 S)))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom

Tactic:
by have := (SpecIso n R).inv_hom_id; simp [map_SpecMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
⊢ reindex id S ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

pp: case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex id S))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
<;>

Goal state after:
case h₁
n : Type u
S : Scheme
⊢ reindex id S ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex id S))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (i ≫ j))) S ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S =
    (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S) ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S

pp: case h₂
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
k : (fun X ↦ X) n₁
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom (i ≫ j))) S))) (coord S k) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S)))
      (coord S k)

Tactic:
<;>

Goal state after:
case h₁
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (i ≫ j))) S ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S =
    (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S) ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S

case h₂
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
k : (fun X ↦ X) n₁
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom (i ≫ j))) S))) (coord S k) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S)))
      (coord S k)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
rw [descColimitType_injective_iff_of_isFiltered]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (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),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ (map n₂ f ≫ reindex i T) ≫ 𝔸(n₁; T) ↘ T = (reindex i S ≫ map n₁ f) ≫ 𝔸(n₁; T) ↘ T

pp: case h₂
n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ ∀ (i_1 : n₁),
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n₂ f ≫ reindex i T))) (coord T i_1) =
      (ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S ≫ map n₁ f))) (coord T i_1)

Tactic:
<;>

Goal state after:
case h₁
n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ (map n₂ f ≫ reindex i T) ≫ 𝔸(n₁; T) ↘ T = (reindex i S ≫ map n₁ f) ≫ 𝔸(n₁; T) ↘ T

case h₂
n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ ∀ (i_1 : n₁),
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n₂ f ≫ reindex i T))) (coord T i_1) =
      (ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S ≫ map n₁ f))) (coord T i_1)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mpr.inl
n : Type u
S : Scheme
h✝ : IsEmpty ↥S
⊢ IsIntegralHom (𝔸(n; S) ↘ S)

pp: case mpr.inr
n : Type u
S : Scheme
h✝ : IsEmpty n
⊢ IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
<;>

Goal state after:
case mpr.inl
n : Type u
S : Scheme
h✝ : IsEmpty ↥S
⊢ IsIntegralHom (𝔸(n; S) ↘ S)

case mpr.inr
n : Type u
S : Scheme
h✝ : IsEmpty n
⊢ IsIntegralHom (𝔸(n; S) ↘ S)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: case refine_2.refine_1
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) ≫ i = 𝟙 (Spec (CommRingCat.of K))

pp: case refine_2.refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) ≫ i = 𝟙 (Spec (CommRingCat.of K))

Tactic:
<;>

Goal state after:
case refine_2.refine_1
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) ≫ i = 𝟙 (Spec (CommRingCat.of K))

case refine_2.refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) ≫ i = 𝟙 (Spec (CommRingCat.of K))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case mp
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ D.support → x ∈ U \ {x | (fun x ↦ D x = 0 x) x}

pp: case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ U \ {x | (fun x ↦ D x = 0 x) x} → x ∈ D.support

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ D.support → x ∈ U \ {x | (fun x ↦ D x = 0 x) x}

case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ U \ {x | (fun x ↦ D x = 0 x) x} → x ∈ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
⊢ ∀ z ∈ U, ∃ t, t ∈ 𝓝 z

Tactic:
exact fun _ _ ↦ ⟨⊤, univ_mem⟩

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
e : X
hz : D e ≠ 0
⊢ (single e 1) e ≤ D e

pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : D z ≠ 0
e : X
he : e ≠ z
⊢ (single z 1) e ≤ D e

Tactic:
· simpa [single_apply] using! Int.lt_iff_le_and_ne.mpr ⟨h.le e, hz.symm⟩

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : D z ≠ 0
e : X
he : e ≠ z
⊢ (single z 1) e ≤ D e
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
hx : x ∈ V
⊢ ((D₁ + D₂).restrict h) x = (D₁.restrict h + D₂.restrict h) x

pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
hx : x ∉ V
⊢ ((D₁ + D₂).restrict h) x = (D₁.restrict h + D₂.restrict h) x

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
hx : x ∈ V
⊢ ((D₁ + D₂).restrict h) x = (D₁.restrict h + D₂.restrict h) x

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
hx : x ∉ V
⊢ ((D₁ + D₂).restrict h) x = (D₁.restrict h + D₂.restrict h) x