mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
R' : Type u_5
S' : Type u_6
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
x : PrimeSpectrum R'
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)

Tactic:
have : IsPushout R R' S S' := Algebra.IsPushout.symm inferInstance

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
R' : Type u_5
S' : Type u_6
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
x : PrimeSpectrum R'
this : IsPushout R R' S S'
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : Flat f
inst✝ : IsFinite f
R : CommRingCat
i : Spec R ⟶ Y
w✝ : IsOpenImmersion i
y' : ↥(Spec R)
⊢ finrank ((pullbackLeftPullbackSndIso f g i).hom ≫ pullback.snd f (i ≫ g)) y' = finrank (pullback.snd f (i ≫ g)) y'

Tactic:
finrank_comp_left_of_isIso

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : Flat f
inst✝ : IsFinite f
R : CommRingCat
i : Spec R ⟶ Y
w✝ : IsOpenImmersion i
y' : ↥(Spec R)
⊢ finrank (pullback.snd f (i ≫ g)) y' = finrank (pullback.snd f (i ≫ g)) y'
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
x : ↥(Spec R)
⊢ 1 x ≤ finrank (X.isoSpec.inv ≫ f) x

Tactic:
finrank_comp_left_of_isIso

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
x : ↥(Spec R)
⊢ 1 x ≤ finrank f x
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x = 0
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x

Tactic:
simp only [ord, hx, AddValuation.map_zero]
    subst hx
    by_contra!
    rw [Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at this
    have art := this.2
    rw [Ideal.span_singleton_zero] at art
    have : IsArtinianRing R :=
      (LinearEquiv.isArtinian_iff (Submodule.quotEquivOfEqBot ⊥ rfl).symm).mpr art
    exact IsDiscreteValuationRing.not_krullDimLE_zero R inferInstance

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (ordFrac R) x = ((IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹

Tactic:
simp [ordFrac_eq_inverse_comp_valuation]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

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

Tactic:
conjugateEquiv_symm_id

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
⊢ 𝟙 l₁ = 𝟙 l₁
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

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

Tactic:
rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₂ adj₂).symm (𝟙 r₂) = 𝟙 l₂

Tactic:
conjugateEquiv_symm_id

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
⊢ 𝟙 l₂ = 𝟙 l₂
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 r₁) = 𝟙 l₁

Tactic:
conjugateEquiv_symm_id

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
⊢ 𝟙 l₁ = 𝟙 l₁
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 : Set (ProjectiveSpectrum 𝒜)
⊢ ↑(vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
by
  ext f
  rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf,
    Submodule.mem_iInf]
  refine forall_congr' fun x => ?_
  rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]

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

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ∀ i ∈ Finset.image x Finset.univ, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
⊢ False

Tactic:
have nonempty :
        ∀ x : A, x ∉ I → {i ∈ (decompose 𝒜 x).support | proj 𝒜 i x ∉ I}.Nonempty := by
        intro x hx
        rw [filter_nonempty_iff]
        contrapose! hx
        simp_rw [proj_apply] at hx
        rw [← sum_support_decompose 𝒜 x]
        exact Ideal.sum_mem _ hx

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
⊢ False
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
⊢ (pullbackComp f (g ≫ h)).inv ≫
      Functor.whiskerRight (pullbackComp g h).inv (pullback f) ≫
        ((pullback h).associator (pullback g) (pullback f)).hom ≫
          (pullback h).whiskerLeft (pullbackComp f g).hom ≫ (pullbackComp (f ≫ g) h).hom =
    eqToHom ⋯

Tactic:
change e₁.inv ≫ e₂.inv ≫ (Functor.associator _ _ _).hom ≫ e₃.hom ≫ e₄.hom = _

Goal state after:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
⊢ e₁.inv ≫ e₂.inv ≫ ((pullback h).associator (pullback g) (pullback f)).hom ≫ e₃.hom ≫ e₄.hom = eqToHom ⋯
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 𝒜
x : Submonoid A
z : HomogeneousLocalization 𝒜 x
n : ℕ
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (c1 ^ n) (c2 ^ n)

Tactic:
by
          change Localization.mk _ _ = Localization.mk _ _
          simp only [num_pow, den_pow]
          convert! congr_arg (fun z : at x => z ^ n) h <;> rw [Localization.mk_pow] <;> rfl

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_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]; mem_tac

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]; mem_tac

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
h1 : IsUnit (val f)
⊢ IsUnit f

Tactic:
rcases h1 with ⟨⟨a, b, eq0, eq1⟩, rfl : a = f.val⟩

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 : AtPrime 𝒜 𝔭
b : at 𝔭.primeCompl
eq0 : val f * b = 1
eq1 : b * val f = 1
⊢ IsUnit 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
hm : 0 < m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (m * n)

Tactic:
rw [mul_comm]; mem_tac

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
⊢ IsUnit (val f) ↔ IsUnit f

Tactic:
refine ⟨fun h1 ↦ ?_, IsUnit.map (algebraMap _ _)⟩
  rcases h1 with ⟨⟨a, b, eq0, eq1⟩, rfl : a = f.val⟩
  obtain ⟨f, rfl⟩ := mk_surjective f
  obtain ⟨b, s, rfl⟩ := IsLocalization.exists_mk'_eq 𝔭.primeCompl b
  rw [val_mk, Localization.mk_eq_mk', ← IsLocalization.mk'_mul, IsLocalization.mk'_eq_iff_eq_mul,
    one_mul, IsLocalization.eq_iff_exists (M := 𝔭.primeCompl)] at eq0
  obtain ⟨c, hc : _ = c.1 * (f.den.1 * s.1)⟩ := eq0
  have : f.num.1 ∉ 𝔭 := by
    exact fun h ↦ mul_mem c.2 (mul_mem f.den_mem s.2)
      (hc ▸ Ideal.mul_mem_left _ c.1 (Ideal.mul_mem_right b _ h))
  refine .of_mul_eq_one (Quotient.mk'' ⟨f.1, f.3, f.2, this⟩) ?_
  rw [← mk_mul, ext_iff_val, val_mk]
  simp [mul_comm f.den.1]

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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (m * n)

Tactic:
rw [mul_comm]; mem_tac

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
hm : 0 < m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (m * n)

Tactic:
rw [mul_comm]; mem_tac

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 j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]; mem_tac

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 j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]; mem_tac

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
⊢ Set.range ⇑(awayMapAux 𝒜 ⋯) ⊆ Set.range val

Tactic:
rintro _ ⟨z, rfl⟩
  obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, j, rfl : _ = b⟩, rfl⟩ := mk_surjective z
  use mk ⟨n+j•e,⟨a*g^j, ?_⟩, ⟨x^j, ?_⟩, j, rfl⟩
  · simp [awayMapAux_mk 𝒜 (hx := hx)]
  · apply SetLike.mul_mem_graded ha
    exact SetLike.pow_mem_graded _ hg
  · rw [hx, mul_pow]
    apply SetLike.mul_mem_graded hb'
    exact SetLike.pow_mem_graded _ hg

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 g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤ =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv
⊢ IsIso (awayToSection 𝒜 f)

Tactic:
rw [← Iso.inv_comp_eq, Iso.eq_comp_inv] at this

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom =
    awayToSection 𝒜 f
⊢ IsIso (awayToSection 𝒜 f)
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'
⊢ Function.Surjective ⇑(TopCat.Hom.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯).inv.base)

Tactic:
by exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective

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 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ Submonoid.map f (Submonoid.powers t) ≤ Submonoid.powers x

Tactic:
Submonoid.map_powers

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' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ Submonoid.powers (f t) ≤ Submonoid.powers x
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hle : U ≤ PrimeSpectrum.basicOpen f
x y : ↑Γ(M, U)
hxy : (fun x ↦ f • x) x = (fun x ↦ f • x) y
⊢ x = y

Tactic:
have := M.isUnit_algebraMap_end_of_le_basicOpen _ hle

Goal state after:
R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hle : U ≤ PrimeSpectrum.basicOpen f
x y : ↑Γ(M, U)
hxy : (fun x ↦ f • x) x = (fun x ↦ f • x) y
this : IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, U))) f)
⊢ x = y
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
⊢ ∑ x, ai x % d * dv x + ∑ x, d * (ai x / d * dv x) - (∑ i, dv i * (ai i / d)) * d = ∑ x, ai x % d * dv x

Tactic:
← Finset.mul_sum,

Goal state after:
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
⊢ ∑ x, ai x % d * dv x + d * ∑ i, ai i / d * dv i - (∑ i, dv i * (ai i / d)) * d = ∑ x, ai x % d * dv x
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 𝒜
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
⊢ 1 ∈ 𝒜 (1 • d)

Tactic:
by simp [hd, GradedOne.one_mem]

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆ Subtype.val '' ↑(maximalIdeal ↥V)

Tactic:
refine .trans ?_ (Set.image_mono <| ((local_hom_TFAE _).out 0 2).mp hV.2)

Goal state after:
K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆ Subtype.val '' ↑(map (Subring.inclusion ⋯) (maximalIdeal ↥(LocalSubring.ofPrime A M).toSubring))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case map_units
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) := ⋯
⊢ ∀ (y : ↥((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl),
    IsUnit ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑y)

Tactic:
rintro ⟨y, hy⟩
    obtain ⟨y, rfl⟩ := HomogeneousLocalization.mk_surjective y
    refine .of_mul_eq_one
      (.mk ⟨y.deg, y.den, y.num, (mk_mem_toSpec_base_apply _ _ _).not.mp hy⟩) <| val_injective _ ?_
    simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mul, val_mk,
      mk_eq_mk', val_one, IsLocalization.mk'_mul_mk'_eq_one']

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂

Tactic:
· simp only [Category.assoc]
      apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
      · simp
      · simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
        exact congrArg CommSq.LiftStruct.l h₁₂

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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : ∀ (S : C), ∃ ι U f, Sieve.ofArrows (fun i ↦ F.obj (U i)) f ∈ J S
S : C
⊢ Nonempty (F.OneHypercoverDenseData J₀ J S)

Tactic:
choose ι U f hf using hF

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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
⊢ Nonempty (F.OneHypercoverDenseData J₀ J S)