# mathlibdocumentation

core.init.core

def id_delta {α : Sort u} :
α → α

The kernel definitional equality test (t =?= s) has special support for id_delta applications. It implements the following rules

1) (id_delta t) =?= t 2) t =?= (id_delta t) 3) (id_delta t) =?= s IF (unfold_of t) =?= s 4) t =?= id_delta s IF t =?= (unfold_of s)

This is mechanism for controlling the delta reduction (aka unfolding) used in the kernel.

We use id_delta applications to address performance problems when type checking lemmas generated by the equation compiler.

def opt_param (α : Sort u) :
α → Sort u

def out_param  :
Sort uSort u

Gadget for marking output parameters in type classes.

def id_rhs (α : Sort u) :
α → α

inductive punit  :
Sort u

def unit  :
Type

An abbreviation for punit.{0}, its most common instantiation. This type should be preferred over punit where possible to avoid unnecessary universe parameters.

def thunk  :
Type uType u

Gadget for defining thunks, thunk parameters have special treatment. Example: given def f (s : string) (t : thunk nat) : nat an application f "hello" 10 is converted into f "hello" (λ _, 10)

inductive true  :
Prop

constant false  :
Prop

constant empty  :
Type

def not  :
Prop → Prop

Logical not.

not P, with notation ¬ P, is the Prop which is true if and only if P is false. It is internally represented as P → false, so one way to prove a goal ⊢ ¬ P is to use intro h, which gives you a new hypothesis h : P and the goal ⊢ false.

A hypothesis h : ¬ P can be used in term mode as a function, so if w : P then h w : false.

Related mathlib tactic: contrapose.

inductive eq {α : Sort u} :
α → α → Prop
• refl : ∀ {α : Sort u} (a : α), a = a

inductive heq {α : Sort u} (a : α) {β : Sort u} :
β → Prop
• refl : ∀ {α : Sort u} (a : α), a == a

Heterogeneous equality.

Its purpose is to write down equalities between terms whose types are not definitionally equal. For example, given x : vector α n and y : vector α (0+n), x = y doesn't typecheck but x == y does.

If you have a goal ⊢ x == y, your first instinct should be to ask (either yourself, or on zulip) if something has gone wrong already. If you really do need to follow this route, you may find the lemmas eq_rec_heq and eq_mpr_heq useful.

structure prod  :
Type uType vType (max u v)
• fst : α
• snd : β

structure pprod  :
Sort uSort vSort (max 1 u v)
• fst : α
• snd : β

Similar to prod, but α and β can be propositions. We use this type internally to automatically generate the brec_on recursor.

structure and  :
Prop → Prop → Prop
• left : a
• right : b

Logical and.

and P Q, with notation P ∧ Q, is the Prop which is true precisely when P and Q are both true.

To prove a goal ⊢ P ∧ Q, you can use the tactic split, which gives two separate goals ⊢ P and ⊢ Q.

Given a hypothesis h : P ∧ Q, you can use the tactic cases h with hP hQ to obtain two new hypotheses hP : P and hQ : Q. See also the obtain or rcases tactics in mathlib.

def and.elim_left {a b : Prop} :
a b → a

def and.elim_right {a b : Prop} :
a b → b

def rfl {α : Sort u} {a : α} :
a = a

theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} :
a = bP aP b

theorem eq.trans {α : Sort u} {a b c : α} :
a = bb = ca = c

theorem eq.symm {α : Sort u} {a b : α} :
a = bb = a

def heq.rfl {α : Sort u} {a : α} :
a == a

theorem eq_of_heq {α : Sort u} {a a' : α} :
a == a'a = a'

inductive sum  :
Type uType vType (max u v)
• inl : Π (α : Type u) (β : Type v), α → α β
• inr : Π (α : Type u) (β : Type v), β → α β

inductive psum  :
Sort uSort vSort (max 1 u v)
• inl : Π (α : Sort u) (β : Sort v), α → psum α β
• inr : Π (α : Sort u) (β : Sort v), β → psum α β

inductive or  :
Prop → Prop → Prop
• inl : ∀ (a b : Prop), a → a b
• inr : ∀ (a b : Prop), b → a b

Logical or.

or P Q, with notation P ∨ Q, is the proposition which is true if and only if P or Q is true.

To prove a goal ⊢ P ∨ Q, if you know which alternative you want to prove, you can use the tactics left (which gives the goal ⊢ P) or right (which gives the goal ⊢ Q).

Given a hypothesis h : P ∨ Q and goal ⊢ R, the tactic cases h will give you two copies of the goal ⊢ R, with the hypothesis h : P in the first, and the hypothesis h : Q in the second.

def or.intro_left {a : Prop} (b : Prop) :
a → a b

def or.intro_right (a : Prop) {b : Prop} :
b → a b

structure sigma {α : Type u} :
(α → Type v)Type (max u v)
• fst : α
• snd : β c.fst

structure psigma {α : Sort u} :
(α → Sort v)Sort (max 1 u v)
• fst : α
• snd : β c.fst

inductive bool  :
Type

structure subtype {α : Sort u} :
(α → Prop)Sort (max 1 u)
• val : α
• property : p c.val

@[class]
inductive decidable  :
Prop → Type
• is_false : Π (p : Prop), ¬p →
• is_true : Π (p : Prop), p →

Instances
def decidable_pred {α : Sort u} :
(α → Prop)Sort (max u 1)

Equations
Instances
def decidable_rel {α : Sort u} :
(α → α → Prop)Sort (max u 1)

Equations
Instances
def decidable_eq  :
Sort uSort (max u 1)

Equations
Instances
inductive option  :
Type uType u
• none : Π (α : Type u),
• some : Π (α : Type u), α →

inductive list  :
Type uType u
• nil : Π (T : Type u), list T
• cons : Π (T : Type u), T → list Tlist T

inductive nat  :
Type

structure unification_constraint  :
Type (u+1)
• α : Type ?
• lhs : c.α
• rhs : c.α

structure unification_hint  :
Type (max (u_1+1) (u_2+1))

@[ext, class]
structure has_zero  :
Type uType u
• zero : α

Instances
@[class]
structure has_one  :
Type uType u
• one : α

Instances
@[class]
Type uType u
• add : α → α → α

Instances
@[class]
structure has_mul  :
Type uType u
• mul : α → α → α

Instances
@[class]
structure has_inv  :
Type uType u
• inv : α → α

Instances
@[class]
structure has_neg  :
Type uType u
• neg : α → α

Instances
@[class]
structure has_sub  :
Type uType u
• sub : α → α → α

Instances
@[class]
structure has_div  :
Type uType u
• div : α → α → α

Instances
@[class]
structure has_dvd  :
Type uType u
• dvd : α → α → Prop

Instances
@[class]
structure has_mod  :
Type uType u
• mod : α → α → α

Instances
@[class]
structure has_le  :
Type uType u
• le : α → α → Prop

Instances
@[class]
structure has_lt  :
Type uType u
• lt : α → α → Prop

Instances
@[class]
structure has_append  :
Type uType u
• append : α → α → α

Instances
@[class]
structure has_andthen  :
Type uType vout_param (Type w)Type (max u v w)
• andthen : α → β → «σ»

Instances
@[class]
structure has_union  :
Type uType u
• union : α → α → α

Instances
@[class]
structure has_inter  :
Type uType u
• inter : α → α → α

Instances
@[class]
structure has_sdiff  :
Type uType u
• sdiff : α → α → α

Instances
@[class]
structure has_equiv  :
Sort uSort (max 1 u)
• equiv : α → α → Prop

Instances
@[class]
structure has_subset  :
Type uType u
• subset : α → α → Prop

Instances
@[class]
structure has_ssubset  :
Type uType u
• ssubset : α → α → Prop

Instances
@[class]
structure has_emptyc  :
Type uType u
• emptyc : α

Instances
@[class]
structure has_insert  :
out_param (Type u)Type vType (max u v)
• insert : α → γ → γ

Instances
@[class]
structure has_singleton  :
out_param (Type u)Type vType (max u v)
• singleton : α → β

Instances
@[class]
structure has_sep  :
out_param (Type u)Type vType (max u v)
• sep : (α → Prop)γ → γ

Instances
@[class]
structure has_mem  :
out_param (Type u)Type vType (max u v)
• mem : α → γ → Prop

Instances
@[class]
structure has_pow  :
Type uType vType (max u v)
• pow : α → β → α

Instances
def ge {α : Type u} [has_le α] :
α → α → Prop

Equations
def gt {α : Type u} [has_lt α] :
α → α → Prop

Equations
• a > b = (b < a)
def superset {α : Type u} [has_subset α] :
α → α → Prop

Equations
def ssuperset {α : Type u} [has_ssubset α] :
α → α → Prop

Equations
def bit0 {α : Type u} [s : has_add α] :
α → α

Equations
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] :
α → α

Equations
@[class]
structure is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [ β] [ β] :
Type
• insert_emptyc_eq : ∀ (x : α), {x} = {x}

Instances

Equations
@[instance]

Equations
@[instance]
def nat.has_one  :

Equations
@[instance]

Equations

Equations

Equations
def nat.prio  :

Equations
def std.prec.max  :

Equations

Equations

Equations
@[class]
structure has_sizeof  :
Sort uSort (max 1 u)
• sizeof : α →

Instances
• default_has_sizeof
• slim_check.sampleable_ext.wf
• slim_check.sampleable.wf
• nat.has_sizeof
• prod.has_sizeof
• sum.has_sizeof
• psum.has_sizeof
• sigma.has_sizeof
• psigma.has_sizeof
• punit.has_sizeof
• bool.has_sizeof
• option.has_sizeof
• list.has_sizeof
• subtype.has_sizeof
• bin_tree.has_sizeof_inst
• inhabited.has_sizeof_inst
• ulift.has_sizeof_inst
• plift.has_sizeof_inst
• has_well_founded.has_sizeof_inst
• setoid.has_sizeof_inst
• char.has_sizeof_inst
• char.has_sizeof
• string_imp.has_sizeof_inst
• string.iterator_imp.has_sizeof_inst
• string.has_sizeof
• has_repr.has_sizeof_inst
• ordering.has_sizeof_inst
• has_lift.has_sizeof_inst
• has_lift_t.has_sizeof_inst
• has_coe.has_sizeof_inst
• has_coe_t.has_sizeof_inst
• has_coe_to_fun.has_sizeof_inst
• has_coe_to_sort.has_sizeof_inst
• has_coe_t_aux.has_sizeof_inst
• has_to_string.has_sizeof_inst
• name.has_sizeof_inst
• functor.has_sizeof_inst
• has_pure.has_sizeof_inst
• has_seq.has_sizeof_inst
• has_seq_left.has_sizeof_inst
• has_seq_right.has_sizeof_inst
• applicative.has_sizeof_inst
• has_orelse.has_sizeof_inst
• alternative.has_sizeof_inst
• has_bind.has_sizeof_inst
• format.color.has_sizeof_inst
• pos.has_sizeof_inst
• binder_info.has_sizeof_inst
• reducibility_hints.has_sizeof_inst
• environment.projection_info.has_sizeof_inst
• environment.implicit_infer_kind.has_sizeof_inst
• tactic.transparency.has_sizeof_inst
• tactic.new_goals.has_sizeof_inst
• tactic.apply_cfg.has_sizeof_inst
• param_info.has_sizeof_inst
• fun_info.has_sizeof_inst
• subsingleton_info.has_sizeof_inst
• occurrences.has_sizeof_inst
• tactic.rewrite_cfg.has_sizeof_inst
• tactic.dsimp_config.has_sizeof_inst
• tactic.dunfold_config.has_sizeof_inst
• tactic.delta_config.has_sizeof_inst
• tactic.unfold_proj_config.has_sizeof_inst
• tactic.simp_config.has_sizeof_inst
• tactic.simp_intros_config.has_sizeof_inst
• interactive.loc.has_sizeof_inst
• cc_config.has_sizeof_inst
• congr_arg_kind.has_sizeof_inst
• tactic.interactive.case_tag.has_sizeof_inst
• tactic.interactive.case_tag.match_result.has_sizeof_inst
• tactic.unfold_config.has_sizeof_inst
• except.has_sizeof_inst
• except_t.has_sizeof_inst
• state_t.has_sizeof_inst
• option_t.has_sizeof_inst
• vm_obj_kind.has_sizeof_inst
• vm_decl_kind.has_sizeof_inst
• ematch_config.has_sizeof_inst
• smt_pre_config.has_sizeof_inst
• smt_config.has_sizeof_inst
• rsimp.config.has_sizeof_inst
• expr.coord.has_sizeof_inst
• preorder.has_sizeof_inst
• partial_order.has_sizeof_inst
• linear_order.has_sizeof_inst
• decidable_linear_order.has_sizeof_inst
• int.has_sizeof_inst
• d_array.has_sizeof_inst
• rbnode.has_sizeof_inst
• rbnode.color.has_sizeof_inst
• widget.mouse_event_kind.has_sizeof_inst
• doc_category.has_sizeof_inst
• tactic_doc_entry.has_sizeof_inst
• pempty.has_sizeof_inst
• dlist.has_sizeof_inst
• function.has_uncurry.has_sizeof_inst
• random_gen.has_sizeof_inst
• std_gen.has_sizeof_inst
• io.error.has_sizeof_inst
• io.mode.has_sizeof_inst
• io.process.stdio.has_sizeof_inst
• io.process.spawn_args.has_sizeof_inst
• parse_result.has_sizeof_inst
• lint_verbosity.has_sizeof_inst
• tactic.explode.status.has_sizeof_inst
• auto.auto_config.has_sizeof_inst
• auto.case_option.has_sizeof_inst
• can_lift.has_sizeof_inst
• norm_cast.label.has_sizeof_inst
• _nest_1_1._nest_1_1.tactic.tactic_script._mut_.has_sizeof_inst
• _nest_1_1.tactic.tactic_script.has_sizeof_inst
• _nest_1_1.list.tactic.tactic_script.has_sizeof_inst
• tactic.tactic_script.has_sizeof_inst
• simps_cfg.has_sizeof_inst
• applicative_transformation.has_sizeof_inst
• traversable.has_sizeof_inst
• is_lawful_traversable.has_sizeof_inst
• semigroup.has_sizeof_inst
• comm_semigroup.has_sizeof_inst
• left_cancel_semigroup.has_sizeof_inst
• right_cancel_semigroup.has_sizeof_inst
• monoid.has_sizeof_inst
• comm_monoid.has_sizeof_inst
• left_cancel_monoid.has_sizeof_inst
• left_cancel_comm_monoid.has_sizeof_inst
• right_cancel_monoid.has_sizeof_inst
• right_cancel_comm_monoid.has_sizeof_inst
• cancel_monoid.has_sizeof_inst
• cancel_comm_monoid.has_sizeof_inst
• group.has_sizeof_inst
• comm_group.has_sizeof_inst
• unique.has_sizeof_inst
• units.has_sizeof_inst
• zero_hom.has_sizeof_inst
• one_hom.has_sizeof_inst
• mul_hom.has_sizeof_inst
• monoid_hom.has_sizeof_inst
• has_sup.has_sizeof_inst
• has_inf.has_sizeof_inst
• semilattice_sup.has_sizeof_inst
• semilattice_inf.has_sizeof_inst
• lattice.has_sizeof_inst
• distrib_lattice.has_sizeof_inst
• has_top.has_sizeof_inst
• has_bot.has_sizeof_inst
• order_top.has_sizeof_inst
• order_bot.has_sizeof_inst
• semilattice_sup_top.has_sizeof_inst
• semilattice_sup_bot.has_sizeof_inst
• semilattice_inf_top.has_sizeof_inst
• semilattice_inf_bot.has_sizeof_inst
• bounded_lattice.has_sizeof_inst
• bounded_distrib_lattice.has_sizeof_inst
• has_compl.has_sizeof_inst
• boolean_algebra.has_sizeof_inst
• equiv.has_sizeof_inst
• mul_zero_class.has_sizeof_inst
• monoid_with_zero.has_sizeof_inst
• cancel_monoid_with_zero.has_sizeof_inst
• comm_monoid_with_zero.has_sizeof_inst
• comm_cancel_monoid_with_zero.has_sizeof_inst
• group_with_zero.has_sizeof_inst
• comm_group_with_zero.has_sizeof_inst
• distrib.has_sizeof_inst
• semiring.has_sizeof_inst
• ring_hom.has_sizeof_inst
• comm_semiring.has_sizeof_inst
• ring.has_sizeof_inst
• comm_ring.has_sizeof_inst
• domain.has_sizeof_inst
• integral_domain.has_sizeof_inst
• mul_equiv.has_sizeof_inst
• ordered_comm_monoid.has_sizeof_inst
• ordered_cancel_comm_monoid.has_sizeof_inst
• ordered_comm_group.has_sizeof_inst
• ordered_semiring.has_sizeof_inst
• linear_ordered_semiring.has_sizeof_inst
• decidable_linear_ordered_semiring.has_sizeof_inst
• ordered_ring.has_sizeof_inst
• linear_ordered_ring.has_sizeof_inst
• linear_ordered_comm_ring.has_sizeof_inst
• decidable_linear_ordered_comm_ring.has_sizeof_inst
• nonneg_ring.has_sizeof_inst
• linear_nonneg_ring.has_sizeof_inst
• canonically_ordered_comm_semiring.has_sizeof_inst
• division_ring.has_sizeof_inst
• field.has_sizeof_inst
• linear_ordered_field.has_sizeof_inst
• discrete_linear_ordered_field.has_sizeof_inst
• multiset.has_sizeof
• function.embedding.has_sizeof_inst
• tactic.interactive.mono_cfg.has_sizeof_inst
• tactic.interactive.mono_selection.has_sizeof_inst
• has_Sup.has_sizeof_inst
• has_Inf.has_sizeof_inst
• complete_lattice.has_sizeof_inst
• complete_linear_order.has_sizeof_inst
• complete_distrib_lattice.has_sizeof_inst
• complete_boolean_algebra.has_sizeof_inst
• rel_hom.has_sizeof_inst
• rel_embedding.has_sizeof_inst
• rel_iso.has_sizeof_inst
• galois_insertion.has_sizeof_inst
• galois_coinsertion.has_sizeof_inst
• directed_order.has_sizeof_inst
• tactic.interactive.rep_arity.has_sizeof_inst
• expr_lens.dir.has_sizeof_inst
• finset.has_sizeof_inst
• fintype.has_sizeof_inst
• has_vsub.has_sizeof_inst
• encodable.has_sizeof_inst
• euclidean_domain.has_sizeof_inst
• rat.has_sizeof_inst
• tactic.abel.normalize_mode.has_sizeof_inst
• submonoid.has_sizeof_inst
• subgroup.has_sizeof_inst
• has_scalar.has_sizeof_inst
• mul_action.has_sizeof_inst
• distrib_mul_action.has_sizeof_inst
• semimodule.has_sizeof_inst
• semimodule.core.has_sizeof_inst
• linear_map.has_sizeof_inst
• con.has_sizeof_inst
• submodule.has_sizeof_inst
• finsupp.has_sizeof_inst
• linear_equiv.has_sizeof_inst
• ring_equiv.has_sizeof_inst
• subsemiring.has_sizeof_inst
• subring.has_sizeof_inst
• algebra.has_sizeof_inst
• alg_hom.has_sizeof_inst
• alg_equiv.has_sizeof_inst
• subalgebra.has_sizeof_inst
• tactic.ring.normalize_mode.has_sizeof_inst
• linarith.ineq.has_sizeof_inst
• linarith.comp.has_sizeof_inst
• linarith.comp_source.has_sizeof_inst
• pos_num.has_sizeof_inst
• num.has_sizeof_inst
• znum.has_sizeof_inst
• tree.has_sizeof_inst
• floor_ring.has_sizeof_inst
• roption.has_sizeof_inst
• free_algebra.pre.has_sizeof_inst
• category_theory.has_hom.has_sizeof_inst
• category_theory.category_struct.has_sizeof_inst
• category_theory.category.has_sizeof_inst
• category_theory.functor.has_sizeof_inst
• category_theory.nat_trans.has_sizeof_inst
• category_theory.iso.has_sizeof_inst
• category_theory.is_iso.has_sizeof_inst
• category_theory.full.has_sizeof_inst
• category_theory.equivalence.has_sizeof_inst
• category_theory.is_equivalence.has_sizeof_inst
• category_theory.ess_surj.has_sizeof_inst
• category_theory.split_mono.has_sizeof_inst
• category_theory.split_epi.has_sizeof_inst
• category_theory.groupoid.has_sizeof_inst
• category_theory.concrete_category.has_sizeof_inst
• category_theory.has_forget₂.has_sizeof_inst
• category_theory.bundled.has_sizeof_inst
• category_theory.bundled_hom.has_sizeof_inst
• category_theory.bundled_hom.parent_projection.has_sizeof_inst
• category_theory.reflects_isomorphisms.has_sizeof_inst
• category_theory.unbundled_hom.has_sizeof_inst
• category_theory.representable.has_sizeof_inst
• category_theory.limits.cone.has_sizeof_inst
• category_theory.limits.cocone.has_sizeof_inst
• category_theory.limits.cone_morphism.has_sizeof_inst
• category_theory.limits.cocone_morphism.has_sizeof_inst
• category_theory.limits.is_limit.has_sizeof_inst
• category_theory.limits.is_colimit.has_sizeof_inst
• category_theory.limits.limit_cone.has_sizeof_inst
• category_theory.limits.colimit_cocone.has_sizeof_inst
• category_theory.limits.walking_pair.has_sizeof_inst
• category_theory.limits.walking_parallel_pair.has_sizeof_inst
• category_theory.limits.walking_parallel_pair_hom.has_sizeof_inst
• category_theory.comma.has_sizeof_inst
• category_theory.comma_morphism.has_sizeof_inst
• category_theory.arrow.lift_struct.has_sizeof_inst
• category_theory.limits.mono_factorisation.has_sizeof_inst
• category_theory.limits.is_image.has_sizeof_inst
• category_theory.limits.image_factorisation.has_sizeof_inst
• category_theory.limits.has_images.has_sizeof_inst
• category_theory.limits.image_map.has_sizeof_inst
• category_theory.limits.has_image_maps.has_sizeof_inst
• category_theory.limits.strong_epi_mono_factorisation.has_sizeof_inst
• category_theory.limits.has_zero_morphisms.has_sizeof_inst
• category_theory.limits.has_zero_object.has_sizeof_inst
• Module.has_sizeof_inst
• Algebra.has_sizeof_inst
• category_theory.fin_category.has_sizeof_inst
• bifunctor.has_sizeof_inst
• is_lawful_bifunctor.has_sizeof_inst
• equiv_functor.has_sizeof_inst
• category_theory.limits.preserves_limit.has_sizeof_inst
• category_theory.limits.preserves_colimit.has_sizeof_inst
• category_theory.limits.preserves_limits_of_shape.has_sizeof_inst
• category_theory.limits.preserves_colimits_of_shape.has_sizeof_inst
• category_theory.limits.preserves_limits.has_sizeof_inst
• category_theory.limits.preserves_colimits.has_sizeof_inst
• category_theory.limits.reflects_limit.has_sizeof_inst
• category_theory.limits.reflects_colimit.has_sizeof_inst
• category_theory.limits.reflects_limits_of_shape.has_sizeof_inst
• category_theory.limits.reflects_colimits_of_shape.has_sizeof_inst
• category_theory.limits.reflects_limits.has_sizeof_inst
• category_theory.limits.reflects_colimits.has_sizeof_inst
• category_theory.liftable_cone.has_sizeof_inst
• category_theory.liftable_cocone.has_sizeof_inst
• category_theory.creates_limit.has_sizeof_inst
• category_theory.creates_limits_of_shape.has_sizeof_inst
• category_theory.creates_limits.has_sizeof_inst
• category_theory.creates_colimit.has_sizeof_inst
• category_theory.creates_colimits_of_shape.has_sizeof_inst
• category_theory.creates_colimits.has_sizeof_inst
• category_theory.lifts_to_limit.has_sizeof_inst
• category_theory.lifts_to_colimit.has_sizeof_inst
• tactic.ring_exp.coeff.has_sizeof_inst
• tactic.ring_exp.ex_type.has_sizeof_inst
• CommRing.colimits.prequotient.has_sizeof_inst
• category_theory.limits.wide_pullback_shape.hom.has_sizeof_inst
• category_theory.limits.wide_pushout_shape.hom.has_sizeof_inst
• category_theory.regular_mono.has_sizeof_inst
• category_theory.normal_mono.has_sizeof_inst
• category_theory.regular_epi.has_sizeof_inst
• category_theory.normal_epi.has_sizeof_inst
• category_theory.limits.bicone.has_sizeof_inst
• category_theory.limits.limit_bicone.has_sizeof_inst
• category_theory.limits.binary_bicone.has_sizeof_inst
• category_theory.limits.binary_biproduct_data.has_sizeof_inst
• category_theory.abelian.has_sizeof_inst
• tactic.tfae.arrow.has_sizeof_inst
• category_theory.monoidal_category.has_sizeof_inst
• category_theory.lax_monoidal_functor.has_sizeof_inst
• category_theory.monoidal_functor.has_sizeof_inst
• category_theory.monoidal_nat_trans.has_sizeof_inst
• category_theory.braided_category.has_sizeof_inst
• category_theory.symmetric_category.has_sizeof_inst
• category_theory.lax_braided_functor.has_sizeof_inst
• category_theory.braided_functor.has_sizeof_inst
• Mon.colimits.prequotient.has_sizeof_inst
• omega.ee.has_sizeof_inst
• omega.ee_state.has_sizeof_inst
• omega.int.preterm.has_sizeof_inst
• omega.int.preform.has_sizeof_inst
• omega.nat.preterm.has_sizeof_inst
• omega.nat.preform.has_sizeof_inst
• lazy_list.has_sizeof_inst
• generalized_continued_fraction.pair.has_sizeof_inst
• generalized_continued_fraction.has_sizeof_inst
• generalized_continued_fraction.int_fract_pair.has_sizeof_inst
• conditionally_complete_lattice.has_sizeof_inst
• conditionally_complete_linear_order.has_sizeof_inst
• conditionally_complete_linear_order_bot.has_sizeof_inst
• filter.has_sizeof_inst
• denumerable.has_sizeof_inst
• filter_basis.has_sizeof_inst
• filter.countable_filter_basis.has_sizeof_inst
• dfinsupp.pre.has_sizeof_inst
• free_magma.has_sizeof_inst
• normalization_monoid.has_sizeof_inst
• gcd_monoid.has_sizeof_inst
• mul_semiring_action.has_sizeof_inst
• faithful_mul_semiring_action.has_sizeof_inst
• mul_action_hom.has_sizeof_inst
• distrib_mul_action_hom.has_sizeof_inst
• mul_semiring_action_hom.has_sizeof_inst
• category_theory.has_shift.has_sizeof_inst
• category_theory.differential_object.has_sizeof_inst
• category_theory.differential_object.hom.has_sizeof_inst
• invertible.has_sizeof_inst
• linear_action.has_sizeof_inst
• initial_seg.has_sizeof_inst
• principal_seg.has_sizeof_inst
• Well_order.has_sizeof_inst
• pequiv.has_sizeof_inst
• multilinear_map.has_sizeof_inst
• dual_pair.has_sizeof_inst
• bilin_form.has_sizeof_inst
• has_bracket.has_sizeof_inst
• lie_ring.has_sizeof_inst
• lie_algebra.has_sizeof_inst
• lie_algebra.morphism.has_sizeof_inst
• lie_algebra.equiv.has_sizeof_inst
• lie_subalgebra.has_sizeof_inst
• lie_module.has_sizeof_inst
• lie_submodule.has_sizeof_inst
• linear_ordered_comm_group_with_zero.has_sizeof_inst
• linear_recurrence.has_sizeof_inst
• ordered_semimodule.has_sizeof_inst
• shelf.has_sizeof_inst
• shelf_hom.has_sizeof_inst
• rack.has_sizeof_inst
• quandle.has_sizeof_inst
• rack.pre_envel_group.has_sizeof_inst
• rack.pre_envel_group_rel'.has_sizeof_inst
• tactic.decl_reducibility.has_sizeof_inst
• topological_space.has_sizeof_inst
• continuous_map.has_sizeof_inst
• homeomorph.has_sizeof_inst
• algebraic_geometry.PresheafedSpace.has_sizeof_inst
• algebraic_geometry.PresheafedSpace.hom.has_sizeof_inst
• Top.sheaf.has_sizeof_inst
• algebraic_geometry.SheafedSpace.has_sizeof_inst
• algebraic_geometry.LocallyRingedSpace.has_sizeof_inst
• TopCommRing.has_sizeof_inst
• uniform_space.core.has_sizeof_inst
• uniform_space.has_sizeof_inst
• continuous_linear_map.has_sizeof_inst
• continuous_linear_equiv.has_sizeof_inst
• local_equiv.has_sizeof_inst
• local_homeomorph.has_sizeof_inst
• Top.prelocal_predicate.has_sizeof_inst
• Top.local_predicate.has_sizeof_inst
• submonoid.localization_map.has_sizeof_inst
• localization_map.has_sizeof_inst
• algebraic_geometry.Scheme.has_sizeof_inst
• cau_seq.is_complete.has_sizeof_inst
• complex.has_sizeof_inst
• affine_subspace.has_sizeof_inst
• affine_map.has_sizeof_inst
• has_edist.has_sizeof_inst
• emetric_space.has_sizeof_inst
• has_dist.has_sizeof_inst
• metric_space.has_sizeof_inst
• has_norm.has_sizeof_inst
• normed_group.has_sizeof_inst
• normed_ring.has_sizeof_inst
• normed_comm_ring.has_sizeof_inst
• normed_field.has_sizeof_inst
• nondiscrete_normed_field.has_sizeof_inst
• normed_space.has_sizeof_inst
• normed_algebra.has_sizeof_inst
• isometric.has_sizeof_inst
• continuous_multilinear_map.has_sizeof_inst
• path.has_sizeof_inst
• measurable_space.has_sizeof_inst
• measurable_equiv.has_sizeof_inst
• measurable_space.dynkin_system.has_sizeof_inst
• measure_theory.outer_measure.has_sizeof_inst
• measure_theory.measure.has_sizeof_inst
• measure_theory.measure.finite_spanning_sets_in.has_sizeof_inst
• measure_theory.measure_space.has_sizeof_inst
• composition.has_sizeof_inst
• composition_as_set.has_sizeof_inst
• implicit_function_data.has_sizeof_inst
• linear_pmap.has_sizeof_inst
• convex_cone.has_sizeof_inst
• measure_theory.simple_func.has_sizeof_inst
• enorm.has_sizeof_inst
• ring_invo.has_sizeof_inst
• sesq_form.has_sizeof_inst
• is_R_or_C.has_sizeof_inst
• has_inner.has_sizeof_inst
• inner_product_space.has_sizeof_inst
• inner_product_space.core.has_sizeof_inst
• category_theory.pairwise.has_sizeof_inst
• category_theory.pairwise.hom.has_sizeof_inst
• category_theory.closed.has_sizeof_inst
• category_theory.monoidal_closed.has_sizeof_inst
• category_theory.functorial.has_sizeof_inst
• category_theory.grothendieck.has_sizeof_inst
• category_theory.grothendieck.hom.has_sizeof_inst
• category_theory.limits.diagram_of_cones.has_sizeof_inst
• category_theory.is_kernel_pair.has_sizeof_inst
• category_theory.reflective.has_sizeof_inst
• Mon_.has_sizeof_inst
• Mon_.hom.has_sizeof_inst
• CommMon_.has_sizeof_inst
• Mod.has_sizeof_inst
• Mod.hom.has_sizeof_inst
• category_theory.lax_monoidal.has_sizeof_inst
• category_theory.simple.has_sizeof_inst
• category_theory.quotient.has_sizeof_inst
• category_theory.sieve.has_sizeof_inst
• category_theory.grothendieck_topology.has_sizeof_inst
• category_theory.is_skeleton_of.has_sizeof_inst
• simple_graph.has_sizeof_inst
• partition.has_sizeof_inst
• nzsnum.has_sizeof_inst
• snum.has_sizeof_inst
• computability.encoding.has_sizeof_inst
• computability.fin_encoding.has_sizeof_inst
• computability.Γ'.has_sizeof_inst
• primcodable.has_sizeof_inst
• nat.partrec.code.has_sizeof_inst
• turing.pointed_map.has_sizeof_inst
• turing.tape.has_sizeof_inst
• turing.dir.has_sizeof_inst
• turing.TM0.stmt.has_sizeof_inst
• turing.TM0.cfg.has_sizeof_inst
• turing.TM1.stmt.has_sizeof_inst
• turing.TM1.cfg.has_sizeof_inst
• turing.TM1to1.Λ'.has_sizeof_inst
• turing.TM0to1.Λ'.has_sizeof_inst
• turing.TM2.stmt.has_sizeof_inst
• turing.TM2.cfg.has_sizeof_inst
• turing.TM2to1.st_act.has_sizeof_inst
• turing.TM2to1.Λ'.has_sizeof_inst
• turing.fin_tm2.has_sizeof_inst
• turing.evals_to.has_sizeof_inst
• turing.evals_to_in_time.has_sizeof_inst
• turing.tm2_computable_aux.has_sizeof_inst
• turing.tm2_computable.has_sizeof_inst
• turing.tm2_computable_in_time.has_sizeof_inst
• turing.tm2_computable_in_poly_time.has_sizeof_inst
• turing.to_partrec.code.has_sizeof_inst
• turing.to_partrec.cont.has_sizeof_inst
• turing.to_partrec.cfg.has_sizeof_inst
• turing.partrec_to_TM2.Γ'.has_sizeof_inst
• turing.partrec_to_TM2.K'.has_sizeof_inst
• turing.partrec_to_TM2.cont'.has_sizeof_inst
• turing.partrec_to_TM2.Λ'.has_sizeof_inst
• bitraversable.has_sizeof_inst
• is_lawful_bitraversable.has_sizeof_inst
• has_fix.has_sizeof_inst
• fin2.has_sizeof_inst
• fin2.is_lt.has_sizeof_inst
• mvfunctor.has_sizeof_inst
• preorder_hom.has_sizeof_inst
• omega_complete_partial_order.has_sizeof_inst
• omega_complete_partial_order.continuous_hom.has_sizeof_inst
• lawful_fix.has_sizeof_inst
• writer_t.has_sizeof_inst
• uliftable.has_sizeof_inst
• W.has_sizeof_inst
• cfilter.has_sizeof_inst
• filter.realizer.has_sizeof_inst
• ctop.has_sizeof_inst
• ctop.realizer.has_sizeof_inst
• locally_finite.realizer.has_sizeof_inst
• fin_enum.has_sizeof_inst
• alist.has_sizeof_inst
• finmap.has_sizeof_inst
• semiquot.has_sizeof_inst
• fp.rmode.has_sizeof_inst
• fp.float_cfg.has_sizeof_inst
• fp.float.has_sizeof_inst
• hash_map.has_sizeof_inst
• valuation.has_sizeof_inst
• pfunctor.has_sizeof_inst
• pfunctor.approx.cofix_a.has_sizeof_inst
• pfunctor.M_intl.has_sizeof_inst
• mvpfunctor.has_sizeof_inst
• mvpfunctor.M.path.has_sizeof_inst
• mvpfunctor.W_path.has_sizeof_inst
• pnat.xgcd_type.has_sizeof_inst
• pnat.xgcd_type.has_sizeof
• mvqpf.has_sizeof_inst
• qpf.has_sizeof_inst
• has_finite_inter.has_sizeof_inst
• zsqrtd.has_sizeof_inst
• circle_deg1_lift.has_sizeof_inst
• subfield.has_sizeof_inst
• intermediate_field.has_sizeof_inst
• intermediate_field.insert.has_sizeof_inst
• perfect_field.has_sizeof_inst
• affine.simplex.has_sizeof_inst
• affine.simplex.points_with_circumcenter_index.has_sizeof_inst
• bundle_trivialization.has_sizeof_inst
• topological_fiber_bundle_core.has_sizeof_inst
• structure_groupoid.has_sizeof_inst
• pregroupoid.has_sizeof_inst
• charted_space.has_sizeof_inst
• charted_space_core.has_sizeof_inst
• structomorph.has_sizeof_inst
• model_with_corners.has_sizeof_inst
• basic_smooth_bundle_core.has_sizeof_inst
• smooth_monoid_morphism.has_sizeof_inst
• lie_group_morphism.has_sizeof_inst
• times_cont_mdiff_map.has_sizeof_inst
• times_diffeomorph.has_sizeof_inst
• semidirect_product.has_sizeof_inst
• nonempty_fin_lin_ord.has_sizeof_inst
• order.ideal.has_sizeof_inst
• order.cofinal.has_sizeof_inst
• derivation.has_sizeof_inst
• pgame.has_sizeof_inst
• pgame.restricted.has_sizeof_inst
• pgame.relabelling.has_sizeof_inst
• pgame.short.has_sizeof_inst
• pgame.list_short.has_sizeof_inst
• pgame.state.has_sizeof_inst
• lists'.has_sizeof_inst
• lists.has_sizeof
• onote.has_sizeof_inst
• pgame.inv_ty.has_sizeof_inst
• pSet.has_sizeof_inst
• pSet.definable.has_sizeof_inst
• bounded_random.has_sizeof_inst
• random.has_sizeof_inst
• side.has_sizeof_inst
• tactic.ring2.csring_expr.has_sizeof_inst
• tactic.ring2.horner_expr.has_sizeof_inst
• slim_check.sampleable.has_sizeof_inst
• slim_check.sampleable_functor.has_sizeof_inst
• slim_check.sampleable_bifunctor.has_sizeof_inst
• slim_check.sampleable_ext.has_sizeof_inst
• slim_check.test_result.has_sizeof_inst
• slim_check.slim_check_cfg.has_sizeof_inst
• slim_check.printable_prop.has_sizeof_inst
• slim_check.testable.has_sizeof_inst
• slim_check.total_function.has_sizeof_inst
• slim_check.injective_function.has_sizeof_inst
• slim_check.injective_function.has_sizeof
• abstract_completion.has_sizeof_inst
• open_subgroup.has_sizeof_inst
• CompHaus.has_sizeof_inst
• CpltSepUniformSpace.has_sizeof_inst
• premetric_space.has_sizeof_inst
• Gromov_Hausdorff.aux_gluing_struct.has_sizeof_inst
• module_doc_info.has_sizeof_inst
• ext_tactic_doc_entry.has_sizeof_inst
• slim_check.total_function.has_sizeof
def sizeof {α : Sort u} [s : has_sizeof α] :
α →

Equations
def default.sizeof (α : Sort u) :
α →

Equations
• = 0
@[instance]
def default_has_sizeof (α : Sort u) :

Equations
@[instance]

Equations
@[instance]
def prod.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof × β)

Equations
@[instance]
def sum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
has_sizeof β)

Equations
@[instance]
def psum.has_sizeof (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :

Equations
@[instance]
def sigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :

Equations
• = {sizeof := sigma.sizeof (λ (a : α), _inst_2 a)}
@[instance]
def psigma.has_sizeof (α : Type u) (β : α → Type v) [has_sizeof α] [Π (a : α), has_sizeof (β a)] :

Equations
• = {sizeof := psigma.sizeof (λ (a : α), _inst_2 a)}
@[instance]

Equations
@[instance]

Equations
@[instance]
def option.has_sizeof (α : Type u) [has_sizeof α] :

Equations
@[instance]
def list.has_sizeof (α : Type u) [has_sizeof α] :

Equations
@[instance]
def subtype.has_sizeof {α : Type u} [has_sizeof α] (p : α → Prop) :

Equations
theorem nat_add_zero (n : ) :
n + 0 = n

def combinator.I {α : Type u₁} :
α → α

Equations
def combinator.K {α : Type u₁} {β : Type u₂} :
α → β → α

Equations
• b = a
def combinator.S {α : Type u₁} {β : Type u₂} {γ : Type u₃} :
(α → β → γ)(α → β)α → γ

Equations
• y z = x z (y z)
inductive bin_tree  :
Type uType u
• empty : Π (α : Type u),
• leaf : Π (α : Type u), α →
• node : Π (α : Type u),

Auxiliary datatype for #[ ... ] notation. #[1, 2, 3, 4] is notation for

bin_tree.node (bin_tree.node (bin_tree.leaf 1) (bin_tree.leaf 2)) (bin_tree.node (bin_tree.leaf 3) (bin_tree.leaf 4))

We use this notation to input long sequences without exhausting the system stack space. Later, we define a coercion from bin_tree into list.

Equations
def infer_instance {α : Type u} [i : α] :
α

Like by apply_instance, but not dependent on the tactic framework.

Equations