Unsolved @ Lean 
An auto-updating collection of wanted proofs (sorry and proof_wanted) in the Lean4 theorem prover across established projects.
The raw list of wanted proofs is also available in ND-JSON at ./repositories.json.
There are currently 416 wanted proofs.
Repositories
Wanted Proofs
Mathlib.Order.KrullDimension.lean:899 (playground)Mathlib.Order.KrullDimension.lean:902 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:39 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:43 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:48 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:61 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:68 (playground)Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic.lean:102 (playground)Mathlib.Computability.TMComputable.lean:310 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:226 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:233 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:240 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:247 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:253 (playground)Mathlib.Combinatorics.SimpleGraph.StronglyRegular.lean:67 (playground)Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic.lean:116 (playground)Mathlib.RingTheory.KrullDimension.Basic.lean:82 (playground)Mathlib.RingTheory.KrullDimension.Basic.lean:85 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:253 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:257 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:381 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:383 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:386 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:391 (playground)FLT.QuaternionAlgebra.NumberField.lean:52FLT.QuaternionAlgebra.NumberField.lean:56FLT.QuaternionAlgebra.NumberField.lean:146FLT.QuaternionAlgebra.NumberField.lean:150FLT.QuaternionAlgebra.NumberField.lean:190FLT.QuaternionAlgebra.NumberField.lean:193FLT.HaarMeasure.MeasurableSpacePadics.lean:67FLT.HaarMeasure.HaarChar.Ring.lean:50FLT.HaarMeasure.HaarChar.Ring.lean:58FLT.HaarMeasure.HaarChar.Ring.lean:59FLT.HaarMeasure.HaarChar.Ring.lean:64FLT.HaarMeasure.HaarChar.Ring.lean:70FLT.HaarMeasure.HaarChar.AddEquiv.lean:12FLT.HaarMeasure.HaarChar.AddEquiv.lean:48FLT.HaarMeasure.HaarChar.AddEquiv.lean:52FLT.HaarMeasure.HaarChar.AddEquiv.lean:57FLT.HaarMeasure.HaarChar.AddEquiv.lean:62FLT.HaarMeasure.HaarChar.AddEquiv.lean:69FLT.HaarMeasure.HaarChar.AddEquiv.lean:75FLT.HaarMeasure.HaarChar.AddEquiv.lean:80FLT.HaarMeasure.HaarChar.AdeleRing.lean:27FLT.HaarMeasure.HaarChar.AdeleRing.lean:38FLT.Mathlib.MeasureTheory.Group.Action.lean:24FLT.Mathlib.MeasureTheory.Group.Action.lean:31FLT.Mathlib.MeasureTheory.Group.Action.lean:36FLT.Mathlib.MeasureTheory.Group.Action.lean:41FLT.DivisionAlgebra.Finiteness.lean:45FLT.DivisionAlgebra.Finiteness.lean:56FLT.DivisionAlgebra.Finiteness.lean:70FLT.DivisionAlgebra.Finiteness.lean:99FLT.DivisionAlgebra.Finiteness.lean:102FLT.DivisionAlgebra.Finiteness.lean:108FLT.DivisionAlgebra.Finiteness.lean:126FLT.DivisionAlgebra.Finiteness.lean:131FLT.DivisionAlgebra.Finiteness.lean:141FLT.DivisionAlgebra.Finiteness.lean:175FLT.DivisionAlgebra.Finiteness.lean:186FLT.Basic.Reductions.lean:327FLT.Basic.Reductions.lean:337FLT.EllipticCurve.Torsion.lean:37FLT.EllipticCurve.Torsion.lean:41FLT.EllipticCurve.Torsion.lean:46FLT.EllipticCurve.Torsion.lean:51FLT.EllipticCurve.Torsion.lean:57FLT.EllipticCurve.Torsion.lean:63FLT.EllipticCurve.Torsion.lean:66FLT.EllipticCurve.Torsion.lean:71FLT.EllipticCurve.Torsion.lean:75FLT.EllipticCurve.Torsion.lean:79FLT.GlobalLanglandsConjectures.GLnDefs.lean:180FLT.GlobalLanglandsConjectures.GLnDefs.lean:190FLT.GlobalLanglandsConjectures.GLzero.lean:48FLT.GlobalLanglandsConjectures.GLzero.lean:74FLT.GlobalLanglandsConjectures.GLzero.lean:118FLT.GlobalLanglandsConjectures.GLzero.lean:119FLT.GlobalLanglandsConjectures.GLzero.lean:120FLT.GlobalLanglandsConjectures.GLzero.lean:121FLT.GlobalLanglandsConjectures.GLzero.lean:122FLT.GlobalLanglandsConjectures.GLzero.lean:127FLT.GlobalLanglandsConjectures.GLzero.lean:128FLT.GlobalLanglandsConjectures.GLzero.lean:129FLT.AutomorphicRepresentation.Example.lean:307FLT.AutomorphicRepresentation.Example.lean:476FLT.AutomorphicRepresentation.Example.lean:1065FLT.AutomorphicRepresentation.Example.lean:1072FLT.AutomorphicRepresentation.Example.lean:1076FLT.AutomorphicRepresentation.Example.lean:1078FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional.lean:21FLT.AutomorphicForm.QuaternionAlgebra.Defs.lean:45FLT.AutomorphicForm.QuaternionAlgebra.Defs.lean:171FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:1147FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:1155FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:1167FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:1173FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:1174FLT.DedekindDomain.AdicValuation.lean:281FLT.NumberField.AdeleRing.lean:29FLT.NumberField.AdeleRing.lean:87FLT.NumberField.AdeleRing.lean:330Seymour.Matroid.Constructors.StandardRepresentation.lean:545Seymour.Matroid.Constructors.StandardRepresentation.lean:633Seymour.Matroid.Constructors.StandardRepresentation.lean:634Seymour.Matroid.Constructors.StandardRepresentation.lean:640Seymour.Matroid.Constructors.StandardRepresentation.lean:642Seymour.Matroid.Constructors.StandardRepresentation.lean:644Seymour.Matroid.Constructors.StandardRepresentation.lean:661Seymour.Matroid.Constructors.StandardRepresentation.lean:665Seymour.Matroid.Operations.Duality.lean:34Seymour.Matroid.Operations.Duality.lean:56Seymour.Matroid.Operations.Duality.lean:57Seymour.Matroid.Operations.Sum1.lean:60Seymour.Matroid.Operations.Sum1.lean:62Seymour.Matroid.Operations.Sum3.lean:184Seymour.Matroid.Operations.Sum3Helper.lean:382Seymour.Matroid.Operations.Sum3Helper.lean:589Seymour.Matroid.Operations.Sum3Helper.lean:690Seymour.Matroid.Operations.Sum3Helper.lean:791Seymour.Matroid.Operations.Sum3Helper.lean:892Seymour.Matroid.Operations.Sum3Helper.lean:993Seymour.HardDirection.lean:8Seymour.Basic.SubmoduleSpans.lean:32Seymour.Basic.SubmoduleSpans.lean:46InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Horn.lean:39InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Horn.lean:99InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Horn.lean:155InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:128InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:129InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:133InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:134InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:135InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:159InfinityCosmos.ForMathlib.InfinityCosmos.Isofibrations.lean:70LeanAPAP.Mathlib.Topology.Algebra.PontryaginDual.lean:12LeanAPAP.Prereqs.LpNorm.Compact.lean:216LeanAPAP.Prereqs.LpNorm.Weighted.lean:107LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:54LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:56LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:95LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:139LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:161LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:184LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:186LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:186LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:186LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:187LeanAPAP.Prereqs.FourierTransform.Convolution.lean:47LeanAPAP.Prereqs.Bohr.Regular.lean:19LeanAPAP.Prereqs.DummyPositivity.lean:18LeanAPAP.Prereqs.DummyPositivity.lean:19LeanAPAP.Prereqs.DummyPositivity.lean:20LeanAPAP.Prereqs.DummyPositivity.lean:22LeanAPAP.Prereqs.DummyPositivity.lean:23LeanAPAP.Prereqs.DummyPositivity.lean:24LeanAPAP.Prereqs.DummyPositivity.lean:25LeanAPAP.Prereqs.DummyPositivity.lean:27LeanAPAP.Prereqs.DummyPositivity.lean:28LeanAPAP.Prereqs.DummyPositivity.lean:29LeanAPAP.Prereqs.DummyPositivity.lean:30LeanAPAP.Prereqs.DummyPositivity.lean:31LeanAPAP.Prereqs.DummyPositivity.lean:32LeanAPAP.Prereqs.DummyPositivity.lean:33LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:50LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:94LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:96LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:98LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:100LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:101LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:131LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:43LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:73LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:75LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:77LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:79LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:80LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:111LeanAPAP.FiniteField.lean:143LeanAPAP.FiniteField.lean:172LeanAPAP.FiniteField.lean:190LeanAPAP.FiniteField.lean:200LeanAPAP.FiniteField.lean:223LeanAPAP.FiniteField.lean:231LeanAPAP.Integer.lean:7LeanCamCombi.GrowthInGroups.Lecture4.lean:25LeanCamCombi.GrowthInGroups.Lecture4.lean:30LeanCamCombi.GrowthInGroups.Lecture4.lean:41LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:24LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:42LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:45LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:46LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:54LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:59LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:60LeanCamCombi.GraphTheory.ExampleSheet1.lean:38LeanCamCombi.GraphTheory.ExampleSheet1.lean:57LeanCamCombi.GraphTheory.ExampleSheet1.lean:70LeanCamCombi.GraphTheory.ExampleSheet1.lean:83LeanCamCombi.GraphTheory.ExampleSheet1.lean:101LeanCamCombi.GraphTheory.ExampleSheet1.lean:113LeanCamCombi.GraphTheory.ExampleSheet1.lean:128LeanCamCombi.GraphTheory.ExampleSheet1.lean:145LeanCamCombi.GraphTheory.ExampleSheet1.lean:160LeanCamCombi.GraphTheory.ExampleSheet1.lean:181LeanCamCombi.GraphTheory.ExampleSheet1.lean:197LeanCamCombi.GraphTheory.ExampleSheet1.lean:214LeanCamCombi.GraphTheory.ExampleSheet1.lean:219LeanCamCombi.GraphTheory.ExampleSheet1.lean:224LeanCamCombi.GraphTheory.ExampleSheet1.lean:247LeanCamCombi.GraphTheory.ExampleSheet1.lean:252LeanCamCombi.StableCombi.Rel.lean:38LeanCamCombi.StableCombi.Rel.lean:41LeanCamCombi.PlainCombi.VanDenBergKesten.lean:97LeanCamCombi.PlainCombi.LittlewoodOfford.lean:33LeanCamCombi.ExtrProbCombi.BinomialRandomGraph.lean:46LeanCamCombi.ExtrProbCombi.BollobasContainment.lean:31LeanCamCombi.ExtrProbCombi.BollobasContainment.lean:37LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:117LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:118LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:126LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:127LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:128LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:129LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:130LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:131LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:132Carleson.Antichain.TileCorrelation.lean:359Carleson.Antichain.TileCorrelation.lean:368Carleson.Antichain.TileCorrelation.lean:370Carleson.Antichain.AntichainOperator.lean:312Carleson.Antichain.AntichainOperator.lean:329Carleson.Antichain.AntichainOperator.lean:334Carleson.Antichain.AntichainOperator.lean:379Carleson.Antichain.AntichainOperator.lean:385Carleson.Antichain.AntichainOperator.lean:420Carleson.Antichain.AntichainOperator.lean:434Carleson.Antichain.AntichainOperator.lean:449Carleson.Antichain.AntichainOperator.lean:499Carleson.Antichain.AntichainTileCount.lean:344Carleson.Antichain.AntichainTileCount.lean:358Carleson.LinearizedMetricCarleson.lean:30Carleson.TwoSidedCarleson.MainTheorem.lean:34Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:49Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:61Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:81Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:87Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:134Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:142Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:150Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:155Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:159Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:197Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:202Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:213Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:219Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:224Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:230Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:236Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:241Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:247Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:253Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:259Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:265Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:271Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:277Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:296Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:312Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:322Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:333Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:349Carleson.TwoSidedCarleson.NontangentialOperator.lean:677Carleson.TwoSidedCarleson.NontangentialOperator.lean:687Carleson.TwoSidedCarleson.NontangentialOperator.lean:698Carleson.TwoSidedCarleson.NontangentialOperator.lean:709Carleson.TwoSidedCarleson.NontangentialOperator.lean:717Carleson.TwoSidedCarleson.NontangentialOperator.lean:724Carleson.TwoSidedCarleson.NontangentialOperator.lean:731Carleson.TwoSidedCarleson.NontangentialOperator.lean:739Carleson.TwoSidedCarleson.NontangentialOperator.lean:750Carleson.ToMathlib.HardyLittlewood.lean:78Carleson.ToMathlib.HardyLittlewood.lean:384Carleson.ToMathlib.HardyLittlewood.lean:415Carleson.ToMathlib.HardyLittlewood.lean:578Carleson.ToMathlib.HardyLittlewood.lean:782Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities.lean:253Carleson.MetricCarleson.lean:33Carleson.TileStructure.lean:524Carleson.ForestOperator.RemainingTiles.lean:372Carleson.ForestOperator.RemainingTiles.lean:387Carleson.ForestOperator.Forests.lean:37Carleson.ForestOperator.Forests.lean:49Carleson.ForestOperator.Forests.lean:257Carleson.ForestOperator.Forests.lean:265Carleson.ForestOperator.Forests.lean:280Carleson.ForestOperator.Forests.lean:352Carleson.ForestOperator.LargeSeparation.lean:971Carleson.ForestOperator.LargeSeparation.lean:1421Carleson.ForestOperator.LargeSeparation.lean:1484Carleson.ForestOperator.LargeSeparation.lean:1502Carleson.ForestOperator.LargeSeparation.lean:1611Carleson.ForestOperator.AlmostOrthogonality.lean:313Carleson.Classical.HilbertStrongType.lean:58Carleson.Classical.HilbertStrongType.lean:68Carleson.Classical.HilbertStrongType.lean:134Carleson.Classical.HilbertStrongType.lean:160Carleson.Classical.HilbertStrongType.lean:168Carleson.Classical.HilbertStrongType.lean:172Carleson.Classical.HilbertStrongType.lean:182Carleson.Classical.HilbertStrongType.lean:192Carleson.Classical.HilbertStrongType.lean:205PFR.MultiTauFunctional.lean:54PFR.MultiTauFunctional.lean:57PFR.MoreRuzsaDist.lean:527PFR.MoreRuzsaDist.lean:760PFR.MoreRuzsaDist.lean:857PFR.MoreRuzsaDist.lean:862PFR.MoreRuzsaDist.lean:868PFR.MoreRuzsaDist.lean:873PFR.TorsionEndgame.lean:50PFR.TorsionEndgame.lean:52PFR.TorsionEndgame.lean:54PFR.TorsionEndgame.lean:58PFR.TorsionEndgame.lean:61PFR.TorsionEndgame.lean:64PFR.TorsionEndgame.lean:67PFR.TorsionEndgame.lean:79PFR.TorsionEndgame.lean:82PFR.TorsionEndgame.lean:89PFR.TorsionEndgame.lean:102PFR.ApproxHomPFR.lean:181PFR.ApproxHomPFR.lean:183PFR.ApproxHomPFR.lean:185PFR.ApproxHomPFR.lean:189PFR.BoundingMutual.lean:36FormalBook.Chapter_08.lean:49FormalBook.Chapter_08.lean:58FormalBook.Chapter_08.lean:66FormalBook.Chapter_08.lean:69FormalBook.Chapter_08.lean:77FormalBook.Chapter_08.lean:80FormalBook.Chapter_08.lean:98FormalBook.Chapter_08.lean:110FormalBook.Chapter_08.lean:118FormalBook.Chapter_08.lean:119FormalBook.Chapter_08.lean:124FormalBook.Chapter_08.lean:127FormalBook.Chapter_02.lean:218FormalBook.Chapter_02.lean:223FormalBook.Chapter_02.lean:227FormalBook.Chapter_20.lean:97FormalBook.Chapter_20.lean:109FormalBook.Chapter_20.lean:120FormalBook.Chapter_05.lean:52FormalBook.Chapter_05.lean:53FormalBook.Chapter_05.lean:58FormalBook.Chapter_05.lean:62FormalBook.Chapter_05.lean:75FormalBook.Chapter_05.lean:78FormalBook.Chapter_05.lean:83FormalBook.Chapter_05.lean:97FormalBook.Chapter_05.lean:103FormalBook.Chapter_05.lean:112FormalBook.Chapter_05.lean:117FormalBook.Chapter_06.lean:69FormalBook.Chapter_06.lean:70FormalBook.Chapter_06.lean:76FormalBook.Chapter_06.lean:77FormalBook.Chapter_06.lean:78FormalBook.Chapter_06.lean:79FormalBook.Chapter_06.lean:83FormalBook.Chapter_06.lean:210FormalBook.Chapter_06.lean:238FormalBook.Chapter_06.lean:242FormalBook.Chapter_06.lean:246FormalBook.Chapter_06.lean:255FormalBook.Chapter_06.lean:256FormalBook.Chapter_06.lean:291FormalBook.Chapter_44.lean:47FormalBook.Chapter_44.lean:53FormalBook.Chapter_44.lean:106FormalBook.Chapter_44.lean:108FormalBook.Chapter_21.lean:30FormalBook.Chapter_07.lean:32FormalBook.Chapter_07.lean:38FormalBook.Chapter_03.lean:37FormalBook.Chapter_03.lean:97FormalBook.Chapter_03.lean:150FormalBook.Chapter_03.lean:154FormalBook.Chapter_03.lean:157FormalBook.Chapter_03.lean:159FormalBook.Chapter_03.lean:174FormalBook.Chapter_04.lean:48FormalBook.Chapter_04.lean:53FormalBook.Chapter_04.lean:85FormalBook.Chapter_04.lean:182FormalBook.Chapter_04.lean:235FormalBook.Chapter_04.lean:244FormalBook.Chapter_04.lean:283FormalBook.Chapter_45.lean:41FormalBook.Chapter_45.lean:58FormalBook.Chapter_01.lean:184FormalBook.Chapter_01.lean:185FormalBook.Chapter_01.lean:186FormalBook.Chapter_01.lean:187FormalBook.Chapter_01.lean:188FormalBook.Chapter_01.lean:189FormalBook.Chapter_01.lean:190FormalBook.Chapter_01.lean:339FormalBook.Chapter_01.lean:360FormalBook.Chapter_24.lean:38FormalBook.Chapter_09.lean:27FormalBook.Chapter_09.lean:31FormalBook.Chapter_09.lean:35FormalBook.Chapter_09.lean:39