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

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
⊢ CommRingCat.ofHom
      (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯) =
    ((stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).inv ≫ PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p) ≫
      (stalkIso ℬ p).hom

Tactic:
]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
⊢ CommRingCat.ofHom
      (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯) =
    ((stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).inv ≫ PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p) ≫
      (stalkIso ℬ p).hom
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
i : ℕ
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0

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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e_y.inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d > 0
⊢ ∑ i, dv i * (ai i / d) * d ≤ ∑ i, ai i • dv i

Tactic:
]

Goal state after:
case e_y.inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d > 0
⊢ ∑ i, dv i * (ai i / d) * d ≤ ∑ i, ai i • dv i
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p))
          ((ConcreteCategory.hom
              ((structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)
                ((ProjectiveSpectrum.comap f hf) p) ⋯))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))

Tactic:
]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p))
          ((ConcreteCategory.hom
              ((structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)
                ((ProjectiveSpectrum.comap f hf) p) ⋯))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case inr
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op = (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

pp: case inr.hU
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1

Tactic:
]

Goal state after:
case inr.hU
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom
            ((toSheafedSpace ℬ).presheaf.germ
              ((Opens.map (sheafedSpaceMap f hf).hom.base).obj (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)) p ⋯))
          ((ConcreteCategory.hom
              ((sheafedSpaceMap f hf).hom.c.app (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))

Tactic:
]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom
            ((toSheafedSpace ℬ).presheaf.germ
              ((Opens.map (sheafedSpaceMap f hf).hom.base).obj (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)) p ⋯))
          ((ConcreteCategory.hom
              ((sheafedSpaceMap f hf).hom.c.app (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_1
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
x : A
hx : x ∈ carrier f_deg q
⊢ 0 ∈ carrier f_deg q

Tactic:
]

Goal state after:
case refine_1
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
x : A
hx : x ∈ carrier f_deg q
⊢ 0 ∈ carrier f_deg q
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom ((toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯))
          (sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c))))

Tactic:
]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom ((toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯))
          (sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c))))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ = val (↑(sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c)) ⟨p, ⋯⟩)

Tactic:
]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ = val (↑(sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c)) ⟨p, ⋯⟩)
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
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d) ∈
    Subalgebra.toSubmodule
      (Algebra.adjoin ↥(𝒜 0)
        {x |
          ∃ a ai,
            ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x})

Tactic:
]

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
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d) ∈
    Subalgebra.toSubmodule
      (Algebra.adjoin ↥(𝒜 0)
        {x |
          ∃ a ai,
            ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x})
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑⟨a, b⟩)

Tactic:
]

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
p : ↥(Proj ℬ)
x : ↑((Proj 𝒜).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base) p))
hx :
  IsUnit
    ((CommRingCat.Hom.hom
        ((stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom ≫
          CommRingCat.ofHom
              (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal
                p.asHomogeneousIdeal.toIdeal ⋯) ≫
            (stalkIso ℬ p).inv))
      x)
⊢ IsUnit x

Tactic:
]

Goal state after:
A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
p : ↥(Proj ℬ)
x : ↑((Proj 𝒜).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base) p))
hx :
  IsUnit
    ((CommRingCat.Hom.hom
        ((stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom ≫
          CommRingCat.ofHom
              (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal
                p.asHomogeneousIdeal.toIdeal ⋯) ≫
            (stalkIso ℬ p).inv))
      x)
⊢ IsUnit x
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op ≫
      (modulesSpecToSheaf.map f).hom.app (op (PrimeSpectrum.basicOpen (unop r))) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op ≫
      (modulesSpecToSheaf.map f).hom.app (op (PrimeSpectrum.basicOpen (unop r)))

Tactic:
]

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

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑⟨a, b⟩)

Tactic:
]

Goal state after:
case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M (basicOpen (unop r)) ≫
      ((modulesSpecToSheaf.map (tilde.map (toOpen M ⊤))).hom ≫ (modulesSpecToSheaf.map (tilde M).fromTildeΓ).hom).app
        (op (basicOpen (unop r))) =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))

Tactic:
]

Goal state after:
case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M (basicOpen (unop r)) ≫
      ((modulesSpecToSheaf.map (tilde.map (toOpen M ⊤))).hom ≫ (modulesSpecToSheaf.map (tilde M).fromTildeΓ).hom).app
        (op (basicOpen (unop r))) =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M ⊤ ≫ (modulesSpecToSheaf.obj (tilde M)).obj.map (homOfLE ⋯).op =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))

Tactic:
]

Goal state after:
case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M ⊤ ≫ (modulesSpecToSheaf.obj (tilde M)).obj.map (homOfLE ⋯).op =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ ((basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯) ≫
      (basicOpen 𝒜 s).ι =
    (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv) ≫ (basicOpen 𝒜 s).ι

Tactic:
]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ ((basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯) ≫
      (basicOpen 𝒜 s).ι =
    (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv) ≫ (basicOpen 𝒜 s).ι
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op = 𝟙 ((modulesSpecToSheaf.obj M).obj.obj (op ⊤))

Tactic:
]

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op = 𝟙 ((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: case e_a
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯ ≫ (basicOpenIsoSpec 𝒜 s hs hi).hom =
    (basicOpenIsoSpec ℬ (f s) ⋯ hi).hom ≫ Spec.map (CommRingCat.ofHom (Away.map f s))

Tactic:
]

Goal state after:
case e_a
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯ ≫ (basicOpenIsoSpec 𝒜 s hs hi).hom =
    (basicOpenIsoSpec ℬ (f s) ⋯ hi).hom ≫ Spec.map (CommRingCat.ofHom (Away.map f s))