../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:114:2: warning: Try `simp at hi` instead of `simpa using hi`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:252:6: warning: Try `simp at this` instead of `simpa using this`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
'Erdos1183.FreeTuple.exists_private_coordinate' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.FreeTuple.dimension_le_ground' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.indexedUnion_mem_of_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.Finset.Shatters.toIndexed' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.FreeTuple.indexedShatters_complementaryFamily' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.IndexedShatters.exists_singleton_traces' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.IndexedShatters.exists_freeTuple' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.card_le_sauer_vc' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.vcDim_complementaryFamily_lt_of_no_freeTuple' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.card_le_sum_choose_of_no_freeTuple' depends on axioms: [propext, Classical.choice, Quot.sound]
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:422:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
'Erdos1183.card_badColorings_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_coloring_no_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.FreeTuple.card_generatedNonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.card_freeGeneratedEdges_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_coloring_no_mono_freeTuple' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_coloring_bounding_unionClosed' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamseyNumber_le_sum_choose' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.cubic_lt_two_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.firstMoment_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.sum_choose_sqrt_le_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamseyNumber_le_sqrt_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.tendsto_nat_sqrt_atTop' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.eventually_succ_sq_lt_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamsey_subexponential_verified' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.Subspace.to_monoBlockCube' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_blockCube_seed' depends on axioms: [propext, Classical.choice, Quot.sound]
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:1112:27: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
'Erdos1183.card_coordinateIntervals' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.blockDelete_embed_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.MonoBlockCube.embed_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_cube_in_coordinateInterval' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.card_coordinateIntervals_le_incidences' depends on axioms: [propext, Classical.choice, Quot.sound]
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:1544:50: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
'Erdos1183.two_mul_pred_pow_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.coding_safe_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.coding_coefficient_lt' depends on axioms: [propext, Quot.sound]
'Erdos1183.genericAtomDelete_injOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.generic_atom_edges_give_unionClosed_family' depends on axioms: [propext, Classical.choice, Quot.sound]
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:1848:16: warning: This simp argument is unused:
  and_left_comm

Hint: Omit it from the simp argument list.
  simp [̵a̵n̵d̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵a̵n̵d̵_̵c̵o̵m̵m̵]̵[̲a̲n̲d̲_̲c̲o̲m̲m̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
'Erdos1183.card_allowedCodingLabels' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.card_codingLabelingsForSlots' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.card_codingLabelings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_label_many_realized' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.exists_label_realized_gt_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionGuaranteed_power_of_seed' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamseyNumber_ge_power_of_seed' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamsey_superpolynomial_verified' depends on axioms: [propext, Classical.choice, Quot.sound]
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3151:2: warning: 'change ((Fintype.card α).choose (A ∪ S).card : ℝ)⁻¹ * ((A ∪ S).card.choose A.card : ℝ)⁻¹ = _' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3321:33: warning: This simp argument is unused:
  Fintype.card_coe

Hint: Omit it from the simp argument list.
  simp [gapPairWeight, Fint̵y̵p̵e̵.̵c̵a̵r̵d̵_̵c̵o̵e̵,̵ ̵F̵i̵n̵set.card_compl]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3321:51: warning: This simp argument is unused:
  Finset.card_compl

Hint: Omit it from the simp argument list.
  simp [gapPairWeight, Fintype.card_coe,̵ ̵F̵i̵n̵s̵e̵t̵.̵c̵a̵r̵d̵_̵c̵o̵m̵p̵l̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3381:4: warning: 'push_cast' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3506:58: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
'Erdos1183.expect_prefixCount' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.lubell_choose_two_le_pairMoment' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.hasBooleanCube_of_lubell_gt_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3618:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3621:2: warning: 'norm_num at hf ht' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3784:60: warning: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
../../../../verified_math/F-026_quantitative-union-ramsey-lower/Main.lean:3784:60: warning: 'omega' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
'Erdos1183.quantitative_blockCube_seed' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamsey_quantitative_lower_verified' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamsey_superpolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamsey_subexponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos1183.unionRamsey_quantitative_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
