case h
X : RingedSpace
V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝.op ⟶ V
f : ↑(X.presheaf.obj X✝.op)
⊢ basicOpen X (↑(X.presheaf.map i) f) = V.unop ⊓ basicOpen X f
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
induction U using Opposite.rec'
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
case h
X : RingedSpace
V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝.op ⟶ V
f : ↑(X.presheaf.obj X✝.op)
⊢ basicOpen X (↑(X.presheaf.map i) f) = V.unop ⊓ basicOpen X f
induction V using Opposite.rec'
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
g : X✝.op.unop ⟶ X✝¹.op.unop := i.unop
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
let g := i.unop
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
g : X✝.op.unop ⟶ X✝¹.op.unop := i.unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
g : X✝.op.unop ⟶ X✝¹.op.unop := i.unop
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
have : i = g.op := rfl
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
g : X✝.op.unop ⟶ X✝¹.op.unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
g : X✝.op.unop ⟶ X✝¹.op.unop := i.unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
clear_value g
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
⊢ basicOpen X (↑(X.presheaf.map g.op) f) = X✝.op.unop ⊓ basicOpen X f
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
i : X✝¹.op ⟶ X✝.op
g : X✝.op.unop ⟶ X✝¹.op.unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = X✝.op.unop ⊓ basicOpen X f
subst this
case h.h.h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) ↔ x✝ ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
⊢ basicOpen X (↑(X.presheaf.map g.op) f) = X✝.op.unop ⊓ basicOpen X f
ext
case h.h.h.h.mp
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) → x✝ ∈ ↑(X✝.op.unop ⊓ basicOpen X f)

case h.h.h.h.mpr
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(X✝.op.unop ⊓ basicOpen X f) → x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
case h.h.h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) ↔ x✝ ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
constructor
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝.op.unop }
hx : IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map g.op) f))
⊢ ↑x ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
case h.h.h.h.mp
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) → x✝ ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
rintro ⟨x, hx : IsUnit _, rfl⟩
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝.op.unop }
hx : IsUnit (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑X✝¹.op.unop) }) x)) f)
⊢ ↑x ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝.op.unop }
hx : IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map g.op) f))
⊢ ↑x ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
erw [show X.presheaf.germ x ((X.presheaf.map g.op) f) = X.presheaf.germ (g x) f
 from X.presheaf.germ_res_apply _ _ _] at hx
no goals
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝.op.unop }
hx : IsUnit (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑X✝¹.op.unop) }) x)) f)
⊢ ↑x ∈ ↑(X✝.op.unop ⊓ basicOpen X f)
exact ⟨x.2, g x, hx, rfl⟩
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝¹.op.unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑X✝.op.unop
⊢ ↑x ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
case h.h.h.h.mpr
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(X✝.op.unop ⊓ basicOpen X f) → x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
rintro ⟨hxV, x, hx, rfl⟩
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝¹.op.unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑X✝.op.unop
⊢ IsUnit (↑(germ X.presheaf { val := ↑x, property := hxV }) (↑(X.presheaf.map g.op) f))
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝¹.op.unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑X✝.op.unop
⊢ ↑x ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
refine' ⟨⟨x, hxV⟩, (_ : IsUnit _), rfl⟩
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝¹.op.unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑X✝.op.unop
⊢ IsUnit
    (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑X✝¹.op.unop) }) { val := ↑x, property := hxV }))
      f)
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝¹.op.unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑X✝.op.unop
⊢ IsUnit (↑(germ X.presheaf { val := ↑x, property := hxV }) (↑(X.presheaf.map g.op) f))
erw [show X.presheaf.germ ⟨x, hxV⟩ (X.presheaf.map g.op f) = X.presheaf.germ (g ⟨x, hxV⟩) f from
  X.presheaf.germ_res_apply _ _ _]
no goals
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj X✝¹.op)
X✝ : Opens ↑↑X.toPresheafedSpace
g : X✝.op.unop ⟶ X✝¹.op.unop
x : { x // x ∈ X✝¹.op.unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑X✝.op.unop
⊢ IsUnit
    (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑X✝¹.op.unop) }) { val := ↑x, property := hxV }))
      f)
exact hx