'ActualMathematics.FiniteRecording.actual_write' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.marker_retained_after' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.read_bank' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.write_extends_delta' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.write_preserves_capacity' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.read_is_faithful' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.propagation_preserves_bank' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'ActualMathematics.FiniteRecording.full_bank_has_no_blank' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.readout_margin' depends on axioms: [propext, Classical.choice, Quot.sound]

'ActualMathematics.FiniteRecording.calibrated_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.writeNext_conserves' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.bank_energy' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.bank_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.complete_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.read_join' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.join_banks_counts' depends on axioms: [propext, Classical.choice, Quot.sound]

RecordingProfile.lean:50:92: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
RecordingProfile.lean:62:52: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
RecordingProfile.lean:69:52: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
'ActualMathematics.FiniteRecording.profileTick_embeds' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.embed_advance' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.profile_intensity' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.profileTick_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.profile_energy' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.readProfiles_embeds' depends on axioms: [propext, Classical.choice, Quot.sound]

'ActualMathematics.FiniteRecording.writeCells_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.writeCells_capacity' depends on axioms: [propext, Quot.sound]
'ActualMathematics.FiniteRecording.wait_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.wait_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.record_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.FiniteRecording.record_capacity' depends on axioms: [propext, Quot.sound]
'ActualMathematics.FiniteRecording.writeCells_count' depends on axioms: [propext, Classical.choice, Quot.sound]