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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)

Tactic:
by
  let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra
  have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
  exact IsOpenImmersion.of_isLocalization (Ideal.Quotient.mk _ f)

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
⊢ I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f ≤ Hom.opensRange (I.glueDataObjMap ⋯)

Tactic:
rw [opensRange_glueDataObjMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ ↔ ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd

Tactic:
constructor
  · rintro rfl; simp
  · obtain ⟨x₁, ⟨f₁, h₁⟩⟩ := f₁
    obtain ⟨x₂, ⟨f₂, h₂⟩⟩ := f₂
    rintro ⟨rfl : x₁ = x₂, e : f₁ = _⟩
    simp [e]

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

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
convert! hU.basicOpen (X.presheaf.map (homOfLE le_top).op r)

Goal state after:
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
· rw [← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_snd_ι, limit.lift_π_assoc, cospan_left, glueDataT'Aux_fst_assoc,
          glueDataT_fst_assoc, Scheme.homOfLE_ι, Category.id_comp]
        rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison forget f g))

Tactic:
refine .of_comp_left (fun x ↦ ?_) <|
    injective_of_mono (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
⊢ ∃ a,
    (⇑(ConcreteCategory.hom (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) ∘
          ⇑(ConcreteCategory.hom (pullbackComparison forget f g)))
        a =
      x
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine Z
h : IsPullback fst snd f g
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)

Tactic:
have : IsAffine P := .of_isPullback h
  have : IsPullback (AffineScheme.ofHom fst) (AffineScheme.ofHom snd) (AffineScheme.ofHom f)
      (AffineScheme.ofHom g) :=
    IsPullback.of_map_of_faithful AffineScheme.forgetToScheme.{u} h
  exact (IsPullback.map AffineScheme.Γ.rightOp this).unop.flip

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ ⇑fst ⁻¹' s ⊆ ⇑(fst ≫ f) ⁻¹' ⇑f '' s

Tactic:
rw [Hom.comp_base, TopCat.coe_comp, ← Set.image_subset_iff, Set.image_comp]

Goal state after:
case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ ⇑f '' ⇑fst '' ⇑fst ⁻¹' s ⊆ ⇑f '' s
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion I.gluedTo

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsPreimmersion)
    _ (iSup_affineOpens_eq_top X)]
  intro U
  rw [← MorphismProperty.cancel_left_of_respectsIso @IsPreimmersion (I.glueDataObjIso U).hom,
    glueDataObjIso_hom_restrict]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
x✝² x✝¹ : (Over Y)ᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x✝ ≫
        (Over.homMk (Hom.toImage (Opposite.unop x✝¹).hom) ⋯).op).unop =
    ((Over.homMk (Hom.toImage (Opposite.unop x✝²).hom) ⋯).op ≫ (𝟭 (Over Y)ᵒᵖ).map x✝).unop

Tactic:
ext1; simp [← cancel_mono (subschemeι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ ((subschemeFunctor Y).rightOp.map ({ app := fun I ↦ eqToHom ⋯, naturality := ⋯ }.app I) ≫
        { app := fun f ↦ (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯).op, naturality := ⋯ }.app
          ((subschemeFunctor Y).rightOp.obj I)).unop =
    (𝟙 ((subschemeFunctor Y).rightOp.obj I)).unop

Tactic:
ext1; simp [← cancel_mono (subschemeι _)]

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) W))

Tactic:
let e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
    Scheme.coprodPresheafObjIso _ ≪≫ Limits.prod.mapIso
      (U.presheaf.mapIso (eqToIso (by simp [← Scheme.Hom.comp_preimage])).op)
      (V.presheaf.mapIso (eqToIso (by simp [← Scheme.Hom.comp_preimage])).op)

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) W))
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

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

Tactic:
← iUnion_range_comap_comp_evalRingHom,

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))))) =
    s.toSet
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ IsIso f

Tactic:
by
  rw [IsClosedImmersion.isIso_iff_ker_eq_bot, ← Scheme.IdealSheafData.support_eq_top_iff,
    ← SetLike.coe_injective.eq_iff, Scheme.Hom.support_ker]
  simp

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

Goal state before:
pp: 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
⊢ IsConstructible (comap f '' s)

Tactic:
by
  refine hf.polynomial_induction
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ ↦ isConstructible_comap_C) ?_ ?_ f s hs
  · intro R _ S _ f hf hf' s hs
    refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_
    rw [range_comap_of_surjective _ f hf]
    exact isRetrocompact_zeroLocus_compl_of_fg hf'
  · intro R _ S _ T _ f g H₁ H₂ s hs
    simp only [comap_comp, Set.image_comp]
    exact H₁ _ (H₂ _ hs)

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

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

Tactic:
refine this _ ?_ ⟨_, rfl⟩

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

Goal state before:
pp: case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) f

Tactic:
← cancel_left_of_respectsIso (P := topologically _) X.isoSpec.inv

Goal state after:
case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)
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.IsQuotientMap ⇑f

Tactic:
rw [Topology.isQuotientMap_iff]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
⊢ Topology.IsCoinducing ⇑f ∧ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ((CommRingCat.Hom.hom
              (Scheme.Hom.app
                (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                  (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
                ⊤)).comp
          (CommRingCat.Hom.hom
            (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))))).comp
      C =
    CommRingCat.Hom.hom (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv)

Tactic:
RingHom.comp_assoc,

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.app
            (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
            ⊤)).comp
      ((CommRingCat.Hom.hom
            (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))).comp
        C) =
    CommRingCat.Hom.hom (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
⊢ topologically (@IsOpenMap) (Spec.map (CommRingCat.ofHom C))

Tactic:
exact MvPolynomial.isOpenMap_comap_C

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
h : IsReduced S
this✝ : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
i : (Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).I₀
this : IsReduced 𝔸(n; S.affineCover.X i)
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).X i)

Tactic:
exact isReduced_of_isOpenImmersion ((isPullback_map _).isoPullback.inv)

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

Goal state before:
pp: case e'_3.f.a
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 := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
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) := ⋯
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) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (Localization.Away c)
hxT₁ : x ∈ ↑T₁
⊢ { f := c * f₁ x.f, n := x.n, g := g₁ x }.toSet ∈ 𝒫 Set.range (comap q₁.toRingHom)

Tactic:
dsimp only [q₁, AlgHom.toRingHom_eq_coe]
          rw [IsScalarTower.coe_toAlgHom,
            localization_away_comap_range (S := Localization.Away c) (r := c),
            BasicConstructibleSetData.toSet, sdiff_eq, ← basicOpen_eq_zeroLocus_compl,
            basicOpen_mul]
          exact Set.inter_subset_right.trans Set.inter_subset_left

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ

Tactic:
rw [← PrimeSpectrum.zeroLocus_singleton_zero]

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ ∀ (a b : X.PartialMap Y), a ≈ b → a.fromFunctionField = b.fromFunctionField

Tactic:
intro f

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f : X.PartialMap Y
⊢ ∀ (b : X.PartialMap Y), f ≈ b → f.fromFunctionField = b.fromFunctionField
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).hom = (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
simp_rw [comp_hom, Hom.toPartialMap_hom, Hom.toPartialMap_domain, morphismRestrict_comp,
      morphismRestrict_id, ← X.topIso_hom, Hom.comp_preimage, Hom.id_preimage,
      Category.comp_id, ← X.topIso.hom.isoImage_preimage_hom_homOfLE, Category.assoc,
      Iso.inv_hom_id_assoc]

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

Goal state before:
pp: case a
⊢ diagonal @Surjective ≤ @UniversallyInjective

Tactic:
rw [← universally_eq_iff.mpr (inferInstance : IsStableUnderBaseChange (diagonal @Surjective)),
      universallyInjective_eq]
    apply universally_mono
    intro X Y f hf x₁ x₂ e
    obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e
    obtain ⟨t, rfl⟩ := hf.1 t
    rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.61} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
x : ↥(pullback ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f j))
⊢ ∃ k hki hkj y,
    (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)
        y =
      x

Tactic:
by
    dsimp at i j x ⊢
    let iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
        pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
      pullbackRightPullbackFstIso _ _ _ ≪≫ pullback.congrHom pullback.condition rfl ≪≫
        pullbackAssoc ..
    have (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) :
        (pullback.lift
          (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) (by simp) (by simp))
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) (by simp) (by simp))
            (by simp)) =
          pullback.map _ _ _ _ (𝟙 Y) (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) (by simp)) (𝟙 X)
            (by simp) (by simp) ≫ iso.inv := by
      apply pullback.hom_ext <;> apply pullback.hom_ext <;> simp [iso]
    obtain ⟨k, hki, hkj, yk, hyk⟩ := 𝒰.exists_lift_trans_eq ((iso.hom ≫ pullback.snd _ _) x)
    refine ⟨k, hki, hkj, show x ∈ Set.range _ from ?_⟩
    rw [this, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Pullback.range_map]
    use iso.hom x
    simp only [Hom.id_base, TopCat.hom_id, ContinuousMap.coe_id, Set.range_id, Set.preimage_univ,
      Set.univ_inter, Set.mem_preimage, Set.mem_range, hom_inv_apply, and_true]
    exact ⟨yk, hyk⟩

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

Goal state before:
pp: S : Scheme
X : Over S
𝒰 : X.left.OpenCover
inst✝¹ : Category.{v_2, u_1} 𝒰.I₀
inst✝ : Cover.LocallyDirected 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
i : 𝒰.I₀
⊢ 𝒰.f i ≫ Over.Hom.left (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w) = g i

Tactic:
by
  simp [glueMorphismsOverOfLocallyDirected]

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

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

Tactic:
subst hij; rfl

Goal state after: