Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/pp.all

Created May 20, 2018 17:03
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save kbuzzard/0ec44e3153d62e9c02d9525abe05c82b to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save kbuzzard/0ec44e3153d62e9c02d9525abe05c82b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
pp.all
X : Type u,
_inst_1 : topological_space.{u} X,
B : set.{u} (set.{u} X),
HB : @topological_space.is_topological_basis.{u} X _inst_1 B,
FPRB : @presheaf_of_rings_on_basis.{u} X _inst_1 B HB,
x : X,
Hstandard :
∀ (U V : set.{u} X),
@has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) U B →
@has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) V B →
@has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X))
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) U V)
B,
a1 b1 c1 : @presheaf_of_rings_on_basis_stalk.stalk.{u} X _inst_1 B HB FPRB x Hstandard,
Ua : set.{u} X,
BUa : @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) Ua B,
Hxa : @has_mem.mem.{u u} X (set.{u} X) (@set.has_mem.{u} X) x Ua,
sa :
@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ua
BUa,
Ub : set.{u} X,
BUb : @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) Ub B,
Hxb : @has_mem.mem.{u u} X (set.{u} X) (@set.has_mem.{u} X) x Ub,
sb :
@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ub
BUb,
Uc : set.{u} X,
BUc : @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) Uc B,
Hxc : @has_mem.mem.{u u} X (set.{u} X) (@set.has_mem.{u} X) x Uc,
sc :
@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Uc
BUc,
H :
@eq.{u+1} (set.{u} X)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
Uc)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ub Uc))
⊢ @eq.{u+1} (@presheaf_of_rings_on_basis_stalk.stalk.aux.{u} X _inst_1 B HB FPRB x Hstandard)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
Uc)
(@_private.2711455563.add_aux._proof_1.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_1.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_2.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@has_add.add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@distrib.to_has_add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@ring.to_distrib.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@comm_ring.to_ring.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@presheaf_of_rings_on_basis.Fring.{u} X _inst_1 B HB FPRB
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_4.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))))))
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ua
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_5.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa))
(@_private.2711455563.add_aux._proof_6.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_7.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
sa)
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ub
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_8.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_9.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_10.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
sb)))
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Uc
BUc
Hxc
sc))
(@_private.2711455563.add_aux._proof_2.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_1.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_2.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@has_add.add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@distrib.to_has_add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@ring.to_distrib.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@comm_ring.to_ring.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@presheaf_of_rings_on_basis.Fring.{u} X _inst_1 B HB FPRB
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_4.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))))))
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ua
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_5.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa))
(@_private.2711455563.add_aux._proof_6.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_7.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
sa)
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ub
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_8.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_9.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_10.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
sb)))
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Uc
BUc
Hxc
sc))
(@has_add.add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
Uc)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_1.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_2.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@has_add.add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@distrib.to_has_add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@ring.to_distrib.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@comm_ring.to_ring.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ub
BUb
Hxb
sb)))
(@presheaf_of_rings_on_basis.Fring.{u} X _inst_1 B HB FPRB
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_4.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ub
BUb
Hxb
sb))))))
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ua
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_5.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa))
(@_private.2711455563.add_aux._proof_6.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_7.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
sa)
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ub
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_8.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_9.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_10.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
sb)))
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Uc
BUc
Hxc
sc)))
(@distrib.to_has_add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
Uc)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_1.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@_private.2711455563.add_aux._proof_2.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb))
(@has_add.add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@distrib.to_has_add.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
x
Ub
BUb
Hxb
sb)))
(@ring.to_distrib.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ub
BUb
Hxb
sb)))
(@comm_ring.to_ring.{u}
(@presheaf_of_types_on_basis.F.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_3.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ub
BUb
Hxb
sb)))
(@presheaf_of_rings_on_basis.Fring.{u} X _inst_1 B HB FPRB
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_4.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ua
BUa
Hxa
sa)
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB
FPRB)
x
Ub
BUb
Hxb
sb))))))
(@presheaf_of_types_on_basis.res.{u} X _inst_1 B HB
(@presheaf_of_rings_on_basis.to_presheaf_of_types_on_basis.{u} X _inst_1 B HB FPRB)
Ua
(@has_inter.inter.{u} (set.{u} X) (@set.has_inter.{u} X) Ua Ub)
(@_private.2711455563.add_aux._proof_5.{u} X _inst_1 B HB FPRB x Hstandard
(@presheaf_on_basis_stalk.aux.mk.{u} X _inst_1 B HB (… B HB FPRB) x Ua BUa Hxa sa))
…
…
sa)
…))
…))
…)
…
…))
…
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment