-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc]
lemma awayι_toSpecZero : awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 _))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).ι ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          (basicOpen 𝒜 1).toSpecΓ ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
rw [reassoc_of% this, ← Scheme.Opens.toSpecΓ_SpecMap_map_assoc, basicOpenToSpec, Category.assoc,
  ← Spec.map_comp, ← Spec.map_comp, ← Spec.map_comp]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).toSpecΓ ≫
      Spec.map
        ((CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1)) ≫ awayToSection 𝒜 1) ≫
          (Proj 𝒜).presheaf.map (homOfLE ⋯).op) =
    (basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)) ≫ awayToSection 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
U : (Proj 𝒜).Opens
e : U = ⊤
⊢ (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯

Tactic:
simp only [← Category.assoc, Iso.comp_inv_eq]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
U : (Proj 𝒜).Opens
e : U = ⊤
⊢ (basicOpen 𝒜 f).ι = ((Proj 𝒜).homOfLE ⋯ ≫ ((Proj 𝒜).isoOfEq e).hom) ≫ (Proj 𝒜).topIso.hom

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).toSpecΓ ≫
      Spec.map
        ((CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1)) ≫ awayToSection 𝒜 1) ≫
          (Proj 𝒜).presheaf.map (homOfLE ⋯).op) =
    (basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)) ≫ awayToSection 𝒜 f)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
rw [toSpecZero, basicOpenToSpec, awayι]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ ((basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι) ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          ((basicOpen 𝒜 1).toSpecΓ ≫ Spec.map (awayToSection 𝒜 1)) ≫
            Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
U : (Proj 𝒜).Opens
e : U = ⊤
⊢ (basicOpen 𝒜 f).ι = ((Proj 𝒜).homOfLE ⋯ ≫ ((Proj 𝒜).isoOfEq e).hom) ≫ (Proj 𝒜).topIso.hom

Tactic:
simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ ((basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι) ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          ((basicOpen 𝒜 1).toSpecΓ ≫ Spec.map (awayToSection 𝒜 1)) ≫
            Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
simp only [Category.assoc, Iso.inv_comp_eq, basicOpenIsoSpec_hom]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ (basicOpen 𝒜 f).ι ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          (basicOpen 𝒜 1).toSpecΓ ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ (basicOpen 𝒜 f).ι ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          (basicOpen 𝒜 1).toSpecΓ ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
have (U) (e : U = ⊤) : (basicOpen 𝒜 f).ι ≫ (Scheme.topIso _).inv ≫ (Scheme.isoOfEq _ e).inv =
    Scheme.homOfLE _ (le_top.trans_eq e.symm) := by
  simp only [← Category.assoc, Iso.comp_inv_eq]
  simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).ι ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          (basicOpen 𝒜 1).toSpecΓ ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))