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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
⊢ QuasiFiniteAt f x

Tactic:
obtain ⟨U, r, hU, hr, hxV, hrV⟩ :
      ∃ (U : Y.Opens) (r : Γ(f.normalization, f.fromNormalization ⁻¹ᵁ U)),
      IsAffineOpen U ∧ IsAffineOpen (f.toNormalization ⁻¹ᵁ f.normalization.basicOpen r) ∧
      x ∈ f.toNormalization ⁻¹ᵁ f.normalization.basicOpen r ∧ Scheme.basicOpen _ r ≤ V y := by
    obtain ⟨_, ⟨W, hW, rfl⟩, hxW, hWV : W ≤ _⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
      hxVy (f.toNormalization ⁻¹ᵁ V y).isOpen
    have : IsAffine W := hW
    let V' := (X.homOfLE hWV ≫ f.toNormalization ∣_ V y ≫ (V y).ι).opensRange
    have hV' : IsAffineOpen V' := isAffineOpen_opensRange _
    have hV'V : V' ≤ V y := by
      simp_rw [V', ← Category.assoc, opensRange_comp]
      exact (image_le_opensRange _ _).trans (by simp)
    have hV'W : f.toNormalization ⁻¹ᵁ V' = W := by
      have : (f.toNormalization ⁻¹ᵁ V y).ι ⁻¹ᵁ f.toNormalization ⁻¹ᵁ V' =
          (f.toNormalization ⁻¹ᵁ V y).ι ⁻¹ᵁ W := by
        rw [← Scheme.Hom.comp_preimage, ← morphismRestrict_ι]
        simp only [V', opensRange_comp, Scheme.Hom.preimage_image_eq, opensRange_homOfLE]
      simpa only [image_preimage_eq_opensRange_inf, Opens.opensRange_ι, ← preimage_inf,
        inf_eq_right.mpr, hV'V, hWV] using congr((f.toNormalization ⁻¹ᵁ V y).ι ''ᵁ $this)
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (f x)) isOpen_univ
    obtain ⟨f₁, f₂, e, hxf⟩ := exists_basicOpen_le_affine_inter (hU.preimage f.fromNormalization)
      hV' (f.toNormalization x) ⟨by simpa [← Scheme.Hom.comp_apply], hV'W.ge hxW⟩
    refine ⟨U, f₁, hU, ?_, hxf, (e.trans_le (f.normalization.basicOpen_le _)).trans hV'V⟩
    rw [e, preimage_basicOpen]
    exact IsAffineOpen.basicOpen (hV'W ▸ hW) _

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
⊢ QuasiFiniteAt f x
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
⊢ IsProper (pullback.snd G.hom f)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this : IsProper G'.hom
⊢ IsIntegral (pullback (pullback.snd G.hom f) (pullback.snd G.hom f))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
this : IsIso (Scheme.Hom.toNormalization f)
⊢ IsIntegralHom (Scheme.Hom.toNormalization f ≫ Scheme.Hom.fromNormalization f)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (f ≫ g)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case id
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
i : WalkingSpan
⊢ IsOpenImmersion (𝟙 ((span f g).obj i)).left

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

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

Goal state before:
pp: R : CommRingCat
⊢ PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (Over.post Γ.rightOp ⋙
      Over.map (ΓSpecIso R).inv.op ⋙ (Over.opEquivOpUnder R).functor ⋙ (commAlgCatEquivUnder R).inverse.op)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_2
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝¹ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨P', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = P'
⊢ ∀ (i : Fin n), (Q' i).IsPrime

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_3
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝¹ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨P', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = P'
⊢ ∀ (i : Fin n), (Q' i).LiesOver Q

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H :
  ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
x : X
hxV : x ∈ V.left
W : Opens ↥U
f : W ⟶ U.overEquivalence.functor.obj V
hW : S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V)
hxW : ⟨x, ⋯⟩ ∈ W
⊢ ∃ U_1 f, ((Sieve.overEquiv V) S).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨_, ((U.overEquivalence.symm.toAdjunction.homEquiv _ _ ).symm f).left,
        ⟨_, _, 𝟙 _, hW, rfl⟩, _, hxW, rfl⟩

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this✝ : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
this : IsOpenImmersion f'
⊢ IsOpenImmersion (f' ≫ U.ι)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Flat R S
inst✝¹ : Module.Finite R S
h : Function.Surjective (comap (algebraMap R S))
p : Ideal R
inst✝ : p.IsMaximal
Q : Ideal S
isPrime✝ : Q.IsPrime
hQ : comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime✝ } = { asIdeal := p, isPrime := ⋯ }
this✝¹ : Q.LiesOver p
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver p Q
this : Nontrivial (Localization.AtPrime p ⊗[R] S)
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)

Tactic:
infer_instance

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
this : IsIso φ
⊢ IsIso (Spec.map φ)

Tactic:
infer_instance

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

Goal state before:
pp: case inr.hg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Smooth (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))

Tactic:
infer_instance

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

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x✝ : ∀ (y : ↥(Spec R)), Smooth (pullback.snd f ((Spec R).fromSpecResidueField y))
y : ↥(Spec R)
⊢ Smooth
    ((pullbackRightPullbackFstIso f ((Spec R).fromSpecResidueField y) (X.affineCover.f i)).inv ≫
      pullback.snd (X.affineCover.f i) (pullback.fst f ((Spec R).fromSpecResidueField y)) ≫
        pullback.snd f ((Spec R).fromSpecResidueField y))

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource (@Flat ⊓ MorphismProperty.diagonal @Flat)

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@Flat ⊓ MorphismProperty.diagonal @Flat)

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : WeaklyEtale f
⊢ WeaklyEtale (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim R + ↑(Nat.card β✝) ≤ ringKrullDim (MvPolynomial β✝ R)

Tactic:
| of_equiv e H =>

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case h_empty
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
⊢ ringKrullDim R + ↑(Nat.card PEmpty.{u_3 + 1}) ≤ ringKrullDim (MvPolynomial PEmpty.{u_3 + 1} R)

Tactic:
| h_empty =>

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : b • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {a * b}) = Module.length R (R ⧸ span {b * a})

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : b • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {b * a}) = Module.length R (R ⧸ span {b * a})
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ ord R a ≤ ord R (a * b)

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
⊢ ord R a ≤ ord R (b * a)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
this : Module.length R (R ⧸ Ideal.span {0}) ≠ ⊤
⊢ False

Tactic:
Module.length_ne_top_iff,

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
this : IsFiniteLength R (R ⧸ Ideal.span {0})
⊢ False
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).topIso.hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this✝ : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot ↑(CommRingCat.of ((i : ι) → ↑(R i)))).toCommRingCatIso.inv)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
j₀ : 𝒰.I₀
i : { i // j i = j₀ }
⊢ Set.range ⇑(f ↑i) ⊆ Set.range ⇑(𝒰.f j₀)

Tactic:
rcases i with ⟨i, rfl⟩

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
i : ι
⊢ Set.range ⇑(f ↑⟨i, ⋯⟩) ⊆ Set.range ⇑(𝒰.f (j i))
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
x✝ : (j₀ : 𝒰.I₀) → ↑(R' j₀)
j₀ : 𝒰.I₀
i : { i // j i = j₀ }
⊢ (fun f x i ↦ f ↑i) ((fun f i ↦ f (j i) ⟨i, ⋯⟩) x✝) j₀ i = x✝ j₀ i

Tactic:
rcases i with ⟨i, rfl⟩

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
x✝ : (j₀ : 𝒰.I₀) → ↑(R' j₀)
i : ι
⊢ (fun f x i ↦ f ↑i) ((fun f i ↦ f (j i) ⟨i, ⋯⟩) x✝) (j i) ⟨i, ⋯⟩ = x✝ (j i) ⟨i, ⋯⟩
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ ↑(basicOpen 𝒜 (f * g)) = ↑(basicOpen 𝒜 f ⊓ basicOpen 𝒜 g)

Tactic:
by simp [zeroLocus_singleton_mul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case hI
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑x).asHomogeneousIdeal.toIdeal.IsPrime

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg✝ f_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
mul_comm

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg✝ f_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
mul_comm

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯ ≫ (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
by
  rw [← germ_restrictStalkNatIso_hom_app f x M hxU, Category.assoc, ← NatTrans.comp_app,
    Iso.hom_inv_id]
  simp

Goal state after: