mathlib-initiative/mathlib-tactics huggingface dataset:
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 : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))

Tactic:
obtain ⟨k, hk : f ^ k = _⟩ := z.den_mem

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 : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: 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)) ⋯
⊢ ↑1 *
      (↑(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) =
    ↑1 *
      (↑(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)

Tactic:
simp; ring

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
⊢ Localization.mk (∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)))
      ⟨f ^ (i + i), ⋯⟩ =
    (algebraMap (A⁰_ f) (Localization.Away f)) (∑ i ∈ range (m + m + 1), g i)

Tactic:
rw [map_sum, mk_sum]

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 : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
⊢ ∑ i_1 ∈ range (m + m + 1),
      Localization.mk ((m + m).choose i_1 • ((proj 𝒜 i) a ^ i_1 * (proj 𝒜 i) b ^ (m + m - i_1))) ⟨f ^ (i + i), ⋯⟩ =
    ∑ x ∈ range (m + m + 1), (algebraMap (A⁰_ f) (Localization.Away f)) (g x)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M N : ModuleCat ↑R
f : M ⟶ N
U : Opens (PrimeSpectrum ↑R)
x : ↑M
⊢ (ModuleCat.Hom.hom (toOpen M U ≫ (modulesSpecToSheaf.map (tilde.map f)).hom.app (op U))) x =
    (ModuleCat.Hom.hom (f ≫ toOpen N U)) x

Tactic:
exact Subtype.ext (funext fun y ↦ IsLocalizedModule.map_apply y.1.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
     (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N) _ x)

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

Goal state before:
pp: case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M (basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map (tilde.map (toOpen M ⊤)) ≫ modulesSpecToSheaf.map (tilde M).fromTildeΓ).hom.app
        (op (basicOpen (unop r))) =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))

Tactic:
ObjectProperty.FullSubcategory.comp_hom

Goal state after:
case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M (basicOpen (unop r)) ≫
      ((modulesSpecToSheaf.map (tilde.map (toOpen M ⊤))).hom ≫ (modulesSpecToSheaf.map (tilde M).fromTildeΓ).hom).app
        (op (basicOpen (unop r))) =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
s : Finset ι' := {x | 0 < dv x}
i : ι'
hi : dv i > 0
⊢ i ∈ s

Tactic:
simpa [s] using hi

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

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
⊢ Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
    ⊤

Tactic:
by
  classical
  let s := Finset.univ.filter (0 < dv ·)
  have := Away.adjoin_mk_prod_pow_eq_top_of_pos hf (ι' := s) (v ∘ Subtype.val) ?_
    (dv ∘ Subtype.val) (fun _ ↦ hxd _) (by simp [s])
  swap
  · rw [← top_le_iff, ← hx, Algebra.adjoin_le_iff, Set.range_subset_iff]
    intro i
    rcases (dv i).eq_zero_or_pos with hi | hi
    · exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩
    exact Algebra.subset_adjoin ⟨⟨i, by simpa [s] using hi⟩, rfl⟩
  rw [← top_le_iff, ← this]
  apply Algebra.adjoin_mono
  rintro _ ⟨a, ai, hai : ∑ x ∈ s.attach, _ = _, h, rfl⟩
  refine ⟨a, fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0, ?_, ?_, ?_⟩
  · simpa [Finset.sum_attach_eq_sum_dite] using hai
  · simp [apply_dite, dite_apply, h]
  · congr 1
    change _ = ∏ x ∈ s.attach, _
    simp [Finset.prod_attach_eq_prod_dite]

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

Goal state before:
pp: case inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d > 0
b : ℕ := ∑ i, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) := {ai | ∑ i, ↑(ai.2 i) * dx i = ↑ai.1 * d}
F : ↑s' → Away 𝒜 f := fun ai ↦ Away.mk 𝒜 hf (↑(↑ai).1) (∏ i, ↑i ^ ↑((↑ai).2 i)) ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ ∑ x, ai x * dx x ≤ ∑ i, dx i * d

Tactic:
mul_comm _ d

Goal state after:
case inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d > 0
b : ℕ := ∑ i, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) := {ai | ∑ i, ↑(ai.2 i) * dx i = ↑ai.1 * d}
F : ↑s' → Away 𝒜 f := fun ai ↦ Away.mk 𝒜 hf (↑(↑ai).1) (∏ i, ↑i ^ ↑((↑ai).2 i)) ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ ∑ x, ai x * dx x ≤ ∑ x, d * dx x
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
x✝¹ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝¹ * x✝), ⋯⟩ =
    ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩ * ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝, ⋯⟩

Tactic:
ext; simp only [map_mul, HomogeneousLocalization.val_mul, Proj.mul_apply]

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

Goal state before:
pp: case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
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_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e

Tactic:
simp; ring

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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    (specStalkEquiv 𝒜 f x f_deg hm).hom ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv

Tactic:
refine CommRingCat.hom_ext <|
    IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).base x).asIdeal.primeCompl
      (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) <| ?_
  ext a
  refine congr($(toStalk_stalkMap_toSpec 𝒜 f x) _).trans ?_
  rw [awayToΓ_ΓToStalk, ← toStalk_specStalkEquiv, Category.assoc]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
j : 𝒰.I₀
⊢ Q (𝒰.X j ↘ S)

Tactic:
← comp_over (𝒰.f j)

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
j : 𝒰.I₀
⊢ Q (𝒰.f j ≫ ((MorphismProperty.Over.forget Q ⊤ S).obj X).left ↘ S)
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 hf).op)) t) = 0

Tactic:
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 ≫ h.q) ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f

Tactic:
by rw [assoc, h.fac, map_comp_assoc]

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

Goal state before:
pp: 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 : Sigma κ
⊢ PrimeSpectrum.basicOpen (a i.fst i.snd) ≤ U ↑i.fst

Tactic:
rw [ha]

Goal state after:
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 : Sigma κ
⊢ PrimeSpectrum.basicOpen (a i.fst i.snd) ≤ ⨆ k, PrimeSpectrum.basicOpen (a i.fst k)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.e_a.e_a.succ
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
n✝ : ℕ
h : d j = n✝ + 1
⊢ (∏ i, d i) * (a * d i₀) + (∏ i, d i) * (d i₀ * (a * (n✝ + 1 - 1))) = (∏ i, d i) * (a * (d i₀ * (n✝ + 1)))

Tactic:
simp; ring

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ qcPrecoverage ⊓ precoverage P ≤ propQCPrecoverage Q

Tactic:
propQCPrecoverage

Goal state after:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ qcPrecoverage ⊓ precoverage P ≤ qcPrecoverage ⊓ precoverage Q
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ (Presieve.ofArrows X π).EffectiveEpimorphic → EffectiveEpiFamily X π

Tactic:
intro (h : Nonempty _)
    rw [Sieve.generateFamily_eq] at h
    constructor
    apply Nonempty.map (effectiveEpiFamilyStructOfIsColimit _ _) h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z✝ : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z✝
hR : Sieve.ofArrows T g ∈ (J.over X) Z✝
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : gi ≫ (fun i ↦ Over.Hom.left (g i)) i = gj ≫ (fun i ↦ Over.Hom.left (g i)) j
⊢ gj ≫ (T j).hom = (Over.mk (gi ≫ (T i).hom)).hom

Tactic:
by dsimp; rw [← Over.w (g i), reassoc_of% hgij, ← Over.w (g j)]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
· rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (∃ ι A B f, W = ofHoms f) → IsSmall.{w, v, u} W

Tactic:
rintro ⟨_, _, _, _, rfl⟩
    infer_instance

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
eq_neg_iff_add_eq_zero,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ + padicValRat p q = 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
by
      have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
      simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) x = 0 ↔ x = 0

Tactic:
by
  simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case e'_2.e'_1
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

pp: case e'_3.e'_6
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

Tactic:
all_goals lia

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ ↑p ^ (-f.valuation) = ↑p ^ (-g.valuation)

Tactic:
← neg_inj,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ -f.valuation = -g.valuation ↔ ↑p ^ (-f.valuation) = ↑p ^ (-g.valuation)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q

Tactic:
· simp [norm, not_equiv_zero_const_of_nonzero hq]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ LimZero (f + g - f)

Tactic:
· simpa only [add_sub_cancel_left, sub_zero] using hg

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ ∀ (k : ℕ), padicNorm p (↑g k) = padicNorm p (↑f k)

Tactic:
simp only [h, forall_const]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ nullHomotopicMap' (hσ' q) =
    nullHomotopicMap' (hσ' q) ≫ (alternatingFaceMapComplex C).map f

Tactic:
nullHomotopicMap'_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ nullHomotopicMap' (hσ' q) =
    nullHomotopicMap' fun i j hij ↦ hσ' q i j hij ≫ ((alternatingFaceMapComplex C).map f).f j
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f j - ↑f (max N N2)) < ε / 3

Tactic:
· exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ‖(↑p)⁻¹‖

Tactic:
rw [norm_inv, norm_p, inv_inv]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ b + (c + a) = f

Tactic:
h3,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ b + 0 = f
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ PInfty).f n = PInfty.f n

Tactic:
exact PInfty_f_idem n

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ PInfty = PInfty

Tactic:
ext n
  exact PInfty_f_idem n

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ ∑ x, (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev

Tactic:
simp only [comp_sum, P_f_naturality_assoc, SimplicialObject.δ_naturality_assoc]

Goal state after: