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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f = vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

Tactic:
apply le_antisymm

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z)) ≤ (vanishingIdeal Z).map f
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))
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x

Tactic:
obtain ⟨y : 𝒰.X i, hy : 𝒰.f i y = f _⟩ :=
    𝒰.covers (f (pullback.fst f f x))

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f ((pullback.fst f f) x)
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x
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
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ≫
          pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
            (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒱 i).f j) ((𝒱 i).f j) (𝟙 (𝒰.X i)) ⋯ ⋯) ≫
        pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
          (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
      w =
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ≫ pullback.diagonal f) w

Tactic:
congr 5

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
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ≫
        pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
          (pullback.snd f (𝒰.f i)) ((𝒱 i).f j) ((𝒱 i).f j) (𝟙 (𝒰.X i)) ⋯ ⋯) ≫
      pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
        (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯ =
    ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ≫ pullback.diagonal f
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
⊢ IsConstructible S.toSet

Tactic:
by
  refine .biUnion S.finite_toSet fun _ _ ↦ .sdiff ?_ ?_
  · rw [← isConstructible_compl]
    exact (isRetrocompact_zeroLocus_compl (Set.finite_range _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl
  · rw [← isConstructible_compl]
    exact (isRetrocompact_zeroLocus_compl (Set.finite_singleton _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl

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

Goal state before:
pp: X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst✝¹ : IsSeparated i
inst✝ : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
⊢ f = g

Tactic:
suffices IsDominant (equalizer.ι f g) from
    ext_of_isDominant_of_isSeparated i H' (equalizer.ι f g) (equalizer.condition _ _)

Goal state after:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst✝¹ : IsSeparated i
inst✝ : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
⊢ IsDominant (equalizer.ι f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

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

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion] at h

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ Scheme.Hom.ker f = ⊥

Tactic:
← Scheme.IdealSheafData.support_eq_top_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ (Scheme.Hom.ker f).support = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: 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
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
a : A
ha : a ∈ s
⊢ (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span ha)]

Goal state after:
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
⊢ (((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        f =
      0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
congr!

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
⊢ ((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) =
    map (algebraMap R x.asIdeal.ResidueField)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ Scheme.Hom.ker f = ⊥

Tactic:
← Scheme.IdealSheafData.support_eq_top_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ (Scheme.Hom.ker f).support = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: ⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
apply le_antisymm

Goal state after:
case a
⊢ @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝² : CompactSpace ↥X
this✝¹ : X.IsQuasiAffine
r : ↑Γ(Y, ⊤)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Hom.appTop f)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r))
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯) =
    CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (homOfLE ⋯).op)

Tactic:
rw [f.map_appLE, Scheme.Hom.appLE]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
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'
i : J
x : F.obj i
i' : J
x' : F.obj i'
eq✝ : c.ι i x = c.ι i' x'
k : J
f : i ⟶ k
f' : i' ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ F.ιColimitType i x = F.ιColimitType i' x'

Tactic:
← F.ιColimitType_map f x,

Goal state after:
case mpr
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'
i : J
x : F.obj i
i' : J
x' : F.obj i'
eq✝ : c.ι i x = c.ι i' x'
k : J
f : i ⟶ k
f' : i' ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ F.ιColimitType k ((ConcreteCategory.hom (F.map f)) x) = F.ιColimitType i' x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsReduced (Spec R)
⊢ IsReduced 𝔸(n; Spec R)

Tactic:
affine_isReduced_iff

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : _root_.IsReduced ↑R
⊢ IsReduced 𝔸(n; Spec R)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddGroup Y
D : locallyFinsuppWithin U Y
⊢ Function.support ⇑(-D) = D.support

Tactic:
coe_neg,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddGroup Y
D : locallyFinsuppWithin U Y
⊢ Function.support (-⇑D) = D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
⊢ ∑ᶠ (x : X), restrict (single x (F x)) ⋯ = F

Tactic:
have : (fun x ↦ (single x (F x)).restrict (subset_univ U)).support ⊆ h.toFinset := by
    intro
    contrapose
    aesop
  rw [finsum_eq_sum_of_support_subset _ this]
  ext z
  by_cases hz : z ∉ U
  · aesop
  simp [restrict_apply]
  by_cases hz : z ∈ F.support
  · aesop
  · aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
rw [injective_iff_map_eq_zero]
  intro y hy
  rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy
  obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ hx hx _ _ hy
  cases Subsingleton.elim iU iV
  have : Nonempty W := ⟨⟨_, hW⟩⟩
  exact map_injective_of_isIntegral X iU e

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ (((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩) =
    inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩) ≫ Hom.stalkMap U.ι ⟨x, hx⟩
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
W₁ W₂ : X.Opens
hW₁ : Dense ↑W₁
hW₂ : Dense ↑W₂
hW₁' : W₁ ≤ f.domain
hW₂' : W₂ ≤ g.domain
H : f.restrict W₁ hW₁ hW₁' = g.restrict W₂ hW₂ hW₂'
⊢ f.equiv g

Tactic:
by
  have e : W₁ = W₂ := congr($(H).domain)
  subst e
  exact ⟨W₁, hW₁, hW₁', hW₂', congr($(H).hom)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ f.equiv (Hom.toPartialMap g) ↔ f.hom = f.domain.ι ≫ g

Tactic:
rw [equiv_iff_of_isSeparated (S := S), ← cancel_epi (X.isoOfEq (inf_top_eq f.domain)).hom]

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    (X.isoOfEq ⋯).hom ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.domain.ι ≫ g
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: ⊢ @UniversallyInjective = diagonal @Surjective

Tactic:
apply le_antisymm

Goal state after:
case a
⊢ @UniversallyInjective ≤ diagonal @Surjective

case a
⊢ diagonal @Surjective ≤ @UniversallyInjective
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⟩
⊢ (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁ =
    (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂

Tactic:
let q := pullback.lift (f := f) (g := f) g₁ g₂ <| by
      simp only [g₁, g₂, Scheme.SpecToEquivOfField_symm_apply, AlgHom.toRingHom_eq_coe,
        Category.assoc, ← f.SpecMap_residueFieldMap_fromSpecResidueField x, ← Spec.map_comp_assoc]
      congr 2
      ext a
      simp only [CommRingCat.hom_comp, RingHom.comp_apply]
      exact (AlgHom.commutes σ₁ a).trans (AlgHom.commutes σ₂ a).symm

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₂ ⋯
⊢ (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁ =
    (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (ConcreteCategory.hom (↾⇑(F.map fi))) xi = (ConcreteCategory.hom (↾⇑(F.map fj))) xj
⊢ (ConcreteCategory.hom ((G ⋙ forget).map fi)) ((s.app i) xi) =
    (ConcreteCategory.hom ((G ⋙ forget).map fj)) ((s.app j) xj)

Tactic:
by
      simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      dsimp at heq
      rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]
      simp

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

Goal state before:
pp: R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
x : PrimeSpectrum R
j : Fin n
⊢ zeroLocus {g.val i} ⊆ zeroLocus {g.val j}

Tactic:
by_cases hij : i = j

Goal state after:
case pos
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
x : PrimeSpectrum R
j : Fin n
hij : i = j
⊢ zeroLocus {g.val i} ⊆ zeroLocus {g.val j}

case neg
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
x : PrimeSpectrum R
j : Fin n
hij : ¬i = j
⊢ zeroLocus {g.val i} ⊆ zeroLocus {g.val j}
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : TopologicalSpace S
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
hfc : ∀ (i : ι), Continuous (f i)
h : ∀ (i : ι), IsOpenMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ i, x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

Tactic:
refine (isOpenMap_sigma.mpr h).exists_opens_image_eq_of_prespectralSpace
      (continuous_sigma_iff.mpr hfc) (fun x hx ↦ ?_) hU hc

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : TopologicalSpace S
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
hfc : ∀ (i : ι), Continuous (f i)
h : ∀ (i : ι), IsOpenMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ i, x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
x : S
hx : x ∈ U
⊢ x ∈ Set.range fun p ↦ f p.fst p.snd
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.fst (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.snd π (𝒰.f i) ≫ u i =
    (pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))).inv ≫
      pullback.snd (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j

Tactic:
← hfac i,

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.fst (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f i) ≫ f =
    (pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))).inv ≫
      pullback.snd (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit (16 * W.Δ) ↔ IsUnit W.Δ

Tactic:
IsUnit.mul_iff,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit 16 ∧ IsUnit W.Δ ↔ IsUnit W.Δ
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k D (n + 1) = numBound k D n * degBound k D n * D n

Tactic:
by
  rw [numBound]

Goal state after: