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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ (-1) ^ (f.natDegree * (f.natDegree - 1)) * (f.leadingCoeff * f.sylvesterDeriv.det) =
    (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff *
      (f.sylvesterDeriv.det * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2))

Tactic:
mul_comm f.natDegree

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ (-1) ^ ((f.natDegree - 1) * f.natDegree) * (f.leadingCoeff * f.sylvesterDeriv.det) =
    (-1) ^ ((f.natDegree - 1) * f.natDegree / 2) * f.leadingCoeff *
      (f.sylvesterDeriv.det * (-1) ^ ((f.natDegree - 1) * f.natDegree / 2))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
⊢ IsCommMonObj G ↔ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η

Tactic:
by
  rw [isCommMonObj_iff_isMulCommutative]
  refine ⟨fun h ↦ ?_, fun heq X ↦ ⟨⟨fun f g ↦ ?_⟩⟩⟩
  · simp [GrpObj.commutator, one_eq_one]
  · simpa [one_eq_one, mul_inv_eq_iff_eq_mul] using congr(lift f g ≫ $heq)

Goal state after:
Module: Mathlib.RingTheory.Finiteness.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✝ : FiniteType T (T ⊗[R] S)
⊢ FiniteType R S

Tactic:
by
  obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := T) (A := T ⊗[R] S)
  have (x : s) := TensorProduct.exists_sum_tmul_eq x.1
  choose k t m h using this
  let f : MvPolynomial (Σ x : s, Fin (k x)) R →ₐ[R] S := MvPolynomial.aeval (fun ⟨x, i⟩ ↦ m x i)
  apply Algebra.FiniteType.of_surjective f
  have hf : Function.Surjective (Algebra.TensorProduct.map (.id T T) f) := by
    rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← hs, adjoin_le_iff]
    intro x hx
    let i : s := ⟨x, hx⟩
    use ∑ (j : Fin (k i)), t i j ⊗ₜ MvPolynomial.X ⟨i, j⟩
    simp [f, ← h, i]
  exact (Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T _).mp hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
  Scheme.Cover.pushforwardIso
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom

Tactic:
IsZariskiLocalAtSource.iff_of_openCover (P := P) 𝒰

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
  Scheme.Cover.pushforwardIso
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
⊢ IsOpenImmersion ((MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S).map (colimit.ι F j))

Tactic:
let e : (colimit F).left ≅ colimit (F ⋙ _) :=
    preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
e : (colimit F).left ≅ colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
⊢ IsOpenImmersion ((MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S).map (colimit.ι F j))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom ≫
      Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ↘ Spec (of S)

Tactic:
rw [← cancel_epi (pullbackSymmetry .. ≪≫ pullbackSpecIso' ..).inv,
      Scheme.canonicallyOverPullback_over, Iso.inv_hom_id_assoc, Iso.trans_inv, Category.assoc,
      pullbackSymmetry_inv_comp_snd]
    exact (pullbackSpecIso_inv_fst ..).symm

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
x : X
⊢ x ∈ V.left → x ∈ U

Tactic:
apply leOfHom V.hom

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
⊢ ((𝟭 (Over U)).obj V).left =
    (({ obj := fun V ↦ { carrier := Subtype.val ⁻¹' ↑V.left, is_open' := ⋯ }, map := fun {X_1 Y} f ↦ homOfLE ⋯,
              map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun W ↦ Over.mk (homOfLE ⋯), map := fun {X_1 Y} f ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯,
              map_comp := ⋯ }).obj
        V).left

Tactic:
by
    ext x
    dsimp
    simp only [SetLike.mem_coe, Set.mem_image, Set.mem_preimage,
      Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right, iff_self_and]
    apply leOfHom V.hom

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
⊢ ∃ S' x x_1, ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑s ⊆ ↑f.range

Tactic:
induction s using Finset.induction with
  | empty =>
    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
  | insert a s has IH =>
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
    have ha := Algebra.IsIntegral.isIntegral (R := R) a
    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
    algebraize [f.toRingHom]
    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
      .trans S' _, .trans (S := S'), .trans _ S' _,
      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
⊢ ord R (a * b) = ord R a + ord R b

Tactic:
simp only [Ring.ord, ← this]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
⊢ Module.length R (R ⧸ span {a * b}) = Module.length R (R ⧸ b • span {a})
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
ha : a ∈ nonZeroDivisors R
⊢ ord R (a * b) = ord R a + ord R b

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
ha : a ∈ nonZeroDivisors R
⊢ ord R (b * a) = ord R a + ord R b
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
this : IsNoetherian R (R ⧸ Ideal.span {0}) ∧ IsArtinian R (R ⧸ Ideal.span {0})
⊢ False

Tactic:
have art := this.2

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
this : IsNoetherian R (R ⧸ Ideal.span {0}) ∧ IsArtinian R (R ⧸ Ideal.span {0})
art : IsArtinian R (R ⧸ Ideal.span {0})
⊢ False
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₂
⊢ 𝟙 r₁ ⊗≫
      (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫ (λ_ r₃).hom

Tactic:
simp only [leftAdjointSquare.vcomp, mateEquiv_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₁ ⊗≫
      (𝟙 (r₁ ≫ 𝟙 c ≫ 𝟙 c) ⊗≫
          r₁ ◁ (𝟙 c ≫ 𝟙 c) ◁ adj₃.unit ⊗≫
            r₁ ◁
                ((α_ (𝟙 c) (𝟙 c) l₃).hom ≫
                    𝟙 c ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                      (α_ (𝟙 c) l₂ (𝟙 d)).inv ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 d ≫ (α_ l₁ (𝟙 d) (𝟙 d)).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (𝟙 d ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((𝟙 d ≫ 𝟙 d) ≫ r₃)) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₃.unit ⊗≫
            r₁ ◁ ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ▷ r₃ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₃ ⊗≫ 𝟙 (𝟙 d ≫ r₃)) ≫
        (λ_ 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 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ vanishingIdeal t
g : A
hg : g ∈ vanishingIdeal t'
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal

Tactic:
mem_vanishingIdeal

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}

Tactic:
exact zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)

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

Goal state before:
pp: case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen 𝒜 r), a ∈ v ∧ v ⊆ u

Tactic:
· rintro p U hp ⟨s, hs⟩
    rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
    obtain ⟨f, hfs, hfp⟩ := hp
    refine ⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, ?_⟩
    rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
    exact zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)

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 : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (algebraMap A (Localization (Submonoid.powers f))) ↑z.num *
        IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩ ∈
      Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
mul_comm,

Goal state after:
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)
⊢ IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩ *
        (algebraMap A (Localization (Submonoid.powers f))) ↑z.num ∈
      Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal
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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : (algebraMap A (at 𝔭.primeCompl)) (↑f.num * b) = 1 * (algebraMap A (at 𝔭.primeCompl)) ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
one_mul,

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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : (algebraMap A (at 𝔭.primeCompl)) (↑f.num * b) = (algebraMap A (at 𝔭.primeCompl)) ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
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 : ℕ
⊢ HomogeneousLocalization.mk
      { deg := m * i + m * i,
        num :=
          ⟨∑ m_1 ∈ range (m + m + 1), (proj 𝒜 i) a ^ m_1 * (proj 𝒜 i) b ^ (m + m - m_1) * ↑((m + m).choose m_1), ⋯⟩,
        den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
mul_comm,

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 : ℕ
⊢ HomogeneousLocalization.mk
      { deg := m * i + m * i,
        num := ⟨∑ x ∈ range (m + m + 1), ↑((m + m).choose x) * ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩,
        den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal
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, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
x : ↥X
hx : x ∈ X.basicOpen (f r)
I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, ⟨r, ⋯⟩⟩
⊢ x ∈ Scheme.Hom.opensRange ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I)

Tactic:
simpa [openCoverOfMapIrrelevantEqTop] using hx

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

Goal state before:
pp: case pos.e_a.e_x
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 := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j) = (proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j) * (proj 𝒜 i) b ^ m

Tactic:
dsimp; rw [mul_assoc, ← pow_add, add_comm (m - j), Nat.add_sub_assoc h1]

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

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

Tactic:
rw [Ideal.map] at hb

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
i : ι
b : B
hb : b ∈ Ideal.span (⇑f '' ↑I.toIdeal)
⊢ ↑(((DirectSum.decompose ℬ) b) i) ∈ Ideal.map f I.toIdeal
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
⊢ v x ≤ 1 → IsIntegral O x

Tactic:
intro h
    obtain ⟨y, rfl⟩ := hv.exists_of_le_one h
    exact ⟨Polynomial.X - .C y, by monicity, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
this : R = ofPrime S.toSubring Q
⊢ x ∈ (ofPrime S.toSubring Q).toSubring

Tactic:
exact LocalSubring.le_ofPrime _ _ (self_mem_adjoin_singleton _ _)

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
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ i * m = m • i

Tactic:
mul_comm,

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
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ m * i = m • i
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp.refine_2
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
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.I₀
fi : (𝒰.X i).asOverProp S ⋯ ⟶ X := Hom.asOverProp (𝒰.f i) S
⊢ R.arrows (Hom.asOverProp (𝒰.f i) S)

Tactic:
have : R.functorPushforward _ ((MorphismProperty.Over.forget Q ⊤ S).map fi) := le _ _ ⟨i⟩

Goal state after:
case mp.refine_2
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
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.I₀
fi : (𝒰.X i).asOverProp S ⋯ ⟶ X := Hom.asOverProp (𝒰.f i) S
this :
  (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows ((MorphismProperty.Over.forget Q ⊤ S).map fi)
⊢ R.arrows (Hom.asOverProp (𝒰.f i) S)