Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: FrischWaugh.lean
SHA-256: e46a071d831088863d817da514ba6526e5bec29cb1ad1921838ae3e96278f5af
Result: passed

'PaperToLean.FrischWaugh.residual_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FrischWaugh.loss_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FrischWaugh.best_nuisance' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FrischWaugh.one_variable_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FrischWaugh.full_loss_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FrischWaugh.unique_coefficients' depends on axioms: [propext, Classical.choice, Quot.sound]