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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
⊢ ⋃ i,
      Set.range
        (comap
          ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
                i).comp
            (algebraMap R
              ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    ⋃ C ∈ ↑s, C.toSet

Tactic:
Set.biUnion_eq_iUnion

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
⊢ ⋃ i,
      Set.range
        (comap
          ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
                i).comp
            (algebraMap R
              ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    ⋃ x, (↑x).toSet
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: R S : CommRingCat
inst✝ : Subsingleton ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : Spec.map ψ ≫ Spec.map φ = 𝟙 (Spec S)
⊢ IsClosedImmersion (Spec.map ψ)

Tactic:
← Spec.map_comp,

Goal state after:
R S : CommRingCat
inst✝ : Subsingleton ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : Spec.map (φ ≫ ψ) = 𝟙 (Spec S)
⊢ IsClosedImmersion (Spec.map ψ)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ Subtype.val ⁻¹' ⇑f '' s =
    ⇑(isoOpensRange (Y.affineCover.f i)).inv ⁻¹'
      ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
refine .trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ Subtype.val ⁻¹' ⇑f '' s =
    ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
      ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case inr
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
    let 𝒰 := X.affineCover.finiteSubcover
    rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]
    refine .iUnion fun i ↦ ?_
    have inst : QuasiCompact (𝒰.f i ≫ f) :=
      HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
    convert! this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩
    rw [Scheme.Hom.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp,
      ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, coe_opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocallyNoetherian Y
inst✝ : LocallyOfFiniteType f
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hUV : V ≤ f ⁻¹ᵁ U
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FinitePresentation

Tactic:
let := (f.appLE U V hUV).hom.toAlgebra

Goal state after:
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocallyNoetherian Y
inst✝ : LocallyOfFiniteType f
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hUV : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FinitePresentation
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
⊢ GeometricallyIrreducible (f ≫ g)

Tactic:
GeometricallyIrreducible.iff_geometricallyIrreducible_fiber

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
⊢ ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n m : ℕ
hp : Monic 1
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) 1 = 0
hp' : ¬1 ≤ natDegree 1
⊢ ↑⟨t, ht⟩ ^ m • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
by simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]

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

Goal state before:
pp: Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f

Tactic:
apply universally_mono

Goal state after:
Z S : Scheme
⊢ @IsIntegralHom ≤ topologically @IsClosedMap
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
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
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
⊢ Polynomial.degree ∘ { val := Function.update e.val j (e.val j %ₘ e.val i) }.val ≠ (ofLex v).1

Tactic:
simp only [hv, ne_eq, not_forall, funext_iff,
            comp_apply]
          use j
          simp only [update_self]
          refine ((degree_modByMonic_lt _ hi).trans_le i_min).ne

Goal state after:
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
this : ∃ n_1 i, (e.val i).degree = ↑n_1 ∧ e.val i ≠ 0
m : ℕ := Nat.find this
i : Fin n
hi : (e.val i).degree = ↑m
hi' : e.val i ≠ 0
j : Fin n
hj : e.val j ≠ 0
⊢ m ≤ (e.val j).natDegree

Tactic:
exact Nat.find_min' _ ⟨j, degree_eq_natDegree hj, hj⟩

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

Goal state before:
pp: 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) (IsLocalRing.closedPoint K) =
    (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) (IsLocalRing.closedPoint K)

Tactic:
by simpa using H x hxS hx

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
⊢ (if w ∈ s then D w else 0) = D w

Tactic:
by_cases hw : w ∈ s

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
hw : w ∈ s
⊢ (if w ∈ s then D w else 0) = D w

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
hw : w ∉ s
⊢ (if w ∈ s then D w else 0) = D w
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
⊢ D⁺.restrict h = (D.restrict h)⁺

Tactic:
by
  ext x
  simp only [locallyFinsuppWithin.restrict_apply, locallyFinsuppWithin.posPart_apply]
  aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx : (ConcreteCategory.hom (StructureSheaf.toStalk (↑R) p)) x = 0
y : ↑R
hy : y ∈ p.asIdeal.primeCompl
hy' : ↑⟨y, hy⟩ * x = 0
n : ℕ
hn : f ^ n * x = 0
⊢ ∃ m, ↑m * x = 0

Tactic:
exact ⟨⟨_, n, rfl⟩, hn⟩

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

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
⊢ f.equiv g → g.equiv f

Tactic:
by
  intro ⟨W, hW, hWl, hWr, e⟩
  exact ⟨W, hW, hWr, hWl, e.symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
⊢ Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left (Over.Hom.left f ≫ i₂.hom)) (Z i₂.left i₂.hom)

Tactic:
exact hstab ..

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

Goal state before:
pp: case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).domain = f.domain

pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).hom = (X.isoOfEq ?e).hom ≫ f.hom

Tactic:
· simp_rw [comp_domain, Hom.toPartialMap_domain, Hom.toPartialMap_hom, Category.comp_id,
      ← X.topIso_hom, ← Hom.inv_image, ← Hom.comp_image, Iso.inv_hom_id, Hom.id_image]

Goal state after:
case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).hom = (X.isoOfEq ⋯).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
⊢ (diagonal @Surjective).universally ≤
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x).universally

Tactic:
apply universally_mono

Goal state after:
case a
⊢ diagonal @Surjective ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
x : BasicConstructibleSetData (Localization.Away c)
hx : x ∈ T₁
k : Fin x.n
⊢ span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound ≤ span R₀ (⋃ i, coeff(e.val i)) ^ e₁.powBound

Tactic:
gcongr; simpa [Set.insert_subset_iff] using ⟨_, _, hi.symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case h
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
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi : (ConcreteCategory.hom ((G ⋙ forget).map fli)) x = (s.app i) xi
hj : (ConcreteCategory.hom ((G ⋙ forget).map flj)) x = (s.app j) xj
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
⊢ ∃ x, (ConcreteCategory.hom ((F ⋙ forget).map fli)) x = xi ∧ (ConcreteCategory.hom ((F ⋙ forget).map flj)) x = xj

Tactic:
obtain ⟨z, h1, h2⟩ := Scheme.Pullback.exists_preimage_pullback xi x hi.symm

Goal state after:
case h
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
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi : (ConcreteCategory.hom ((G ⋙ forget).map fli)) x = (s.app i) xi
hj : (ConcreteCategory.hom ((G ⋙ forget).map flj)) x = (s.app j) xj
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
z : ↥(pullback (s.app i) (G.map fli))
h1 : (pullback.fst (s.app i) (G.map fli)) z = xi
h2 : (pullback.snd (s.app i) (G.map fli)) z = x
⊢ ∃ x, (ConcreteCategory.hom ((F ⋙ forget).map fli)) x = xi ∧ (ConcreteCategory.hom ((F ⋙ forget).map flj)) x = xj
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i) = Set.range ⇑(colimit.ι d.functor i)

Tactic:
ext x
  refine ⟨fun ⟨ui, h⟩ ↦ ?_, ?_⟩
  · obtain ⟨j, xj, rfl⟩ := IsLocallyDirected.ι_jointly_surjective _ x
    obtain ⟨k, fi, fj, uk, rfl, h⟩ := 𝒰.exists_of_f_eq_f ui (d.natTrans.app j xj) <| by
      simp only [h, functorOfLocallyDirected_obj, ← Scheme.Hom.comp_apply, ι_toBase]
    obtain ⟨xk, rfl, h2⟩ := exists_preimage_of_isPullback (d.equifibered fj) xj uk <| by
      apply (𝒰.f j).injective
      simp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply, ← ι_toBase, Scheme.Hom.comp_apply, ← h]
      simp [← Scheme.Hom.comp_apply]
    use d.functor.map fi xk
    simp [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
  · rintro ⟨y, rfl⟩
    use d.natTrans.app i y
    rw [← Scheme.Hom.comp_apply, ι_toBase]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: 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 : (Cover.pullbackCoverOver' S 𝒰 f).I₀
⊢ (Cover.pullbackCoverOver' S 𝒰 f).f j ≫ W ↘ S = (Cover.pullbackCoverOver' S 𝒰 f).X j ↘ S

Tactic:
by exact Over.w (pullback.snd ((𝒰.f j).asOver S) (f.asOver S))

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

Goal state before:
pp: case hab.refine_2
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) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
⊢ ⋃ i, coeff(c'.val i) ⊆ ↑(coeffSubmodule R₀ c)

Tactic:
refine Set.iUnion_subset fun k ↦ ?_
              simp only [update_apply, hi', modByMonic_one, c']
              split_ifs
              · rintro _ ⟨_, rfl⟩
                exact zero_mem _
              · exact (Set.subset_iUnion (fun i ↦ coeff(c.val i)) k).trans
                  (Set.subset_union_right.trans Submodule.subset_span)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).Δ = f W.Δ

Tactic:
by
  simp only [Δ, map_b₂, map_b₄, map_b₆, map_b₈]
  map_simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := C⁻¹.u * C.u, r := C⁻¹.r * ↑C.u ^ 2 + C.r, s := ↑C.u * C⁻¹.s + C.s,
      t := C⁻¹.t * ↑C.u ^ 3 + C⁻¹.r * C.s * ↑C.u ^ 2 + C.t } =
    1

Tactic:
one_def,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := C⁻¹.u * C.u, r := C⁻¹.r * ↑C.u ^ 2 + C.r, s := ↑C.u * C⁻¹.s + C.s,
      t := C⁻¹.t * ↑C.u ^ 3 + C⁻¹.r * C.s * ↑C.u ^ 2 + C.t } =
    { u := 1, r := 0, s := 0, t := 0 }