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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ min ((ordFrac R) x) ((ordFrac R) y) ≤ (ordFrac R) (x + y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h : (ordFrac R) x = (ordFrac R) y
⊢ ∃ u, u • x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
⊢ (ordHom x hx) ((ConcreteCategory.hom (X.germToFunctionField U)) f) = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
⊢ ord 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
⊢ ord f x = Multiplicative.toAdd (unzero ⋯)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
hz : coheight z = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ ord f z = n ↔ (ordHom z hz) f = ↑(Multiplicative.ofAdd n)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x y : ↥X
hx : coheight x = 1
hy : coheight y = 1
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
⊢ ord f x ≤ ord g y ↔ (ordHom x hx) f ≤ (ordHom y hy) g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ n ≤ ord f x ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
⊢ a • f ≠ 0

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
⊢ ord f x ≤ ord (a • f) x

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ R x) i) '' s) = ⊤
⊢ Ideal.span s = ⊤

Tactic:
by

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
⊢ V ⊆ ⋃ i, (basicOpen ↑i).carrier

Tactic:
by

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

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

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 ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).carrier

Tactic:
by

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 ⊆ ⋃ i ∈ t, (basicOpen i).carrier
⊢ V ⊆ (zeroLocus t)ᶜ

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) =
    rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ)
      ((mateEquiv adj₄ adj₆) δ)

Tactic:
by

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₁
⊢ (conjugateEquiv adj₁ adj₂) α =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom

Tactic:
by

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 : ι
⊢ Ideal.span (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ⊤

Tactic:
by

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
⊢ U = ⊤

Tactic:
by

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

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₂
⊢ (conjugateEquiv adj₁ adj₂).symm α =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
by

Goal state after:
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
⊢ Scheme.Hom.coborderRange g = ⊤

Tactic:
by

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₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁

Tactic:
by

Goal state after:
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 (Scheme.Hom.coborderRange g).ι

Tactic:
by

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₁
⊢ 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
by

Goal state after:
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 = ⊤
⊢ IsClosedImmersion g

Tactic:
by

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

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₁).symm (𝟙 r₁) = 𝟙 l₁

Tactic:
by

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

Goal state after:
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
⊢ (conjugateEquiv adj (Adjunction.id c)) α = (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
by

Goal state after:
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
⊢ IsIso g

Tactic:
by

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
⊢ sigmaSpec R ≫ f = sigmaSpec R ≫ g

Tactic:
by

Goal state after:
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
⊢ (conjugateEquiv adj (Adjunction.id c)).symm α = adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

Tactic:
by

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

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
⊢ (mateEquiv adj adj) ((λ_ l).hom ≫ (ρ_ l).inv) = (ρ_ r).hom ≫ (λ_ r).inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (conjugateEquiv adj ((Adjunction.id a).comp adj')) ((λ_ l').hom ≫ φ) = (conjugateEquiv adj adj') φ ≫ (ρ_ r').inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (conjugateEquiv adj (adj'.comp (Adjunction.id b))) ((ρ_ l').hom ≫ φ) = (conjugateEquiv adj adj') φ ≫ (λ_ r').inv

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
⊢ Function.Injective (pointsPi R X)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
⊢ (conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂')) (l₁ ◁ φ) = (conjugateEquiv adj₂ adj₂') φ ▷ r₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
⊢ Function.Surjective (pointsPi R X)

Tactic:
rintro f
  refine ⟨Spec.map (CommRingCat.ofHom
    (RingHom.pi fun i ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).1)) ≫ X.isoSpec.inv, ?_⟩
  ext i : 1
  simp only [pointsPi, ← Spec.map_comp_assoc, Iso.comp_inv_eq]
  exact Spec.map_preimage _

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
⊢ Function.Surjective (pointsPi R X)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
⊢ (conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂)) (φ ▷ l₂) = r₂ ◁ (conjugateEquiv adj₁ adj₁') φ

Tactic:
by

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
i : ι
⊢ ∃ j, Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f j))

Tactic:
by

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)))
j₀ : 𝒰.I₀
i : { i // j i = j₀ }
⊢ Set.range ⇑(f ↑i) ⊆ Set.range ⇑(𝒰.f j₀)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₃ : l₃ ⊣ r₃
⊢ (conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃)) (α_ l₁ l₂ l₃).hom = (α_ r₃ r₂ r₁).hom

Tactic:
by

Goal state after:
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₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom =
    𝟙 r₁ ⊗≫
      rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 r₃

Tactic:
by

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))
x✝ : (j₀ : 𝒰.I₀) → ↑(R' j₀)
j₀ : 𝒰.I₀
i : { i // j i = j₀ }
⊢ (fun f x i ↦ f ↑i) ((fun f i ↦ f (j i) ⟨i, ⋯⟩) x✝) j₀ i = x✝ j₀ i

Tactic:
by

Goal state after:
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₁ ⊗≫
      rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫ (λ_ r₃).hom

Tactic:
by

Goal state after:
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₂
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₃) β = (conjugateEquiv adj₁ adj₃) (β ≫ α)

Tactic:
by

Goal state after:
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₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β)

Tactic:
by

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₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₁) β = 𝟙 r₁

Tactic:
by

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₁
⊢ (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 l₁

Tactic:
by

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

Goal state after: