mathlib-initiative/mathlib-tactics huggingface dataset:
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 : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
x : ↥(unop U)
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ unop U
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal
hy :
  ∀ (x : ↥V),
    (fun x ↦ a (i x)) x = HomogeneousLocalization.mk { deg := j, num := ⟨r, r_mem⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (-a) (i x)

Tactic:
refine ⟨V, m, i, j, ⟨-r, neg_mem r_mem⟩, ⟨s, s_mem⟩, nin, fun y => ?_⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
x : ↥(unop U)
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ unop U
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal
hy :
  ∀ (x : ↥V),
    (fun x ↦ a (i x)) x = HomogeneousLocalization.mk { deg := j, num := ⟨r, r_mem⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
y : ↥V
⊢ (fun x ↦ (-a) (i x)) y = HomogeneousLocalization.mk { deg := j, num := ⟨-r, ⋯⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
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 : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
rw [carrier, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk', IsLocalization.mk'_eq_mul_mk'_one,
    mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_under,
    IsLocalization.under_map_of_isPrime_disjoint (.powers f)]
  · rfl
  · infer_instance
  · exact (disjoint_powers_iff_notMem_of_isPrime _).mpr x.2
  · exact isUnit_of_invertible _

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 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι = (basicOpen 𝒜 x).ι

Tactic:
← basicOpenIsoSpec_hom _ _ f_deg hm,

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'
x : A
hx : x = f * g
⊢ (Proj 𝒜).homOfLE ⋯ ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).hom ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι =
    (basicOpen 𝒜 x).ι
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) = Set.range ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯)))

Tactic:
rw [← pullbackAwayιIso_inv_fst 𝒜 f_deg hm g_deg hm' rfl]
    simp only [TopologicalSpace.Opens.map_coe, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]
    rw [Set.range_eq_univ.mpr (by exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective),
      ← opensRange_awayι _ _ g_deg hm']
    simp [IsOpenImmersion.range_pullbackFst]

Goal state after:
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 = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
c : ℕ
hc : c ∈ DFinsupp.support ((DirectSum.decompose 𝒜) x)
this : c ≠ 0
⊢ ↑(((DirectSum.decompose 𝒜) x) c) ∈ Ideal.span (Set.range fun x ↦ x.snd.fst)

Tactic:
exact Ideal.subset_span ⟨⟨c, _, this.bot_lt, by simp⟩, rfl⟩

Goal state after:
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
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
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
⊢ mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x ↦ f ^ x) 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:
by_cases hfj : f ^ j = 0

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
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : f ^ j = 0
⊢ mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x ↦ f ^ x) 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}

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
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
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x ↦ f ^ x) 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}
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e_y.inl
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d = 0
⊢ ∑ i, dv i * (ai i / d) ≤ a

pp: case e_y.inr
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d > 0
⊢ ∑ i, dv i * (ai i / d) ≤ a

Tactic:
· simp [hd]

Goal state after:
case e_y.inr
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d > 0
⊢ ∑ i, dv i * (ai i / d) ≤ a
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
⊢ (tilde.functor R).essImage M

Tactic:
let g := (tilde.functor _).preimage <| (tildeFinsupp _).hom ≫ P.relations.π ≫ kernel.ι _ ≫
    (tildeFinsupp _).inv

Goal state after:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : ModuleCat.of (↑R) (P.relations.I →₀ ↑R) ⟶ ModuleCat.of (↑R) (P.generators.I →₀ ↑R) :=
  (tilde.functor R).preimage
    ((tildeFinsupp P.relations.I).hom ≫ P.relations.π ≫ kernel.ι P.generators.π ≫ (tildeFinsupp P.generators.I).inv)
⊢ (tilde.functor R).essImage M
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Field K
V : ValuationSubring K
⊢ IsIntegrallyClosed ↥V.toSubring

Tactic:
rw [← V.integer_valuation]; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : Existence f
⊢ SpecializingMap ⇑f

Tactic:
intro x'

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
⊢ ∀ ⦃b : ↥Y⦄, flip (fun x1 x2 ↦ x1 ⤳ x2) b (f x') → ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' x' ∧ f a' = b
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A B : LocalSubring K
hB : A ≤ B
hB' : IsMax B
⊢ ∃ B, A ≤ B.toLocalSubring

Tactic:
obtain ⟨B, rfl⟩ := B.exists_valuationRing_of_isMax hB'

Goal state after:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
B : ValuationSubring K
hB : A ≤ B.toLocalSubring
hB' : IsMax B.toLocalSubring
⊢ ∃ B, A ≤ B.toLocalSubring
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
A : LocalSubring K
⊢ A ∈ s → A ≤ { toSubring := ⨆ i, (↑i).toSubring, isLocalRing := ⋯ }

Tactic:
hA

Goal state after:
case refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
A : LocalSubring K
hA : A ∈ s
⊢ A ≤ { toSubring := ⨆ i, (↑i).toSubring, isLocalRing := ⋯ }
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
      Scheme.Hom.app (lft ≫ pullback.fst i₂ f) ⊤ ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom =
    CommRingCat.ofHom (algebraMap R K)

Tactic:
rw [pullback.lift_fst]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
      Scheme.Hom.app (Spec.map (CommRingCat.ofHom (algebraMap R K))) ⊤ ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom =
    CommRingCat.ofHom (algebraMap R K)
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
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑z.den * ↑y.num)) (i + z.deg + y.deg)) =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
⊢ ↑(((decompose 𝒜) c) i) * (↑z.den * ↑y.num) = ↑(((decompose 𝒜) c) i) * (↑y.den * ↑z.num)

Tactic:
coe_decompose_mul_add_of_right_mem,

Goal state after:
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
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑z.den)) (i + z.deg)) * ↑y.num =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
⊢ ↑(((decompose 𝒜) c) i) * (↑z.den * ↑y.num) = ↑(((decompose 𝒜) c) i) * (↑y.den * ↑z.num)

case b_mem
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
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑z.den * ↑y.num)) (i + z.deg + y.deg)) =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
⊢ ↑y.num ∈ 𝒜 y.deg
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z : (((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A).obj (op ⟨X, x⟩)
⊢ ∃ X_1 x_1 z_1,
    (ConcreteCategory.hom (Φ.toPresheafFiber X_1 x_1 P)) z_1 =
      (ConcreteCategory.hom
          (((forget A).mapCocone (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P))).ι.app (op ⟨X, x⟩)))
        z

Tactic:
exact ⟨X, x, z, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝¹ : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (Φ.fiber.map f))

Tactic:
← mono_iff_injective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝¹ : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst✝ : Mono f
⊢ Mono (Φ.fiber.map f)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0

Tactic:
rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f) = { down := f }

Tactic:
rw [uliftYonedaEquiv_apply]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (((uliftYoneda.{v', v, u} J).map f).hom.app (op X))) { down := 𝟙 X } = { down := f }
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg.succ
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
i : J
hi : ¬IsMax i
a✝ : i = s.top → HasColimitsOfShape α C
hi₀ : Order.succ i = s.top
⊢ HasColimitsOfShape α C

Tactic:
obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
      have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
hi : i < ⊥
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀)

Tactic:
by simp at hi

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, c.incl.app b ≫ φ₁ = c.incl.app b ≫ φ₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₁ =
    ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₂

Tactic:
simpa using hj' k hk

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ ¬IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))

Tactic:
intro h
    rw [isIso_iff_yoneda_map_bijective] at h
    obtain ⟨a, ha⟩ := (h G).2 (pushout.inr _ _)
    exact hf a (by simpa using ha =≫ pushout.desc p f pullback.condition)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
⊢ (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f

Tactic:
let t := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
⊢ (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a n : ℕ
⊢ padicValNat p (a ^ n) = n * padicValNat p a

Tactic:
simpa only [← @Nat.cast_inj ℤ, push_cast] using padicValRat.pow a

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x).valuation = ↑x.valuation

Tactic:
by
  simp [valuation, valuation_coe_nonneg]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ¬IsUnit z ↔ ‖z‖ < 1

Tactic:
simpa using mem_nonunits

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : x < 0
⊢ { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } (↑p ^ x.natAbs) =
    ↑(Multiplicative.ofAdd x)

Tactic:
by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b

Tactic:
simp_rw [padicValInt]
  rw [Int.natAbs_mul, padicValNat.mul] <;> rwa [Int.natAbs_ne_zero]

Goal state after: