case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ ↑(basicOpen X (f * g)) = ↑(basicOpen X f ⊓ basicOpen X g)
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ basicOpen X (f * g) = basicOpen X f ⊓ basicOpen X g
ext1
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ 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)}
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ ↑(basicOpen X (f * g)) = ↑(basicOpen X f ⊓ basicOpen X g)
dsimp [RingedSpace.basicOpen]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ 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)})
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ 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)}
rw [← Set.image_inter Subtype.coe_injective]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ 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)})
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ 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)})
congr
case h.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
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)})
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
⊢ 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)})
ext x
no goals
case h.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj U.op)
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)})
simp [map_mul, Set.mem_image]