Elementary inequality #39437

Proved

WorkbookCorrected.plus_39437

by carlok · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

(4047119176083805434265797025038021928486031972132662244174559604184067419413015502417514974704977005414384999988162591895766948918300642522977247338363917771668970779777753527826553766164546256964525856356114840905252374846498470910816583027184585800488129263597372039799778564485664338125234605261302370308604614868072617657123918173702445398366372322417434461601835309856992659660645653354614982750057572432041379859274621442110811520402648801863164500752396924910917623673324044214615457098569078938740922192534352031793431514803832251398086982109873975990680483415025253862068383663792120185419392432427204656247460543873615272534865334565495292291157356677830410985218619709013493998389092605131022902504911498593633347264706681721293652471377650548764901431929174984592169115453817959530854752141647645901647151985905453578107850692346583151685738820236711443200200370759572763275556424988614859872450040999806736417711161867598247053231428559798621463671209722370673825312340737340040170538154747860020316103015044122614154424900774992662352026100988597837653170000257771822429952467665040616029657024007252152817562615366751065630904467862012544141768156684504749231917987624625441324843621995406946736998517482823746027862698245952830337345108841325062714188374174983144485739647545172292802582223373116803265421066730099489162411963449260642972869629203644155625461676880959109239303433327706961238191826247718877073151851011905211548035289914844279236392583020933100443913551676806035413657248899891307999372822542339404148694132855322857220343144060871665339542683864136487216591052371374189059947138910852889040308750708844047045992546837771181081229834457431263089449331493573058322424466575497422513671327399076639665725541499091/6280080974999750442868657555435444540579708836483241131071786594354764588473769562703702061098338887611658549781091577141872352053742525426275706682010214404239227993369890590148121652418985009676596005782077199438651812682339885750690749146836527099022479591921678469734687276623386685465457056854359693981892033579856745106074125155964744383014159480098509389791942564806045375312640398774957690826163824237696200799187134480558402777258419336929289091528248362386557019968138875505743742466823204465606777830097693654563016523391140977822807937541833794832478832878770567775017257113270889295544650352401436890956365245475674671830441334949744001976510269165635438875363697929508479383306095423486351727948441430093876935282430416479026415742946056853383779821293522356450091088408046601249920983014112397410721578591908874802098707014842718148959014476813186360431291604804165982857223645779037277859396853705567733612771102428725827909781931769151169095189808653909447490353780821423670955433960727193491321892104245992630787635612578447464667760433833838933844903831795014773466332196119272991017178921280213984496379833140544846689390922127145330327723868963437344660239542630448589319383251610369923700415980239592641642891877516772598343356793489004987136981993997884015563506030817734845598904357881177763858027969399244632978642504512196132313421512096866559381023281576515518374633241518994052047718860235604263786170765358856646061298557858246139995518953318232548478220319927256538545029890121594116618828694968005114630126141871743061719746913756314853861498737784699496616182770144322476614639522413344049438341294225874892400232631414896063289640437244981427317240701406915860792889133928042568217413365918177184603750400000000:ℚ) < (5/3:ℚ)

holds by direct arithmetic evaluation.

Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_39437, which omitted a compilable colon/type annotation and/or used a preamble of only Mathlib.Analysis.Complex.Basic.

Source: InternLM Lean-Workbook, record lean_workbook_plus_39437 (Apache-2.0).

Preamble

import Mathlib.Data.Rat.Defs
import Mathlib.Tactic.NormNum

Formal statement

theorem WorkbookCorrected.plus_39437 : (4047119176083805434265797025038021928486031972132662244174559604184067419413015502417514974704977005414384999988162591895766948918300642522977247338363917771668970779777753527826553766164546256964525856356114840905252374846498470910816583027184585800488129263597372039799778564485664338125234605261302370308604614868072617657123918173702445398366372322417434461601835309856992659660645653354614982750057572432041379859274621442110811520402648801863164500752396924910917623673324044214615457098569078938740922192534352031793431514803832251398086982109873975990680483415025253862068383663792120185419392432427204656247460543873615272534865334565495292291157356677830410985218619709013493998389092605131022902504911498593633347264706681721293652471377650548764901431929174984592169115453817959530854752141647645901647151985905453578107850692346583151685738820236711443200200370759572763275556424988614859872450040999806736417711161867598247053231428559798621463671209722370673825312340737340040170538154747860020316103015044122614154424900774992662352026100988597837653170000257771822429952467665040616029657024007252152817562615366751065630904467862012544141768156684504749231917987624625441324843621995406946736998517482823746027862698245952830337345108841325062714188374174983144485739647545172292802582223373116803265421066730099489162411963449260642972869629203644155625461676880959109239303433327706961238191826247718877073151851011905211548035289914844279236392583020933100443913551676806035413657248899891307999372822542339404148694132855322857220343144060871665339542683864136487216591052371374189059947138910852889040308750708844047045992546837771181081229834457431263089449331493573058322424466575497422513671327399076639665725541499091/6280080974999750442868657555435444540579708836483241131071786594354764588473769562703702061098338887611658549781091577141872352053742525426275706682010214404239227993369890590148121652418985009676596005782077199438651812682339885750690749146836527099022479591921678469734687276623386685465457056854359693981892033579856745106074125155964744383014159480098509389791942564806045375312640398774957690826163824237696200799187134480558402777258419336929289091528248362386557019968138875505743742466823204465606777830097693654563016523391140977822807937541833794832478832878770567775017257113270889295544650352401436890956365245475674671830441334949744001976510269165635438875363697929508479383306095423486351727948441430093876935282430416479026415742946056853383779821293522356450091088408046601249920983014112397410721578591908874802098707014842718148959014476813186360431291604804165982857223645779037277859396853705567733612771102428725827909781931769151169095189808653909447490353780821423670955433960727193491321892104245992630787635612578447464667760433833838933844903831795014773466332196119272991017178921280213984496379833140544846689390922127145330327723868963437344660239542630448589319383251610369923700415980239592641642891877516772598343356793489004987136981993997884015563506030817734845598904357881177763858027969399244632978642504512196132313421512096866559381023281576515518374633241518994052047718860235604263786170765358856646061298557858246139995518953318232548478220319927256538545029890121594116618828694968005114630126141871743061719746913756314853861498737784699496616182770144322476614639522413344049438341294225874892400232631414896063289640437244981427317240701406915860792889133928042568217413365918177184603750400000000:ℚ) < (5/3:ℚ) := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_39437; Apache-2.0; corrects Open node d25db93d-b985-43d5-a140-8a68eb1dd6e8

View graph