mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ (λ_ l₂).inv ≫
      (𝟙 (𝟙 c ≫ l₂) ⊗≫
          adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫ l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂ ⊗≫ l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d)) ≫
        (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
]

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₂).inv ≫
      (𝟙 (𝟙 c ≫ l₂) ⊗≫
          adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫ l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂ ⊗≫ l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d)) ≫
        (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom
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)ᶜ
this : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ⊤
⊢ U = ⊤

Tactic:
have : Ideal.span s = ⊤ := top_le_iff.mp
    ((Ideal.span_eq_top_of_span_image_evalRingHom _ ht this).ge.trans (Ideal.span_mono hts))

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)ᶜ
this✝ : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ⊤
this : Ideal.span s = ⊤
⊢ U = ⊤
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₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).topIso.hom

Tactic:
]

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).topIso.hom
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₁
⊢ 𝟙 r₁ ⊗≫ ((ρ_ r₁).hom ≫ (λ_ r₁).inv) ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ ((ρ_ r₁).hom ≫ (λ_ r₁).inv) ⊗≫ 𝟙 r₁ = 𝟙 r₁
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this✝ : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
]

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this✝ : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)
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₁).symm (𝟙 r₁) = 𝟙 l₁

Tactic:
Equiv.symm_apply_eq,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ = (conjugateEquiv adj₁ adj₁) (𝟙 l₁)
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₁
⊢ 𝟙 r₁ = 𝟙 r₁

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
I : Ideal ↑(CommRingCat.of ((i : ι) → ↑(R i)))
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ I))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R

Tactic:
]

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
I : Ideal ↑(CommRingCat.of ((i : ι) → ↑(R i)))
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ I))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫
      (𝟙 (r ≫ 𝟙 c) ⊗≫
          r ◁ 𝟙 c ◁ (Adjunction.id c).unit ⊗≫
            r ◁ ((λ_ (𝟙 c)).hom ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        (λ_ (𝟙 c)).hom =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫
      (𝟙 (r ≫ 𝟙 c) ⊗≫
          r ◁ 𝟙 c ◁ (Adjunction.id c).unit ⊗≫
            r ◁ ((λ_ (𝟙 c)).hom ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        (λ_ (𝟙 c)).hom =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ (λ_ (𝟙 c)).inv ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            l ◁ ((ρ_ r).hom ≫ α ≫ (λ_ (𝟙 c)).inv) ▷ 𝟙 c ⊗≫ l ◁ 𝟙 c ◁ (Adjunction.id c).counit ⊗≫ 𝟙 (l ≫ 𝟙 c)) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ (λ_ (𝟙 c)).inv ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            l ◁ ((ρ_ r).hom ≫ α ≫ (λ_ (𝟙 c)).inv) ▷ 𝟙 c ⊗≫ l ◁ 𝟙 c ◁ (Adjunction.id c).counit ⊗≫ 𝟙 (l ≫ 𝟙 c)) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
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
this : IsIso (equalizer.ι f g)
⊢ equalizer.ι f g ≫ g = equalizer.ι f g ≫ g

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ a, pointsPi R X a = f

Tactic:
let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ ∃ a, pointsPi R X a = f
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ 𝟙 r₁ ⊗≫
      (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫ (λ_ r₃).hom

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ 𝟙 r₁ ⊗≫
      (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫ (λ_ r₃).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

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

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β
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₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
⊢ 𝟙 r₁ = 𝟙 r₁

Tactic:
]

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₁
⊢ 𝟙 l₁ = 𝟙 l₁

Tactic:
]

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₁
⊢ 𝟙 r₁ = 𝟙 r₁

Tactic:
]

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₁
⊢ 𝟙 r₂ = 𝟙 r₂

Tactic:
]

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₂
⊢ 𝟙 l₂ = 𝟙 l₂

Tactic:
]

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₂
⊢ 𝟙 l₁ = 𝟙 l₁

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ f ↑⟨i, ⋯⟩ = f i

Tactic:
]

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

Tactic:
ext x
  exact (Submodule.gi _ _).gc s x.asHomogeneousIdeal.toIdeal

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 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ (⨅ (_ : i ∈ t), i.asHomogeneousIdeal).toIdeal) ↔
    f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ (⨅ (_ : i ∈ t), i.asHomogeneousIdeal).toIdeal) ↔
    f ∈ {f | ∀ x ∈ t, f ∈ x.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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ t → f ∈ x.asHomogeneousIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal

Tactic:
]

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 𝒜)
f : A
⊢ (∀ x ∈ t, f ∈ x.asHomogeneousIdeal) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal

Tactic:
]

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:
]

Goal state after:
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')
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 𝒜)
r : A
⊢ (∃ y ∈ (vanishingIdeal t).toIdeal, ∃ z ∈ (vanishingIdeal t').toIdeal, y + z = r) →
    ∀ x ∈ t ∩ t', 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 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ (∃ y ∈ (vanishingIdeal t).toIdeal, ∃ z ∈ (vanishingIdeal t').toIdeal, y + z = r) →
    ∀ x ∈ t ∩ t', r ∈ x.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 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal

Tactic:
]

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 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α))) = α

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α))) = α
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.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ 𝟙 (r₁ ≫ g) ⊗≫ (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 (h ≫ r₃) =
    (mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ 𝟙 (r₁ ≫ g) ⊗≫ (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 (h ≫ r₃) =
    (mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β)
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 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
⊢ ⋂ i, ↑i ∈ Set.range (zeroLocus 𝒜)

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
⊢ ⋂ i, ↑i ∈ Set.range (zeroLocus 𝒜)
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 𝒜)
⊢ (∃ s, Z = zeroLocus 𝒜 s) ↔ ∃ s, Z = zeroLocus 𝒜 s

Tactic:
]

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 : Set A
⊢ ∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
s : Set A
⊢ ∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1
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 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
t' : Set (ProjectiveSpectrum 𝒜)
ht' : ∃ s, t' = zeroLocus 𝒜 s
ht : t ⊆ t'
⊢ ∃ s, t' = zeroLocus 𝒜 s

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
t' : Set (ProjectiveSpectrum 𝒜)
ht' : ∃ s, t' = zeroLocus 𝒜 s
ht : t ⊆ t'
⊢ ∃ s, t' = zeroLocus 𝒜 s
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h₁
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
fs : Set A
ht' : IsClosed (zeroLocus 𝒜 fs)
ht : fs ⊆ ↑(vanishingIdeal t)
⊢ x ∈ zeroLocus 𝒜 fs

Tactic:
]

Goal state after:
case h₁
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
fs : Set A
ht' : IsClosed (zeroLocus 𝒜 fs)
ht : fs ⊆ ↑(vanishingIdeal t)
⊢ x ∈ zeroLocus 𝒜 fs
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)

Tactic:
]

Goal state after:
case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal 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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).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 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f
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 g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g