mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: R : TopCommRingCat
⊢ Continuous ⇑(RingHom.id R.α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X✝ Y✝ Z✝ : TopCommRingCat
f : { f // Continuous ⇑f }
g : { f // Continuous ⇑f }
⊢ Continuous ⇑((↑g).comp ↑f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ f ≫ ⟨↑e_Ring.symm, ⋯⟩ = 𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ ⟨↑e_Ring.symm, ⋯⟩ ≫ f = 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ const f g₁ U hu₁ * const g₁ g₂ U hu₂ = const f g₂ U hu₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ const g₁ g₂ U hu₂ * const f g₁ U hu₁ = const f g₂ U hu₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (F.map (𝟙 U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
H : g₁ • f₂ = g₂ • f₁
x : ↥(unop (op U))
⊢ ↑(const f₁ g₁ U hu₁) x = ↑(const f₂ g₂ U hu₂) x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ { I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
by

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
U : Opens ↑(PrimeSpectrum.Top R)
m : M
⊢ U ≤ basicOpen 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯) =
    CommRingCat.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ (fun U_1 ↦ U_1 ≤ Scheme.Hom.opensRange U.ι) = fun V ↦ V ≤ U

Tactic:
by

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
U : Opens ↑(PrimeSpectrum.Top R)
x✝¹ x✝ : M
⊢ const (x✝¹ + x✝) 1 U ⋯ = const x✝¹ 1 U ⋯ + const x✝ 1 U ⋯

Tactic:
by

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
U : Opens ↑(PrimeSpectrum.Top R)
x✝¹ : R
x✝ : M
⊢ const (x✝¹ • x✝) 1 U ⋯ = (RingHom.id R) x✝¹ • const x✝ 1 U ⋯

Tactic:
by

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
U : Opens ↑(PrimeSpectrum.Top R)
f : M
⊢ U ≤ basicOpen 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R
⊢ basicOpen f ≤ basicOpen 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop U) ↑x ⋯)) (S ↑x) ≤
    Submonoid.comap (CommRingCat.Hom.hom (F.map i))
      (⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) (S ↑x))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen r

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen r

Tactic:
by
  rw [Scheme.Opens.ι_image_basicOpen', Scheme.basicOpen_res_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.ι ''ᵁ (↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r

Tactic:
by

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
f : R
⊢ ∀ (x : ↥(Submonoid.powers f)),
    IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) ↑x)

Tactic:
simp only [Subtype.forall]
    exact Submonoid.powers_le (P := (IsUnit.submonoid _).comap (algebraMap R _)).mpr
      (isUnit_basicOpen_end ..)

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
f : R
⊢ ∀ (x : ↥(Submonoid.powers f)),
    IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) ↑x)

Tactic:
by

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
s : R
f : M
g : ↥(Submonoid.powers s)
⊢ basicOpen s ≤ basicOpen ↑g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
V : (↑U).Opens
r : ↑Γ(↑U, V)
x : ↥U
⊢ x ∈ (↑U).basicOpen r ↔ ↑x ∈ X.basicOpen r

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ Set.range ⇑U.ι ⊆ Set.range ⇑V.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.homOfLE ⋯ = 𝟙 ↑U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
⊢ Mono F.presheaf.toTotalQuotientPresheaf

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R), f.unop ≫ (x * y) = f.unop ≫ x * f.unop ≫ y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R), f.unop ≫ (x + y) = f.unop ≫ x + f.unop ≫ y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (X.homOfLE e).base = (Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ 1 • s ^ n • f = s ^ n • f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
⊢ 1 ≫ (forget₂ TopCommRingCat TopCat).map φ = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥X
hx : x ∈ U
⊢ (X.homOfLE e) ⟨x, hx⟩ = ⟨x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
g : ↥(Submonoid.powers s)
⊢ (toBasicOpenₗ R M s) (LocalizedModule.mk f g) = const f (↑g) (basicOpen s) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑((X.homOfLE e) x) = ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝¹ x✝ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
⊢ (x✝¹ * x✝) ≫ (forget₂ TopCommRingCat TopCat).map φ =
    x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ * x✝ ≫ (forget₂ TopCommRingCat TopCat).map φ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
⊢ 0 ≫ (forget₂ TopCommRingCat TopCat).map φ = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
y : ↥X
hyU : y ∈ U
hyW : ⟨y, hyU⟩ ∈ ↑(X.homOfLE e ⁻¹ᵁ W)
⊢ ⟨y, ⋯⟩ ∈ ↑W

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
n : ℕ
hn : f ^ n ∈ ⊥.colon {d • a - b • c}
⊢ ⟨f ^ n, ⋯⟩ • d • a = ⟨f ^ n, ⋯⟩ • b • c

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
this : f ∈ (⊥.colon {d • a - b • c}).radical
⊢ LocalizedModule.mk a b = LocalizedModule.mk c d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝¹ x✝ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
⊢ (x✝¹ + x✝) ≫ (forget₂ TopCommRingCat TopCat).map φ =
    x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ + x✝ ≫ (forget₂ TopCommRingCat TopCat).map φ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
y : ↥↑V
hyW : y ∈ ↑W
hyU : (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base) y ∈ ↑U
⊢ ⟨↑y, hyU⟩ ∈ ↑(X.homOfLE e ⁻¹ᵁ W)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
R : TopCommRingCat
X : TopCatᵒᵖ
⊢ continuousFunctions.pullback (𝟙 X) R = 𝟙 (continuousFunctions X R)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R : TopCommRingCat
X : TopCommRingCat
⊢ { app := fun X_1 ↦ continuousFunctions.map X_1 (𝟙 X), naturality := ⋯ } =
    𝟙
      { obj := fun X_1 ↦ continuousFunctions X_1 X, map := fun {x x_1} f ↦ continuousFunctions.pullback f X,
        map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W = V.ι ''ᵁ W ⊓ U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W ≤ V.ι ''ᵁ W

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u : ↥(↑⟨p, hfp⟩).asIdeal.primeCompl
hu : u • ⟨↑d, ⋯⟩ • a = u • ⟨↑b, ⋯⟩ • c
⊢ ↑u ∈ ↑(⊥.colon {d • a - b • c})

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Function.Injective ⇑(toBasicOpenₗ R M f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
W' : (↑U).Opens
e' : W' ≤ X.homOfLE e ⁻¹ᵁ W
⊢ Hom.appLE (X.homOfLE e) W W' e' = X.presheaf.map (homOfLE ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ IsOpenImmersion (X.homOfLE e)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
this : V.ι ''ᵁ ?m.39 ≤ U.ι ''ᵁ W
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).inv = X.presheaf.map (homOfLE ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ 1 • ⟨g j, ⋯⟩ • g i • f j = 1 • ⟨g i * g j, ⋯⟩ • f j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (fun x ↦ V.ι ''ᵁ x) (Hom.opensRange (X.homOfLE e)) = (fun x ↦ V.ι ''ᵁ x) (V.ι ⁻¹ᵁ U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings ↑(⨆ i, U i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U V : X.Opens
i : U ⟶ V
⊢ X.homOfLE ⋯ ≫ (Over.mk V.ι).hom = (Over.mk U.ι).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U : X.Opens
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = 𝟙 (Over.mk U.ι)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = Over.homMk (X.homOfLE ⋯) ⋯ ≫ Over.homMk (X.homOfLE ⋯) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ ∀ {X_1 Y : X.Opensᵒᵖ} (f : X_1 ⟶ Y),
    (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map f ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
      (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
⊢ Set.range ⇑((U.ι ⁻¹ᵁ V).ι ≫ U.ι) = Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : X.Opens
⊢ Set.range ⇑(U.ι ≫ f) = Set.range ⇑(f ''ᵁ U).ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ 1 • ⟨g i * g j, ⋯⟩ • f i = 1 • ⟨g i, ⋯⟩ • g j • f i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ (isoImage f U).hom ≫ Y.homOfLE ⋯ = X.homOfLE e ≫ (isoImage f V).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ (isoImage f U).inv ≫ X.homOfLE e = Y.homOfLE ⋯ ≫ (isoImage f V).inv

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
V : (↑U).Opens
⊢ (Hom.isoImage U.ι V).inv ≫ V.ι = X.homOfLE ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ Set.range ⇑f = Set.range ⇑(opensRange f).ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ (isoOpensRange f).hom ≫ (opensRange f).ι = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ (isoOpensRange f).inv ≫ f = (opensRange f).ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U = V
⊢ Set.range ⇑U.ι = Set.range ⇑V.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.isoOfEq ⋯ = Iso.refl ↑U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ⇑(TopCat.Hom.hom f.base) '' ↑(f ⁻¹ᵁ U) = Set.range ⇑U.ι

Tactic:
Opens.range_ι

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ⇑(TopCat.Hom.hom f.base) '' ↑(f ⁻¹ᵁ U) = ↑U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ↑(f ⁻¹ᵁ U) ≅ ↑U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ V.ι ''ᵁ V.ι ⁻¹ᵁ U = U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι) = Set.range ⇑U.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f : ↑R
⊢ Set.range ⇑(Scheme.Opens.ι (PrimeSpectrum.basicOpen f)) =
    Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f : ↑R
⊢ (basicOpenIsoSpecAway f).hom ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))) =
    Scheme.Opens.ι (PrimeSpectrum.basicOpen f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away x)

Tactic:
by

Goal state after: