mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
inst✝² : CommRing R✝
inst✝¹ : CommRing S✝
f : R✝ →+* S✝
hf : f.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝ : CommRing R
S : Type u_2
⊢ ∀ [inst : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)

Tactic:
_

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f : R✝ →+* S✝
hf : f.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
⊢ ∀ (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_2
R✝ : Type u_1
S : Type u_2
inst✝¹ : CommRing R✝
inst✝ : CommRing S
f : R✝ →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
⊢ ∀ [inst : CommRing R] (S : Type u_1) [inst_1 : CommRing S] (T : Type u_2) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)

Tactic:
_

Goal state after:
case refine_2
R✝ : Type u_1
S : Type u_2
inst✝² : CommRing R✝
inst✝¹ : CommRing S
f : R✝ →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (S : Type u_1) [inst : CommRing S] (T : Type u_2) [inst_1 : CommRing T] (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝² : CommRing R✝
inst✝¹ : CommRing S✝
f : R✝ →+* S✝
hf : f.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝ : CommRing R
S : Type u_1
⊢ ∀ [inst : CommRing S] (T : Type u_2) [inst_1 : CommRing T] (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)

Tactic:
_

Goal state after:
case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f : R✝ →+* S✝
hf : f.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
⊢ ∀ (T : Type u_2) [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f : R✝ →+* S✝
hf : f.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
T : Type u_2
⊢ ∀ [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)

Tactic:
_

Goal state after:
case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
f : R✝ →+* S✝
hf : f.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
T : Type u_2
inst✝ : CommRing T
⊢ ∀ (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
← IsNilpotent.map_iff e.injective,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent (e ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0

Tactic:
← IsNilpotent.map_iff e.injective,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ IsNilpotent (e ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f)) ↔
    map (algebraMap R x.asIdeal.ResidueField) f = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ IsNilpotent
      ((Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField)
        ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f)) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
← IsNilpotent.map_iff e.injective,

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ IsNilpotent
      (e
        ((Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f))) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
Opens.map_coe,

Goal state after:
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (⇑f ⁻¹' ↑U)
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
⊢ IsOpen {x}

Tactic:
obtain ⟨W, hW1, hW2, _⟩ := exists_isAffineOpen_mem_and_subset (TopologicalSpace.Opens.mem_top x)

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 ⊆ ↑⊤
⊢ IsOpen {x}
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: 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] (y : Spec (of K) ⟶ Y) ⦃Z : Scheme⦄ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)),
    IsPullback fst snd f y → P Z

Tactic:
_

Goal state after:
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
⊢ ∀ (y : Spec (of K) ⟶ Y) ⦃Z : Scheme⦄ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)), IsPullback fst snd f y → P Z
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
K : Type u
⊢ ∀ [inst : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)

Tactic:
_

Goal state after:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝² : CommRing R
f : X ⟶ Spec (of R)
inst✝¹ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
K : Type u
inst✝ : Field K
⊢ ∀ (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)
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)
⊢ IsReduced X

Tactic:
by
  let pt (Z : irreducibleComponents Y) := Y.presheaf.stalk Z.property.1.genericPoint
  have hpt (Z : _) : IsField (pt Z) :=
    isField_stalk_of_closure_mem_irreducibleComponents _ _ (by
      rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]
      exact Z.property)
  let (Z : _) := (hpt Z).toField
  let Z := ∐ fun Z ↦ Spec (pt Z)
  let g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk _
  have : Finite Z := (sigmaMk _).finite_iff.mp inferInstance
  have : QuasiCompact g := ⟨fun _ _ _ ↦ (Set.toFinite _).isCompact⟩
  have H : IsSchemeTheoreticallyDominant g := by
    rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]
    intro y
    let z : Z := Sigma.ι (fun Z ↦ Spec (pt Z)) ⟨_, irreducibleComponent_mem_irreducibleComponents y⟩
      (IsLocalRing.closedPoint _)
    have hz : g z ⤳ y := by
      simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]
      exact (IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent
    exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)
  suffices IsReduced (pullback f g) from IsSchemeTheoreticallyDominant.isReduced (pullback.fst f g)
  have H := IsUniversalColimit.isPullback_of_isColimit_left
    (X := fun Z ↦ Spec (pt Z))
    (FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct _))
    (fun Z ↦ Y.fromSpecStalk _) g f _ _ (fun _ ↦ .of_hasPullback _ _) (coproductIsCoproduct _)
  apply +allowSynthFailures @isReduced_of_isOpenImmersion (f := H.isoPullback.inv)
  apply +allowSynthFailures @IsReduced.of_openCover (𝒰 := sigmaOpenCover _)
  exact fun i ↦ GeometricallyReduced.geometrically_isReduced _ _ _ (.of_hasPullback _ _)

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

Goal state before:
pp: case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ IsIrreducible (⇑f ⁻¹' s)

Tactic:
refine hs.preimage_of_isPreirreducible_fiber _ hf
      (fun x ↦ (this isIrreducible_singleton ⟨_, rfl⟩).isPreirreducible) ?_

Goal state after:
case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ (s ∩ Set.range ⇑f).Nonempty
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ (s ∩ Set.range ⇑f).Nonempty

Tactic:
rw [Set.range_eq_univ.mpr f.surjective, Set.inter_univ]

Goal state after:
case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ s.Nonempty
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ (topologically @IsClosedMap).universally f

Tactic:
rw [universallyClosed_iff]

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

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem (e (e.symm x))

Tactic:
apply RingHom.isIntegralElem_map

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
⊢ Epi (Scheme.forgetToLocallyRingedSpace.map f)

Tactic:
apply CategoryTheory.Functor.epi_of_epi_map (LocallyRingedSpace.forgetToSheafedSpace)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
⊢ Epi (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f))
Module: Mathlib.Topology.LocallyFinsupp

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

Tactic:
constructor <;> intro hx

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
hx : 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
hx : x ∈ U \ {x | (fun x ↦ D x = 0 x) x}
⊢ x ∈ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support).Finite
a✝ : X
⊢ (a✝ ∈ t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0) → a✝ ∈ t ∩ D.support

Tactic:
_

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support).Finite
a✝¹ : X
a✝ : a✝¹ ∈ t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0
⊢ a✝¹ ∈ t ∩ 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✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x✝ : X
⊢ x✝ ∈ V → (D.restrict h) x✝ = D x✝

Tactic:
_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x✝ : X
a✝ : x✝ ∈ V
⊢ (D.restrict h) x✝ = D x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
⊢ (diagonal @Surjective).universally ≤ @UniversallyInjective

Tactic:
universallyInjective_eq

Goal state after:
case a
⊢ (diagonal @Surjective).universally ≤
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x).universally
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
⊢ ∀ [inst : Field K], Injective fun g ↦ g ≫ f

Tactic:
_

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
⊢ Injective fun g ↦ g ≫ f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
q : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ pullback f f := pullback.lift g₁ g₂ ⋯
⊢ (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁ =
    (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂

Tactic:
have q_fst : q ≫ pullback.fst f f = g₁ := pullback.lift_fst _ _ _

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
q : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ pullback f f := pullback.lift g₁ g₂ ⋯
q_fst : q ≫ pullback.fst f f = g₁
⊢ (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁ =
    (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.73} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.73} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
xj : ↥(d.cover.X j) := (pullback.snd (d.cover.f i) (d.cover.f j)) x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ ∃ k hki hkj y, (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x

Tactic:
use k, fi, fj

Goal state after:
case h
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.73} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.73} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := ⋯
xj : ↥(d.cover.X j) := ⋯
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ ∃ y, (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.I₀
⊢ P ((Over.forget S).map (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)))

Tactic:
← PreservesPullback.iso_hom_fst,

Goal state after:
case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.I₀
⊢ P
    ((PreservesPullback.iso (Over.forget S) (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)).hom ≫
      pullback.fst ((Over.forget S).map (Hom.asOver f S)) ((Over.forget S).map (Hom.asOver (𝒰.f j) S)))
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₁
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
_

Goal state after:
case hP₁
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n { val := 0 }
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₁
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
R₀ : Type u_1
⊢ ∀ [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
_

Goal state after:
case hP₁
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
R₀ : Type u_1
inst✝ : CommRing R₀
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n { val := 0 }
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₁
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
R₀ : Type u_1
inst✝ : CommRing R₀
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
_

Goal state after:
case hP₁
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
⊢ Statement R₀ R n { val := 0 }
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_

Goal state after:
case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e