mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R := ⋯
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
⊢ Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i)))) ≤
    RingHom.ker f

Tactic:
· simp only [Ideal.span_le, Set.range_subset_iff, SetLike.mem_coe, RingHom.mem_ker, map_sub,
      eval₂Hom_C, RingHom.coe_coe, eval₂Hom_map_hom, coe_eval₂Hom, sub_eq_zero, f]
    simp only [← algebraMap_eq, AlgHom.comp_algebraMap_of_tower, ← aeval_def]
    intro i
    generalize universalFactorizationMap R n m k hn (X i) = p
    change AlgHom.id R _ p = ((aeval _).comp (tensorEquivSum R _ _ R).toAlgHom) p
    congr 1
    ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H✝ : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
trans ((homEquiv Q.ResidueField m k hn p) (φi.comp φ)).1.2
    · simp [homEquiv_comp_snd, φ, φi]
    · rw [H]
      simp [homEquiv, UniversalFactorizationRing.homEquiv, factor₂,
        MonicDegreeEq.map, Polynomial.map_map]
      rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
x : I.Cotangent
⊢ ((AlgebraTensorModule.curry (f ∘ₗ tensorCotangentHom R T I)) 1) x =
    ((AlgebraTensorModule.curry (hₐ.toLinearMap ∘ₗ g)) 1) x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
x : ↥I
⊢ ((AlgebraTensorModule.curry (f ∘ₗ tensorCotangentHom R T I)) 1) (I.toCotangent x) =
    ((AlgebraTensorModule.curry (hₐ.toLinearMap ∘ₗ g)) 1) (I.toCotangent x)
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 (F.mapId x)

Tactic:
rw [mapId_eq_eqToHom]
  infer_instance

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

Goal state before:
pp: case h₁
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ ((pullbackSpecIso ↑R ↑A ↑A).inv ≫ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom) ≫
      pullback.snd (Spec A ↘ Spec R) (Spec A ↘ Spec R) =
    (Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv) ≫
      pullback.snd (Spec A ↘ Spec R) (Spec A ↘ Spec R)

Tactic:
simp [AlgHom.toUnder, specOverSpec, over, OverClass.hom, h₂]

Goal state after:
case h₁
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) =
    Spec.map (CommRingCat.ofHom ↑↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ∀ (m : ℕ), ↑m ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
intro n

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
⊢ ↑n ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
⊢ (conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂')) (l₁ ◁ φ) = (conjugateEquiv adj₂ adj₂') φ ▷ r₁

Tactic:
have := mateEquiv_hcomp adj₁ adj₁ adj₂ adj₂' ((λ_ _).hom ≫ (ρ_ _).inv)
    ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv)

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
this :
  (mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂'))
      (leftAdjointSquare.hcomp ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv)) =
    rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₁) ((λ_ l₁).hom ≫ (ρ_ l₁).inv))
      ((mateEquiv adj₂ adj₂') ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv))
⊢ (conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂')) (l₁ ◁ φ) = (conjugateEquiv adj₂ adj₂') φ ▷ r₁
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case mpr
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u
⊢ f ∉ z.asHomogeneousIdeal

Tactic:
obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
        exact fun rid => hz (z.1.2 i rid)

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 ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
h :
  HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
i : ℕ
hi : ¬i = n
⊢ (HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }).val =
    HomogeneousLocalization.val 0

Tactic:
simp only [proj_apply, decompose_of_mem_ne _ hn (Ne.symm hi), zero_pow hm.ne',
      HomogeneousLocalization.val_mk, Localization.mk_zero, HomogeneousLocalization.val_zero]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : DecidableEq ι
𝒜 : ι → σ
inst✝⁶ : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : SetLike τ B
inst✝³ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝² : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
⊢ val ((localRingHom f I J hIJ) x) = (Localization.localRingHom I J (↑f) hIJ) (val x)

Tactic:
obtain ⟨⟨i, x, s, hs⟩, rfl⟩ := x.mk_surjective
  simp [localRingHom, map_mk]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case w.refine_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
⊢ (f * g) ^ j ∈ 𝒜 (n + j • e)

Tactic:
mul_pow

Goal state after:
case w.refine_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
⊢ f ^ j * g ^ j ∈ 𝒜 (n + j • e)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Function.Surjective ⇑(TopCat.Hom.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯).inv.base)

Tactic:
exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ X ⟶ Proj 𝒜

Tactic:
refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).glueMorphisms
    (fun ri ↦ toBasicOpenOfGlobalSections 𝒜 f rfl ri.2.2.1 ri.2.2.2 ≫ Scheme.Opens.ι _) ?_
  rintro x y
  let e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x)
      ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅ (X.basicOpen (f (x.snd.fst * y.snd.fst))) :=
    (isPullback_opens_inf _ _).isoPullback.symm ≪≫ X.isoOfEq (by simp)
  rw [← cancel_epi e.inv]
  trans toBasicOpenOfGlobalSections 𝒜 f rfl (Nat.add_pos_left x.2.2.1 y.1)
    (SetLike.mul_mem_graded x.2.2.2 y.2.2.2) ≫ (Scheme.Opens.ι _)
  · simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
      homOfLE_toBasicOpenOfGlobalSections_ι _ _ rfl rfl y.2.2.2
  · simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
      (homOfLE_toBasicOpenOfGlobalSections_ι _ _ (mul_comm _ _) (add_comm _ _) x.2.2.2).symm

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Goal state before:
pp: case add
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b x✝ y✝ : B
hx✝ : x✝ ∈ Submodule.span B (⇑f '' ↑I.toIdeal)
hy✝ : y✝ ∈ Submodule.span B (⇑f '' ↑I.toIdeal)
a✝¹ : ∀ (i : ι), ↑(((DirectSum.decompose ℬ) x✝) i) ∈ Ideal.map f I.toIdeal
a✝ : ∀ (i : ι), ↑(((DirectSum.decompose ℬ) y✝) i) ∈ Ideal.map f I.toIdeal
i : ι
⊢ ↑(((DirectSum.decompose ℬ) (x✝ + y✝)) i) ∈ Ideal.map f I.toIdeal

Tactic:
simp [*, Ideal.add_mem]

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

Goal state before:
pp: case refine_1
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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
⊢ 0 • x ∈ carrier f_deg q

Tactic:
rw [zero_smul]

Goal state after:
case refine_1
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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
⊢ 0 ∈ carrier f_deg q
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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk ((a * ↑(((decompose 𝒜) x) (i - n))) ^ m) ⟨f ^ i, ⋯⟩ =
    Localization.mk (a ^ m) ⟨f ^ n, ⋯⟩ * Localization.mk (↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ (i - n), ⋯⟩

Tactic:
mul_pow

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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk (a ^ m * ↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ i, ⋯⟩ =
    Localization.mk (a ^ m) ⟨f ^ n, ⋯⟩ * Localization.mk (↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ (i - n), ⋯⟩
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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ ny →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) y ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
intro n

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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
⊢ n ≠ ny →
    HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal
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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ nx →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) x ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
intro n

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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
⊢ n ≠ nx →
    HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal
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
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    HomogeneousLocalization.mk z ∈ x.asIdeal

Tactic:
← FromSpec.num_mem_carrier_iff f_deg hm x

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
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    ↑z.num ∈ FromSpec.carrier f_deg x
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
⊢ ∀ {f' : X' ⟶ X} {g' : X' ⟶ Y'}, IsPullback f' g' f Y'_to_Y → Existence f → Existence g'

Tactic:
X'_to_X

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
⊢ ∀ {g' : X' ⟶ Y'}, IsPullback X'_to_X g' f Y'_to_Y → Existence f → Existence g'
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
⊢ (Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver) ≤ (Sieve.overEquiv X) R ↔
    Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X) R

Tactic:
rw [overEquiv_generate_toPresieveOver_eq_ofArrows]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
s : Cone F
m : s.pt ⟶ (liftedCone F).pt
h : ∀ (j : I), m ≫ (liftedCone F).π.app j = s.π.app j
i : I
⊢ ↑m ≫ limit.π (F ⋙ π A) i = ↑⟨limit.lift (F ⋙ π A) ((π A).mapCone s), ⋯⟩ ≫ limit.π (F ⋙ π A) i

Tactic:
by simpa using congrArg Subtype.val (h i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
⊢ ⊤ = ⨆ i, PrimeSpectrum.basicOpen (a i.fst i.snd)

Tactic:
rw [IsOpenCover] at hs

Goal state after:
case refine_1
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : ⨆ i, U ↑i = ⊤
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
⊢ ⊤ = ⨆ i, PrimeSpectrum.basicOpen (a i.fst i.snd)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
⊢ data.sieve f ∈ J₀ X₀

Tactic:
by
  have := IsDenseSubsite.isCoverDense J₀ J F
  have := IsDenseSubsite.isLocallyFull J₀ J F
  rw [← functorPushforward_mem_iff J₀ J F]
  let R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W := fun W p hp ↦
      Sieve.bind (Sieve.coverByImage F W).arrows (fun U π hπ ↦
        Sieve.pullback hπ.some.lift
          (Sieve.functorPushforward F (F.imageSieve (hπ.some.map ≫ p))))
  refine J.superset_covering ?_
    (J.bind_covering (J.pullback_stable f (data.toOneHypercover.mem₀)) (R := R)
    (fun W p hp ↦ J.bind_covering (F.is_cover_of_isCoverDense J W) ?_))
  · rintro W' _ ⟨W, _, p, hp, ⟨Y₀, a, b, hb, ⟨U, c, d, ⟨x₁, w₁⟩, fac⟩, rfl⟩, rfl⟩
    have hp' := Sieve.ofArrows.fac hp
    dsimp at hp'
    refine ⟨U, x₁, d, ⟨Sieve.ofArrows.i hp,
      F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp, ?_⟩, ?_⟩
    · rw [w₁, assoc, assoc, assoc, assoc, hp']
    · rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_assoc]
  · intro U π hπ
    apply J.pullback_stable
    apply functorPushforward_imageSieve_mem

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝³ : Category.{v₀, u₀} C₀
inst✝² : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows (F.map d ≫ F.map b ≫ (data a.Y).f i ≫ a.f)

Tactic:
simpa only [assoc] using S.1.downward_closed a.hf (F.map d ≫ F.map b ≫ (data a.Y).f i)

Goal state after: