/root/interactive/lean/phase8/RealNoise.lean:369:19: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
'NimAudit.RealNoise.natCast_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.inv_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.pow_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.add_mul_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.gs_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.two_pOf' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.pOf_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.chan_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mUp_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.archimedean_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mUp_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mUp_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mUp_ge_16' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.majority_succeeds' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.any_rule_needs' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.ach_of_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.ach_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mMin_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mMin_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mMin_theta' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mMin_scaled' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.zero_samples_never' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.zero_signal_never' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.err_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.ach_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.ach_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.ach_iff_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.mMin_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_agree_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.agree_eq_pOf' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_repeated' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_bias_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_samples' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flipAch_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_mMin' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.flip_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.bernoulli_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.eventually_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.cnt_true_replicate' depends on axioms: [propext, Quot.sound]
'NimAudit.RealNoise.maj_replicate' depends on axioms: [propext, Quot.sound]
'NimAudit.RealNoise.reuse_no_gain' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.reuse_any_rule' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.reuse_never' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RealNoise.remark_real' depends on axioms: [propext, Classical.choice, Quot.sound]