mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0

Tactic:
← Scheme.Hom.appLE_map _ ((Opens.map _).map w).le (homOfLE <| hwle i).op,

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' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appLE (𝒰.f i) ⊤ ((Opens.map (𝒰.f i).base).obj U) ⋯ ≫ (𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom φ) g) =
    0
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
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x

Tactic:
let j := (𝒱 i).idx z

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))
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f)).Opens
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    Scheme.Hom.app f ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
Scheme.Hom.congr_app (f.liftCoborder_ι).symm (f.coborderRange.ι ''ᵁ U)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f)).Opens
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    (Scheme.Hom.app (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
          ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫
        X.presheaf.map (eqToHom ⋯).op) ≫
      X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsDominant (Scheme.Hom.coborderRange f).ι

Tactic:
rw [isDominant_iff, DenseRange, Scheme.Opens.range_ι]
  exact dense_coborder

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = (pullback.diagonal f) x

Tactic:
let j := (𝒱 i).idx z

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = (pullback.diagonal f) x
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_1
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (i : X ⟶ Y),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : Y ⟶ Z),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)

Tactic:
intro X Y Z i hi f hf
      change IsIso i at hi
      change IsLocallyClosed _
      simpa only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
        Set.range_eq_univ.mpr i.surjective, Set.image_univ]

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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
⊢ f = g

Tactic:
let U' : Over Z := Over.mk (ι ≫ f ≫ s)

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
⊢ f = g
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi : i = ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (algebraMap R I.ResidueField) ((LinearMap.mul R A) f).charpoly.leadingCoeff = 1

Tactic:
((LinearMap.mul R A) f).charpoly_monic,

Goal state after:
case inr.mpr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi : i = ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (algebraMap R I.ResidueField) 1 = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H :
  (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∉
    nilradical ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})

Tactic:
nilradical_eq_sInf,

Goal state after:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H : (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∉ sInf {J | J.IsPrime}
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ I N = I n

Tactic:
rw [IsLocalization.ideal_eq_iInf_under_map_away hS (I N),
      IsLocalization.ideal_eq_iInf_under_map_away hS (I n),
      iInf_subtype', iInf_subtype']

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I n))
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
⊢ Topology.IsCoinducing ⇑f ∧ Function.Surjective ⇑f

Tactic:
refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦
    ⟨fun hs ↦ ?_, fun hs ↦ hs.preimage f.continuous⟩, f.surjective⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
⊢ IsOpen s
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Flat (Spec.map (Scheme.Hom.appTop f)) ∧ Surjective (Spec.map (Scheme.Hom.appTop f)) ↔
    Flat (Spec.map (Scheme.Hom.appTop f)) ∧
      Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))

Tactic:
surjective_iff

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Flat (Spec.map (Scheme.Hom.appTop f)) ∧ Function.Surjective ⇑(Spec.map (Scheme.Hom.appTop f)) ↔
    Flat (Spec.map (Scheme.Hom.appTop f)) ∧
      Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ (CommRingCat.Hom.hom f).Flat ∧ Surjective (Spec.map f) ↔
    (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))

Tactic:
surjective_iff

Goal state after:
R S : CommRingCat
f : R ⟶ S
⊢ (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective ⇑(Spec.map f) ↔
    (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
this✝ : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.toPreZeroHypercover.1
this : topologically (@IsOpenMap) (⋯.isoPullback.hom ≫ pullback.snd (𝔸(n; S) ↘ S) (S.affineCover.f i))
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)

Goal state after:
case inr
n : Type u
S : Scheme
this✝ : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.toPreZeroHypercover.1
this : topologically (@IsOpenMap) (pullback.snd (𝔸(n; S) ↘ S) (S.affineCover.f i))
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
⊢ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.degree < v

Tactic:
rw [hv]

Goal state after:
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
⊢ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.degree < e.degree
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
f : X → Y
h : support f ⊆ U
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite

Tactic:
have : f.support = (U \ {x | f x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_sdiff, mem_ofPred_eq, iff_and_self]
    exact (h ·)

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x | f x = 0 x}
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: case convert_2
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ IsPreirreducible Set.univ

pp: case convert_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ (Set.univ ∩ Set.range ⇑f).Nonempty

Tactic:
· apply PreirreducibleSpace.isPreirreducible_univ (X := Y)

Goal state after:
case convert_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ (Set.univ ∩ Set.range ⇑f).Nonempty
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
obtain ⟨U, hU, g, hg⟩ := X.presheaf.exists_germ_eq f
  obtain ⟨_, ⟨A, hA, rfl⟩, hxA, hAU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hU U.isOpen
  have : Nonempty A := ⟨_, hxA⟩
  let gA : Γ(X, A) := X.presheaf.map (homOfLE hAU).op g
  have h_germ_gA : X.presheaf.germ A (genericPoint X) hxA gA = f := by
    simp only [← hg, ← X.presheaf.germ_res_apply (homOfLE hAU) (genericPoint X) hxA g, gA]
    rfl
  have hxV : genericPoint X ∈ X.basicOpen gA := by
    rwa [Scheme.mem_basicOpen X gA (genericPoint X) hxA, h_germ_gA, isUnit_iff_ne_zero]
  have : Nonempty (X.basicOpen gA) := ⟨⟨_, hxV⟩⟩
  refine ⟨X.basicOpen gA, hA.basicOpen gA,
    X.presheaf.map (X.basicOpen_le gA).hom.op gA, ‹_›, ?_,
    X.toRingedSpace.isUnit_res_basicOpen gA⟩
  simpa using h_germ_gA

Goal state after:
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
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁✝ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₁ : (D.map (Over.Hom.left f) ≫ D.map k.hom) x ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U

Tactic:
rwa [← D.map_comp, Over.w f] at h₁

Goal state after:
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
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
⊢ Surjective (pullback.diagonal f)

Tactic:
surjective_iff

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
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
⊢ Function.Surjective ⇑(pullback.diagonal 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 : Surjective (pullback.diagonal f)
this : UniversallyInjective f
⊢ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable

Tactic:
surjective_iff

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), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hxy
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := ⋯
k : Fin n
a✝ : k ∈ Finset.univ
⊢ (Function.update c.val j (c.val j %ₘ c.val i) k).degree ≤ (c.val k).degree

Tactic:
update_apply

Goal state after:
case hxy
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
k : Fin n
a✝ : k ∈ Finset.univ
⊢ (if k = j then c.val j %ₘ c.val i else c.val k).degree ≤ (c.val k).degree