ProjectEulerSolutions.lean

-- This file is autogenerated by generate_lean_toplevel.py; do not edit manually.
import ProjectEulerSolutions.P1
import ProjectEulerSolutions.Equiv.P1
import ProjectEulerSolutions.P2
import ProjectEulerSolutions.Equiv.P2
import ProjectEulerSolutions.P3
import ProjectEulerSolutions.Equiv.P3
import ProjectEulerSolutions.P4
import ProjectEulerSolutions.Equiv.P4
import ProjectEulerSolutions.P5
import ProjectEulerSolutions.Equiv.P5
import ProjectEulerSolutions.P6
import ProjectEulerSolutions.Equiv.P6
import ProjectEulerSolutions.P7
import ProjectEulerSolutions.Equiv.P7
import ProjectEulerSolutions.P8
import ProjectEulerSolutions.Equiv.P8
import ProjectEulerSolutions.P9
import ProjectEulerSolutions.Equiv.P9
import ProjectEulerSolutions.P10
import ProjectEulerSolutions.Equiv.P10
import ProjectEulerSolutions.P11
import ProjectEulerSolutions.Equiv.P11
import ProjectEulerSolutions.P12
import ProjectEulerSolutions.Equiv.P12
import ProjectEulerSolutions.P13
import ProjectEulerSolutions.Equiv.P13
import ProjectEulerSolutions.P14
import ProjectEulerSolutions.Equiv.P14
import ProjectEulerSolutions.P15
import ProjectEulerSolutions.Equiv.P15
import ProjectEulerSolutions.P16
import ProjectEulerSolutions.Equiv.P16
import ProjectEulerSolutions.P17
import ProjectEulerSolutions.Equiv.P17
import ProjectEulerSolutions.P18
import ProjectEulerSolutions.Equiv.P18
import ProjectEulerSolutions.P19
import ProjectEulerSolutions.Equiv.P19
import ProjectEulerSolutions.P20
import ProjectEulerSolutions.Equiv.P20
import ProjectEulerSolutions.P21
import ProjectEulerSolutions.Equiv.P21
import ProjectEulerSolutions.P22
import ProjectEulerSolutions.Equiv.P22
import ProjectEulerSolutions.P23
import ProjectEulerSolutions.Equiv.P23
import ProjectEulerSolutions.P24
import ProjectEulerSolutions.Equiv.P24
import ProjectEulerSolutions.P25
import ProjectEulerSolutions.Equiv.P25
import ProjectEulerSolutions.P26
import ProjectEulerSolutions.Equiv.P26
import ProjectEulerSolutions.P27
import ProjectEulerSolutions.Equiv.P27
import ProjectEulerSolutions.P28
import ProjectEulerSolutions.Equiv.P28
import ProjectEulerSolutions.P29
import ProjectEulerSolutions.Equiv.P29
import ProjectEulerSolutions.P30
import ProjectEulerSolutions.Equiv.P30
import ProjectEulerSolutions.P31
import ProjectEulerSolutions.Equiv.P31
import ProjectEulerSolutions.P32
import ProjectEulerSolutions.Equiv.P32
import ProjectEulerSolutions.P33
import ProjectEulerSolutions.Equiv.P33
import ProjectEulerSolutions.P34
import ProjectEulerSolutions.Equiv.P34
import ProjectEulerSolutions.P35
import ProjectEulerSolutions.Equiv.P35
import ProjectEulerSolutions.P36
import ProjectEulerSolutions.Equiv.P36
import ProjectEulerSolutions.P37
import ProjectEulerSolutions.Equiv.P37
import ProjectEulerSolutions.P38
import ProjectEulerSolutions.Equiv.P38
import ProjectEulerSolutions.P39
import ProjectEulerSolutions.Equiv.P39
import ProjectEulerSolutions.P40
import ProjectEulerSolutions.Equiv.P40
import ProjectEulerSolutions.P41
import ProjectEulerSolutions.Equiv.P41
import ProjectEulerSolutions.P42
import ProjectEulerSolutions.Equiv.P42
import ProjectEulerSolutions.P43
import ProjectEulerSolutions.Equiv.P43
import ProjectEulerSolutions.P44
import ProjectEulerSolutions.Equiv.P44
import ProjectEulerSolutions.P45
import ProjectEulerSolutions.Equiv.P45
import ProjectEulerSolutions.P46
import ProjectEulerSolutions.Equiv.P46
import ProjectEulerSolutions.P47
import ProjectEulerSolutions.Equiv.P47
import ProjectEulerSolutions.P48
import ProjectEulerSolutions.Equiv.P48
import ProjectEulerSolutions.P49
import ProjectEulerSolutions.Equiv.P49
import ProjectEulerSolutions.P50
import ProjectEulerSolutions.Equiv.P50
import ProjectEulerSolutions.P51
import ProjectEulerSolutions.Equiv.P51
import ProjectEulerSolutions.P52
import ProjectEulerSolutions.Equiv.P52
import ProjectEulerSolutions.P53
import ProjectEulerSolutions.Equiv.P53
import ProjectEulerSolutions.P54
import ProjectEulerSolutions.Equiv.P54
import ProjectEulerSolutions.P55
import ProjectEulerSolutions.Equiv.P55
import ProjectEulerSolutions.P56
import ProjectEulerSolutions.Equiv.P56
import ProjectEulerSolutions.P57
import ProjectEulerSolutions.Equiv.P57
import ProjectEulerSolutions.P58
import ProjectEulerSolutions.Equiv.P58
import ProjectEulerSolutions.P59
import ProjectEulerSolutions.Equiv.P59
import ProjectEulerSolutions.P60
import ProjectEulerSolutions.Equiv.P60
import ProjectEulerSolutions.P61
import ProjectEulerSolutions.Equiv.P61
import ProjectEulerSolutions.P62
import ProjectEulerSolutions.Equiv.P62
import ProjectEulerSolutions.P63
import ProjectEulerSolutions.Equiv.P63
import ProjectEulerSolutions.P64
import ProjectEulerSolutions.Equiv.P64
import ProjectEulerSolutions.P65
import ProjectEulerSolutions.Equiv.P65
import ProjectEulerSolutions.P66
import ProjectEulerSolutions.Equiv.P66
import ProjectEulerSolutions.P67
import ProjectEulerSolutions.Equiv.P67
import ProjectEulerSolutions.P68
import ProjectEulerSolutions.Equiv.P68
import ProjectEulerSolutions.P69
import ProjectEulerSolutions.Equiv.P69
import ProjectEulerSolutions.P70
import ProjectEulerSolutions.Equiv.P70
import ProjectEulerSolutions.P71
import ProjectEulerSolutions.Equiv.P71
import ProjectEulerSolutions.P72
import ProjectEulerSolutions.Equiv.P72
import ProjectEulerSolutions.P73
import ProjectEulerSolutions.Equiv.P73
import ProjectEulerSolutions.P74
import ProjectEulerSolutions.Equiv.P74
import ProjectEulerSolutions.P75
import ProjectEulerSolutions.Equiv.P75
import ProjectEulerSolutions.P76
import ProjectEulerSolutions.Equiv.P76
import ProjectEulerSolutions.P77
import ProjectEulerSolutions.Equiv.P77
import ProjectEulerSolutions.P78
import ProjectEulerSolutions.Equiv.P78
import ProjectEulerSolutions.P79
import ProjectEulerSolutions.Equiv.P79
import ProjectEulerSolutions.P80
import ProjectEulerSolutions.Equiv.P80
import ProjectEulerSolutions.P81
import ProjectEulerSolutions.Equiv.P81
import ProjectEulerSolutions.P82
import ProjectEulerSolutions.Equiv.P82
import ProjectEulerSolutions.P83
import ProjectEulerSolutions.Equiv.P83
import ProjectEulerSolutions.P84
import ProjectEulerSolutions.Equiv.P84
import ProjectEulerSolutions.P85
import ProjectEulerSolutions.Equiv.P85
import ProjectEulerSolutions.P86
import ProjectEulerSolutions.Equiv.P86
import ProjectEulerSolutions.P87
import ProjectEulerSolutions.Equiv.P87
import ProjectEulerSolutions.P88
import ProjectEulerSolutions.Equiv.P88
import ProjectEulerSolutions.P89
import ProjectEulerSolutions.Equiv.P89
import ProjectEulerSolutions.P90
import ProjectEulerSolutions.Equiv.P90
import ProjectEulerSolutions.P91
import ProjectEulerSolutions.Equiv.P91
import ProjectEulerSolutions.P92
import ProjectEulerSolutions.Equiv.P92
import ProjectEulerSolutions.P93
import ProjectEulerSolutions.Equiv.P93
import ProjectEulerSolutions.P94
import ProjectEulerSolutions.Equiv.P94
import ProjectEulerSolutions.P95
import ProjectEulerSolutions.Equiv.P95
import ProjectEulerSolutions.P96
import ProjectEulerSolutions.Equiv.P96
import ProjectEulerSolutions.P97
import ProjectEulerSolutions.Equiv.P97
import ProjectEulerSolutions.P98
import ProjectEulerSolutions.Equiv.P98
import ProjectEulerSolutions.P99
import ProjectEulerSolutions.Equiv.P99
import ProjectEulerSolutions.P100
import ProjectEulerSolutions.Equiv.P100

example : ProjectEulerStatements.P1.naive = ProjectEulerSolutions.P1.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P1.equiv

example : ProjectEulerStatements.P2.naive = ProjectEulerSolutions.P2.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P2.equiv

example : ProjectEulerStatements.P3.naive = ProjectEulerSolutions.P3.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P3.equiv

example : ProjectEulerStatements.P4.naive = ProjectEulerSolutions.P4.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P4.equiv

example : ProjectEulerStatements.P5.naive = ProjectEulerSolutions.P5.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P5.equiv

example : ProjectEulerStatements.P6.naive = ProjectEulerSolutions.P6.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P6.equiv

example : ProjectEulerStatements.P7.naive = ProjectEulerSolutions.P7.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P7.equiv

example : ProjectEulerStatements.P8.naive = ProjectEulerSolutions.P8.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P8.equiv

example : ProjectEulerStatements.P9.naive = ProjectEulerSolutions.P9.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P9.equiv

example : ProjectEulerStatements.P10.naive = ProjectEulerSolutions.P10.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P10.equiv

example : ProjectEulerStatements.P11.naive = ProjectEulerSolutions.P11.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P11.equiv

example : ProjectEulerStatements.P12.naive = ProjectEulerSolutions.P12.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P12.equiv

example : ProjectEulerStatements.P13.naive = ProjectEulerSolutions.P13.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P13.equiv

example : ProjectEulerStatements.P14.naive = ProjectEulerSolutions.P14.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P14.equiv

example : ProjectEulerStatements.P15.naive = ProjectEulerSolutions.P15.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P15.equiv

example : ProjectEulerStatements.P16.naive = ProjectEulerSolutions.P16.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P16.equiv

example : ProjectEulerStatements.P17.naive = ProjectEulerSolutions.P17.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P17.equiv

example : ProjectEulerStatements.P18.naive = ProjectEulerSolutions.P18.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P18.equiv

example : ProjectEulerStatements.P19.naive = ProjectEulerSolutions.P19.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P19.equiv

example : ProjectEulerStatements.P20.naive = ProjectEulerSolutions.P20.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P20.equiv

example : ProjectEulerStatements.P21.naive = ProjectEulerSolutions.P21.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P21.equiv

example : ProjectEulerStatements.P22.naive = ProjectEulerSolutions.P22.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P22.equiv

example : ProjectEulerStatements.P23.naive = ProjectEulerSolutions.P23.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P23.equiv

example : ProjectEulerStatements.P24.naive = ProjectEulerSolutions.P24.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P24.equiv

example : ProjectEulerStatements.P25.naive = ProjectEulerSolutions.P25.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P25.equiv

example : ProjectEulerStatements.P26.naive = ProjectEulerSolutions.P26.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P26.equiv

example : ProjectEulerStatements.P27.naive = ProjectEulerSolutions.P27.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P27.equiv

example : ProjectEulerStatements.P28.naive = ProjectEulerSolutions.P28.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P28.equiv

example : ProjectEulerStatements.P29.naive = ProjectEulerSolutions.P29.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P29.equiv

example : ProjectEulerStatements.P30.naive = ProjectEulerSolutions.P30.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P30.equiv

example : ProjectEulerStatements.P31.naive = ProjectEulerSolutions.P31.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P31.equiv

example : ProjectEulerStatements.P32.naive = ProjectEulerSolutions.P32.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P32.equiv

example : ProjectEulerStatements.P33.naive = ProjectEulerSolutions.P33.solve := by
  exact ProjectEulerSolutions.P33.equiv

example : ProjectEulerStatements.P34.naive = ProjectEulerSolutions.P34.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P34.equiv

example : ProjectEulerStatements.P35.naive = ProjectEulerSolutions.P35.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P35.equiv

example : ProjectEulerStatements.P36.naive = ProjectEulerSolutions.P36.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P36.equiv

example : ProjectEulerStatements.P37.naive = ProjectEulerSolutions.P37.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P37.equiv

example : ProjectEulerStatements.P38.naive = ProjectEulerSolutions.P38.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P38.equiv

example : ProjectEulerStatements.P39.naive = ProjectEulerSolutions.P39.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P39.equiv

example : ProjectEulerStatements.P40.naive = ProjectEulerSolutions.P40.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P40.equiv

example : ProjectEulerStatements.P41.naive = ProjectEulerSolutions.P41.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P41.equiv

example : ProjectEulerStatements.P42.naive = ProjectEulerSolutions.P42.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P42.equiv

example : ProjectEulerStatements.P43.naive = ProjectEulerSolutions.P43.solve := by
  exact ProjectEulerSolutions.P43.equiv

example : ProjectEulerStatements.P44.naive = ProjectEulerSolutions.P44.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P44.equiv

example : ProjectEulerStatements.P45.naive = ProjectEulerSolutions.P45.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P45.equiv

example : ProjectEulerStatements.P46.naive = ProjectEulerSolutions.P46.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P46.equiv

example : ProjectEulerStatements.P47.naive = ProjectEulerSolutions.P47.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P47.equiv

example : ProjectEulerStatements.P48.naive = ProjectEulerSolutions.P48.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P48.equiv

example : ProjectEulerStatements.P49.naive = ProjectEulerSolutions.P49.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P49.equiv

example : ProjectEulerStatements.P50.naive = ProjectEulerSolutions.P50.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P50.equiv

example : ProjectEulerStatements.P51.naive = ProjectEulerSolutions.P51.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P51.equiv

example : ProjectEulerStatements.P52.naive = ProjectEulerSolutions.P52.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P52.equiv

example : ProjectEulerStatements.P53.naive = ProjectEulerSolutions.P53.solve := by
  exact ProjectEulerSolutions.P53.equiv

example : ProjectEulerStatements.P54.naive = ProjectEulerSolutions.P54.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P54.equiv

example : ProjectEulerStatements.P55.naive = ProjectEulerSolutions.P55.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P55.equiv

example : ProjectEulerStatements.P56.naive = ProjectEulerSolutions.P56.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P56.equiv

example : ProjectEulerStatements.P57.naive = ProjectEulerSolutions.P57.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P57.equiv

example : ProjectEulerStatements.P58.naive = ProjectEulerSolutions.P58.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P58.equiv

example : ProjectEulerStatements.P59.naive = ProjectEulerSolutions.P59.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P59.equiv

example : ProjectEulerStatements.P60.naive = ProjectEulerSolutions.P60.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P60.equiv

example : ProjectEulerStatements.P61.naive = ProjectEulerSolutions.P61.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P61.equiv

example : ProjectEulerStatements.P62.naive = ProjectEulerSolutions.P62.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P62.equiv

example : ProjectEulerStatements.P63.naive = ProjectEulerSolutions.P63.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P63.equiv

example : ProjectEulerStatements.P64.naive = ProjectEulerSolutions.P64.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P64.equiv

example : ProjectEulerStatements.P65.naive = ProjectEulerSolutions.P65.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P65.equiv

example : ProjectEulerStatements.P66.naive = ProjectEulerSolutions.P66.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P66.equiv

example : ProjectEulerStatements.P67.naive = ProjectEulerSolutions.P67.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P67.equiv

example : ProjectEulerStatements.P68.naive = ProjectEulerSolutions.P68.solve := by
  exact ProjectEulerSolutions.P68.equiv

example : ProjectEulerStatements.P69.naive = ProjectEulerSolutions.P69.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P69.equiv

example : ProjectEulerStatements.P70.naive = ProjectEulerSolutions.P70.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P70.equiv

example : ProjectEulerStatements.P71.naive = ProjectEulerSolutions.P71.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P71.equiv

example : ProjectEulerStatements.P72.naive = ProjectEulerSolutions.P72.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P72.equiv

example : ProjectEulerStatements.P73.naive = ProjectEulerSolutions.P73.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P73.equiv

example : ProjectEulerStatements.P74.naive = ProjectEulerSolutions.P74.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P74.equiv

example : ProjectEulerStatements.P75.naive = ProjectEulerSolutions.P75.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P75.equiv

example : ProjectEulerStatements.P76.naive = ProjectEulerSolutions.P76.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P76.equiv

example : ProjectEulerStatements.P77.naive = ProjectEulerSolutions.P77.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P77.equiv

example : ProjectEulerStatements.P78.naive = ProjectEulerSolutions.P78.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P78.equiv

example : ProjectEulerStatements.P79.naive = ProjectEulerSolutions.P79.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P79.equiv

example : ProjectEulerStatements.P80.naive = ProjectEulerSolutions.P80.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P80.equiv

example : ProjectEulerStatements.P81.naive = ProjectEulerSolutions.P81.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P81.equiv

example : ProjectEulerStatements.P82.naive = ProjectEulerSolutions.P82.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P82.equiv

example : ProjectEulerStatements.P83.naive = ProjectEulerSolutions.P83.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P83.equiv

example : ProjectEulerStatements.P84.naive = ProjectEulerSolutions.P84.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P84.equiv

example : ProjectEulerStatements.P85.naive = ProjectEulerSolutions.P85.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P85.equiv

example : ProjectEulerStatements.P86.naive = ProjectEulerSolutions.P86.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P86.equiv

example : ProjectEulerStatements.P87.naive = ProjectEulerSolutions.P87.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P87.equiv

example : ProjectEulerStatements.P88.naive = ProjectEulerSolutions.P88.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P88.equiv

example : ProjectEulerStatements.P89.naive = ProjectEulerSolutions.P89.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P89.equiv

example : ProjectEulerStatements.P90.naive = ProjectEulerSolutions.P90.solve := by
  exact ProjectEulerSolutions.P90.equiv

example : ProjectEulerStatements.P91.naive = ProjectEulerSolutions.P91.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P91.equiv

example : ProjectEulerStatements.P92.naive = ProjectEulerSolutions.P92.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P92.equiv

example : ProjectEulerStatements.P93.naive = ProjectEulerSolutions.P93.solve := by
  exact ProjectEulerSolutions.P93.equiv

example : ProjectEulerStatements.P94.naive = ProjectEulerSolutions.P94.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P94.equiv

example : ProjectEulerStatements.P95.naive = ProjectEulerSolutions.P95.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P95.equiv

example : ProjectEulerStatements.P96.naive = ProjectEulerSolutions.P96.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P96.equiv

example : ProjectEulerStatements.P97.naive = ProjectEulerSolutions.P97.solve := by
  exact ProjectEulerSolutions.P97.equiv

example : ProjectEulerStatements.P98.naive = ProjectEulerSolutions.P98.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P98.equiv

example : ProjectEulerStatements.P99.naive = ProjectEulerSolutions.P99.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P99.equiv

example : ProjectEulerStatements.P100.naive = ProjectEulerSolutions.P100.solve := by
  apply (funext_iff).2
  simpa [funext_iff] using ProjectEulerSolutions.P100.equiv