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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
⊢ span {a * x} ≤ span {x}

Tactic:
Ideal.span_singleton_le_span_singleton

Goal state after:
R : Type u_1
inst✝ : CommRing R
a x : R
⊢ x ∣ a * x
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
⊢ ord R x ≤ ord R (a * x)

Tactic:
simp only [ord]
  suffices Ideal.span {a * x} ≤ Ideal.span {x} by
    let g : (R ⧸ Ideal.span {a * x}) →ₗ[R] (R ⧸ Ideal.span {x}) := Submodule.factor this
    refine Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)
  rw [Ideal.span_singleton_le_span_singleton]
  exact Dvd.intro_left (algebraMap R R a) rfl

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

Goal state before:
pp: case pos.top.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

Tactic:
simp

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

Goal state before:
pp: case pos.top.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ↑a✝) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝

Tactic:
simp

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

Goal state before:
pp: case pos.coe.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

Tactic:
simp

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

Goal state before:
pp: case top
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ = 0 ↔ ⊤ = ⊤

Tactic:
simp

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

Goal state before:
pp: case coe
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t) ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ V ⊆ ⋃ i ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t), (basicOpen i).carrier

Tactic:
simpa using ht

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range (comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (fun i ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier

Tactic:
simp

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range (comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i)) ⊆
    Set.range ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R x)) i)))
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
⊢ I = ⊥

Tactic:
by
  refine le_bot_iff.mp fun x hx ↦ ?_
  ext i
  simpa [← Category.assoc, Ideal.Quotient.eq_zero_iff_mem.mpr hx] using
    congr((Spec.preimage (Sigma.ι (Spec <| R ·) i ≫ $hf)).hom x).symm

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

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

Tactic:
by
  rw [conjugateEquiv_apply, mateEquiv_apply']
  calc
    _ = 𝟙 _ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 r₁ := by
      rw [adj₁.right_triangle]
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ equalizer.lift (sigmaSpec R) ⋯ ≫ equalizer.ι f g = sigmaSpec R

Tactic:
simp

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₂
α : l₂ ⟶ l₁
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 l₁

Tactic:
simp

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₂
α : l₂ ⟶ l₁
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 l₂

Tactic:
simp

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₂
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 r₂

Tactic:
simp

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₂
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 r₁

Tactic:
simp

Goal state after:
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 𝒜
s s' : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s) ∪ zeroLocus 𝒜 ↑(Ideal.span s')

Tactic:
simp

Goal state after:
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 𝒜
⊢ zeroLocus 𝒜 Set.univ = ∅

Tactic:
simp

Goal state after:
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 𝒜
Z : Set (ProjectiveSpectrum 𝒜)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus 𝒜 s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

Goal state after:
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 (closure t) = vanishingIdeal t

Tactic:
have : (vanishingIdeal (zeroLocus 𝒜 (vanishingIdeal t))).toIdeal = _ := (gc_ideal 𝒜).u_l_u_eq_u t
  ext1
  rw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this
  exact this

Goal state after:
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 𝒜
⊢ ↑(basicOpen 𝒜 1) = ↑⊤

Tactic:
simp

Goal state after:
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 𝒜
⊢ ↑(basicOpen 𝒜 0) = ↑⊥

Tactic:
simp

Goal state after:
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 𝒜
⊢ IsTopologicalBasis (Set.range fun r ↦ ↑(basicOpen 𝒜 r))

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
  · rintro _ ⟨r, rfl⟩
    exact isOpen_basicOpen 𝒜
  · 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.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁹ : Semiring A
inst✝⁸ : Semiring B
inst✝⁷ : Semiring C
inst✝⁶ : Semiring D
inst✝⁵ : SetLike σ A
inst✝⁴ : SetLike τ B
inst✝³ : SetLike ψ C
inst✝² : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
inst✝¹ : AddSubmonoidClass σ A
inst✝ : AddSubmonoidClass τ B
f : 𝒜 →+*ᵍ ℬ
i : ι
⊢ ↑⟨f ↑0, ⋯⟩ = ↑0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁹ : Semiring A
inst✝⁸ : Semiring B
inst✝⁷ : Semiring C
inst✝⁶ : Semiring D
inst✝⁵ : SetLike σ A
inst✝⁴ : SetLike τ B
inst✝³ : SetLike ψ C
inst✝² : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
inst✝¹ : AddSubmonoidClass σ A
inst✝ : AddSubmonoidClass τ B
f : 𝒜 →+*ᵍ ℬ
i : ι
x y : ↥(𝒜 i)
⊢ ↑⟨f ↑(x + y), ⋯⟩ = ↑(⟨f ↑x, ⋯⟩ + ⟨f ↑y, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: X : Scheme
M : X.Modules
U V : X.Opens
i : U ⟶ V
r : ↑Γ(X, V)
x✝ : ↑Γ(M, V)
⊢ (AddCommGrpCat.Hom.hom (smul r ≫ M.presheaf.map i.op)) x✝ =
    (AddCommGrpCat.Hom.hom (M.presheaf.map i.op ≫ smul ((ConcreteCategory.hom (X.presheaf.map i.op)) r))) x✝

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ pullback (f ≫ g ≫ h) = pullback ((f ≫ g) ≫ h)

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ pullback (f ≫ 𝟙 Y) = pullback f

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ pullback (𝟙 X ≫ f) = pullback f

Tactic:
simp

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

Goal state before:
pp: case refine_1
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U✝ V : X.Opens
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsOpenImmersion f✝
inst✝¹ : IsOpenImmersion g
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
r : ↑Γ(X, Opposite.unop U)
x : ↑Γ(Y, f ''ᵁ Opposite.unop U)
⊢ r * (ConcreteCategory.hom (Hom.appIso f (Opposite.unop U)).hom) x =
    (ConcreteCategory.hom (Hom.appIso f (Opposite.unop U)).hom)
      ((ConcreteCategory.hom (Hom.appIso f (Opposite.unop U)).inv) r * x)

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
x✝ : X.Opens
⊢ (𝟭 X.Opens).obj x✝ = 𝟙 X ''ᵁ x✝

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ U = 𝟙 X ''ᵁ U

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ 𝟙 X ''ᵁ U = U

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
x✝ : X.Opens
⊢ (Hom.opensFunctor f ⋙ Hom.opensFunctor g).obj x✝ = (f ≫ g) ''ᵁ x✝

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M✝ N K : X.Modules
φ : M✝ ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
M : Z.Modules
⊢ g ''ᵁ Opposite.unop ((Hom.opensFunctor f).op.obj (Opposite.op U)) = (f ≫ g) ''ᵁ Opposite.unop (Opposite.op U)

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M✝ N K : X.Modules
φ : M✝ ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
M : Z.Modules
⊢ (f ≫ g) ''ᵁ Opposite.unop (Opposite.op U) = g ''ᵁ Opposite.unop ((Hom.opensFunctor f).op.obj (Opposite.op U))

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝³ : IsOpenImmersion f✝
inst✝² : IsOpenImmersion g
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
x✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ
inst✝ : IsOpenImmersion f
⊢ ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
                  (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)).app
              Y.ringCatSheaf).hom.app
      x✝ =
    {
            hom :=
              Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                (forget₂ CommRingCat RingCat) }.hom.app
      x✝

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)).app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ sheafCompose (Opens.grothendieckTopology ↥(Spec S))
        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
      TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
        sheafCompose (Opens.grothendieckTopology ↥(Spec R))
          (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv)) ≅
    sheafCompose (Opens.grothendieckTopology ↥(Spec S))
        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
      TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
        sheafCompose (Opens.grothendieckTopology ↥(Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))

Tactic:
refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_

Goal state after:
case refine_1
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
⊢ ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
              (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
            TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
              sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).obj
        M).obj ≅
    ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
              (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
            TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
              sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).obj
        M).obj

case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (f : X ⟶ Y),
    (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) ?refine_1).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) ?refine_1).hom ≫
        (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).map
          f
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
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x ↦ f ^ x) n ∈ 𝒜 (n • d)
⊢ val (Away.mk 𝒜 hf n s hs) = (mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }).val

Tactic:
simp

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 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
f : A
n : ℕ
⊢ (fun x ↦ g f ^ x) n = g ((fun x ↦ f ^ x) n)

Tactic:
simp

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

Goal state before:
pp: case e'_4
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))
⊢ (n * (e + 1)) • (d + 1) = n • (d + 1 + e) + (n * d) • e

Tactic:
simp

Goal state after:
case e'_4
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))
⊢ n * (e + 1) * (d + 1) = n * (d + 1 + e) + n * d * e
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

Goal state after:
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)) ⋯
⊢ x ^ (n * (e + 1)) * (s * (g ^ (d + 1) * g ^ e) ^ n) = x ^ n * (x ^ e) ^ n * (s * g ^ (n * d) * g ^ (n * (e + 1)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
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).1 ∈ 𝒜 c

Tactic:
simp

Goal state after: