mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case e'_3
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ (⨅ i, vanishingIdeal (t i)).toIdeal = ⨅ i, (vanishingIdeal (t i)).toIdeal

Tactic:
;

Goal state after:
case e'_3
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ (⨅ i, vanishingIdeal (t i)).toIdeal = ⨅ i, (vanishingIdeal (t i)).toIdeal
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 𝒜)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Tactic:
intro r

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 𝒜)
r : A
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
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 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal

Tactic:
;

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal
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 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ

Tactic:
;

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ
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 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ r ∉ ↑x.asHomogeneousIdeal

Tactic:
;

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ r ∉ ↑x.asHomogeneousIdeal
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ ↑y ∈ ℬ i

Tactic:
;

Goal state after:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ ↑y ∈ ℬ i
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x✝ : ↥(𝒜 i)
⊢ ↑((fun y ↦ ⟨EquivLike.inv e ↑y, ⋯⟩) (subtypeMap e i x✝)) = ↑x✝

Tactic:
;

Goal state after:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x✝ : ↥(𝒜 i)
⊢ ↑((fun y ↦ ⟨EquivLike.inv e ↑y, ⋯⟩) (subtypeMap e i x✝)) = ↑x✝
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x✝ : ↥(ℬ i)
⊢ ↑(subtypeMap e i ((fun y ↦ ⟨EquivLike.inv e ↑y, ⋯⟩) x✝)) = ↑x✝

Tactic:
;

Goal state after:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x✝ : ↥(ℬ i)
⊢ ↑(subtypeMap e i ((fun y ↦ ⟨EquivLike.inv e ↑y, ⋯⟩) x✝)) = ↑x✝
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:
;

Goal state after:
ι : 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
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:
;

Goal state after:
ι : 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, ⋯⟩)
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 𝒜
V U : Opens ↑(ProjectiveSpectrum.top 𝒜)
i : V ⟶ U
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : ℕ
r s : ↥(𝒜 j)
h : ∀ (x : ↥U), ↑s ∉ (↑x).asHomogeneousIdeal
w : ∀ (x : ↥U), f x = HomogeneousLocalization.mk { deg := j, num := r, den := s, den_mem := ⋯ }
⊢ IsFraction fun x ↦ f (i x)

Tactic:
;

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
V U : Opens ↑(ProjectiveSpectrum.top 𝒜)
i : V ⟶ U
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : ℕ
r s : ↥(𝒜 j)
h : ∀ (x : ↥U), ↑s ∉ (↑x).asHomogeneousIdeal
w : ∀ (x : ↥U), f x = HomogeneousLocalization.mk { deg := j, num := r, den := s, den_mem := ⋯ }
⊢ IsFraction fun x ↦ f (i x)
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}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
⊢ False

Tactic:
have mem_max₂ : max₂ ∈ set₂ := max'_mem set₂ (nonempty y rid₂)

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
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
⊢ False
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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
m : α
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (m • c1) (m • c2)

Tactic:
change Localization.mk _ _ = Localization.mk _ _

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
m : α
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk ↑(m • c1).num ⟨↑(m • c1).den, ⋯⟩ = Localization.mk ↑(m • c2).num ⟨↑(m • c2).den, ⋯⟩
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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk (n • ↑x✝.num) ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩

Tactic:
;

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk (n • ↑x✝.num) ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (-c1) (-c2)

Tactic:
change Localization.mk _ _ = Localization.mk _ _

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk ↑(-c1).num ⟨↑(-c1).den, ⋯⟩ = Localization.mk ↑(-c2).num ⟨↑(-c2).den, ⋯⟩
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
this : (Hom.opensFunctor f ⋙ Opens.map f.base).IsContinuous (Opens.grothendieckTopology ↥X)
  (Opens.grothendieckTopology ↥X) :=
  Functor.isContinuous_comp (Hom.opensFunctor f) (Opens.map f.base) (Opens.grothendieckTopology ↥X)
    (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X)
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ (RingCat.Hom.hom
        ((({
                    hom :=
                      Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                        (forget₂ CommRingCat RingCat) } ≫
                  ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
                        (Opens.grothendieckTopology ↥Y)).map
                    (Hom.toRingCatSheafHom f)) ≫
                (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun U ↦ eqToIso ⋯) ⋯).hom RingCat
                      (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
                  X.ringCatSheaf).hom.app
          U))
      x =
    (RingCat.Hom.hom ((𝟙 X.ringCatSheaf).hom.app U)) x

Tactic:
;

Goal state after:
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
this : (Hom.opensFunctor f ⋙ Opens.map f.base).IsContinuous (Opens.grothendieckTopology ↥X)
  (Opens.grothendieckTopology ↥X) :=
  Functor.isContinuous_comp (Hom.opensFunctor f) (Opens.map f.base) (Opens.grothendieckTopology ↥X)
    (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X)
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ (RingCat.Hom.hom
        ((({
                    hom :=
                      Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                        (forget₂ CommRingCat RingCat) } ≫
                  ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
                        (Opens.grothendieckTopology ↥Y)).map
                    (Hom.toRingCatSheafHom f)) ≫
                (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun U ↦ eqToIso ⋯) ⋯).hom RingCat
                      (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
                  X.ringCatSheaf).hom.app
          U))
      x =
    (RingCat.Hom.hom ((𝟙 X.ringCatSheaf).hom.app U)) x
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = Localization.mk (-↑y.num) ⟨↑y.den, ⋯⟩

Tactic:
;

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = Localization.mk (-↑y.num) ⟨↑y.den, ⋯⟩
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:
change Localization.mk _ _ = Localization.mk _ _

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 𝒜
x : Submonoid A
z : HomogeneousLocalization 𝒜 x
n : ℕ
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk ↑(c1 ^ n).num ⟨↑(c1 ^ n).den, ⋯⟩ = Localization.mk ↑(c2 ^ n).num ⟨↑(c2 ^ n).den, ⋯⟩
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
U : Y.Opensᵒᵖ
x : ↑(((𝟭 Y.Opens).op ⋙ Y.ringCatSheaf.obj).obj U)
⊢ (RingCat.Hom.hom ((Functor.whiskerRight (NatTrans.op ⋯.adjunction.counit) Y.ringCatSheaf.obj).app U)) x =
    (RingCat.Hom.hom
        (((Hom.toRingCatSheafHom f).hom ≫
              (Opens.map f.base).op.whiskerLeft
                {
                    hom :=
                      Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                        (forget₂ CommRingCat RingCat) }.hom).app
          U))
      x

Tactic:
;

Goal state after:
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
U : Y.Opensᵒᵖ
x : ↑(((𝟭 Y.Opens).op ⋙ Y.ringCatSheaf.obj).obj U)
⊢ (RingCat.Hom.hom ((Functor.whiskerRight (NatTrans.op ⋯.adjunction.counit) Y.ringCatSheaf.obj).app U)) x =
    (RingCat.Hom.hom
        (((Hom.toRingCatSheafHom f).hom ≫
              (Opens.map f.base).op.whiskerLeft
                {
                    hom :=
                      Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                        (forget₂ CommRingCat RingCat) }.hom).app
          U))
      x
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
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ c1 + c3 ≈ c2 + c4

Tactic:
change Localization.mk _ _ = Localization.mk _ _

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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk ↑(c1 + c3).num ⟨↑(c1 + c3).den, ⋯⟩ = Localization.mk ↑(c2 + c4).num ⟨↑(c2 + c4).den, ⋯⟩
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.Opensᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (𝟙 (Opposite.op (Opposite.unop U)))

Tactic:
;

Goal state after:
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.Opensᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (𝟙 (Opposite.op (Opposite.unop U)))
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 : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
;

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_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)
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✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso (𝟙 X) (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
                  (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
              X.ringCatSheaf).hom.app
      x✝ =
    (𝟙 X.ringCatSheaf).hom.app x✝

Tactic:
;

Goal state after:
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✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso (𝟙 X) (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
                  (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
              X.ringCatSheaf).hom.app
      x✝ =
    (𝟙 X.ringCatSheaf).hom.app x✝
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
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 ∈ 𝒜 (i * m)

Tactic:
;

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_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)
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
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ c1 * c3 ≈ c2 * c4

Tactic:
change Localization.mk _ _ = Localization.mk _ _

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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk ↑(c1 * c3).num ⟨↑(c1 * c3).den, ⋯⟩ = Localization.mk ↑(c2 * c4).num ⟨↑(c2 * c4).den, ⋯⟩
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 : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
;

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