mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : 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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)

Tactic:
add_smul,

Goal state after:
case neg
ι : 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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + k • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)
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' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ (Localization.r (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl)
    ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩)
    (↑((fun x_1 ↦
              { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩,
                den_mem := ⋯ })
            { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
      ⟨↑((fun x_1 ↦
                { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩,
                  den_mem := ⋯ })
              { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
        ⋯⟩)

Tactic:
Localization.r_iff_exists

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ ∃ c,
    ↑c *
        (↑(↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
                ⟨↑((fun x_1 ↦
                          { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                            den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                        { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                  ⋯⟩).2 *
          ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).1) =
      ↑c *
        (↑((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).2 *
          (↑((fun x_1 ↦
                      { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                        den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).1)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ (Localization.r (Submonoid.powers x)) (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩)
    (1, 1)

Tactic:
Localization.r_iff_exists

Goal state after:
case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ ∃ c,
    ↑c * (↑(1, 1).2 * (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩).1) =
      ↑c * (↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩).2 * (1, 1).1)
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'
⊢ awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g = PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)

Tactic:
ext1

Goal state after:
σ : 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'
⊢ ↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) = ↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case surj.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 : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ (Localization.r (Submonoid.powers x)) (s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n)
    (s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩)

Tactic:
Localization.r_iff_exists

Goal state after:
case surj.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 : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ ∃ c,
    ↑c *
        (↑(s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩).2 *
          (s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n).1) =
      ↑c *
        (↑(s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n).2 *
          (s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩).1)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : 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 = ⊤
⊢ Ideal.span (Set.range fun x ↦ x.snd.fst) ≤ (HomogeneousIdeal.irrelevant 𝒜).toIdeal

pp: case a
σ : 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 = ⊤
⊢ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range fun x ↦ x.snd.fst)

Tactic:
· rw [Ideal.span_le, Set.range_subset_iff]
        rintro ⟨i, r, hi0, hri⟩
        simp [-ZeroMemClass.coe_eq_zero,
          DirectSum.decompose_of_mem_ne 𝒜 hri hi0.ne']

Goal state after:
case a
σ : 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 = ⊤
⊢ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range fun x ↦ x.snd.fst)
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 = ⊤
H : Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ TopologicalSpace.IsOpenCover fun ir ↦ X.basicOpen (f ir.snd.fst)

Tactic:
ext1

Goal state after:
σ : 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 = ⊤
H : Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ ↑(⨆ ir, X.basicOpen (f ir.snd.fst)) = ↑⊤
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ ((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.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

Tactic:
ext1

Goal state after:
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
      (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)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (fun x1 x2 ↦ x1 ⤳ x2) y (f x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯, K := ↑(X.residueField x'),
            field := X.instFieldCarrierResidueField x', algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯,
            i₁ := X.fromSpecResidueField x', i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (fun x1 x2 ↦ x1 ⤳ x2) (l (closedPoint ↥A))
    ((Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l) (closedPoint ↑(X.residueField x')))

Tactic:
exact (specializes_closedPoint _).map l.continuous

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

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ n = j * (d + e)

Tactic:
apply DirectSum.degree_eq_of_mem_mem 𝒜 hb'

Goal state after:
case hxj
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))

case hx
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ≠ 0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * d), ⋯⟩, den_mem := ⋯ }
⊢ (Localization.r (Submonoid.powers x))
    (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)), ⟨x ^ (j * (e + 1)), ⋯⟩ * ⟨x ^ (j * d), ⋯⟩)
    (a, ⟨x ^ j, ⋯⟩)

Tactic:
Localization.r_iff_exists

Goal state after:
case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * d), ⋯⟩, den_mem := ⋯ }
⊢ ∃ c,
    ↑c *
        (↑(a, ⟨x ^ j, ⋯⟩).2 *
          (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
              ⟨x ^ (j * (e + 1)), ⋯⟩ * ⟨x ^ (j * d), ⋯⟩).1) =
      ↑c *
        (↑(a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
                ⟨x ^ (j * (e + 1)), ⋯⟩ * ⟨x ^ (j * d), ⋯⟩).2 *
          (a, ⟨x ^ j, ⋯⟩).1)
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
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
⊢ (commSq.i₁ ≫ X'_to_X) ≫ f = Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ ≫ Y'_to_Y

Tactic:
simp only [Category.assoc, hP.w, reassoc_of% commSq.commSq.w]

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

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
⊢ IsClosedImmersion
    (e₂.inv ≫
      ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1) ((affineOpenCover 𝒜).openCover.f (i, j).2)
              (toSpecZero 𝒜)).inv ≫
          snd (diagonal (toSpecZero 𝒜))
            ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                  (toSpecZero 𝒜)).f
              (i, j))) ≫
        e₁.hom)

Tactic:
have : Function.Surjective F := lift_awayMapₐ_awayMapₐ_surjective 𝒜 i.2.2 j.2.2 rfl i.1.2

Goal state after:
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ IsClosedImmersion
    (e₂.inv ≫
      ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1) ((affineOpenCover 𝒜).openCover.f (i, j).2)
              (toSpecZero 𝒜)).inv ≫
          snd (diagonal (toSpecZero 𝒜))
            ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                  (toSpecZero 𝒜)).f
              (i, j))) ≫
        e₁.hom)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t) = 0

Tactic:
· rw [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp,
          ← homOfLE_comp ((basicOpen_mul_le_left f (g i))) hf, op_comp, M.presheaf.map_comp_apply]
        simp [hs]

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
X✝ : C
data✝ : F.OneHypercoverDenseData J₀ J X✝
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
⊢ F.map p ≫ F.map g ≫ f = F.map (p ≫ g) ≫ f

Tactic:
map_comp_assoc

Goal state after:
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
X✝ : C
data✝ : F.OneHypercoverDenseData J₀ J X✝
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
⊢ F.map p ≫ F.map g ≫ f = F.map p ≫ F.map g ≫ f
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst✝¹ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑((𝒰.X i).residueField y) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst✝ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑((𝒰.X i).residueField y) →ₐ[↑(S.residueField ((𝒰.f i) y))] Ω := IsSepClosed.lift
⊢ Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a

Tactic:
ext1

Goal state after:
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := ⋯
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := ⋯
algInst✝¹ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑((𝒰.X i).residueField y) := ⋯
algInst✝ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑(CommRingCat.of Ω) := ⋯
b : ↑((𝒰.X i).residueField y) →ₐ[↑(S.residueField ((𝒰.f i) y))] Ω := ⋯
⊢ CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom) = CommRingCat.Hom.hom a
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_2
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
have : IsRegularEpi (Spec.map f) :=
      isRegularEpi_of_flat_of_surjective_of_isAffine _

Goal state after:
case refine_2
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : IsRegularEpi (Spec.map f)
⊢ Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))