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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i j : Fin (m + k)
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map i))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation j) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑j - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑j - ↑j₁)
          else 0)
        ((finCongr ⋯) i)

Tactic:
obtain ⟨i | i, rfl⟩ := finSumFinEquiv.surjective i

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
j : Fin (m + k)
i : Fin m
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inl i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation j) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑j - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑j - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inl i)))

case inr
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
j : Fin (m + k)
i : Fin k
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation j) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑j - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑j - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inr i)))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : f.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
· obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hf0; simp

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsCoprime ↑(factor₁ m k hn p) ↑(factor₂ m k hn p)

Tactic:
← Polynomial.isUnit_resultant_iff_isCoprime (factor₁ m k hn p).monic,

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit ((↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p))
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c₀ : ↥(G ⊗ G).left
hc₃ : c₀ ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c₀ ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c₀ ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
⊢ False

Tactic:
obtain ⟨⟨c, hc⟩, e⟩ := (pointEquivClosedPoint (G ⊗ G).hom).surjective ⟨c₀, hc₃⟩

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c₀ : ↥(G ⊗ G).left
hc₃ : c₀ ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c₀ ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c₀ ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c₀, hc₃⟩
⊢ False
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
⊢ fTn ((toNormalization (pullback.snd f fT)) ↑v) = (toNormalization f) x

Tactic:
by simp only [← hv₂, ← Scheme.Hom.comp_apply]; simp [fTn]

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

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
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Smooth R S

Tactic:
refine ⟨?_, .of_finitePresentation_tensorProduct_of_faithfullyFlat T⟩

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
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ FormallySmooth R S
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
f : S →ₐ[R] T
⊢ Spec.map (CommRingCat.ofHom f.toRingHom) ≫ Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R) =
    Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)

Tactic:
by simp [specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp]

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

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

Tactic:
subst hx

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ Module.length R (R ⧸ Ideal.span {0}) = ⊤
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x ≠ 1
⊢ ord (f * g) x = ord f x + ord g x

pp: case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x = 1
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
· simp [hx]

Goal state after:
case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x = 1
⊢ ord (f * g) x = ord f x + ord g x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x ≠ 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x = 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

Tactic:
· simp [hx]

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x = 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x ≠ 1
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x = 1
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
· simp [hx]

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x = 1
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x ≠ 1
⊢ ord f x ≤ ord (a • f) x

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
⊢ ord f x ≤ ord (a • f) x

Tactic:
· simp [hx]

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
⊢ ord f x ≤ ord (a • f) x
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₃) β = (conjugateEquiv adj₁ adj₃) (β ≫ α)

Tactic:
simp only [conjugateEquiv_apply]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ ((ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom =
    (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫ (λ_ r₃).hom
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 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i ↦ Classical.choose ⋯
H : ⋂ i, zeroLocus 𝒜 (f i) ∈ Set.range (zeroLocus 𝒜)
i : ↑Zs
⊢ ↑i = zeroLocus 𝒜 (f i)

Tactic:
exact (Classical.choose_spec (h i.2)).symm

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a + b) (i x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩
  rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, hwb, wb⟩
  refine
    ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
      ⟨sb * ra + sa * rb,
        add_mem (add_comm jb ja ▸ mul_mem_graded sb_mem ra_mem : sb * ra ∈ 𝒜 (ja + jb))
          (mul_mem_graded sa_mem rb_mem)⟩,
      ⟨sa * sb, mul_mem_graded sa_mem sb_mem⟩, fun y ↦
        y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩
  rintro ⟨y, hy⟩
  simp only [Subtype.forall, Opens.apply_mk] at wa wb
  simp [wa y hy.1, wb y hy.2, ext_iff_val, add_mk, add_comm (sa * rb)]

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal

Tactic:
exact f.den_mem

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

Goal state before:
pp: X : Scheme
M N : X.Modules
φ : M ⟶ N
⊢ IsIso φ ↔ ∀ (U : X.Opens), IsIso (app φ U)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (toPresheaf X), NatTrans.isIso_iff_isIso_app]
  simp [Opposite.op_surjective.forall]

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

Goal state before:
pp: X : Scheme
M N : X.Modules
φ : M ⟶ N
U : X.Opens
inst✝ : IsIso φ
⊢ Hom.app (inv φ) U = inv (Hom.app φ U)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Goal state after:
X : Scheme
M N : X.Modules
φ : M ⟶ N
U : X.Opens
inst✝ : IsIso φ
⊢ Hom.app φ U ≫ Hom.app (inv φ) U = 𝟙 Γ(M, U)
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ -Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = -Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩

Tactic:
exact congr_arg Neg.neg h

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

Goal state before:
pp: case refine_1
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U✝ V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : Y.Opensᵒᵖ
x : ↑(((𝟭 Y.Opens).op ⋙ Y.ringCatSheaf.obj).obj U)
⊢ (RingCat.Hom.hom ((Functor.whiskerRight (NatTrans.op ⋯.adjunction.counit) Y.ringCatSheaf.obj).app U)) x =
    (RingCat.Hom.hom
        (((Hom.toRingCatSheafHom f).hom ≫
              (Opens.map f.base).op.whiskerLeft
                {
                    hom :=
                      Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                        (forget₂ CommRingCat RingCat) }.hom).app
          U))
      x

Tactic:
exact congr($((f.app_appIso_inv _).symm).hom x)

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ Localization.mk (↑a • g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
subst hx

Goal state after:
ι : 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 𝒜
f g : A
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away (f * g))) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ Localization.mk (↑a • g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨(f * g) ^ i, ⋯⟩
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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ val ((awayMap 𝒜 hg hx) a) = (awayMapAux 𝒜 ⋯) a

Tactic:
let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
    (h := (val_injective _).hasLeftInverse.choose_spec)
  dsimp [awayMap]
  convert_to! (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
    range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _
  rw [e.apply_symm_apply]

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

Goal state before:
pp: case exists_of_eq.succ
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))

Tactic:
subst hx

Goal state after:
case exists_of_eq.succ
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := (awayMap 𝒜 hg ⋯).toAlgebra
hc :
  ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ m * (a * g ^ n)) =
    ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ n * (b * g ^ m))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos
ι : 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
apply Submodule.subset_span

Goal state after:
case pos
ι : 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := ⋯
⊢ ModuleCat.Hom.hom
        (((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj).map
            i ≫
          ModuleCat.ofHom
            (IsLocalizedModule.lift (Submonoid.powers (unop g))
              (ModuleCat.Hom.hom
                (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
              (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯)) ∘ₗ
      ModuleCat.Hom.hom
        (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))) =
    ModuleCat.Hom.hom
        (ModuleCat.ofHom
            (IsLocalizedModule.lift (Submonoid.powers (unop f))
              (ModuleCat.Hom.hom
                (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
              (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) ≫
          ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).map i) ∘ₗ
      ModuleCat.Hom.hom
        (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f)))

Tactic:
· dsimp [← ModuleCat.hom_comp]
          rw [tilde.toOpen_res_assoc]
          ext x
          dsimp
          simp only [IsLocalizedModule.lift_apply, ← ModuleCat.comp_apply, ← Functor.map_comp]
          rfl

Goal state after: