Hydra

📁 Source: Mathlib/Logic/Hydra.lean

Statistics

Metric	Count
Definitions CutExpand	1
Theorems cutExpand, acc_of_singleton, cutExpand_add_left, cutExpand_add_right, cutExpand_add_single, cutExpand_closed, cutExpand_double, cutExpand_double_left, cutExpand_fibration, cutExpand_iff, cutExpand_le_invImage_lex, cutExpand_pair_left, cutExpand_pair_right, cutExpand_single_add, cutExpand_singleton, cutExpand_singleton_singleton, cutExpand_zero, instIsWellFoundedMultisetCutExpand, not_cutExpand_zero, cutExpand	20
Total	21

Acc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cutExpand 📖	mathematical	—	Multiset Relation.CutExpand Multiset.instSingleton	—	Relation.acc_of_singleton Multiset.erase_singleton zero_add

Relation

Definitions

Name	Category	Theorems
CutExpand 📖	MathDef	18 math math: WellFounded.cutExpand, cutExpand_double_left, cutExpand_add_left, cutExpand_double, Acc.cutExpand, cutExpand_singleton, cutExpand_zero, cutExpand_single_add, cutExpand_pair_left, cutExpand_fibration, cutExpand_le_invImage_lex, cutExpand_singleton_singleton, cutExpand_pair_right, cutExpand_iff, cutExpand_add_right, instIsWellFoundedMultisetCutExpand, not_cutExpand_zero, cutExpand_add_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
acc_of_singleton 📖	—	Multiset CutExpand Multiset.instSingleton	—	—	Multiset.induction not_cutExpand_zero Multiset.singleton_add Acc.of_fibration cutExpand_fibration Acc.prod_gameAdd Multiset.forall_mem_cons
cutExpand_add_left 📖	mathematical	—	CutExpand Multiset Multiset.instAdd	—	add_assoc add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd
cutExpand_add_right 📖	mathematical	—	CutExpand Multiset Multiset.instAdd	—	add_comm cutExpand_add_left
cutExpand_add_single 📖	mathematical	—	CutExpand Multiset Multiset.instAdd Multiset.instSingleton	—	cutExpand_add_left cutExpand_singleton_singleton
cutExpand_closed 📖	—	CutExpand Multiset Multiset.instMembership	—	—	cutExpand_iff Multiset.mem_add Multiset.mem_of_mem_erase
cutExpand_double 📖	mathematical	—	CutExpand Multiset Multiset.instInsert Multiset.instSingleton	—	cutExpand_singleton
cutExpand_double_left 📖	mathematical	—	CutExpand Multiset Multiset.instInsert Multiset.instSingleton	—	cutExpand_add_right cutExpand_double
cutExpand_fibration 📖	mathematical	—	Fibration Multiset Prod.GameAdd CutExpand Multiset.instAdd	—	Multiset.add_singleton_eq_iff Multiset.mem_add add_assoc add_comm Multiset.singleton_add Multiset.cons_erase Multiset.erase_add_left_pos add_right_comm Multiset.erase_add_right_pos
cutExpand_iff 📖	mathematical	—	CutExpand Multiset Multiset.instMembership Multiset.instAdd Multiset.erase	—	Multiset.mem_add Multiset.erase_add_left_pos irrefl
cutExpand_le_invImage_lex 📖	mathematical	—	Pi.hasLe Multiset Prop.le CutExpand Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.Lex Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder Compl.compl Pi.instCompl Prop.instCompl DFunLike.coe AddEquiv Multiset.instAdd Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid EquivLike.toFunLike AddEquiv.instEquivLike Multiset.toFinsupp	—	Multiset.count_add Multiset.count_singleton add_zero Multiset.count_eq_zero Multiset.count_singleton_self irrefl_of
cutExpand_pair_left 📖	mathematical	—	CutExpand Multiset Multiset.instInsert Multiset.instSingleton	—	cutExpand_add_right cutExpand_singleton_singleton
cutExpand_pair_right 📖	mathematical	—	CutExpand Multiset Multiset.instInsert Multiset.instSingleton	—	cutExpand_add_left cutExpand_singleton_singleton
cutExpand_single_add 📖	mathematical	—	CutExpand Multiset Multiset.instAdd Multiset.instSingleton	—	cutExpand_add_right cutExpand_singleton_singleton
cutExpand_singleton 📖	mathematical	—	CutExpand Multiset Multiset.instSingleton	—	add_comm
cutExpand_singleton_singleton 📖	mathematical	—	CutExpand Multiset Multiset.instSingleton	—	cutExpand_singleton Multiset.mem_singleton
cutExpand_zero 📖	mathematical	—	CutExpand Multiset Multiset.instZero Multiset.instSingleton	—	add_comm
instIsWellFoundedMultisetCutExpand 📖	mathematical	—	IsWellFounded Multiset CutExpand	—	WellFounded.cutExpand IsWellFounded.wf
not_cutExpand_zero 📖	mathematical	—	CutExpand Multiset Multiset.instZero	—	cutExpand_iff

WellFounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cutExpand 📖	mathematical	—	Multiset Relation.CutExpand	—	irrefl Relation.acc_of_singleton Acc.cutExpand

---

← Back to Index