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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ openToLocalizationₗ R M ⊤ x _root_.trivial =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ openToLocalizationₗ R M ⊤ x _root_.trivial =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen
      ((ConcreteCategory.hom ((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen
      ((ConcreteCategory.hom ((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    f.c.app (op ⊤) ≫ ((pushforward CommRingCat f.base).obj X.presheaf).map (Y.toΓSpecMapBasicOpen r).leTop.op

Tactic:
]

Goal state after:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    f.c.app (op ⊤) ≫ ((pushforward CommRingCat f.base).obj X.presheaf).map (Y.toΓSpecMapBasicOpen r).leTop.op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x))
      s =
    (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)))
      s

Tactic:
germ_stalkToLocalizationₗ_assoc,

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x)) s =
    (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)))
      s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(X.basicOpen f) ⊆ ↑U

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(X.basicOpen f) ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x)) s =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen g) x hxg))
      ((ConcreteCategory.hom ((structurePresheafInModuleCat R M).map igU.hom.op)) s)

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x)) s =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen g) x hxg))
      ((ConcreteCategory.hom ((structurePresheafInModuleCat R M).map igU.hom.op)) s)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r))

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : ↑x ∈ X.basicOpen r
⊢ X.basicOpen r ≤ V

Tactic:
simpa [Scheme.image_basicOpen] using! (U.ι.image_mono h₂).trans (U.ι.image_preimage_le _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
x✝ : M
⊢ (ConcreteCategory.hom (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))) x✝ =
    (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
x✝ : M
⊢ (ConcreteCategory.hom (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))) x✝ =
    (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    (algebraMap ↑R ↑((structureSheaf ↑R).presheaf.stalk p)) x ∈
      IsLocalRing.maximalIdeal ↑((structureSheaf ↑R).presheaf.stalk p)

Tactic:
]

Goal state after:
case w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    (algebraMap ↑R ↑((structureSheaf ↑R).presheaf.stalk p)) x ∈
      IsLocalRing.maximalIdeal ↑((structureSheaf ↑R).presheaf.stalk p)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y : C
f : X ⟶ Y
𝒰 : PreZeroHypercover Y
hR : 𝒰.presieve₀ ∈ K.coverings Y
⊢ (∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀),
      P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))) ↔
    ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y : C
f : X ⟶ Y
𝒰 : PreZeroHypercover Y
hR : 𝒰.presieve₀ ∈ K.coverings Y
⊢ (∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀),
      P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))) ↔
    ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
m : M
⊢ (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) (r • (toOpenₗ R M ⊤) m) =
    (ConcreteCategory.hom (toStalk R x)) r •
      (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) m)

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
m : M
⊢ (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) (r • (toOpenₗ R M ⊤) m) =
    (ConcreteCategory.hom (toStalk R x)) r •
      (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) m)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
this : HasPullback f (𝒰.f i)
⊢ P (pullback.snd f (𝒰.f i))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
this : HasPullback f (𝒰.f i)
⊢ P (pullback.snd f (𝒰.f i))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
]

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (pullback.snd f (𝒰.restrictIndexOfSmall.f i))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (pullback.snd f (𝒰.restrictIndexOfSmall.f i))
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
R : Presieve X
hR : R ∈ K.coverings X
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f)

Tactic:
Precoverage.mem_iff_exists_zeroHypercover

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
⊢ (∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)) ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f g → P (g ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
⊢ (∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)) ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f g → P (g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (𝒰.restrictIndexOfSmall.f i ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (𝒰.restrictIndexOfSmall.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of ↑(unop (op (CommRingCat.of R)))))).unop ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app (op ⊤) ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of ↑(unop (op (CommRingCat.of R)))))).unop ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app (op ⊤) ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀),
    MorphismProperty.isomorphisms C (pullback.snd (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀),
    MorphismProperty.isomorphisms C (pullback.snd (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op)

Tactic:
Scheme.Hom.appLE_map,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (Γ.rightOp.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f) ≫
          locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (Γ.rightOp.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f) ≫
          locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ f.unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ f.unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op