X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ IsUnit f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit f
choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x (h x)
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ U ≤ iSup V

X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
⊢ IsUnit f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ IsUnit f
have hcover : U ≤ iSup V
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
⊢ IsUnit f
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ U ≤ iSup V

X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
⊢ IsUnit f
. intro x hxU
  erw [Opens.mem_iSup]
  exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsUnit f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
⊢ IsUnit f
choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsCompatible (sheaf X).val V g

X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
⊢ IsUnit f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsUnit f
have ic : IsCompatible (sheaf X).val V g
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ IsUnit f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
⊢ IsUnit f
obtain ⟨gl, gl_spec, -⟩ := X.sheaf.existsUnique_gluing' V U iVU hcover g ic
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ f * gl = 1
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ IsUnit f
apply isUnit_of_mul_eq_one f gl
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ ∀ (i : { x // x ∈ U }),
    (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) (f * gl) =
      (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) 1
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ f * gl = 1
apply X.sheaf.eq_of_locally_eq' V U iVU hcover
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) (f * gl) =
    (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ ∀ (i : { x // x ∈ U }),
    (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) (f * gl) =
      (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) 1
intro i
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) (f * gl) = ↑((sheaf X).val.map (iVU i).op) 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) (f * gl) =
    (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) 1
change X.sheaf.1.map _ _ = X.sheaf.1.map _ 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) f * ↑((sheaf X).val.map (iVU i).op) gl = 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) (f * gl) = ↑((sheaf X).val.map (iVU i).op) 1
rw [RingHom.map_one, RingHom.map_mul]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
i : { x // x ∈ U }
gl_spec : (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ ↑((sheaf X).val.map (iVU i).op) f * ↑((sheaf X).val.map (iVU i).op) gl = 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
gl_spec : ∀ (i : { x // x ∈ U }), (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) f * ↑((sheaf X).val.map (iVU i).op) gl = 1
specialize gl_spec i
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
i : { x // x ∈ U }
gl_spec : ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ ↑((sheaf X).val.map (iVU i).op) f * ↑((sheaf X).val.map (iVU i).op) gl = 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
i : { x // x ∈ U }
gl_spec : (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (iVU i).op) gl = g i
⊢ ↑((sheaf X).val.map (iVU i).op) f * ↑((sheaf X).val.map (iVU i).op) gl = 1
change X.sheaf.1.map _ _ = _ at gl_spec
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
i : { x // x ∈ U }
gl_spec : ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ ↑((sheaf X).val.map (iVU i).op) f * g i = 1
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
i : { x // x ∈ U }
gl_spec : ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ ↑((sheaf X).val.map (iVU i).op) f * ↑((sheaf X).val.map (iVU i).op) gl = 1
rw [gl_spec]
no goals
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj U.op)
i : { x // x ∈ U }
gl_spec : ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ ↑((sheaf X).val.map (iVU i).op) f * g i = 1
exact hg i
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ U ≤ iSup V
intro x hxU
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
erw [Opens.mem_iSup]
no goals
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x) =
    (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y)
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsCompatible (sheaf X).val V g
intro x y
case ic.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ ∀ (x_1 : { x_1 // x_1 ∈ V x ⊓ V y }),
    (CategoryTheory.forget CommRingCat).map (germ (Sheaf.presheaf (sheaf X)) x_1)
        ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
      (CategoryTheory.forget CommRingCat).map (germ (Sheaf.presheaf (sheaf X)) x_1)
        ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x) =
    (CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y)
apply section_ext X.sheaf (V x ⊓ V y)
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (CategoryTheory.forget CommRingCat).map
      (germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
    (CategoryTheory.forget CommRingCat).map
      (germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
case ic.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ ∀ (x_1 : { x_1 // x_1 ∈ V x ⊓ V y }),
    (CategoryTheory.forget CommRingCat).map (germ (Sheaf.presheaf (sheaf X)) x_1)
        ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
      (CategoryTheory.forget CommRingCat).map (germ (Sheaf.presheaf (sheaf X)) x_1)
        ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
rintro ⟨z, hzVx, hzVy⟩
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (CategoryTheory.forget CommRingCat).map
      (Limits.colimit.ι
        (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
          Sheaf.presheaf (sheaf X))
        { obj := V x, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V x)) }.op)
      (g x) =
    (CategoryTheory.forget CommRingCat).map
      (Limits.colimit.ι
        (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
          Sheaf.presheaf (sheaf X))
        { obj := V y, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V y)) }.op)
      (g y)
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (CategoryTheory.forget CommRingCat).map
      (germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
    (CategoryTheory.forget CommRingCat).map
      (germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      ((CategoryTheory.forget CommRingCat).map ((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
erw [germ_res_apply, germ_res_apply]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V x, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V x)) }.op)
        (g x) =
    ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V y, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V y)) }.op)
        (g y)
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (CategoryTheory.forget CommRingCat).map
      (Limits.colimit.ι
        (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
          Sheaf.presheaf (sheaf X))
        { obj := V x, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V x)) }.op)
      (g x) =
    (CategoryTheory.forget CommRingCat).map
      (Limits.colimit.ι
        (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
          Sheaf.presheaf (sheaf X))
        { obj := V y, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V y)) }.op)
      (g y)
apply (IsUnit.mul_right_inj (h ⟨z, (iVU x).le hzVx⟩)).mp
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V x, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V x)) }.op)
        (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V y, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V y)) }.op)
        (g y)
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V x, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V x)) }.op)
        (g x) =
    ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V y, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V y)) }.op)
        (g y)
rw [←show X.presheaf.germ ⟨z, hzVx⟩ (X.presheaf.map (iVU x).op f) =
  X.presheaf.germ ⟨z, ((iVU x) ⟨z, hzVx⟩).2⟩ f from
  X.presheaf.germ_res_apply (iVU x) ⟨z, hzVx⟩ f]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ X.presheaf { val := z, property := hzVx }) (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ X.presheaf { val := z, property := hzVy }) (g y)
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V x, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V x)) }.op)
        (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      (CategoryTheory.forget CommRingCat).map
        (Limits.colimit.ι
          (Functor.op (OpenNhds.inclusion ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }) ⋙
            Sheaf.presheaf (sheaf X))
          { obj := V y, property := (_ : ↑{ val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) } ∈ ↑(V y)) }.op)
        (g y)
change X.presheaf.germ ⟨z, hzVx⟩ _ * (X.presheaf.germ ⟨z, hzVx⟩ _) =
  X.presheaf.germ ⟨z, hzVx⟩ _ * X.presheaf.germ ⟨z, hzVy⟩ (g y)
no goals
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => ↑(X.presheaf.obj (V x).op)) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ X.presheaf { val := z, property := hzVx }) (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ X.presheaf { val := z, property := hzVy }) (g y)
rw [← RingHom.map_mul,
  congr_arg (X.presheaf.germ (⟨z, hzVx⟩ : V x)) (hg x),
  show X.presheaf.germ ⟨z, hzVx⟩ (X.presheaf.map (iVU x).op f) =
    X.presheaf.germ ⟨z, ((iVU x) ⟨z, hzVx⟩).2⟩ f from X.presheaf.germ_res_apply _ _ f,
  ← show X.presheaf.germ ⟨z, hzVy⟩ (X.presheaf.map (iVU y).op f) =
      X.presheaf.germ ⟨z, ((iVU x) ⟨z, hzVx⟩).2⟩ f from
      X.presheaf.germ_res_apply (iVU y) ⟨z, hzVy⟩ f,
  ← RingHom.map_mul,
  congr_arg (X.presheaf.germ (⟨z, hzVy⟩ : V y)) (hg y), RingHom.map_one, RingHom.map_one]