[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
obtain ⟨g', heq⟩ := h.exists_right_inv
[GOAL]
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
g' : (CategoryTheory.forget CommRingCat).obj (stalk X.presheaf ↑x)
heq : ↑(germ X.presheaf x) f * g' = 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.germ_exist x.1 g'
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
let W := U ⊓ V
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
have hxW : x.1 ∈ W :=
  ⟨x.2, hxV⟩
    -- Porting note : `erw` can't write into `HEq`, so this is replaced with another `HEq` in the
      -- desired form
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
replace heq :
  (X.presheaf.germ ⟨x.val, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) =
    (X.presheaf.germ ⟨x.val, hxW⟩) 1
[GOAL]
case heq
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
[PROOFSTEP]
dsimp [germ]
[GOAL]
case heq
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ↑(Limits.colimit.ι ((OpenNhds.inclusion ↑x).op ⋙ X.presheaf)
          (op { obj := U ⊓ V, property := (_ : ↑{ val := ↑x, property := hxW } ∈ U ⊓ V) }))
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(Limits.colimit.ι ((OpenNhds.inclusion ↑x).op ⋙ X.presheaf)
          (op { obj := U ⊓ V, property := (_ : ↑{ val := ↑x, property := hxW } ∈ U ⊓ V) }))
      1
[PROOFSTEP]
erw [map_mul, map_one,
  show X.presheaf.germ ⟨x, hxW⟩ ((X.presheaf.map (U.infLELeft V).op) f) = X.presheaf.germ x f from
    X.presheaf.germ_res_apply (Opens.infLELeft U V) ⟨x.1, hxW⟩ f,
  show X.presheaf.germ ⟨x, hxW⟩ (X.presheaf.map (U.infLERight V).op g) = X.presheaf.germ ⟨x, hxV⟩ g from
    X.presheaf.germ_res_apply (Opens.infLERight U V) ⟨x.1, hxW⟩ g]
[GOAL]
case heq
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
[PROOFSTEP]
exact heq
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
obtain ⟨W', hxW', i₁, i₂, heq'⟩ := X.presheaf.germ_eq x.1 hxW hxW _ _ heq
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  ↑(X.presheaf.map i₁.op)
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(X.presheaf.map i₂.op) 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
use W', i₁ ≫ Opens.infLELeft U V, hxW'
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  ↑(X.presheaf.map i₁.op)
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(X.presheaf.map i₂.op) 1
⊢ IsUnit (↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f)
[PROOFSTEP]
rw [(X.presheaf.map i₂.op).map_one, (X.presheaf.map i₁.op).map_mul] at heq' 
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  ↑(X.presheaf.map i₁.op) (↑(X.presheaf.map (Opens.infLELeft U V).op) f) *
      ↑(X.presheaf.map i₁.op) (↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    1
⊢ IsUnit (↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f)
[PROOFSTEP]
rw [← comp_apply, ← X.presheaf.map_comp, ← comp_apply, ← X.presheaf.map_comp, ← op_comp] at heq' 
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' : ↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f * ↑(X.presheaf.map ((Opens.infLERight U V).op ≫ i₁.op)) g = 1
⊢ IsUnit (↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f)
[PROOFSTEP]
exact isUnit_of_mul_eq_one _ _ heq'
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit f
[PROOFSTEP]
choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x (h x)
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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
[PROOFSTEP]
have hcover : U ≤ iSup V
[GOAL]
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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
[PROOFSTEP]
intro x hxU
[GOAL]
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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)
[PROOFSTEP]
erw [Opens.mem_iSup]
[GOAL]
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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
[PROOFSTEP]
exact
  ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
    -- Let `g x` denote the inverse of `f` in `U x`.
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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
[PROOFSTEP]
choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsUnit f
[PROOFSTEP]
have ic : IsCompatible (sheaf X).val V g
[GOAL]
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsCompatible (sheaf X).val V g
[PROOFSTEP]
intro x y
[GOAL]
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x) =
    ↑((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y)
[PROOFSTEP]
apply section_ext X.sheaf (V x ⊓ V y)
[GOAL]
case ic.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 }),
    ↑(germ (Sheaf.presheaf (sheaf X)) x_1) (↑((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
      ↑(germ (Sheaf.presheaf (sheaf X)) x_1) (↑((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
[PROOFSTEP]
rintro ⟨z, hzVx, hzVy⟩
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      (↑((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
    ↑(germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      (↑((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
[PROOFSTEP]
erw [germ_res_apply, germ_res_apply]
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (Sheaf.presheaf (sheaf X))
          ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V x)) })
            { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
      (g x) =
    ↑(germ (Sheaf.presheaf (sheaf X))
          ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V y)) })
            { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
      (g y)
[PROOFSTEP]
apply (IsUnit.mul_right_inj (h ⟨z, (iVU x).le hzVx⟩)).mp
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V x)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g x) =
    ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V y)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g y)
[PROOFSTEP]
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]
  -- Porting note : change was not necessary in Lean3
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V x)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V y)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g y)
[PROOFSTEP]
change
  X.presheaf.germ ⟨z, hzVx⟩ _ * (X.presheaf.germ ⟨z, hzVx⟩ _) =
    X.presheaf.germ ⟨z, hzVx⟩ _ * X.presheaf.germ ⟨z, hzVy⟩ (g y)
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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)
[PROOFSTEP]
rw [← RingHom.map_mul, congr_arg (X.presheaf.germ (⟨z, hzVx⟩ : V x)) (hg x),
  -- Porting note : now need explicitly typing the rewritesshow
    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,
  -- Porting note : now need explicitly typing the rewrites←
  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]
  -- We claim that these local inverses glue together to a global inverse of `f`.
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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
[PROOFSTEP]
obtain ⟨gl, gl_spec, -⟩ := X.sheaf.existsUnique_gluing' V U iVU hcover g ic
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ IsUnit f
[PROOFSTEP]
apply isUnit_of_mul_eq_one f gl
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ f * gl = 1
[PROOFSTEP]
apply X.sheaf.eq_of_locally_eq' V U iVU hcover
[GOAL]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((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
[PROOFSTEP]
intro i
[GOAL]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((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
[PROOFSTEP]
rw [RingHom.map_one, RingHom.map_mul, gl_spec]
[GOAL]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
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 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) 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 (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) f * g i = 1
[PROOFSTEP]
exact hg i
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsOpen (Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)})
[PROOFSTEP]
rw [isOpen_iff_forall_mem_open]
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ (x : ↑↑X.toPresheafedSpace),
    x ∈ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} →
      ∃ t, t ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
⊢ ∃ t, t ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen t ∧ ↑x ∈ t
[PROOFSTEP]
obtain ⟨V, i, hxV, hf⟩ := X.isUnit_res_of_isUnit_germ U f x hx
[GOAL]
case intro.intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
⊢ ∃ t, t ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen t ∧ ↑x ∈ t
[PROOFSTEP]
use V.1
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
⊢ V.carrier ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen V.carrier ∧ ↑x ∈ V.carrier
[PROOFSTEP]
refine' ⟨_, V.2, hxV⟩
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
⊢ V.carrier ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)}
[PROOFSTEP]
intro y hy
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ y ∈ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)}
[PROOFSTEP]
use(⟨y, i.le hy⟩ : U)
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ { val := y, property := (_ : y ∈ ↑U) } ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧
    ↑{ val := y, property := (_ : y ∈ ↑U) } = y
[PROOFSTEP]
rw [Set.mem_setOf_eq]
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ IsUnit (↑(germ X.presheaf { val := y, property := (_ : y ∈ ↑U) }) f) ∧ ↑{ val := y, property := (_ : y ∈ ↑U) } = y
[PROOFSTEP]
constructor
[GOAL]
case h.left
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ IsUnit (↑(germ X.presheaf { val := y, property := (_ : y ∈ ↑U) }) f)
[PROOFSTEP]
convert RingHom.isUnit_map (X.presheaf.germ ⟨y, hy⟩) hf
[GOAL]
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ ↑(germ X.presheaf { val := y, property := (_ : y ∈ ↑U) }) f =
    ↑(germ X.presheaf { val := y, property := hy }) (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
exact (X.presheaf.germ_res_apply i ⟨y, hy⟩ f).symm
[GOAL]
case h.right
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ ↑{ val := y, property := (_ : y ∈ ↑U) } = y
[PROOFSTEP]
rfl
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f ↔ IsUnit (↑(germ X.presheaf x) f)
[PROOFSTEP]
constructor
[GOAL]
case mp
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f → IsUnit (↑(germ X.presheaf x) f)
[PROOFSTEP]
rintro ⟨x, hx, a⟩
[GOAL]
case mp.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x✝ x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x✝
⊢ IsUnit (↑(germ X.presheaf x✝) f)
[PROOFSTEP]
cases Subtype.eq a
[GOAL]
case mp.intro.intro.refl
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x
⊢ IsUnit (↑(germ X.presheaf x) f)
[PROOFSTEP]
exact hx
[GOAL]
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
⊢ IsUnit (↑(germ X.presheaf x) f) → ↑x ∈ basicOpen X f
[PROOFSTEP]
intro h
[GOAL]
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑x ∈ basicOpen X f
[PROOFSTEP]
exact ⟨x, h, rfl⟩
[GOAL]
X : RingedSpace
f : ↑(X.presheaf.obj (op ⊤))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ basicOpen X f ≤ U
[PROOFSTEP]
rintro _ ⟨x, _, rfl⟩
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
left✝ : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
⊢ ↑x ∈ ↑U
[PROOFSTEP]
exact x.2
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsUnit (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f)
[PROOFSTEP]
apply isUnit_of_isUnit_germ
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ (x : { x // x ∈ basicOpen X f }),
    IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
[PROOFSTEP]
rintro ⟨_, ⟨x, (hx : IsUnit _), rfl⟩⟩
[GOAL]
case h.mk.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit
    (↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
[PROOFSTEP]
convert hx
[GOAL]
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f) =
    ↑(germ X.presheaf x) f
[PROOFSTEP]
convert X.presheaf.germ_res_apply _ _ _
[GOAL]
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) = V.unop ⊓ basicOpen X f
[PROOFSTEP]
induction U using Opposite.rec'
[GOAL]
case h
X : RingedSpace
V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝ ⟶ V
f : ↑(X.presheaf.obj (op X✝))
⊢ basicOpen X (↑(X.presheaf.map i) f) = V.unop ⊓ basicOpen X f
[PROOFSTEP]
induction V using Opposite.rec'
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
let g := i.unop
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
g : (op X✝).unop ⟶ (op X✝¹).unop := i.unop
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
have : i = g.op := rfl
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
g : (op X✝).unop ⟶ (op X✝¹).unop := i.unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
clear_value g
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
g : (op X✝).unop ⟶ (op X✝¹).unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
subst this
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
⊢ basicOpen X (↑(X.presheaf.map g.op) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
ext
[GOAL]
case h.h.h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) ↔ x✝ ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
constructor
[GOAL]
case h.h.h.h.mp
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) → x✝ ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
rintro ⟨x, hx : IsUnit _, rfl⟩
[GOAL]
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝).unop }
hx : IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map g.op) f))
⊢ ↑x ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
erw [X.presheaf.germ_res_apply _ _ _] at hx 
[GOAL]
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝).unop }
hx : IsUnit (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op X✝¹).unop) }) x)) f)
⊢ ↑x ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
exact ⟨x.2, g x, hx, rfl⟩
[GOAL]
case h.h.h.h.mpr
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑((op X✝).unop ⊓ basicOpen X f) → x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
[PROOFSTEP]
rintro ⟨hxV, x, hx, rfl⟩
[GOAL]
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝¹).unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑(op X✝).unop
⊢ ↑x ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
[PROOFSTEP]
refine' ⟨⟨x, hxV⟩, (_ : IsUnit _), rfl⟩
[GOAL]
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝¹).unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑(op X✝).unop
⊢ IsUnit (↑(germ X.presheaf { val := ↑x, property := hxV }) (↑(X.presheaf.map g.op) f))
[PROOFSTEP]
erw [X.presheaf.germ_res_apply _ _ _]
[GOAL]
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝¹).unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑(op X✝).unop
⊢ IsUnit
    (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op X✝¹).unop) }) { val := ↑x, property := hxV }))
      f)
[PROOFSTEP]
exact hx
[GOAL]
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) = basicOpen X f
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X f
[PROOFSTEP]
rw [X.basicOpen_res i f]
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ V.unop ⊓ basicOpen X f ≤ basicOpen X f
[PROOFSTEP]
exact inf_le_right
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
have := X.basicOpen_res (inv i) (X.presheaf.map i f)
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(X.presheaf.map (inv i)) (↑(X.presheaf.map i) f)) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
rw [← comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id, id_apply] at this 
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X f = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
rw [this]
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X f = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
exact inf_le_right
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ basicOpen X (f * g) = basicOpen X f ⊓ basicOpen X g
[PROOFSTEP]
ext1
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ ↑(basicOpen X (f * g)) = ↑(basicOpen X f ⊓ basicOpen X g)
[PROOFSTEP]
dsimp [RingedSpace.basicOpen]
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} =
    Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∩ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) g)}
[PROOFSTEP]
rw [← Set.image_inter Subtype.coe_injective]
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} =
    (fun a => ↑a) '' ({x | IsUnit (↑(germ X.presheaf x) f)} ∩ {x | IsUnit (↑(germ X.presheaf x) g)})
[PROOFSTEP]
congr
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} =
    (fun a => ↑a) '' ({x | IsUnit (↑(germ X.presheaf x) f)} ∩ {x | IsUnit (↑(germ X.presheaf x) g)})
[PROOFSTEP]
ext x
[GOAL]
case h.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} ↔
    x ∈ (fun a => ↑a) '' ({x | IsUnit (↑(germ X.presheaf x) f)} ∩ {x | IsUnit (↑(germ X.presheaf x) g)})
[PROOFSTEP]
simp [map_mul, Set.mem_image]
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ basicOpen X f = U
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ basicOpen X f ≤ U
[PROOFSTEP]
exact X.basicOpen_le f
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ U ≤ basicOpen X f
[PROOFSTEP]
intro x hx
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(basicOpen X f)
[PROOFSTEP]
erw [X.mem_basicOpen f (⟨x, hx⟩ : U)]
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ IsUnit (↑(germ X.presheaf { val := x, property := hx }) f)
[PROOFSTEP]
exact RingHom.isUnit_map _ hf
