diff --git a/Leaff/Diff.lean b/Leaff/Diff.lean index e65ff31..7a3eabf 100644 --- a/Leaff/Diff.lean +++ b/Leaff/Diff.lean @@ -122,34 +122,45 @@ Note: this declaration also occurs as `shouldIgnore` in the Lean 4 file `test/le -- TODO maybe isBlackListed from mathlib instead? or something else that removes mk.inj and sizeOf_spec open Lean + +-- TODO shorten after https://github.com/leanprover/lean4/pull/3058 +deriving instance BEq for ReducibilityHints +deriving instance BEq for DefinitionVal +deriving instance BEq for QuotKind +deriving instance BEq for QuotVal +deriving instance BEq for InductiveVal +deriving instance BEq for ConstantInfo + +-- TODO simplify binders (a b : Name) /-- A type representing single differences between two environments, limited to changes that a user might wish to see. -/ inductive Diff : Type - | added (name : Name) - | removed (name : Name) - | renamed (oldName newName : Name) (namespaceOnly : Bool) + | added (const : ConstantInfo) (relevantModule : Name) -- TODO use constantinfo in others too + | removed (name : Name) (relevantModule : Name) + | renamed (oldName newName : Name) (namespaceOnly : Bool) (relevantModule : Name) | movedToModule (name oldModuleName newModuleName : Name) -- maybe args here - | proofChanged (name : Name) (isProofRelevant : Bool) -- TODO maybe value changed also for defs - | typeChanged (name : Name) - | speciesChanged (name : Name) (fro to : String) -- species is axiom, def, thm, opaque, quot, induct, ctor, rec - | movedWithinModule (name : Name) + | proofChanged (name : Name) (isProofRelevant : Bool) (relevantModule : Name) -- TODO maybe value changed also for defs + | typeChanged (name : Name) (relevantModule : Name) + | speciesChanged (name : Name) (fro to : String) (relevantModule : Name) -- species is axiom, def, thm, opaque, quot, induct, ctor, rec + | movedWithinModule (name : Name) (relevantModule : Name) | extensionEntriesModified (ext : Name) -- TODO maybe delete? - | docChanged (name : Name) -- TODO how does module/other doc fit in here - | docAdded (name : Name) - | docRemoved (name : Name) + | docChanged (name : Name) (relevantModule : Name) -- TODO how does module/other doc fit in here + | docAdded (name : Name) (relevantModule : Name) + | docRemoved (name : Name) (relevantModule : Name) | moduleAdded (name : Name) | moduleRemoved (name : Name) | moduleRenamed (oldName newName : Name) - | attributeAdded (attrName name : Name) - | attributeRemoved (attrName name : Name) - | attributeChanged (attrName name : Name) + | attributeAdded (attrName name : Name) (relevantModule : Name) + | attributeRemoved (attrName name : Name) (relevantModule : Name) + | attributeChanged (attrName name : Name) (relevantModule : Name) | directImportAdded (module importName : Name) -- these might be pointless | directImportRemoved (module importName : Name) | transitiveImportAdded (module importName : Name) | transitiveImportRemoved (module importName : Name) -deriving DecidableEq, Repr +-- deriving DecidableEq, Repr +deriving BEq -- what combinations? all pairs? -- renamed and proof modified @@ -164,71 +175,102 @@ namespace Diff /-- Priority for displaying diffs, lower numbers are more important and should come first in the output. These should all be distinct as it is what we use to group diffs also -/ def prio : Diff → Nat - | .added _ => 80 - | .removed _ => 90 - | .renamed _ _ false => 200 - | .renamed _ _ true => 210 + | .added _ _ => 80 + | .removed _ _ => 90 + | .renamed _ _ false _ => 200 + | .renamed _ _ true _ => 210 | .movedToModule _ _ _ => 220 - | .movedWithinModule _ => 310 - | .proofChanged _ true => 110 -- if the declaration is proof relevant (i.e. a def) then it is more important - | .proofChanged _ _ => 250 - | .typeChanged _ => 100 - | .speciesChanged _ _ _ => 140 + | .movedWithinModule _ _ => 310 + | .proofChanged _ true _ => 110 -- if the declaration is proof relevant (i.e. a def) then it is more important + | .proofChanged _ _ _ => 250 + | .typeChanged _ _ => 100 + | .speciesChanged _ _ _ _ => 140 | .extensionEntriesModified _ => 150 - | .docChanged _ => 240 - | .docAdded _ => 230 - | .docRemoved _ => 160 + | .docChanged _ _ => 240 + | .docAdded _ _ => 230 + | .docRemoved _ _ => 160 | .moduleAdded _ => 105 | .moduleRemoved _ => 107 | .moduleRenamed _ _ => 170 - | .attributeAdded _ _ => 180 - | .attributeRemoved _ _ => 190 - | .attributeChanged _ _ => 260 + | .attributeAdded _ _ _ => 180 + | .attributeRemoved _ _ _ => 190 + | .attributeChanged _ _ _ => 260 | .directImportAdded _ _ => 195 | .directImportRemoved _ _ => 270 | .transitiveImportAdded _ _ => 330 | .transitiveImportRemoved _ _ => 340 -- TODO maybe order this in src to make it clearer +def mod : Diff → Name + | .added _ m + | .removed _ m + | .renamed _ _ _ m + | .movedWithinModule _ m + | .proofChanged _ _ m + | .typeChanged _ m + | .speciesChanged _ _ _ m + | .docChanged _ m + | .docAdded _ m + | .docRemoved _ m + | .moduleAdded m + | .moduleRemoved m + | .attributeAdded _ _ m + | .attributeRemoved _ _ m + | .attributeChanged _ _ m => m + | .movedToModule _ _ _ + | .moduleRenamed _ _ + | .extensionEntriesModified _ + | .directImportAdded _ _ + | .directImportRemoved _ _ + | .transitiveImportAdded _ _ + | .transitiveImportRemoved _ _ => Name.anonymous + open Std + -- TODO can we make the output richer, -- colours (sort of handled by diff format in github) -- links / messagedata in the infoview maybe extracted as links somehow -- especially for the diffs command --- TODO group by module name using @@module@@ open ToFormat in def summarize (diffs : List Diff) : MessageData := Id.run do - if diffs = [] then return "No differences found." - let mut out : MessageData := ("Found differences:" : MessageData).compose Format.line + if diffs == [] then return "No differences found." + let mut out : MessageData := "Found differences:" ++ Format.line let mut diffs := diffs.toArray diffs := diffs.qsort (fun a b => a.prio < b.prio) + let mut oldmod : Name := Name.anonymous for d in diffs do - out := out.compose <| match d with - | .added name => m!"+ added {Expr.const name []}\n" - | .removed name => m!"- removed {name}\n" - | .renamed oldName newName true => m!"! renamed {oldName} → {newName} (changed namespace)\n" - | .renamed oldName newName false => m!"! renamed {oldName} → {newName}\n" - | .movedToModule name oldModuleName newModuleName => m!"! moved {name} from {oldModuleName} to {newModuleName}\n" - | .movedWithinModule name => m!"! moved {name} within module\n" - | .proofChanged name true => m!"! value changed for {name}\n" - | .proofChanged name false => m!"! proof changed for {name}\n" - | .typeChanged name => m!"! type changed for {name}\n" - | .speciesChanged name fro to => m!"! {name} changed from {fro} to {to}\n" - | .extensionEntriesModified ext => m!"! extension entry modified for {ext}\n" - | .docChanged name => m!"! doc modified for {name}\n" - | .docAdded name => m!"+ doc added to {name}\n" - | .docRemoved name => m!"- doc removed from {name}\n" - | .moduleAdded name => m!"+ module added {name}\n" - | .moduleRemoved name => m!"- module removed {name}\n" - | .moduleRenamed oldName newName => m!"! module renamed {oldName} → {newName}\n" - | .attributeAdded attrName name => m!"+ attribute {attrName} added to {name}\n" - | .attributeRemoved attrName name => m!"- attribute {attrName} removed from {name}\n" - | .attributeChanged attrName name => m!"! attribute {attrName} changed for {name}\n" - | .directImportAdded module importName => m!"+ direct import {importName} added to {module}\n" - | .directImportRemoved module importName => m!"- direct import {importName} removed from {module}\n" - | .transitiveImportAdded module importName => m!"+ transitive import {importName} added to {module}\n" - | .transitiveImportRemoved module importName => m!"- transitive import {importName} removed from {module}\n" - out := out.compose (format s!"{diffs.size} differences") + let mod := d.mod + if mod != oldmod then + oldmod := mod + out := out ++ m!"@@ {mod} @@\n" + out := out ++ (match d with + -- TODO add expr to all of these + | .added const _ => m!"+ added {Expr.const const.name (const.levelParams.map mkLevelParam)}" + | .removed name _ => m!"- removed {Expr.const name []}" + | .renamed oldName newName true _ => m!"! renamed {oldName} → {newName} (changed namespace)" + | .renamed oldName newName false _ => m!"! renamed {oldName} → {newName}" + | .movedToModule name oldModuleName newModuleName => m!"! moved {name} from {oldModuleName} to {newModuleName}" + | .movedWithinModule name _ => m!"! moved {name} within _ ule" + | .proofChanged name true _ => m!"! value changed for {name}" + | .proofChanged name false _ => m!"! proof changed for {name}" + | .typeChanged name _ => m!"! type changed for {name}" + | .speciesChanged name fro to _ => m!"! {name} changed from {fro} to {to}" + | .extensionEntriesModified ext => m!"! extension entry modified for {ext}" + | .docChanged name _ => m!"! doc _ ified for {name}" + | .docAdded name _ => m!"+ doc added to {name}" + | .docRemoved name _ => m!"- doc removed from {name}" + | .moduleAdded name => m!"+ module added {name}" + | .moduleRemoved name => m!"- module removed {name}" + | .moduleRenamed oldName newName => m!"! module renamed {oldName} → {newName}" + | .attributeAdded attrName name _ => m!"+ attribute {attrName} added to {name}" + | .attributeRemoved attrName name _ => m!"- attribute {attrName} removed from {name}" + | .attributeChanged attrName name _ => m!"! attribute {attrName} changed for {name}" + | .directImportAdded module importName => m!"+ direct import {importName} added to {module}" + | .directImportRemoved module importName => m!"- direct import {importName} removed from {module}" + | .transitiveImportAdded module importName => m!"+ transitive import {importName} added to {module}" + | .transitiveImportRemoved module importName => m!"- transitive import {importName} removed from {module}") + ++ "\n" + out := out ++ m!"{diffs.size} differences" pure out end Diff @@ -303,6 +345,12 @@ deriving instance BEq for DeclarationRanges open private docStringExt in Lean.findDocString? +-- TODO upstream?? +def moduleName (env : Environment) (n : Name) : Name := +match env.getModuleIdxFor? n with +| some modIdx => env.allImportedModuleNames[modIdx.toNat]! +| none => env.mainModule + /-- Take the diff between an old and new state of some environment extension, at the moment we hardcode the extensions we are interested in, as it is not clear how we can go beyond that. -/ def diffExtension (old new : Environment) @@ -330,7 +378,7 @@ def diffExtension (old new : Environment) for (a, b) in ns do if !a.isInternalDetail then continue if os.find? (revRenames.findD a a) != b then - out := .movedWithinModule a :: out + out := .movedWithinModule a (moduleName new a) :: out | `Lean.docStringExt => do -- Note this is `` not `, as docStringExt is actually private let os := MapDeclarationExtension.getImportedState docStringExt old let ns := MapDeclarationExtension.getImportedState docStringExt new @@ -338,15 +386,15 @@ def diffExtension (old new : Environment) if a.isInternalDetail then continue if ¬ os.contains (revRenames.findD a a) then - out := .docAdded a :: out + out := .docAdded a (moduleName new a) :: out else if os.find! (revRenames.findD a a) != doc then - out := .docChanged a :: out + out := .docChanged a (moduleName new a) :: out for (a, _b) in os do if a.isInternalDetail then continue if ¬ ns.contains (renames.findD a a) then - out := .docRemoved (renames.findD a a) :: out + out := .docRemoved (renames.findD a a) (moduleName new (renames.findD a a)) :: out | ``Lean.protectedExt => do let os := TagDeclarationExtension.getImportedState protectedExt old let ns := TagDeclarationExtension.getImportedState protectedExt new @@ -354,12 +402,12 @@ def diffExtension (old new : Environment) if a.isInternalDetail then continue if ¬ os.contains (revRenames.findD a a) then - out := .attributeAdded `protected a :: out + out := .attributeAdded `protected a (moduleName new a) :: out for a in os do if a.isInternalDetail then continue if ¬ ns.contains (renames.findD a a) then - out := .attributeRemoved `protected (renames.findD a a) :: out + out := .attributeRemoved `protected (renames.findD a a) (moduleName new (renames.findD a a)) :: out | ``Lean.noncomputableExt => do let os := TagDeclarationExtension.getImportedState noncomputableExt old let ns := TagDeclarationExtension.getImportedState noncomputableExt new @@ -367,12 +415,12 @@ def diffExtension (old new : Environment) if a.isInternalDetail then continue if ¬ os.contains (revRenames.findD a a) then - out := .attributeAdded `noncomputable a :: out + out := .attributeAdded `noncomputable a (moduleName new a) :: out for a in os do if a.isInternalDetail then continue if ¬ ns.contains (renames.findD a a) then - out := .attributeRemoved `noncomputable (renames.findD a a) :: out + out := .attributeRemoved `noncomputable (renames.findD a a) (moduleName new (renames.findD a a)) :: out | ``Lean.Meta.globalInstanceExtension => do -- TODO test this, is this the relevant ext? let os := Lean.Meta.globalInstanceExtension.getState old let ns := Lean.Meta.globalInstanceExtension.getState new @@ -380,12 +428,12 @@ def diffExtension (old new : Environment) if a.isInternalDetail then continue if ¬ os.contains (revRenames.findD a a) then - out := .attributeAdded `instance a :: out + out := .attributeAdded `instance a (moduleName new a) :: out for (a, _) in os do if a.isInternalDetail then continue if ¬ ns.contains (renames.findD a a) then - out := .attributeRemoved `instance (renames.findD a a) :: out + out := .attributeRemoved `instance (renames.findD a a) (moduleName new (renames.findD a a)) :: out -- TODO maybe alias -- TODO maybe deprecated -- TODO maybe implementedBy @@ -412,12 +460,12 @@ def diffExtension (old new : Environment) if a.isInternalDetail then continue if ¬ os.outParamMap.contains (revRenames.findD a a) then - out := .attributeAdded `class a :: out + out := .attributeAdded `class a (moduleName new a) :: out for (a, _b) in os.outParamMap do if a.isInternalDetail then continue if ¬ ns.outParamMap.contains (renames.findD a a) then - out := .attributeRemoved `class (renames.findD a a) :: out + out := .attributeRemoved `class (renames.findD a a) (moduleName new (renames.findD a a)) :: out | _ => pure () -- if newEntries.size ≠ oldEntries.size then -- -- m!"-- {ext.name} extension: {(newEntries.size - oldEntries.size : Int)} new entries" @@ -460,7 +508,7 @@ relevantTraits.foldl (fun h t => mixHash (hash (t.val c e)) h) 13 -- TODO can we -- mixHash (hash <| module.val c e) <| mixHash (hash <| species.val c e) <| mixHash (hash <| name.val c e) <| mixHash (type.val c e |>.hash) (value.val c e |>.hash) /-- the list of trait combinations used below -/ -def traitCombinations : List (List Trait):= [[name],[value],[name, value],[type],[type, value],[name, value, module],[type, value, module],[species],[module]] +def traitCombinations : List (List Trait) := [[name],[value],[name, value],[type],[type, value],[name, value, module],[type, value, module],[species],[module]] def constantDiffs (old new : Environment) : List Diff := Id.run do -- dbg_trace new.header.moduleNames -- dbg_trace new.header.moduleData[2]!.imports @@ -520,55 +568,53 @@ def constantDiffs (old new : Environment) : List Diff := Id.run do -- dbg_trace a.name -- dbg_trace f a new -- [name, type, value, species, module] -- TODO check order + -- TODO can we make this cleaner if let some (bn, _) := hs.find? (f a new) then if t == [name] then - out := .renamed bn a.name false :: out -- TODO namespace only? + out := .renamed bn a.name false (moduleName new a.name) :: out -- TODO namespace only? explained := explained.insert (a.name, false) |>.insert (bn, true) continue if t == [value] then - out := .proofChanged a.name false :: out -- TODO check if proof relevant + out := .proofChanged a.name false (moduleName new a.name) :: out -- TODO check if proof relevant explained := explained.insert (a.name, false) |>.insert (bn, true) continue if t == [name, value] then - out := .renamed bn a.name false :: out -- TODO namespace only? - out := .proofChanged a.name false :: out -- TODO check if proof relevant + out := .renamed bn a.name false (moduleName new a.name) :: out -- TODO namespace only? + out := .proofChanged a.name false (moduleName new a.name) :: out -- TODO check if proof relevant explained := explained.insert (a.name, false) |>.insert (bn, true) continue - if t == [type] then -- this is very unlikely? - out := .typeChanged a.name :: out + if t == [type] then -- this is very unlikely, that the type changes but not the value + out := .typeChanged a.name (moduleName new a.name) :: out explained := explained.insert (a.name, false) |>.insert (bn, true) continue if t == [type, value] then - out := .typeChanged a.name :: out - out := .proofChanged a.name false :: out -- TODO check if proof relevant + out := .typeChanged a.name (moduleName new a.name) :: out + out := .proofChanged a.name false (moduleName new a.name) :: out -- TODO check if proof relevant explained := explained.insert (a.name, false) |>.insert (bn, true) if t == [name, value, module] then - out := .renamed bn a.name false :: out -- TODO namespace only? - out := .proofChanged a.name false :: out -- TODO check if proof relevant - out := .movedToModule a.name old.allImportedModuleNames[(old.const2ModIdx.find! bn).toNat]! - new.allImportedModuleNames[(new.const2ModIdx.find! a.name).toNat]! :: out + out := .renamed bn a.name false (moduleName new a.name) :: out -- TODO namespace only? + out := .proofChanged a.name false (moduleName new a.name) :: out -- TODO check if proof relevant + out := .movedToModule a.name (moduleName old bn) (moduleName new a.name) :: out explained := explained.insert (a.name, false) |>.insert (bn, true) continue if t == [type, value, module] then - out := .typeChanged a.name :: out - out := .proofChanged a.name false :: out -- TODO check if proof relevant - out := .movedToModule a.name old.allImportedModuleNames[(old.const2ModIdx.find! bn).toNat]! - new.allImportedModuleNames[(new.const2ModIdx.find! a.name).toNat]! :: out + out := .typeChanged a.name (moduleName new a.name) :: out + out := .proofChanged a.name false (moduleName new a.name) :: out -- TODO check if proof relevant + out := .movedToModule a.name (moduleName old bn) (moduleName new a.name) :: out explained := explained.insert (a.name, false) |>.insert (bn, true) continue if t == [species] then - out := .speciesChanged a.name (speciesDescription (new.constants.find! bn)) (speciesDescription a) :: out + out := .speciesChanged a.name (speciesDescription (new.constants.find! bn)) (speciesDescription a) (moduleName new a.name) :: out explained := explained.insert (a.name, false) |>.insert (bn, true) continue if t == [module] then - out := .movedToModule a.name old.allImportedModuleNames[(old.const2ModIdx.find! a.name).toNat]! - new.allImportedModuleNames[(new.const2ModIdx.find! a.name).toNat]! :: out + out := .movedToModule a.name (moduleName old bn) (moduleName new a.name) :: out explained := explained.insert (a.name, false) |>.insert (bn, true) continue for a in afters do - if !explained.contains (a.name, false) then out := .added a.name :: out + if !explained.contains (a.name, false) then out := .added a (moduleName new a.name) :: out for b in befores do - if !explained.contains (b.name, true) then out := .removed b.name :: out + if !explained.contains (b.name, true) then out := .removed b.name (moduleName old b.name) :: out pure out /-- for debugging purposes -/ @@ -590,10 +636,11 @@ For instance if a decl is removed, then so will all of its attributes. -/ def minimizeDiffs (diffs : List Diff) : List Diff := Id.run do let mut init := diffs for diff in init do - if let .removed n := diff then + if let .removed n _ := diff then init := init.filter fun - | .docRemoved m => m != n - | .attributeRemoved _ m => m != n + | .docRemoved m _ => m != n + | .attributeRemoved _ m _ => m != n + -- TODO more here | _ => true pure init @@ -601,7 +648,7 @@ def extractRenames (diffs : List Diff) : NameMap Name := Id.run do let mut out := mkNameMap Name for diff in diffs do match diff with - | .renamed old new _ => out := out.insert old new + | .renamed old new _ _ => out := out.insert old new | _ => pure () pure out diff --git a/README.md b/README.md index e564741..8d4da1b 100644 --- a/README.md +++ b/README.md @@ -21,187 +21,682 @@ You may face many issues, especially if the diff is too big, if there are differ ```diff $ ./runleaff.sh Mathlib ../test-mathlib2/ ../test-mathlib/ Found differences: -+ added Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection -+ added Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq -+ added Fin.inhabitedFinOneAdd -+ added MeasureTheory.Integrable -+ added norm_withSeminorms -+ added Module.Flat.iff_rTensor_injective' -+ added Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq -+ added Submodule.exists_fg_le_eq_rTensor_inclusion -+ added Fin.inhabited -+ added Affine.Simplex.orthogonalProjection_circumcenter -+ added Fin.default_eq_zero -+ added Fin.eq_zero -+ added Fin.uniqueFinOne -+ added EuclideanGeometry.eq_or_eq_reflection_of_dist_eq -+ added Affine.Simplex.dist_circumcenter_sq_eq_sq_sub_circumradius -- removed inhabitedFinOneAdd -- removed Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection -- removed Fin.unique -- removed Affine.Simplex.dist_circumcenter_sq_eq_sq_sub_circumradius -- removed Fin.default_eq_zero -- removed Fin.eq_zero -- removed EuclideanGeometry.eq_or_eq_reflection_of_dist_eq -- removed Affine.Simplex.orthogonalProjection_circumcenter -- removed norm_withSeminorms -- removed MeasureTheory.Integrable -- removed Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq -- removed instInhabitedFinSucc -- removed Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq -! type changed for Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection -! type changed for Affine.Simplex.orthogonalProjectionSpan -! type changed for Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq -+ direct import Mathlib.Init.Data.Fin.Basic added to Mathlib.Data.Countable.Defs -+ direct import Mathlib.Init.Data.Fin.Basic added to Mathlib.Data.Fin.Basic -+ direct import Mathlib.Init.Data.Fin.Basic added to Mathlib.Data.List.Nodup -! proof changed for FirstOrder.Language.card_functions_sum_skolem₁ -! proof changed for parallelepiped_orthonormalBasis_one_dim -! proof changed for Matrix.vec_single_eq_const -! proof changed for Real.exists_rat_eq_convergent' -! proof changed for spectrum.exp_mem_exp -! proof changed for MeasureTheory.Memℒp.variance_eq -! proof changed for ProbabilityTheory.IndepFun.variance_sum -! proof changed for MeasureTheory.integrable_comp_mul_right_iff -! proof changed for Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero -! proof changed for Matrix.det_fin_two -! proof changed for sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair -! proof changed for Orientation.eq_or_eq_neg_of_isEmpty -! proof changed for MeasureTheory.integrable_comp_smul_iff -! proof changed for Memℓp.add -! proof changed for mellin_hasDerivAt_of_isBigO_rpow -! proof changed for MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub -! proof changed for FiniteDimensional.basisUnique -! proof changed for MeasureTheory.hasSum_integral_iUnion_ae -! proof changed for NormedField.exists_lt_nnnorm_lt -! proof changed for banach_steinhaus -! proof changed for Affine.Simplex.eq_circumcenter_of_dist_eq -! proof changed for Padic.exi_rat_seq_conv_cauchy -! proof changed for ModularGroup.T_pow_mul_apply_one -! proof changed for hasMellin_one_Ioc -! proof changed for EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne -! proof changed for AlgebraicTopology.DoldKan.HigherFacesVanish.induction -! proof changed for MeasureTheory.integrable_finset_sum -! proof changed for MeasureTheory.Integrable.div_const -! proof changed for ENNReal.rpow_arith_mean_le_arith_mean2_rpow -! proof changed for MeasureTheory.integral_sub_average -! proof changed for Orientation.rotation_eq_matrix_toLin -! proof changed for Cardinal.power_one -! proof changed for MeasureTheory.integrableOn_empty -! proof changed for FirstOrder.Language.Formula.realize_rel₂ -! proof changed for WittVector.select_add_select_not -! proof changed for NormedSpace.equicontinuous_TFAE -! proof changed for Real.toNNReal_eq_nat_cast -! proof changed for FinVec.sum_eq -! proof changed for Matrix.mul_fin_three -! proof changed for hasDerivAt_integral_of_dominated_loc_of_lip -! proof changed for MeasureTheory.integrableOn_Ioi_comp_mul_left_iff -! proof changed for torusIntegral_dim1 -! proof changed for Affine.Simplex.circumcenter_eq_point -! proof changed for bernsteinPolynomial.derivative_succ_aux -! proof changed for Basis.eq_bot_of_rank_eq_zero -! proof changed for Seminorm.cont_withSeminorms_normedSpace -! proof changed for integrable_mul_exp_neg_mul_sq -! proof changed for QuaternionAlgebra.instNontrivialQuaternionAlgebra -! proof changed for convolution_assoc -! proof changed for FormalMultilinearSeries.rightInv_coeff -! proof changed for GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I -! proof changed for MeasureTheory.set_integral_prod +@@ Mathlib.Algebra.GroupPower.Order @@ ++ added le_of_pow_le_pow_left.{u_2} ++ added pow_le_pow_iff_left.{u_2} ++ added pow_right_injective.{u_2} +@@ Mathlib.Data.Nat.Pow @@ ++ added Nat.pow_lt_pow_left ++ added Nat.pow_le_pow_right ++ added Nat.pow_lt_pow_iff_left +@@ Mathlib.Algebra.GroupPower.Order @@ ++ added pow_lt_pow_iff_left.{u_2} ++ added pow_lt_pow_right_of_lt_one.{u_2} ++ added pow_right_inj.{u_2} ++ added pow_lt_pow_left.{u_2} +@@ Mathlib.Data.Nat.Pow @@ ++ added Nat.pow_le_pow_iff_left ++ added Nat.pow_le_pow_left +@@ Mathlib.Algebra.GroupPower.Order @@ ++ added pow_left_strictMonoOn.{u_2} ++ added pow_lt_pow_right.{u_2} +@@ Mathlib.Data.Nat.Pow @@ +- removed Nat.pow_lt_pow_of_lt_left +@@ Mathlib.Algebra.GroupPower.Order @@ +- removed pow_lt_pow +@@ Mathlib.Data.Nat.Pow @@ +- removed Nat.pow_le_iff_le_right +- removed Nat.pow_le_iff_le_left +- removed Nat.pow_right_strictMono +@@ Mathlib.Algebra.GroupPower.Order @@ +- removed pow_lt_pow_of_lt_left +- removed self_le_pow +@@ Mathlib.Data.Nat.Pow @@ +- removed Nat.pow_lt_pow_of_lt_right +@@ Mathlib.Combinatorics.Additive.Behrend @@ +- removed Behrend.two_le_nValue +@@ Mathlib.Data.Nat.Pow @@ +- removed Nat.pow_lt_iff_lt_right +- removed Nat.pow_lt_iff_lt_left +@@ Mathlib.Algebra.GroupPower.Order @@ +- removed strictMonoOn_pow +- removed le_of_pow_le_pow +- removed pow_lt_pow_of_lt_one +@@ Mathlib.NumberTheory.LucasLehmer @@ +! type changed for LucasLehmer.sMod_lt +@@ Mathlib.Algebra.GroupPower.Order @@ +! type changed for pow_left_inj +! type changed for one_le_pow_iff_of_nonneg +@@ Mathlib.Data.Nat.Pow @@ +! type changed for StrictMono.nat_pow +! type changed for Nat.one_lt_two_pow +@@ Mathlib.Algebra.GroupPower.Order @@ +! type changed for pow_lt_one_iff_of_nonneg +! type changed for pow_eq_one_iff_of_nonneg +@@ Mathlib.Data.Nat.Pow @@ +! type changed for Nat.pow_left_strictMono +@@ Mathlib.Algebra.GroupPower.Order @@ +! type changed for pow_le_one_iff_of_nonneg +@@ Mathlib.NumberTheory.Divisors @@ +! type changed for Nat.properDivisors_prime_pow +@@ Mathlib.NumberTheory.LucasLehmer @@ +! type changed for LucasLehmer.mersenne_int_pos +@@ Mathlib.Algebra.GroupPower.Order @@ +! type changed for one_lt_pow_iff_of_nonneg +@@ Mathlib.Combinatorics.Additive.Behrend @@ +! type changed for Behrend.bound +@@ Mathlib.NumberTheory.Multiplicity @@ +! type changed for padicValNat.pow_sub_pow +@@ Mathlib.NumberTheory.LucasLehmer @@ +! type changed for LucasLehmer.mersenne_int_ne_zero +@@ Mathlib.Data.Nat.Pow @@ +! type changed for Nat.one_lt_pow +@@ Mathlib.Algebra.GroupPower.Order @@ +! type changed for abs_pow_eq_one +@@ Mathlib.NumberTheory.Multiplicity @@ +! type changed for padicValNat.pow_two_sub_pow +@@ Mathlib.Data.Nat.Pow @@ +! type changed for Nat.pow_left_injective +! type changed for Nat.one_lt_pow_iff +@@ Mathlib.NumberTheory.LucasLehmer @@ +! type changed for LucasLehmer.sMod_nonneg +@@ Mathlib.Data.Nat.Pow @@ ++ attribute protected added to Nat.pow_le_pow_iff_left ++ attribute protected added to Nat.pow_right_injective ++ attribute protected added to Nat.pow_le_pow_left ++ attribute protected added to Nat.pow_lt_pow_left ++ attribute protected added to Nat.pow_left_strictMono ++ attribute protected added to Nat.pow_le_pow_right ++ attribute protected added to Nat.pow_lt_pow_iff_left +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed le_of_nsmul_le_nsmul → le_of_nsmul_le_nsmul_right' +! renamed pow_lt_pow_iff' → pow_lt_pow_iff_right' +! renamed le_of_pow_le_pow' → le_of_pow_le_pow_left' +! renamed nsmul_strictMono_right → nsmul_left_strictMono +! renamed nsmul_le_nsmul → nsmul_le_nsmul_left +@@ Mathlib.Algebra.GroupPower.Order @@ +! renamed pow_lt_pow_iff_of_lt_one → pow_lt_pow_iff_right_of_lt_one +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed pow_strictMono_left → pow_right_strictMono' +@@ Mathlib.Algebra.GroupPower.Order @@ +! renamed pow_lt_pow_iff → pow_lt_pow_iff_right +! renamed pow_le_pow_iff → pow_le_pow_iff_right +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed pow_le_pow_of_le_one' → pow_le_pow_right_of_le_one' +! renamed pow_strictMono_right' → pow_left_strictMono +! renamed StrictMono.nsmul_left → StrictMono.const_nsmul +! renamed Monotone.nsmul_left → Monotone.const_nsmul +@@ Mathlib.Algebra.GroupPower.Order @@ +! renamed pow_le_pow → pow_le_pow_right +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed nsmul_le_nsmul_of_nonpos → nsmul_le_nsmul_left_of_nonpos +! renamed pow_le_pow' → pow_le_pow_right' +@@ Mathlib.Algebra.GroupPower.Order @@ +! renamed pow_le_pow_of_le_left → pow_le_pow_left +! renamed lt_of_pow_lt_pow → lt_of_pow_lt_pow_left +! renamed self_lt_pow → lt_self_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed pow_le_pow_of_le_left' → pow_le_pow_left' +@@ Mathlib.RingTheory.Ideal.Operations @@ +! renamed Ideal.pow_le_pow → Ideal.pow_le_pow_right +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed lt_of_nsmul_lt_nsmul → lt_of_nsmul_lt_nsmul_right +@@ Mathlib.Algebra.GroupPower.Order @@ +! renamed pow_mono → pow_right_mono +! renamed pow_lt_pow₀ → pow_lt_pow_right₀ +! renamed pow_strictMono_right → pow_right_strictMono +@@ Mathlib.Data.Real.ENNReal @@ +! renamed ENNReal.pow_lt_pow_of_lt_left → ENNReal.pow_lt_pow_left +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed nsmul_lt_nsmul → nsmul_lt_nsmul_left +! renamed pow_lt_pow' → pow_lt_pow_right' +@@ Mathlib.Algebra.GroupPower.Order @@ +! renamed strictAnti_pow → pow_right_strictAnti +@@ Mathlib.RingTheory.DedekindDomain.Ideal @@ +! renamed Ideal.strictAnti_pow → Ideal.pow_right_strictAnti +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed lt_of_pow_lt_pow' → lt_of_pow_lt_pow_left' +@@ Mathlib.RingTheory.Ideal.Operations @@ +! renamed Ideal.pow_mono → Ideal.pow_right_mono +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed nsmul_strictMono_left → nsmul_right_strictMono +! renamed nsmul_le_nsmul_iff → nsmul_le_nsmul_iff_left +@@ Mathlib.Algebra.GroupPower.Lemmas @@ +! renamed zpow_strictMono_right → zpow_right_strictMono +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! renamed StrictMono.pow_right' → StrictMono.pow_const +! renamed nsmul_le_nsmul_of_le_right → nsmul_le_nsmul_right +! renamed pow_le_pow_iff' → pow_le_pow_iff_right' +! renamed nsmul_lt_nsmul_iff → nsmul_lt_nsmul_iff_left +@@ Mathlib.Data.Nat.Pow @@ ++ doc added to Nat.pow_le_pow_left +@@ Mathlib.Algebra.GroupPower.Order @@ ++ doc added to pow_left_strictMonoOn ++ doc added to pow_right_strictMono +@@ Mathlib.Data.Nat.Pow @@ ++ doc added to Nat.pow_left_strictMono ++ doc added to Nat.pow_le_pow_right +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! doc _ ified for pow_left_strictMono +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_eq_one_iff_of_nonneg +@@ Mathlib.NumberTheory.LucasLehmer @@ +! proof changed for LucasLehmer.mersenne_int_pos +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for StrictMono.const_nsmul +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.pow_left_injective +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Monotone.const_nsmul +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for StrictMono.nat_pow +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_le_pow_right +@@ Mathlib.NumberTheory.LucasLehmer @@ +! proof changed for LucasLehmer.sMod_nonneg +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_le_nsmul_left_of_nonpos +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for one_lt_pow_iff_of_nonneg +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_le_pow_right' +! proof changed for nsmul_right_strictMono +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_le_pow_left +@@ Mathlib.Combinatorics.Additive.Behrend @@ +! proof changed for Behrend.bound +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for lt_of_pow_lt_pow_left +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for StrictMono.pow_const +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for lt_self_pow +! proof changed for one_le_pow_iff_of_nonneg +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_le_pow_left' +! proof changed for nsmul_le_nsmul_right +! proof changed for le_of_nsmul_le_nsmul_right' +@@ Mathlib.NumberTheory.Multiplicity @@ +! proof changed for padicValNat.pow_sub_pow +@@ Mathlib.Data.Nat.Factorization.Basic @@ +! proof changed for Nat.factorization_lt +@@ Mathlib.Algebra.Order.Archimedean @@ +! proof changed for exists_lt_nsmul +@@ Mathlib.Analysis.InnerProductSpace.Basic @@ +! proof changed for eq_of_norm_le_re_inner_eq_norm_sq +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Right.pow_nonpos +@@ Mathlib.Data.Nat.Log @@ +! proof changed for Nat.log_pow +@@ Mathlib.FieldTheory.Finite.Basic @@ +! proof changed for FiniteField.X_pow_card_pow_sub_X_natDegree_eq +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Right.pow_le_one_of_le +@@ Mathlib.Data.Nat.Factorial.Basic @@ +! proof changed for Nat.pow_sub_lt_descFactorial' +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for MonovaryOn.nsmul_left +@@ Mathlib.Computability.Ackermann @@ +! proof changed for ack_three +@@ Mathlib.Analysis.SpecialFunctions.Exp @@ +! proof changed for Real.tendsto_exp_div_pow_atTop +@@ Mathlib.Data.Nat.Size @@ +! proof changed for Nat.size_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_nonneg +@@ Mathlib.Computability.Ackermann @@ +! proof changed for ack_add_one_sq_lt_ack_add_four +@@ Mathlib.GroupTheory.Archimedean @@ +! proof changed for AddSubgroup.exists_isLeast_pos +@@ Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree @@ +! proof changed for Polynomial.cardPowDegree_anti_archimedean +@@ Mathlib.Data.Nat.Factorization.Basic @@ +! proof changed for Nat.factorization_le_of_le_pow +@@ Mathlib.Analysis.InnerProductSpace.Basic @@ +! proof changed for InnerProductSpace.toUniformConvexSpace +@@ Mathlib.NumberTheory.NumberField.Discriminant @@ +! proof changed for NumberField.discr_gt_one +@@ Mathlib.RingTheory.DiscreteValuationRing.TFAE @@ +! proof changed for DiscreteValuationRing.TFAE +@@ Mathlib.NumberTheory.PellMatiyasevic @@ +! proof changed for Pell.eq_pow_of_pell +@@ Mathlib.NumberTheory.NumberField.Discriminant @@ +! proof changed for NumberField.abs_discr_ge +@@ Mathlib.RingTheory.WittVector.Frobenius @@ +! proof changed for WittVector.map_frobeniusPoly.key₂ +@@ Mathlib.NumberTheory.ClassNumber.Finite @@ +! proof changed for ClassGroup.norm_lt +@@ Mathlib.Analysis.Analytic.Composition @@ +! proof changed for FormalMultilinearSeries.comp_summable_nnreal +@@ Mathlib.Analysis.SpecificLimits.FloorPow @@ +! proof changed for sum_div_pow_sq_le_div_sq +@@ Mathlib.Algebra.GeomSum @@ +! proof changed for nat_sub_dvd_pow_sub_pow +@@ Mathlib.Analysis.Calculus.FDeriv.Measurable @@ +! proof changed for RightDerivMeasurableAux.D_subset_differentiable_set +@@ Mathlib.Data.Complex.Exponential @@ +! proof changed for Real.cos_two_neg +@@ Mathlib.RingTheory.Polynomial.Basic @@ +! proof changed for Polynomial.Monic.geom_sum +@@ Mathlib.Topology.Metrizable.Uniformity @@ +! proof changed for UniformSpace.metrizable_uniformity +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for sq_lt_sq +@@ Mathlib.FieldTheory.Finite.Polynomial @@ +! proof changed for MvPolynomial.degrees_indicator +@@ Mathlib.Analysis.Asymptotics.Asymptotics @@ +! proof changed for Asymptotics.IsBigOWith.of_pow +@@ Mathlib.NumberTheory.Padics.PadicIntegers @@ +! proof changed for PadicInt.norm_le_pow_iff_le_valuation +@@ Mathlib.Analysis.Complex.Basic @@ +! proof changed for Complex.nnnorm_eq_one_of_pow_eq_one +@@ Mathlib.Analysis.PSeries @@ +! proof changed for Finset.sum_condensed_le +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.one_lt_two_pow' +@@ Mathlib.NumberTheory.DirichletCharacter.Bounds @@ +! proof changed for DirichletCharacter.unit_norm_eq_one +@@ Mathlib.Analysis.PSeries @@ +! proof changed for ENNReal.tsum_condensed_le +@@ Mathlib.RingTheory.DiscreteValuationRing.TFAE @@ +! proof changed for exists_maximalIdeal_pow_eq_of_principal +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for AntivaryOn.pow_left +@@ Mathlib.Analysis.SpecificLimits.FloorPow @@ +! proof changed for sum_div_nat_floor_pow_sq_le_div_sq +@@ Mathlib.NumberTheory.SumFourSquares @@ ! proof changed for Int.lt_of_sum_four_squares_eq_mul -! proof changed for HasFTaylorSeriesUpToOn.hasFDerivWithinAt -! proof changed for MeasureTheory.IntegrableOn.smul_continuousOn -! proof changed for Cardinal.instNontrivialCardinal -! proof changed for HomotopyGroup.pi1EquivFundamentalGroup -! proof changed for MeasureTheory.integrable_finset_sum_measure -! proof changed for MeasureTheory.exists_upperSemicontinuous_lt_integral_gt -! proof changed for GeneralizedContinuedFraction.abs_sub_convergents_le -! proof changed for IsCyclotomicExtension.discr_prime_pow -! proof changed for exists_linearIndependent_pair_of_one_lt_rank -! proof changed for ProbabilityTheory.measure_le_le_exp_mul_mgf -! proof changed for ProbabilityTheory.condCdf' -! proof changed for MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict -! proof changed for IsNoetherianRing.strongRankCondition -! proof changed for MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le -! proof changed for GeneralizedContinuedFraction.of_convergence_epsilon -! proof changed for linearIndependent_fin2 -! proof changed for Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter -! proof changed for MeasureTheory.Integrable.comp_div_right -! proof changed for banach_steinhaus_iSup_nnnorm -! proof changed for NNReal.rpow_arith_mean_le_arith_mean2_rpow -! proof changed for MeasurableSpace.cardinal_generateMeasurable_le_continuum -! proof changed for MeasureTheory.Integrable.prod_smul -! proof changed for not_disjoint_segment_convexHull_triple -! proof changed for Orientation.volumeForm_robust' -! proof changed for ProbabilityTheory.iIndepFun.integrable_exp_mul_sum -! proof changed for Behrend.box_zero -! proof changed for FirstOrder.Language.Term.realize_functions_apply₂ -! proof changed for MeasureTheory.memℒp_two_iff_integrable_sq -! proof changed for ProbabilityTheory.variance_def' -! proof changed for SimpleGraph.pathGraph_connected -! proof changed for groupCohomology.dOne_comp_eq -! proof changed for MeasureTheory.integrable_smul_measure -! proof changed for Affine.Simplex.circumsphere_unique_dist_eq -! proof changed for Cardinal.one_power -! proof changed for Module.Flat.iff_rTensor_injective -! proof changed for SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul -! proof changed for MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ -! proof changed for Affine.Simplex.eq_circumradius_of_dist_eq -! proof changed for MeasureTheory.setToFun_finset_sum' -! proof changed for Seminorm.cont_normedSpace_to_withSeminorms -! proof changed for MeasureTheory.integrable_average -! proof changed for MeasureTheory.integrableOn_map_equiv -! proof changed for MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part -! proof changed for ProbabilityTheory.IndepFun.integrable_exp_mul_add -! proof changed for MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le -! proof changed for groupCohomology.dZero_comp_eq -! proof changed for MeasureTheory.IntegrableOn.continuousOn_smul -! proof changed for MeasureTheory.Integrable.convolution_integrand -! proof changed for Cardinal.mk_eq_one -! proof changed for Pell.exists_of_not_isSquare -! proof changed for MeasureTheory.Measure.haar.addPrehaar_mono -! proof changed for Fin.sum_univ_one -! proof changed for Cardinal.lift_one -! proof changed for Besicovitch.exists_goodδ -! proof changed for MeasureTheory.integrable_comp_div_left +@@ Mathlib.Algebra.GroupPower.Lemmas @@ +! proof changed for zpow_le_zpow_iff +@@ Mathlib.NumberTheory.Liouville.LiouvilleWith @@ +! proof changed for Liouville.frequently_exists_num +@@ Mathlib.Analysis.SpecialFunctions.Log.Deriv @@ +! proof changed for Real.abs_log_sub_add_sum_range_le +@@ Mathlib.RingTheory.DedekindDomain.Ideal @@ +! proof changed for Ideal.pow_lt_self +@@ Mathlib.Combinatorics.SetFamily.FourFunctions @@ +! proof changed for Finset.card_le_card_diffs +@@ Mathlib.NumberTheory.Liouville.Basic @@ +! proof changed for Liouville.transcendental +@@ Mathlib.Analysis.SpecificLimits.Normed @@ +! proof changed for summable_geometric_iff_norm_lt_1 +@@ Mathlib.Algebra.IsPrimePow @@ +! proof changed for isPrimePow_nat_iff_bounded +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Left.one_le_pow_of_le +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.pow_lt_pow_succ +@@ Mathlib.Data.Polynomial.Degree.CardPowDegree @@ +! proof changed for Polynomial.cardPowDegree_isEuclidean +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.pow_right_injective +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Left.pow_nonpos +@@ Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology @@ +! proof changed for Ideal.adic_module_basis +@@ Mathlib.NumberTheory.PellMatiyasevic @@ +! proof changed for Pell.eq_pow_of_pell_lem +@@ Mathlib.Analysis.NormedSpace.FiniteDimension @@ +! proof changed for Basis.op_nnnorm_le +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_pos_iff +! proof changed for sq_lt_one_iff +@@ Mathlib.RingTheory.Henselian @@ +! proof changed for IsAdicComplete.henselianRing +@@ Mathlib.Analysis.ODE.PicardLindelof @@ +! proof changed for PicardLindelof.FunSpace.dist_iterate_next_le +@@ Mathlib.NumberTheory.Divisors @@ +! proof changed for Nat.prod_properDivisors_prime_pow +@@ Mathlib.MeasureTheory.Integral.PeakFunction @@ +! proof changed for tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos +@@ Mathlib.NumberTheory.Bertrand @@ +! proof changed for centralBinom_le_of_no_bertrand_prime +@@ Mathlib.Data.Nat.Bitwise @@ +! proof changed for Nat.testBit_two_pow_of_ne +@@ Mathlib.NumberTheory.FLT.Four @@ +! proof changed for Fermat42.coprime_of_minimal +@@ Mathlib.Analysis.Analytic.Composition @@ +! proof changed for HasFPowerSeriesAt.comp +@@ Mathlib.Algebra.Tropical.Basic @@ +! proof changed for Tropical.add_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Right.one_le_pow_of_le +@@ Mathlib.Data.Nat.Log @@ +! proof changed for Nat.clog_anti_left +@@ Mathlib.MeasureTheory.Measure.Hausdorff @@ +! proof changed for MeasureTheory.hausdorffMeasure_pi_real +@@ Mathlib.Combinatorics.Additive.PluenneckeRuzsa @@ +! proof changed for Finset.card_pow_div_pow_le +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Antivary.nsmul_right +@@ Mathlib.Algebra.GroupPower.Lemmas @@ +! proof changed for strictMono_pow_bit1 +@@ Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar @@ +! proof changed for MeasureTheory.Measure.addHaar_submodule +@@ Mathlib.Data.Nat.Factorial.Basic @@ +! proof changed for Nat.ascFactorial_lt_pow_add +@@ Mathlib.Topology.Algebra.Polynomial @@ +! proof changed for Polynomial.coeff_bdd_of_roots_le +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Antivary.pow_right +@@ Mathlib.Topology.Algebra.InfiniteSum.Order @@ +! proof changed for Finite.of_summable_const +@@ Mathlib.Analysis.PSeries @@ +! proof changed for sum_Ioo_inv_sq_le +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for le_self_pow +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.pow_dvd_pow_iff_pow_le_pow +@@ Mathlib.RingTheory.Polynomial.Basic @@ +! proof changed for Polynomial.coeff_prod_mem_ideal_pow_tsub +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Antivary.pow_left +@@ Mathlib.NumberTheory.NumberField.Units @@ +! proof changed for NumberField.Units.dirichletUnitTheorem.seq_next +@@ Mathlib.Computability.Ackermann @@ +! proof changed for exists_lt_ack_of_nat_primrec +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for MonovaryOn.pow_right +@@ Mathlib.Analysis.SpecialFunctions.JapaneseBracket @@ +! proof changed for finite_integral_rpow_sub_one_pow_aux +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for MonovaryOn.nsmul_right +@@ Mathlib.Algebra.Order.Field.Basic @@ +! proof changed for one_div_pow_lt_one_div_pow_of_lt +@@ Mathlib.NumberTheory.RamificationInertia @@ +! proof changed for Ideal.ramificationIdx_spec +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Monovary.pow_right +! proof changed for AntivaryOn.pow_left₀ +@@ Mathlib.Analysis.NormedSpace.Multilinear.Basic @@ +! proof changed for ContinuousMultilinearMap.continuous_eval +@@ Mathlib.Analysis.Calculus.Taylor @@ +! proof changed for taylor_mean_remainder_bound +@@ Mathlib.RingTheory.Etale @@ +! proof changed for Algebra.FormallySmooth.of_split +@@ Mathlib.Analysis.Complex.UpperHalfPlane.Metric @@ +! proof changed for UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_mono_left +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for sq_le_sq +@@ Mathlib.Data.Num.Lemmas @@ +! proof changed for Num.castNum_shiftRight +@@ Mathlib.Data.Nat.Size @@ +! proof changed for Nat.size_shiftLeft' +@@ Mathlib.RingTheory.Finiteness @@ +! proof changed for Ideal.exists_radical_pow_le_of_fg +@@ Mathlib.Analysis.Analytic.Inverse @@ +! proof changed for FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos +@@ Mathlib.NumberTheory.Padics.RingHoms @@ +! proof changed for PadicInt.appr_lt +@@ Mathlib.Data.Nat.Factorization.Basic @@ +! proof changed for Nat.Ico_filter_pow_dvd_eq +@@ Mathlib.Order.Filter.Archimedean @@ +! proof changed for Filter.Tendsto.atTop_nsmul_const +@@ Mathlib.Data.Real.Pi.Leibniz @@ +! proof changed for Real.tendsto_sum_pi_div_four +@@ Mathlib.Analysis.Calculus.BumpFunction.Normed @@ +! proof changed for ContDiffBump.measure_closedBall_div_le_integral +@@ Mathlib.Analysis.NormedSpace.Star.Multiplier @@ +! proof changed for DoubleCentralizer.instCstarRing +@@ Mathlib.Analysis.NormedSpace.Multilinear.Basic @@ +! proof changed for MultilinearMap.continuous_of_bound +@@ Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma @@ +! proof changed for szemeredi_regularity +@@ Mathlib.Analysis.InnerProductSpace.Rayleigh @@ +! proof changed for IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn +@@ Mathlib.NumberTheory.ModularForms.JacobiTheta.Basic @@ +! proof changed for exists_summable_bound_exp_mul_sq +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for sq_le_one_iff +@@ Mathlib.Analysis.SpecificLimits.Basic @@ +! proof changed for tendsto_pow_atTop_nhds_0_iff +! proof changed for summable_one_div_pow_of_le +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_four_le_pow_two_of_pow_two_le +@@ Mathlib.Analysis.SpecialFunctions.Pow.Continuity @@ +! proof changed for NNReal.eventually_pow_one_div_le +@@ Mathlib.Computability.AkraBazzi.GrowsPolynomially @@ +! proof changed for AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos +@@ Mathlib.NumberTheory.RamificationInertia @@ +! proof changed for Ideal.quotientToQuotientRangePowQuotSucc_surjective +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for AntivaryOn.nsmul_left +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for one_lt_sq_iff +@@ Mathlib.NumberTheory.Multiplicity @@ +! proof changed for multiplicity.Nat.pow_sub_pow +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.one_lt_pow' +@@ Mathlib.Analysis.Analytic.Constructions @@ +! proof changed for formalMultilinearSeries_geometric_radius +@@ Mathlib.NumberTheory.Padics.PadicVal @@ +! proof changed for range_pow_padicValNat_subset_divisors' +@@ Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots @@ +! proof changed for IsPrimitiveRoot.sub_one_norm_two +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for MonovaryOn.pow_left₀ +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.lt_of_pow_dvd_right +@@ Mathlib.Data.Polynomial.Degree.CardPowDegree @@ +! proof changed for Polynomial.cardPowDegree_apply +@@ Mathlib.NumberTheory.LucasLehmer @@ +! proof changed for LucasLehmer.residue_eq_zero_iff_sMod_eq_zero +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for sq_eq_sq_iff_abs_eq_abs +@@ Mathlib.Algebra.GroupPower.Lemmas @@ +! proof changed for zpow_lt_zpow_iff +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Monovary.pow_left₀ +@@ Mathlib.Algebra.Order.Field.Basic @@ +! proof changed for one_div_pow_le_one_div_pow_of_le +@@ Mathlib.RingTheory.Artinian @@ +! proof changed for IsArtinianRing.isNilpotent_jacobson_bot +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for one_le_sq_iff +@@ Mathlib.RingTheory.Ideal.Operations @@ +! proof changed for Ideal.pow_le_self +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Monovary.nsmul_right +@@ Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology @@ +! proof changed for is_ideal_adic_pow +@@ Mathlib.Data.Nat.Log @@ +! proof changed for Nat.log_eq_iff +@@ Mathlib.RingTheory.Polynomial.Cyclotomic.Expand @@ +! proof changed for Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP +@@ Mathlib.Analysis.Analytic.Basic @@ +! proof changed for HasFPowerSeriesOnBall.uniform_geometric_approx +@@ Mathlib.RingTheory.Perfection @@ +! proof changed for PreTilt.valAux_add +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for AntivaryOn.pow_right +@@ Mathlib.RingTheory.Valuation.Integral @@ +! proof changed for Valuation.Integers.mem_of_integral +@@ Mathlib.NumberTheory.Multiplicity @@ +! proof changed for Nat.two_pow_sub_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Right.pow_nonneg +@@ Mathlib.Analysis.Normed.Field.Basic @@ +! proof changed for norm_map_one_of_pow_eq_one +@@ Mathlib.NumberTheory.LucasLehmer @@ +! proof changed for one_lt_mersenne +@@ Mathlib.Combinatorics.SetFamily.Kleitman @@ +! proof changed for Finset.card_biUnion_le_of_intersecting +@@ Mathlib.Algebra.Homology.LocalCohomology @@ +! proof changed for localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Left.pow_nonneg +@@ Mathlib.Analysis.BoxIntegral.Basic @@ +! proof changed for BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO +@@ Mathlib.NumberTheory.RamificationInertia @@ +! proof changed for Ideal.ramificationIdx_lt +@@ Mathlib.Data.Nat.Factorial.Basic @@ +! proof changed for Nat.factorial_mul_pow_sub_le_factorial +@@ Mathlib.RingTheory.DedekindDomain.Ideal @@ +! proof changed for Ideal.pow_succ_lt_pow +@@ Mathlib.NumberTheory.Liouville.LiouvilleNumber @@ +! proof changed for LiouvilleNumber.aux_calc +@@ Mathlib.Analysis.Distribution.SchwartzSpace @@ +! proof changed for Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux +@@ Mathlib.Data.Nat.Factorial.Basic @@ +! proof changed for Nat.pow_sub_le_descFactorial +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.pow_dvd_pow_iff_le_right +@@ Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology @@ +! proof changed for Ideal.adic_basis +@@ Mathlib.Combinatorics.Additive.PluenneckeRuzsa @@ +! proof changed for Finset.card_nsmul_sub_nsmul_le +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Monovary.nsmul_left +@@ Mathlib.Combinatorics.Additive.Behrend @@ +! proof changed for Behrend.sum_sq_le_of_mem_box +@@ Mathlib.MeasureTheory.Group.AddCircle @@ +! proof changed for AddCircle.isAddFundamentalDomain_of_ae_ball +@@ Mathlib.GroupTheory.Schreier @@ +! proof changed for Subgroup.card_commutator_le_of_finite_commutatorSet +@@ Mathlib.Data.Nat.Log @@ +! proof changed for Nat.log_anti_left +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Monotone.pow_right +@@ Mathlib.Data.Nat.Factorial.Basic @@ +! proof changed for Nat.ascFactorial_le_pow_add +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for MonovaryOn.pow_left +@@ Mathlib.Data.Complex.Exponential @@ +! proof changed for Real.one_sub_div_pow_le_exp_neg +@@ Mathlib.Analysis.SpecificLimits.FloorPow @@ +! proof changed for mul_pow_le_nat_floor_pow +@@ Mathlib.Topology.UnitInterval @@ +! proof changed for Set.Icc.monotone_addNSMul +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_lt_self_of_lt_one +@@ Mathlib.Order.Filter.AtTopBot @@ +! proof changed for Filter.Tendsto.nsmul_atTop +@@ Mathlib.Topology.EMetricSpace.Paracompact @@ +! proof changed for EMetric.instParacompactSpace +@@ Mathlib.FieldTheory.Finite.Basic @@ +! proof changed for FiniteField.X_pow_card_pow_sub_X_ne_zero +@@ Mathlib.Probability.StrongLaw @@ +! proof changed for ProbabilityTheory.strong_law_aux1 +@@ Mathlib.RingTheory.QuotientNilpotent @@ +! proof changed for Ideal.IsNilpotent.induction_on +@@ Mathlib.Combinatorics.Additive.Behrend @@ +! proof changed for Behrend.le_N +@@ Mathlib.Analysis.Convex.SpecificFunctions.Deriv @@ +! proof changed for strictConvexOn_pow +@@ Mathlib.Data.Real.Pi.Bounds @@ +! proof changed for Real.pi_lt_sqrtTwoAddSeries +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for sq_eq_sq +@@ Mathlib.Analysis.Calculus.FDeriv.Measurable @@ +! proof changed for FDerivMeasurableAux.D_subset_differentiable_set +@@ Mathlib.NumberTheory.Divisors @@ +! proof changed for Nat.mem_properDivisors_prime_pow +@@ Mathlib.Algebra.GroupPower.Lemmas @@ +! proof changed for zpow_lt_zpow +@@ Mathlib.Data.Nat.Squarefree @@ +! proof changed for Nat.sq_mul_squarefree_of_pos +@@ Mathlib.Combinatorics.SimpleGraph.Regularity.Increment @@ +! proof changed for SzemerediRegularity.card_increment +@@ Mathlib.Data.Polynomial.Degree.CardPowDegree @@ +! proof changed for Polynomial.cardPowDegree +@@ Mathlib.NumberTheory.FermatPsp @@ +! proof changed for Nat.exists_infinite_pseudoprimes +@@ Mathlib.Analysis.Analytic.Basic @@ ! proof changed for HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal -! proof changed for finOneEquiv -! proof changed for groupCohomology.oneCochainsLequiv -! proof changed for MeasureTheory.Memℒp.integrable_norm_rpow' -! proof changed for Fin.prod_univ_one -! proof changed for MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul -! proof changed for FiniteField.X_pow_card_sub_X_natDegree_eq -! proof changed for MeasureTheory.Integrable.simpleFunc_mul -! proof changed for convolutionExistsAt_flip -! proof changed for MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero -! proof changed for ZMod.instUnique -! proof changed for MeasureTheory.Integrable.sub -! proof changed for integrable_exp_neg_mul_sq -! proof changed for FirstOrder.Language.BoundedFormula.realize_rel₂ -! proof changed for ConvolutionExistsAt.integrable_swap -! proof changed for MeasureTheory.Measure.haar.prehaar_mono -! proof changed for Orientation.abs_areaForm_le -! proof changed for EuclideanSpace.volume_ball -! proof changed for ProbabilityTheory.integrable_gaussianPdfReal -! proof changed for ProbabilityTheory.condCdf'_def -! proof changed for Matrix.det_fin_one -! proof changed for MeasureTheory.integral_fintype -! proof changed for Fin.sum_univ_two -! proof changed for Orientation.abs_areaForm_of_orthogonal -! proof changed for MeasurableEmbedding.integrableOn_map_iff -! proof changed for Mathlib.Meta.NormNum.isRat_eq_false -! proof changed for integral_mul_cpow_one_add_sq -! proof changed for Fin.prod_univ_two -! proof changed for VectorFourier.fourier_integral_convergent_iff -! proof changed for NormedSpace.toLocallyConvexSpace' -! proof changed for Rat.numberField_discr -! proof changed for Matrix.mul_fin_two -! proof changed for Orientation.areaForm_le -! proof changed for Matrix.det_fin_three -! proof changed for Action.diagonalOneIsoLeftRegular -! proof changed for MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt -! proof changed for catalan_one -! proof changed for MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le -- direct import Mathlib.Init.Data.Fin.Basic removed from Mathlib.Logic.Unique -181 differences -total 6.29s +@@ Mathlib.RingTheory.DedekindDomain.Ideal @@ +! proof changed for Ideal.exists_mem_pow_not_mem_pow_succ +@@ Mathlib.Combinatorics.Additive.Behrend @@ +! proof changed for Behrend.dValue_pos +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for lt_of_mul_self_lt_mul_self +@@ Mathlib.Topology.MetricSpace.HausdorffDistance @@ +! proof changed for IsOpen.exists_iUnion_isClosed +@@ Mathlib.NumberTheory.RamificationInertia @@ +! proof changed for Ideal.quotientToQuotientRangePowQuotSucc_injective +@@ Mathlib.Data.Polynomial.Degree.Lemmas @@ +! proof changed for Polynomial.natDegree_comp_le +@@ Mathlib.Data.Complex.Exponential @@ +! proof changed for Real.sinh_lt_cosh +@@ Mathlib.Data.Nat.Choose.Factorization @@ +! proof changed for Nat.factorization_choose_of_lt_three_mul +@@ Mathlib.Data.Real.ENNReal @@ +! proof changed for ENNReal.zpow_le_of_le +@@ Mathlib.Topology.UnitInterval @@ +! proof changed for Set.Icc.addNSMul_eq_right +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for Left.pow_le_one_of_le +@@ Mathlib.Data.Nat.Log @@ +! proof changed for Nat.log_le_clog +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Antivary.pow_left₀ +@@ Mathlib.Data.Nat.Log @@ +! proof changed for Nat.clog_pow +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for Antivary.nsmul_left +@@ Mathlib.NumberTheory.Padics.RingHoms @@ +! proof changed for PadicInt.nthHomSeq_one +@@ Mathlib.Analysis.SpecificLimits.Basic @@ +! proof changed for tendsto_add_one_pow_atTop_atTop_of_pos +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for one_le_pow_of_one_le' +@@ Mathlib.Combinatorics.Additive.Behrend @@ +! proof changed for Behrend.roth_lower_bound_explicit +! proof changed for Behrend.dValue +@@ Mathlib.Algebra.Order.Monovary @@ +! proof changed for AntivaryOn.nsmul_right +! proof changed for Monovary.pow_left +@@ Mathlib.Data.Nat.Bitwise @@ +! proof changed for Nat.append_lt +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_le_nsmul_iff_left +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.pow_left_strictMono +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_le_pow_iff_right' +@@ Mathlib.NumberTheory.LucasLehmer @@ +! proof changed for LucasLehmer.mersenne_int_ne_zero +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_lt_nsmul_iff_left +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.one_lt_two_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_lt_pow_iff_right' +@@ Mathlib.NumberTheory.Divisors @@ +! proof changed for Nat.properDivisors_prime_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for le_of_pow_le_pow_left' +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_le_one_iff_of_nonneg +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_left_strictMono +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for abs_pow_eq_one +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for nsmul_le_nsmul_left +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_left_inj +! proof changed for pow_lt_pow_iff_right_of_lt_one +@@ Mathlib.NumberTheory.Multiplicity @@ +! proof changed for padicValNat.pow_two_sub_pow +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_right_strictMono' +@@ Mathlib.NumberTheory.LucasLehmer @@ +! proof changed for LucasLehmer.sMod_lt +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_lt_pow_iff_right +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.one_lt_pow +@@ Mathlib.Algebra.GroupPower.Order @@ +! proof changed for pow_le_pow_iff_right +! proof changed for pow_lt_one_iff_of_nonneg +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_le_pow_right_of_le_one' +@@ Mathlib.Data.Nat.Pow @@ +! proof changed for Nat.one_lt_pow_iff +@@ Mathlib.Algebra.GroupPower.CovariantClass @@ +! proof changed for pow_left_strictMono +366 differences +total 9.85s ```