From e52263548c5e0fa16524ad9d3943d05217f2f27e Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 31 Oct 2023 09:38:50 +0000 Subject: [PATCH] chore: bump toolchain to v4.3.0-rc1 (#8051) This incorporates changes from * #7845 * #7847 * #7853 * #7872 (was never actually made to work, but the diffs in `nightly-testing` are unexciting: we need to fully qualify a few names) They can all be closed when this is merged. Co-authored-by: Scott Morrison Co-authored-by: Eric Wieser --- Mathlib/Algebra/Algebra/Operations.lean | 5 +-- Mathlib/Algebra/BigOperators/Ring.lean | 2 +- Mathlib/Algebra/Homology/Homology.lean | 22 ------------ Mathlib/Algebra/Homology/Single.lean | 16 --------- Mathlib/Algebra/Jordan/Basic.lean | 2 +- Mathlib/Algebra/Order/CompleteField.lean | 3 +- .../GammaSpecAdjunction.lean | 1 - Mathlib/Analysis/Analytic/Inverse.lean | 4 ++- Mathlib/Analysis/MeanInequalities.lean | 10 ++++++ Mathlib/CategoryTheory/Comma.lean | 5 ++- .../CategoryTheory/DifferentialObject.lean | 10 +++--- Mathlib/CategoryTheory/Functor/Flat.lean | 2 +- .../Idempotents/FunctorCategories.lean | 1 - .../SimpleGraph/Regularity/Chunk.lean | 5 ++- Mathlib/Data/Complex/Module.lean | 2 +- Mathlib/Data/Ordmap/Ordset.lean | 4 +-- Mathlib/Data/Prod/TProd.lean | 2 +- Mathlib/Data/Set/Basic.lean | 8 ++--- Mathlib/Data/UInt.lean | 15 +++++--- Mathlib/Lean/Meta/DiscrTree.lean | 28 ++++++++------- .../CliffordAlgebra/Grading.lean | 29 ++------------- .../LinearAlgebra/QuadraticForm/Complex.lean | 2 +- Mathlib/Logic/Equiv/Set.lean | 6 +--- Mathlib/MeasureTheory/Function/Jacobian.lean | 3 +- Mathlib/MeasureTheory/Function/L1Space.lean | 7 +++- .../MeasureTheory/Measure/OuterMeasure.lean | 2 +- .../LegendreSymbol/GaussEisensteinLemmas.lean | 2 +- Mathlib/NumberTheory/Padics/RingHoms.lean | 3 ++ Mathlib/NumberTheory/PythagoreanTriples.lean | 5 +++ Mathlib/Probability/Kernel/Composition.lean | 36 +++++++++---------- Mathlib/Probability/Kernel/WithDensity.lean | 2 ++ .../RingTheory/MvPolynomial/Homogeneous.lean | 2 +- Mathlib/Tactic/Cache.lean | 14 ++++---- Mathlib/Tactic/LibrarySearch.lean | 22 +++++++----- Mathlib/Tactic/NormNum/Core.lean | 13 ++++--- Mathlib/Tactic/Positivity/Core.lean | 13 ++++--- Mathlib/Tactic/Propose.lean | 12 ++++--- Mathlib/Tactic/Relation/Rfl.lean | 2 +- Mathlib/Tactic/Relation/Trans.lean | 15 +++++--- Mathlib/Tactic/Rewrites.lean | 33 +++++++++-------- Mathlib/Tactic/Widget/Calc.lean | 4 +-- Mathlib/Topology/Constructions.lean | 2 +- Mathlib/Topology/DenseEmbedding.lean | 3 +- lake-manifest.json | 32 ++++++++--------- lean-toolchain | 2 +- 45 files changed, 199 insertions(+), 214 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index eb6d57ea59ae3..29a6286f3cd8e 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -463,10 +463,7 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n obtain ⟨r, rfl⟩ := hx exact hr r revert hx - -- porting note: workaround for lean4#1926, was `simp_rw [pow_succ']` - suffices h_lean4_1926 : ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (by rwa [pow_succ']) from - fun hx => h_lean4_1926 (by rwa [← pow_succ']) - -- porting note: end workaround + simp_rw [pow_succ'] intro hx exact Submodule.mul_induction_on' (fun m hm x ih => hmul _ _ hm (n_ih _) _ ih) diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean index 7829914c0d162..077ee0a10bda1 100644 --- a/Mathlib/Algebra/BigOperators/Ring.lean +++ b/Mathlib/Algebra/BigOperators/Ring.lean @@ -147,7 +147,7 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) : rw [prod_ite] congr 1 exact prod_bij' - (fun a _ => a.1) (by simp; tauto) (by simp) + (fun a _ => a.1) (by simp) (by simp) (fun a ha => ⟨a, (mem_filter.1 ha).1⟩) (fun a ha => by simp at ha; simp; tauto) (by simp) (by simp) exact prod_bij' diff --git a/Mathlib/Algebra/Homology/Homology.lean b/Mathlib/Algebra/Homology/Homology.lean index 4854308d36537..5bd6b088a8ae0 100644 --- a/Mathlib/Algebra/Homology/Homology.lean +++ b/Mathlib/Algebra/Homology/Homology.lean @@ -303,16 +303,6 @@ def homology'Functor [HasCokernels V] (i : ι) : HomologicalComplex V c ⥤ V wh -- here, but universe implementation details get in the way... obj C := C.homology' i map {C₁ C₂} f := homology'.map _ _ (f.sqTo i) (f.sqFrom i) rfl - map_id _ := by - simp only - ext1 - simp only [homology'.π_map, kernelSubobjectMap_id, Hom.sqFrom_id, Category.id_comp, - Category.comp_id] - map_comp _ _ := by - simp only - ext1 - simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology'.π_map_assoc, homology'.π_map, - Category.assoc] #align homology_functor homology'Functor /-- The homology functor from `ι`-indexed complexes to `ι`-graded objects in `V`. -/ @@ -320,18 +310,6 @@ def homology'Functor [HasCokernels V] (i : ι) : HomologicalComplex V c ⥤ V wh def gradedHomology'Functor [HasCokernels V] : HomologicalComplex V c ⥤ GradedObject ι V where obj C i := C.homology' i map {C C'} f i := (homology'Functor V c i).map f - map_id _ := by - ext - simp only [GradedObject.categoryOfGradedObjects_id] - ext - simp only [homology'.π_map, homology'Functor_map, kernelSubobjectMap_id, Hom.sqFrom_id, - Category.id_comp, Category.comp_id] - map_comp _ _ := by - ext - simp only [GradedObject.categoryOfGradedObjects_comp] - ext - simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology'.π_map_assoc, homology'.π_map, - homology'Functor_map, Category.assoc] #align graded_homology_functor gradedHomology'Functor end diff --git a/Mathlib/Algebra/Homology/Single.lean b/Mathlib/Algebra/Homology/Single.lean index bced93d1a583a..ed740c9a88d5a 100644 --- a/Mathlib/Algebra/Homology/Single.lean +++ b/Mathlib/Algebra/Homology/Single.lean @@ -131,14 +131,6 @@ def single₀ : V ⥤ ChainComplex V ℕ where match n with | 0 => f | n + 1 => 0 } - map_id X := by - ext (_|_) - · rfl - · simp - map_comp f g := by - ext (_|_) - · rfl - · simp #align chain_complex.single₀ ChainComplex.single₀ @[simp] @@ -328,14 +320,6 @@ def single₀ : V ⥤ CochainComplex V ℕ where match n with | 0 => f | n + 1 => 0 } - map_id X := by - ext (_|_) - · rfl - · simp - map_comp f g := by - ext (_|_) - · rfl - · simp #align cochain_complex.single₀ CochainComplex.single₀ @[simp] diff --git a/Mathlib/Algebra/Jordan/Basic.lean b/Mathlib/Algebra/Jordan/Basic.lean index 9357ea96be7fb..10b66852e895f 100644 --- a/Mathlib/Algebra/Jordan/Basic.lean +++ b/Mathlib/Algebra/Jordan/Basic.lean @@ -194,7 +194,7 @@ private theorem aux0 {a b c : A} : ⁅L (a + b + c), L ((a + b + c) * (a + b + c simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero] abel -set_option maxHeartbeats 400000 in +set_option maxHeartbeats 300000 in private theorem aux1 {a b c : A} : ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ diff --git a/Mathlib/Algebra/Order/CompleteField.lean b/Mathlib/Algebra/Order/CompleteField.lean index 0debf923fce4b..b290f004d4725 100644 --- a/Mathlib/Algebra/Order/CompleteField.lean +++ b/Mathlib/Algebra/Order/CompleteField.lean @@ -155,7 +155,8 @@ theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b := rw [coe_mem_cutMap_iff] exact_mod_cast sub_lt_comm.mp hq₁q · rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩ - refine' ⟨qa + qb, _, by norm_cast⟩ + -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. + refine' ⟨qa + qb, _, by beta_reduce; norm_cast⟩ rw [mem_setOf_eq, cast_add] exact add_lt_add ha hb #align linear_ordered_field.cut_map_add LinearOrderedField.cutMap_add diff --git a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean index 41b4c8fd4738c..97298a1fae244 100644 --- a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean +++ b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean @@ -199,7 +199,6 @@ theorem toΓSpecSheafedSpace_app_eq : dsimp at this rw [←this] dsimp - congr #align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_app_eq AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean index e64a7c0b3e6d0..31868233e51b2 100644 --- a/Mathlib/Analysis/Analytic/Inverse.lean +++ b/Mathlib/Analysis/Analytic/Inverse.lean @@ -563,7 +563,9 @@ theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F) -- conclude that all coefficients satisfy `aⁿ Qₙ ≤ (I + 1) a`. let a' : NNReal := ⟨a, apos.le⟩ suffices H : (a' : ENNReal) ≤ (p.rightInv i).radius - · apply lt_of_lt_of_le _ H; exact_mod_cast apos + · apply lt_of_lt_of_le _ H + -- Prior to leanprover/lean4#2734, this was `exact_mod_cast apos`. + simpa only [ENNReal.coe_pos] apply le_radius_of_bound _ ((I + 1) * a) fun n => ?_ by_cases hn : n = 0 · have : ‖p.rightInv i n‖ = ‖p.rightInv i 0‖ := by congr <;> try rw [hn] diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index 2bb8327742321..7bca745c9c5f5 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -609,6 +609,8 @@ theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjugateExponent q) (hf : ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by lift f to ι → ℝ≥0 using hf lift g to ι → ℝ≥0 using hg + -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. + beta_reduce at * norm_cast at * exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum #align real.inner_le_Lp_mul_Lq_tsum_of_nonneg Real.inner_le_Lp_mul_Lq_tsum_of_nonneg @@ -637,6 +639,8 @@ theorem inner_le_Lp_mul_Lq_hasSum_of_nonneg (hpq : p.IsConjugateExponent q) {A B lift g to ι → ℝ≥0 using hg lift A to ℝ≥0 using hA lift B to ℝ≥0 using hB + -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. + beta_reduce at * norm_cast at hf_sum hg_sum obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum refine' ⟨C, C.prop, hC, _⟩ @@ -674,6 +678,8 @@ theorem Lp_add_le_tsum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p) := by lift f to ι → ℝ≥0 using hf lift g to ι → ℝ≥0 using hg + -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. + beta_reduce at * norm_cast0 at * exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum #align real.Lp_add_le_tsum_of_nonneg Real.Lp_add_le_tsum_of_nonneg @@ -702,9 +708,13 @@ theorem Lp_add_le_hasSum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : lift g to ι → ℝ≥0 using hg lift A to ℝ≥0 using hA lift B to ℝ≥0 using hB + -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. + beta_reduce at hfA hgB norm_cast at hfA hgB obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB use C + -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. + beta_reduce norm_cast exact ⟨zero_le _, hC₁, hC₂⟩ #align real.Lp_add_le_has_sum_of_nonneg Real.Lp_add_le_hasSum_of_nonneg diff --git a/Mathlib/CategoryTheory/Comma.lean b/Mathlib/CategoryTheory/Comma.lean index 489d3e03f7277..17f9ed66f228f 100644 --- a/Mathlib/CategoryTheory/Comma.lean +++ b/Mathlib/CategoryTheory/Comma.lean @@ -167,9 +167,8 @@ theorem eqToHom_left (X Y : Comma L R) (H : X = Y) : #align category_theory.comma.eq_to_hom_left CategoryTheory.Comma.eqToHom_left @[simp] -theorem eqToHom_right (X Y : Comma L R) (H : X = Y) : CommaMorphism.right (eqToHom H) = eqToHom (by - cases H - rfl) := by +theorem eqToHom_right (X Y : Comma L R) (H : X = Y) : + CommaMorphism.right (eqToHom H) = eqToHom (by cases H; rfl) := by cases H rfl #align category_theory.comma.eq_to_hom_right CategoryTheory.Comma.eqToHom_right diff --git a/Mathlib/CategoryTheory/DifferentialObject.lean b/Mathlib/CategoryTheory/DifferentialObject.lean index 440bd01778d6e..e52f2713ca2d9 100644 --- a/Mathlib/CategoryTheory/DifferentialObject.lean +++ b/Mathlib/CategoryTheory/DifferentialObject.lean @@ -219,12 +219,10 @@ variable [(shiftFunctor C (1 : S)).PreservesZeroMorphisms] open scoped ZeroObject -instance hasZeroObject : HasZeroObject (DifferentialObject S C) := by - -- Porting note(https://github.com/leanprover-community/mathlib4/issues/4998): added `aesop_cat` - -- Porting note: added `simp only [eq_iff_true_of_subsingleton]` - refine' ⟨⟨⟨0, 0, by aesop_cat⟩, fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩, - fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩⟩⟩ <;> ext <;> - simp only [eq_iff_true_of_subsingleton] +instance hasZeroObject : HasZeroObject (DifferentialObject S C) where + zero := ⟨{ obj := 0, d := 0 }, + { unique_to := fun X => ⟨⟨⟨{ f := 0 }⟩, fun f => by ext⟩⟩, + unique_from := fun X => ⟨⟨⟨{ f := 0 }⟩, fun f => by ext⟩⟩ }⟩ #align category_theory.differential_object.has_zero_object CategoryTheory.DifferentialObject.hasZeroObject end DifferentialObject diff --git a/Mathlib/CategoryTheory/Functor/Flat.lean b/Mathlib/CategoryTheory/Functor/Flat.lean index 655d7b3b20828..33280fbd6fd05 100644 --- a/Mathlib/CategoryTheory/Functor/Flat.lean +++ b/Mathlib/CategoryTheory/Functor/Flat.lean @@ -208,7 +208,7 @@ theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F)) intro j injection c₀.π.naturality (BiconeHom.left j) with _ e₁ injection c₀.π.naturality (BiconeHom.right j) with _ e₂ - simpa (config := {zeta := false}) using e₁.symm.trans e₂ + simpa using e₁.symm.trans e₂ have : c.extend g₁.right = c.extend g₂.right := by unfold Cone.extend congr 1 diff --git a/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean b/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean index 545ea9debd3a9..e15dcdf2a94eb 100644 --- a/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean +++ b/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean @@ -80,7 +80,6 @@ instance functor_category_isIdempotentComplete [IsIdempotentComplete C] : use Y, i, e constructor · ext j - apply equalizer.hom_ext dsimp rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id] · ext j diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean index 647bd26f36382..0ec26e2331238 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean @@ -450,7 +450,10 @@ private theorem edgeDensity_star_not_uniform [Nonempty α] set s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) set t : ℝ := ↑(G.edgeDensity U V) have hrs : |r - s| ≤ ε / 5 := abs_density_star_sub_density_le_eps hPε hε₁ hUVne hUV - have hst : ε ≤ |s - t| := by exact_mod_cast G.nonuniformWitness_spec hUVne hUV + have hst : ε ≤ |s - t| := by + -- After leanprover/lean4#2734, we need to do the zeta reduction before `norm_cast`. + unfold_let s t + exact_mod_cast G.nonuniformWitness_spec hUVne hUV have hpr : |p - r| ≤ ε ^ 5 / 49 := average_density_near_total_density hPα hPε hε₁ star_subset_chunk star_subset_chunk have hqt : |q - t| ≤ ε ^ 5 / 49 := by diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean index 085514d0a279e..8f833afe4071b 100644 --- a/Mathlib/Data/Complex/Module.lean +++ b/Mathlib/Data/Complex/Module.lean @@ -479,7 +479,7 @@ lemma IsSelfAdjoint.coe_realPart {x : A} (hx : IsSelfAdjoint x) : (ℜ x : A) = x := hx.coe_selfAdjointPart_apply ℝ -lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) : +nonrec lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) : ℑ x = 0 := by rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero] diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean index c9224969e1b44..1b88800c6b9c8 100644 --- a/Mathlib/Data/Ordmap/Ordset.lean +++ b/Mathlib/Data/Ordmap/Ordset.lean @@ -408,7 +408,7 @@ theorem Sized.dual_iff {t : Ordnode α} : Sized (.dual t) ↔ Sized t := theorem Sized.rotateL {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (rotateL l x r) := by cases r; · exact hl.node' hr - rw [rotateL]; split_ifs + rw [Ordnode.rotateL]; split_ifs · exact hl.node3L hr.2.1 hr.2.2 · exact hl.node4L hr.2.1 hr.2.2 #align ordnode.sized.rotate_l Ordnode.Sized.rotateL @@ -1247,7 +1247,7 @@ theorem Valid'.rotateL {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : V have ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1 := by intros; linarith have hlp : size l > 0 → ¬size rl + size rr ≤ 1 := fun l0 hb => absurd (le_trans (le_trans (Nat.mul_le_mul_left _ l0) H2) hb) (by decide) - rw [rotateL]; split_ifs with h + rw [Ordnode.rotateL]; split_ifs with h · have rr0 : size rr > 0 := (mul_lt_mul_left (by decide)).1 (lt_of_le_of_lt (Nat.zero_le _) h : ratio * 0 < _) suffices BalancedSz (size l) (size rl) ∧ BalancedSz (size l + size rl + 1) (size rr) by diff --git a/Mathlib/Data/Prod/TProd.lean b/Mathlib/Data/Prod/TProd.lean index b80958ce652d9..3133a6173ee3f 100644 --- a/Mathlib/Data/Prod/TProd.lean +++ b/Mathlib/Data/Prod/TProd.lean @@ -177,7 +177,7 @@ theorem elim_preimage_pi [DecidableEq ι] {l : List ι} (hnd : l.Nodup) (h : ∀ simp [h] rw [← h2, ← mk_preimage_tprod, preimage_preimage] simp only [TProd.mk_elim hnd h] - dsimp; rfl + dsimp #align set.elim_preimage_pi Set.elim_preimage_pi end Set diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index ad94851310a79..dd9bd9a81c24f 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -2202,19 +2202,15 @@ theorem powerset_singleton (x : α) : 𝒫({x} : Set α) = {∅, {x}} := by /-! ### Sets defined as an if-then-else -/ ---Porting note: New theorem to prove `mem_dite` lemmas. --- `simp [h]` where `h : p` does not simplify `∀ (h : p), x ∈ s h` any more. --- https://github.com/leanprover/lean4/issues/1926 theorem mem_dite (p : Prop) [Decidable p] (s : p → Set α) (t : ¬ p → Set α) (x : α) : (x ∈ if h : p then s h else t h) ↔ (∀ h : p, x ∈ s h) ∧ ∀ h : ¬p, x ∈ t h := by split_ifs with hp · exact ⟨fun hx => ⟨fun _ => hx, fun hnp => (hnp hp).elim⟩, fun hx => hx.1 hp⟩ · exact ⟨fun hx => ⟨fun h => (hp h).elim, fun _ => hx⟩, fun hx => hx.2 hp⟩ ---Porting note: Old proof was `split_ifs; simp [h]` theorem mem_dite_univ_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) : (x ∈ if h : p then t h else univ) ↔ ∀ h : p, x ∈ t h := by - simp [mem_dite] + split_ifs <;> simp_all #align set.mem_dite_univ_right Set.mem_dite_univ_right @[simp] @@ -2225,7 +2221,7 @@ theorem mem_ite_univ_right (p : Prop) [Decidable p] (t : Set α) (x : α) : theorem mem_dite_univ_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) : (x ∈ if h : p then univ else t h) ↔ ∀ h : ¬p, x ∈ t h := by - simp [mem_dite] + split_ifs <;> simp_all #align set.mem_dite_univ_left Set.mem_dite_univ_left @[simp] diff --git a/Mathlib/Data/UInt.lean b/Mathlib/Data/UInt.lean index fcb8553156a0d..bc17670d8751f 100644 --- a/Mathlib/Data/UInt.lean +++ b/Mathlib/Data/UInt.lean @@ -5,15 +5,20 @@ import Mathlib.Algebra.GroupWithZero.Defs import Mathlib.Algebra.Ring.Basic import Mathlib.Data.ZMod.Defs -lemma UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size -> (ofNat a).val = a := Nat.mod_eq_of_lt +lemma UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size → ((ofNat a).val : Nat) = a := + Nat.mod_eq_of_lt -lemma UInt16.val_eq_of_lt {a : Nat} : a < UInt16.size -> (ofNat a).val = a := Nat.mod_eq_of_lt +lemma UInt16.val_eq_of_lt {a : Nat} : a < UInt16.size → ((ofNat a).val : Nat) = a := + Nat.mod_eq_of_lt -lemma UInt32.val_eq_of_lt {a : Nat} : a < UInt32.size -> (ofNat a).val = a := Nat.mod_eq_of_lt +lemma UInt32.val_eq_of_lt {a : Nat} : a < UInt32.size → ((ofNat a).val : Nat) = a := + Nat.mod_eq_of_lt -lemma UInt64.val_eq_of_lt {a : Nat} : a < UInt64.size -> (ofNat a).val = a := Nat.mod_eq_of_lt +lemma UInt64.val_eq_of_lt {a : Nat} : a < UInt64.size → ((ofNat a).val : Nat) = a := + Nat.mod_eq_of_lt -lemma USize.val_eq_of_lt {a : Nat} : a < USize.size -> (ofNat a).val = a := Nat.mod_eq_of_lt +lemma USize.val_eq_of_lt {a : Nat} : a < USize.size → ((ofNat a).val : Nat) = a := + Nat.mod_eq_of_lt instance UInt8.neZero : NeZero UInt8.size := ⟨by decide⟩ diff --git a/Mathlib/Lean/Meta/DiscrTree.lean b/Mathlib/Lean/Meta/DiscrTree.lean index d41556daad7cf..cbaa6819972af 100644 --- a/Mathlib/Lean/Meta/DiscrTree.lean +++ b/Mathlib/Lean/Meta/DiscrTree.lean @@ -18,12 +18,12 @@ namespace Lean.Meta.DiscrTree Inserts a new key into a discrimination tree, but only if it is not of the form `#[*]` or `#[=, *, *, *]`. -/ -def insertIfSpecific [BEq α] (d : DiscrTree α s) - (keys : Array (DiscrTree.Key s)) (v : α) : DiscrTree α s := +def insertIfSpecific [BEq α] (d : DiscrTree α) + (keys : Array Key) (v : α) (config : WhnfCoreConfig) : DiscrTree α := if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then d else - d.insertCore keys v + d.insertCore keys v config /-- Find keys which match the expression, or some subexpression. @@ -36,31 +36,33 @@ Implementation: we reverse the results from `getMatch`, so that we return lemmas matching larger subexpressions first, and amongst those we return more specific lemmas first. -/ -partial def getSubexpressionMatches (d : DiscrTree α s) (e : Expr) : MetaM (Array α) := do +partial def getSubexpressionMatches (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : + MetaM (Array α) := do match e with | .bvar _ => return #[] | .forallE _ _ _ _ => forallTelescope e (fun args body => do args.foldlM (fun acc arg => do - pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg))) - (← d.getSubexpressionMatches body).reverse) + pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg) config)) + (← d.getSubexpressionMatches body config).reverse) | .lam _ _ _ _ | .letE _ _ _ _ _ => lambdaLetTelescope e (fun args body => do args.foldlM (fun acc arg => do - pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg))) - (← d.getSubexpressionMatches body).reverse) + pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg) config)) + (← d.getSubexpressionMatches body config).reverse) | _ => - e.foldlM (fun a f => do pure <| a ++ (← d.getSubexpressionMatches f)) (← d.getMatch e).reverse + e.foldlM (fun a f => do + pure <| a ++ (← d.getSubexpressionMatches f config)) (← d.getMatch e config).reverse variable {m : Type → Type} [Monad m] /-- The explicit stack of `Trie.mapArrays` -/ -private inductive Ctxt {α β s} +private inductive Ctxt {α β} | empty : Ctxt - | ctxt : Array (Key s × Trie β s) → Array β → Array (Key s × Trie α s) → Key s → Ctxt → Ctxt + | ctxt : Array (Key × Trie β) → Array β → Array (Key × Trie α) → Key → Ctxt → Ctxt /-- Apply a function to the array of values at each node in a `DiscrTree`. -/ -partial def Trie.mapArrays (t : Trie α s) (f : Array α → Array β) : Trie β s := +partial def Trie.mapArrays (t : Trie α) (f : Array α → Array β) : Trie β := let .node vs0 cs0 := t go (.mkEmpty cs0.size) (f vs0) cs0.reverse Ctxt.empty where @@ -77,7 +79,7 @@ where go (.mkEmpty cs'.size) (f vs') cs'.reverse (.ctxt cs vs todo.pop k ps) /-- Apply a function to the array of values at each node in a `DiscrTree`. -/ -def mapArrays (d : DiscrTree α s) (f : Array α → Array β) : DiscrTree β s := +def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β := { root := d.root.map (fun t => t.mapArrays f) } end Lean.Meta.DiscrTree diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean index f19cae568ea29..2d4f7909ad377 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean @@ -173,26 +173,9 @@ theorem evenOdd_induction (n : ZMod 2) {P : ∀ x, x ∈ evenOdd Q n → Prop} (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) : P x hx := by apply Submodule.iSup_induction' (C := P) _ (hr 0 (Submodule.zero_mem _)) @hadd refine' Subtype.rec _ - -- porting note: was `simp_rw [Subtype.coe_mk, ZMod.nat_coe_zmod_eq_iff, add_comm n.val]` - -- leanprover/lean4#1926 is to blame. - dsimp only [Subtype.coe_mk] - let hlean1926 : ∀ val : ℕ, ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n := by - intro val - simp_rw [ZMod.nat_coe_zmod_eq_iff, add_comm n.val] - have := fun val : ℕ => forall_prop_congr' - (q := fun property => ∀ x (hx : x ∈ LinearMap.range (ι Q) ^ val), - P x (Submodule.mem_iSup_of_mem { val := val, property := property } hx)) - (hq := fun property => Iff.rfl) (hp := hlean1926 val) - simp_rw [this]; clear this - -- end porting note + simp_rw [ZMod.nat_coe_zmod_eq_iff, add_comm n.val] rintro n' ⟨k, rfl⟩ xv - -- porting note: was `simp_rw [pow_add, pow_mul]` - -- leanprover/lean4#1926 is to blame. - refine (forall_prop_congr' (hq := fun property => Iff.rfl) ( - show xv ∈ LinearMap.range (ι Q) ^ (2 * k + ZMod.val n) - ↔ xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n by - simp_rw [pow_add, pow_mul])).mpr ?_ - -- end porting note + simp_rw [pow_add, pow_mul] intro hxv induction hxv using Submodule.mul_induction_on' with | hm a ha b hb => @@ -205,13 +188,7 @@ theorem evenOdd_induction (n : ZMod 2) {P : ∀ x, x ∈ evenOdd Q n → Prop} apply hadd ihx ihy | hmul x hx n'' y hy ihy => revert hx - -- porting note: was `simp_rw [pow_two]` - -- leanprover/lean4#1926 is to blame. - let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 - ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by - rw [pow_two] - refine (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr ?_ - -- end porting note + simp_rw [pow_two] intro hx2 induction hx2 using Submodule.mul_induction_on' with | hm m hm n hn => diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean index 997dd5e7d6123..9a09c469912d6 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean @@ -54,7 +54,7 @@ noncomputable def isometryEquivSumSquares [DecidableEq ι] (w' : ι → ℂ) : split_ifs with h · simp only [h, zero_smul, zero_mul] have hww' : w' j = w j := by simp only [dif_neg h, Units.val_mk0] - simp only [one_mul, Units.val_mk0, smul_eq_mul] + simp (config := {zeta := false}) only [one_mul, Units.val_mk0, smul_eq_mul] rw [hww'] suffices v j * v j = w j ^ (-(1 / 2 : ℂ)) * w j ^ (-(1 / 2 : ℂ)) * w j * v j * v j by rw [this]; ring diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean index 527038b2b336b..e866f50c4868e 100644 --- a/Mathlib/Logic/Equiv/Set.lean +++ b/Mathlib/Logic/Equiv/Set.lean @@ -661,11 +661,7 @@ theorem preimage_piEquivPiSubtypeProd_symm_pi {α : Type*} {β : α → Type*} ( simp only [mem_preimage, mem_univ_pi, prod_mk_mem_set_prod_eq, Subtype.forall, ← forall_and] refine' forall_congr' fun i => _ dsimp only [Subtype.coe_mk] - -- Porting note: Two lines below were `by_cases hi <;> simp [hi]` - -- This regression is https://github.com/leanprover/lean4/issues/1926 - by_cases hi : p i - · simp [forall_prop_of_true hi, forall_prop_of_false (not_not.2 hi), hi] - · simp [forall_prop_of_false hi, hi, forall_prop_of_true hi] + by_cases hi : p i <;> simp [hi] #align equiv.preimage_pi_equiv_pi_subtype_prod_symm_pi Equiv.preimage_piEquivPiSubtypeProd_symm_pi -- See also `Equiv.sigmaFiberEquiv`. diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean index 31adc5dc37b32..d2f3721665fee 100644 --- a/Mathlib/MeasureTheory/Function/Jacobian.lean +++ b/Mathlib/MeasureTheory/Function/Jacobian.lean @@ -243,7 +243,8 @@ theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCou obtain ⟨q, hq⟩ : ∃ q, F q = (n, z, p) := hF _ -- then `x` belongs to `t q`. apply mem_iUnion.2 ⟨q, _⟩ - simp (config := { zeta := false }) only [hq, subset_closure hnz, hp, mem_inter_iff, and_true, hnz] + simp (config := { zeta := false }) only [K, hq, mem_inter_iff, hp, and_true] + exact subset_closure hnz #align exists_closed_cover_approximates_linear_on_of_has_fderiv_within_at exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt variable [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index 9e757fa94011f..e8c37b1b68b8a 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -404,6 +404,8 @@ theorem HasFiniteIntegral.smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] (∫⁻ a : α, ‖c • f a‖₊ ∂μ) ≤ ∫⁻ a : α, ‖c‖₊ * ‖f a‖₊ ∂μ := by refine' lintegral_mono _ intro i + -- After leanprover/lean4#2734, we need to do beta reduction `exact_mod_cast` + beta_reduce exact_mod_cast (nnnorm_smul_le c (f i)) _ < ∞ := by rw [lintegral_const_mul'] @@ -667,7 +669,10 @@ theorem Integrable.add' {f g : α → β} (hf : Integrable f μ) (hg : Integrabl HasFiniteIntegral (f + g) μ := calc (∫⁻ a, ‖f a + g a‖₊ ∂μ) ≤ ∫⁻ a, ‖f a‖₊ + ‖g a‖₊ ∂μ := - lintegral_mono fun a => by exact_mod_cast nnnorm_add_le _ _ + lintegral_mono fun a => by + -- After leanprover/lean4#2734, we need to do beta reduction before `exact_mod_cast` + beta_reduce + exact_mod_cast nnnorm_add_le _ _ _ = _ := (lintegral_nnnorm_add_left hf.aestronglyMeasurable _) _ < ∞ := add_lt_top.2 ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩ #align measure_theory.integrable.add' MeasureTheory.Integrable.add' diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean index 72deaa828e630..aa596c5706556 100644 --- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean @@ -129,7 +129,7 @@ generalising to `Sort`. -/ theorem iUnion_null_iff' (m : OuterMeasure α) {ι : Prop} {s : ι → Set α} : m (⋃ i, s i) = 0 ↔ ∀ i, m (s i) = 0 := ⟨ fun h i => mono_null m (subset_iUnion s i) h, - by by_cases i : ι <;> simp [i]; exact (fun h => h (Iff.mpr (Iff.of_eq (eq_true i)) trivial)) ⟩ + by by_cases i : ι <;> simp [i]⟩ #align measure_theory.outer_measure.Union_null_iff' MeasureTheory.OuterMeasure.iUnion_null_iff' theorem biUnion_null_iff (m : OuterMeasure α) {s : Set β} (hs : s.Countable) {t : β → Set α} : diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean index e7038a2862a05..f008ccd93a3a8 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean @@ -83,7 +83,7 @@ private theorem gauss_lemma_aux₁ (p : ℕ) [Fact p.Prime] {a : ℤ} (∏ x in Ico 1 (p / 2).succ, if (a * x : ZMod p).val ≤ p / 2 then (1 : ZMod p) else -1) = ∏ x in (Ico 1 (p / 2).succ).filter fun x : ℕ => ¬(a * x : ZMod p).val ≤ p / 2, -1 := prod_bij_ne_one (fun x _ _ => x) - (fun x => by split_ifs <;> simp_all (config := { contextual := true })) + (fun x => by split_ifs <;> (dsimp; simp_all)) (fun _ _ _ _ _ _ => id) (fun b h _ => ⟨b, by simp_all [-not_le]⟩) (by intros; split_ifs at * <;> simp_all) rw [prod_mul_distrib, this, prod_const] diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean index b08fc29368fc3..c5980b3b24eea 100644 --- a/Mathlib/NumberTheory/Padics/RingHoms.lean +++ b/Mathlib/NumberTheory/Padics/RingHoms.lean @@ -508,6 +508,9 @@ theorem isCauSeq_nthHom (r : R) : IsCauSeq (padicNorm p) fun n => nthHom f r n : use k intro j hj refine' lt_of_le_of_lt _ hk + -- Need to do beta reduction first, as `norm_cast` doesn't. + -- Added to adapt to leanprover/lean4#2734. + beta_reduce norm_cast rw [← padicNorm.dvd_iff_norm_le] exact_mod_cast pow_dvd_nthHom_sub f_compat r k j hj diff --git a/Mathlib/NumberTheory/PythagoreanTriples.lean b/Mathlib/NumberTheory/PythagoreanTriples.lean index 5be1ba662c767..d6726a57c49f1 100644 --- a/Mathlib/NumberTheory/PythagoreanTriples.lean +++ b/Mathlib/NumberTheory/PythagoreanTriples.lean @@ -485,6 +485,11 @@ theorem isPrimitiveClassified_of_coprime_of_odd_of_pos (hc : Int.gcd x y = 1) (h let m := (q.den : ℤ) let n := q.num have hm0 : m ≠ 0 := by + -- Added to adapt to leanprover/lean4#2734. + -- Without `unfold_let`, `norm_cast` can't see the coercion. + -- One might try `zeta := true` in `Tactic.NormCast.derive`, + -- but that seems to break many other things. + unfold_let m norm_cast apply Rat.den_nz q have hq2 : q = n / m := (Rat.num_div_den q).symm diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index ae67dc630686d..27ef08a67dd46 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -697,15 +697,15 @@ theorem lintegral_prodMkLeft (κ : kernel α β) (ca : γ × α) (g : β → ℝ #align probability_theory.kernel.lintegral_prod_mk_left ProbabilityTheory.kernel.lintegral_prodMkLeft instance IsMarkovKernel.prodMkLeft (κ : kernel α β) [IsMarkovKernel κ] : - IsMarkovKernel (prodMkLeft γ κ) := by rw [prodMkLeft]; infer_instance + IsMarkovKernel (prodMkLeft γ κ) := by rw [kernel.prodMkLeft]; infer_instance #align probability_theory.kernel.is_markov_kernel.prod_mk_left ProbabilityTheory.kernel.IsMarkovKernel.prodMkLeft instance IsFiniteKernel.prodMkLeft (κ : kernel α β) [IsFiniteKernel κ] : - IsFiniteKernel (prodMkLeft γ κ) := by rw [prodMkLeft]; infer_instance + IsFiniteKernel (prodMkLeft γ κ) := by rw [kernel.prodMkLeft]; infer_instance #align probability_theory.kernel.is_finite_kernel.prod_mk_left ProbabilityTheory.kernel.IsFiniteKernel.prodMkLeft instance IsSFiniteKernel.prodMkLeft (κ : kernel α β) [IsSFiniteKernel κ] : - IsSFiniteKernel (prodMkLeft γ κ) := by rw [prodMkLeft]; infer_instance + IsSFiniteKernel (prodMkLeft γ κ) := by rw [kernel.prodMkLeft]; infer_instance #align probability_theory.kernel.is_s_finite_kernel.prod_mk_left ProbabilityTheory.kernel.IsSFiniteKernel.prodMkLeft /-- Define a `kernel (β × α) γ` from a `kernel (α × β) γ` by taking the comap of `Prod.swap`. -/ @@ -728,15 +728,15 @@ theorem lintegral_swapLeft (κ : kernel (α × β) γ) (a : β × α) (g : γ #align probability_theory.kernel.lintegral_swap_left ProbabilityTheory.kernel.lintegral_swapLeft instance IsMarkovKernel.swapLeft (κ : kernel (α × β) γ) [IsMarkovKernel κ] : - IsMarkovKernel (swapLeft κ) := by rw [swapLeft]; infer_instance + IsMarkovKernel (swapLeft κ) := by rw [kernel.swapLeft]; infer_instance #align probability_theory.kernel.is_markov_kernel.swap_left ProbabilityTheory.kernel.IsMarkovKernel.swapLeft instance IsFiniteKernel.swapLeft (κ : kernel (α × β) γ) [IsFiniteKernel κ] : - IsFiniteKernel (swapLeft κ) := by rw [swapLeft]; infer_instance + IsFiniteKernel (swapLeft κ) := by rw [kernel.swapLeft]; infer_instance #align probability_theory.kernel.is_finite_kernel.swap_left ProbabilityTheory.kernel.IsFiniteKernel.swapLeft instance IsSFiniteKernel.swapLeft (κ : kernel (α × β) γ) [IsSFiniteKernel κ] : - IsSFiniteKernel (swapLeft κ) := by rw [swapLeft]; infer_instance + IsSFiniteKernel (swapLeft κ) := by rw [kernel.swapLeft]; infer_instance #align probability_theory.kernel.is_s_finite_kernel.swap_left ProbabilityTheory.kernel.IsSFiniteKernel.swapLeft /-- Define a `kernel α (γ × β)` from a `kernel α (β × γ)` by taking the map of `Prod.swap`. -/ @@ -759,15 +759,15 @@ theorem lintegral_swapRight (κ : kernel α (β × γ)) (a : α) {g : γ × β #align probability_theory.kernel.lintegral_swap_right ProbabilityTheory.kernel.lintegral_swapRight instance IsMarkovKernel.swapRight (κ : kernel α (β × γ)) [IsMarkovKernel κ] : - IsMarkovKernel (swapRight κ) := by rw [swapRight]; infer_instance + IsMarkovKernel (swapRight κ) := by rw [kernel.swapRight]; infer_instance #align probability_theory.kernel.is_markov_kernel.swap_right ProbabilityTheory.kernel.IsMarkovKernel.swapRight instance IsFiniteKernel.swapRight (κ : kernel α (β × γ)) [IsFiniteKernel κ] : - IsFiniteKernel (swapRight κ) := by rw [swapRight]; infer_instance + IsFiniteKernel (swapRight κ) := by rw [kernel.swapRight]; infer_instance #align probability_theory.kernel.is_finite_kernel.swap_right ProbabilityTheory.kernel.IsFiniteKernel.swapRight instance IsSFiniteKernel.swapRight (κ : kernel α (β × γ)) [IsSFiniteKernel κ] : - IsSFiniteKernel (swapRight κ) := by rw [swapRight]; infer_instance + IsSFiniteKernel (swapRight κ) := by rw [kernel.swapRight]; infer_instance #align probability_theory.kernel.is_s_finite_kernel.swap_right ProbabilityTheory.kernel.IsSFiniteKernel.swapRight /-- Define a `kernel α β` from a `kernel α (β × γ)` by taking the map of the first projection. -/ @@ -789,15 +789,15 @@ theorem lintegral_fst (κ : kernel α (β × γ)) (a : α) {g : β → ℝ≥0 #align probability_theory.kernel.lintegral_fst ProbabilityTheory.kernel.lintegral_fst instance IsMarkovKernel.fst (κ : kernel α (β × γ)) [IsMarkovKernel κ] : IsMarkovKernel (fst κ) := by - rw [fst]; infer_instance + rw [kernel.fst]; infer_instance #align probability_theory.kernel.is_markov_kernel.fst ProbabilityTheory.kernel.IsMarkovKernel.fst instance IsFiniteKernel.fst (κ : kernel α (β × γ)) [IsFiniteKernel κ] : IsFiniteKernel (fst κ) := by - rw [fst]; infer_instance + rw [kernel.fst]; infer_instance #align probability_theory.kernel.is_finite_kernel.fst ProbabilityTheory.kernel.IsFiniteKernel.fst instance IsSFiniteKernel.fst (κ : kernel α (β × γ)) [IsSFiniteKernel κ] : IsSFiniteKernel (fst κ) := - by rw [fst]; infer_instance + by rw [kernel.fst]; infer_instance #align probability_theory.kernel.is_s_finite_kernel.fst ProbabilityTheory.kernel.IsSFiniteKernel.fst /-- Define a `kernel α γ` from a `kernel α (β × γ)` by taking the map of the second projection. -/ @@ -819,15 +819,15 @@ theorem lintegral_snd (κ : kernel α (β × γ)) (a : α) {g : γ → ℝ≥0 #align probability_theory.kernel.lintegral_snd ProbabilityTheory.kernel.lintegral_snd instance IsMarkovKernel.snd (κ : kernel α (β × γ)) [IsMarkovKernel κ] : IsMarkovKernel (snd κ) := by - rw [snd]; infer_instance + rw [kernel.snd]; infer_instance #align probability_theory.kernel.is_markov_kernel.snd ProbabilityTheory.kernel.IsMarkovKernel.snd instance IsFiniteKernel.snd (κ : kernel α (β × γ)) [IsFiniteKernel κ] : IsFiniteKernel (snd κ) := by - rw [snd]; infer_instance + rw [kernel.snd]; infer_instance #align probability_theory.kernel.is_finite_kernel.snd ProbabilityTheory.kernel.IsFiniteKernel.snd instance IsSFiniteKernel.snd (κ : kernel α (β × γ)) [IsSFiniteKernel κ] : IsSFiniteKernel (snd κ) := - by rw [snd]; infer_instance + by rw [kernel.snd]; infer_instance #align probability_theory.kernel.is_s_finite_kernel.snd ProbabilityTheory.kernel.IsSFiniteKernel.snd end FstSnd @@ -932,15 +932,15 @@ theorem lintegral_prod (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel α #align probability_theory.kernel.lintegral_prod ProbabilityTheory.kernel.lintegral_prod instance IsMarkovKernel.prod (κ : kernel α β) [IsMarkovKernel κ] (η : kernel α γ) - [IsMarkovKernel η] : IsMarkovKernel (κ ×ₖ η) := by rw [prod]; infer_instance + [IsMarkovKernel η] : IsMarkovKernel (κ ×ₖ η) := by rw [kernel.prod]; infer_instance #align probability_theory.kernel.is_markov_kernel.prod ProbabilityTheory.kernel.IsMarkovKernel.prod instance IsFiniteKernel.prod (κ : kernel α β) [IsFiniteKernel κ] (η : kernel α γ) - [IsFiniteKernel η] : IsFiniteKernel (κ ×ₖ η) := by rw [prod]; infer_instance + [IsFiniteKernel η] : IsFiniteKernel (κ ×ₖ η) := by rw [kernel.prod]; infer_instance #align probability_theory.kernel.is_finite_kernel.prod ProbabilityTheory.kernel.IsFiniteKernel.prod instance IsSFiniteKernel.prod (κ : kernel α β) (η : kernel α γ) : - IsSFiniteKernel (κ ×ₖ η) := by rw [prod]; infer_instance + IsSFiniteKernel (κ ×ₖ η) := by rw [kernel.prod]; infer_instance #align probability_theory.kernel.is_s_finite_kernel.prod ProbabilityTheory.kernel.IsSFiniteKernel.prod end Prod diff --git a/Mathlib/Probability/Kernel/WithDensity.lean b/Mathlib/Probability/Kernel/WithDensity.lean index 392b43ca1ae83..9d86218cbec7a 100644 --- a/Mathlib/Probability/Kernel/WithDensity.lean +++ b/Mathlib/Probability/Kernel/WithDensity.lean @@ -203,6 +203,8 @@ theorem isSFiniteKernel_withDensity_of_isFiniteKernel (κ : kernel α β) [IsFin refine' isSFiniteKernel_sum fun n => _ suffices IsFiniteKernel (withDensity κ (fs n)) by haveI := this; infer_instance refine' isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => _ + -- After leanprover/lean4#2734, we need to do beta reduction before `norm_cast` + beta_reduce norm_cast calc fs n a b ≤ min (f a b) (n + 1) := tsub_le_self diff --git a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean index 98b6b6b01f6f3..ed0570655eda9 100644 --- a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean +++ b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean @@ -204,7 +204,7 @@ theorem prod {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : #align mv_polynomial.is_homogeneous.prod MvPolynomial.IsHomogeneous.prod theorem totalDegree (hφ : IsHomogeneous φ n) (h : φ ≠ 0) : totalDegree φ = n := by - rw [totalDegree] + rw [MvPolynomial.totalDegree] apply le_antisymm · apply Finset.sup_le intro d hd diff --git a/Mathlib/Tactic/Cache.lean b/Mathlib/Tactic/Cache.lean index 694382dd9063e..fe14e684f7ae5 100644 --- a/Mathlib/Tactic/Cache.lean +++ b/Mathlib/Tactic/Cache.lean @@ -142,19 +142,20 @@ The first will store declarations in the current file, the second will store declarations from imports (and will hopefully be "read-only" after creation). -/ @[reducible] def DiscrTreeCache (α : Type) : Type := - DeclCache (DiscrTree α true × DiscrTree α true) + DeclCache (DiscrTree α × DiscrTree α) /-- Build a `DiscrTreeCache`, from a function that returns a collection of keys and values for each declaration. -/ def DiscrTreeCache.mk [BEq α] (profilingName : String) - (processDecl : Name → ConstantInfo → MetaM (Array (Array (DiscrTree.Key true) × α))) + (processDecl : Name → ConstantInfo → MetaM (Array (Array DiscrTree.Key × α))) (post? : Option (Array α → Array α) := none) - (init : Option (DiscrTree α true) := none) : + (init : Option (DiscrTree α) := none) + (config : WhnfCoreConfig) : IO (DiscrTreeCache α) := let updateTree := fun name constInfo tree => do - return (← processDecl name constInfo).foldl (fun t (k, v) => t.insertIfSpecific k v) tree + return (← processDecl name constInfo).foldl (fun t (k, v) => t.insertIfSpecific k v config) tree let addDecl := fun name constInfo (tree₁, tree₂) => do return (← updateTree name constInfo tree₁, tree₂) let addLibraryDecl := fun name constInfo (tree₁, tree₂) => do @@ -175,8 +176,9 @@ it will rebuild the discrimination tree for the current file multiple times, and it would be more efficient to call `c.get` once, and then call `DiscrTree.getMatch` multiple times. -/ -def DiscrTreeCache.getMatch (c : DiscrTreeCache α) (e : Expr) : MetaM (Array α) := do +def DiscrTreeCache.getMatch (c : DiscrTreeCache α) (e : Expr) (config : WhnfCoreConfig) : + MetaM (Array α) := do let (locals, imports) ← c.get -- `DiscrTree.getMatch` returns results in batches, with more specific lemmas coming later. -- Hence we reverse this list, so we try out more specific lemmas earlier. - return (← locals.getMatch e).reverse ++ (← imports.getMatch e).reverse + return (← locals.getMatch e config).reverse ++ (← imports.getMatch e config).reverse diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean index 40ff9bee4abfe..0a253265cc904 100644 --- a/Mathlib/Tactic/LibrarySearch.lean +++ b/Mathlib/Tactic/LibrarySearch.lean @@ -31,6 +31,9 @@ open Lean Meta Std.Tactic.TryThis initialize registerTraceClass `Tactic.librarySearch initialize registerTraceClass `Tactic.librarySearch.lemmas +/-- Configuration for `DiscrTree`. -/ +def discrTreeConfig : WhnfCoreConfig := {} + /-- A "modifier" for a declaration. * `none` indicates the original declaration, @@ -47,17 +50,17 @@ instance : ToString DeclMod where /-- Prepare the discrimination tree entries for a lemma. -/ def processLemma (name : Name) (constInfo : ConstantInfo) : - MetaM (Array (Array (DiscrTree.Key true) × (Name × DeclMod))) := do + MetaM (Array (Array DiscrTree.Key × (Name × DeclMod))) := do if constInfo.isUnsafe then return #[] if ← name.isBlackListed then return #[] withNewMCtxDepth do withReducible do let (_, _, type) ← forallMetaTelescope constInfo.type - let keys ← DiscrTree.mkPath type + let keys ← DiscrTree.mkPath type discrTreeConfig let mut r := #[(keys, (name, .none))] match type.getAppFnArgs with | (``Iff, #[lhs, rhs]) => do - return r.push (← DiscrTree.mkPath rhs, (name, .mp)) - |>.push (← DiscrTree.mkPath lhs, (name, .mpr)) + return r.push (← DiscrTree.mkPath rhs discrTreeConfig, (name, .mp)) + |>.push (← DiscrTree.mkPath lhs discrTreeConfig, (name, .mpr)) | _ => return r /-- Insert a lemma into the discrimination tree. -/ @@ -66,15 +69,15 @@ def processLemma (name : Name) (constInfo : ConstantInfo) : -- `build/lib/MathlibExtras/LibrarySearch.extra` -- so that the cache is rebuilt. def addLemma (name : Name) (constInfo : ConstantInfo) - (lemmas : DiscrTree (Name × DeclMod) true) : MetaM (DiscrTree (Name × DeclMod) true) := do + (lemmas : DiscrTree (Name × DeclMod)) : MetaM (DiscrTree (Name × DeclMod)) := do let mut lemmas := lemmas for (key, value) in ← processLemma name constInfo do - lemmas := lemmas.insertIfSpecific key value + lemmas := lemmas.insertIfSpecific key value discrTreeConfig return lemmas /-- Construct the discrimination tree of all lemmas. -/ def buildDiscrTree : IO (DiscrTreeCache (Name × DeclMod)) := - DiscrTreeCache.mk "apply?: init cache" processLemma + DiscrTreeCache.mk "apply?: init cache" processLemma (config := discrTreeConfig) -- Sort so lemmas with longest names come first. -- This is counter-intuitive, but the way that `DiscrTree.getMatch` returns results -- means that the results come in "batches", with more specific matches *later*. @@ -98,9 +101,10 @@ Retrieve the current current of lemmas. initialize librarySearchLemmas : DiscrTreeCache (Name × DeclMod) ← unsafe do let path ← cachePath if (← path.pathExists) then - let (d, _r) ← unpickle (DiscrTree (Name × DeclMod) true) path + let (d, _r) ← unpickle (DiscrTree (Name × DeclMod)) path -- We can drop the `CompactedRegion` value; we do not plan to free it DiscrTreeCache.mk "apply?: using cache" processLemma (init := some d) + (config := discrTreeConfig) else buildDiscrTree @@ -145,7 +149,7 @@ def librarySearchCore (goal : MVarId) (required : List Expr) (solveByElimDepth := 6) : Nondet MetaM (List MVarId) := .squash fun _ => do let ty ← goal.getType - let lemmas := (← librarySearchLemmas.getMatch ty).toList + let lemmas := (← librarySearchLemmas.getMatch ty discrTreeConfig).toList trace[Tactic.librarySearch.lemmas] m!"Candidate library_search lemmas:\n{lemmas}" return (Nondet.ofList lemmas).filterMapM fun (lem, mod) => observing? <| librarySearchLemma lem mod required solveByElimDepth goal diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean index ddb35ca06aa60..6ebf7ed63e1d7 100644 --- a/Mathlib/Tactic/NormNum/Core.lean +++ b/Mathlib/Tactic/NormNum/Core.lean @@ -51,22 +51,25 @@ def mkNormNumExt (n : Name) : ImportM NormNumExt := do /-- Each `norm_num` extension is labelled with a collection of patterns which determine the expressions to which it should be applied. -/ -abbrev Entry := Array (Array (DiscrTree.Key true)) × Name +abbrev Entry := Array (Array DiscrTree.Key) × Name /-- The state of the `norm_num` extension environment -/ structure NormNums where /-- The tree of `norm_num` extensions. -/ - tree : DiscrTree NormNumExt true := {} + tree : DiscrTree NormNumExt := {} /-- Erased `norm_num`s. -/ erased : PHashSet Name := {} deriving Inhabited +/-- Configuration for `DiscrTree`. -/ +def discrTreeConfig : WhnfCoreConfig := {} + /-- Environment extensions for `norm_num` declarations -/ initialize normNumExt : ScopedEnvExtension Entry (Entry × NormNumExt) NormNums ← -- we only need this to deduplicate entries in the DiscrTree have : BEq NormNumExt := ⟨fun _ _ ↦ false⟩ /- Insert `v : NormNumExt` into the tree `dt` on all key sequences given in `kss`. -/ - let insert kss v dt := kss.foldl (fun dt ks ↦ dt.insertCore ks v) dt + let insert kss v dt := kss.foldl (fun dt ks ↦ dt.insertCore ks v discrTreeConfig) dt registerScopedEnvExtension { mkInitial := pure {} ofOLeanEntry := fun _ e@(_, n) ↦ return (e, ← mkNormNumExt n) @@ -84,7 +87,7 @@ def derive {α : Q(Type u)} (e : Q($α)) (post := false) : MetaM (Result e) := d profileitM Exception "norm_num" (← getOptions) do let s ← saveState let normNums := normNumExt.getState (← getEnv) - let arr ← normNums.tree.getMatch e + let arr ← normNums.tree.getMatch e discrTreeConfig for ext in arr do if (bif post then ext.post else ext.pre) && ! normNums.erased.contains ext.name then try @@ -177,7 +180,7 @@ initialize registerBuiltinAttribute { let e ← elabTerm stx none let (_, _, e) ← lambdaMetaTelescope (← mkLambdaFVars (← getLCtx).getFVars e) return e - DiscrTree.mkPath e + DiscrTree.mkPath e discrTreeConfig normNumExt.add ((keys, declName), ext) kind | _ => throwUnsupportedSyntax erase := fun declName => do diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 060f6d5e9addb..755eb8cbe93ee 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -62,16 +62,19 @@ def mkPositivityExt (n : Name) : ImportM PositivityExt := do let { env, opts, .. } ← read IO.ofExcept <| unsafe env.evalConstCheck PositivityExt opts ``PositivityExt n +/-- Configuration for `DiscrTree`. -/ +def discrTreeConfig : WhnfCoreConfig := {} + /-- Each `positivity` extension is labelled with a collection of patterns which determine the expressions to which it should be applied. -/ -abbrev Entry := Array (Array (DiscrTree.Key true)) × Name +abbrev Entry := Array (Array DiscrTree.Key) × Name /-- Environment extensions for `positivity` declarations -/ initialize positivityExt : PersistentEnvExtension Entry (Entry × PositivityExt) - (List Entry × DiscrTree PositivityExt true) ← + (List Entry × DiscrTree PositivityExt) ← -- we only need this to deduplicate entries in the DiscrTree have : BEq PositivityExt := ⟨fun _ _ => false⟩ - let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v) dt + let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v discrTreeConfig) dt registerPersistentEnvExtension { mkInitial := pure ([], {}) addImportedFn := fun s => do @@ -101,7 +104,7 @@ initialize registerBuiltinAttribute { let e ← elabTerm stx none let (_, _, e) ← lambdaMetaTelescope (← mkLambdaFVars (← getLCtx).getFVars e) return e - DiscrTree.mkPath e + DiscrTree.mkPath e discrTreeConfig setEnv <| positivityExt.addEntry env ((keys, declName), ext) | _ => throwUnsupportedSyntax } @@ -287,7 +290,7 @@ def orElse (t₁ : Strictness zα pα e) (t₂ : MetaM (Strictness zα pα e)) : def core (e : Q($α)) : MetaM (Strictness zα pα e) := do let mut result := .none trace[Tactic.positivity] "trying to prove positivity of {e}" - for ext in ← (positivityExt.getState (← getEnv)).2.getMatch e do + for ext in ← (positivityExt.getState (← getEnv)).2.getMatch e discrTreeConfig do try result ← orElse result <| ext.eval zα pα e catch err => diff --git a/Mathlib/Tactic/Propose.lean b/Mathlib/Tactic/Propose.lean index 4099f6aafbd6a..6363dc110517f 100644 --- a/Mathlib/Tactic/Propose.lean +++ b/Mathlib/Tactic/Propose.lean @@ -42,7 +42,10 @@ open Lean Meta Std.Tactic.TryThis initialize registerTraceClass `Tactic.propose -initialize proposeLemmas : DeclCache (DiscrTree Name true) ← +/-- Configuration for `DiscrTree`. -/ +def discrTreeConfig : WhnfCoreConfig := {} + +initialize proposeLemmas : DeclCache (DiscrTree Name) ← DeclCache.mk "have?: init cache" {} fun name constInfo lemmas => do if constInfo.isUnsafe then return lemmas if ← name.isBlackListed then return lemmas @@ -50,7 +53,8 @@ initialize proposeLemmas : DeclCache (DiscrTree Name true) ← let (mvars, _, _) ← forallMetaTelescope constInfo.type let mut lemmas := lemmas for m in mvars do - lemmas := lemmas.insertIfSpecific (← DiscrTree.mkPath (← inferType m)) name + let path ← DiscrTree.mkPath (← inferType m) discrTreeConfig + lemmas := lemmas.insertIfSpecific path name discrTreeConfig pure lemmas /-- Shortcut for calling `solveByElim`. -/ @@ -73,11 +77,11 @@ We look up candidate lemmas from a discrimination tree using the first such expr Returns an array of pairs, containing the names of found lemmas and the resulting application. -/ -def propose (lemmas : DiscrTree Name s) (type : Expr) (required : Array Expr) +def propose (lemmas : DiscrTree Name) (type : Expr) (required : Array Expr) (solveByElimDepth := 15) : MetaM (Array (Name × Expr)) := do guard !required.isEmpty let ty ← whnfR (← instantiateMVars (← inferType required[0]!)) - let candidates ← lemmas.getMatch ty + let candidates ← lemmas.getMatch ty discrTreeConfig candidates.filterMapM fun lem : Name => try trace[Tactic.propose] "considering {lem}" diff --git a/Mathlib/Tactic/Relation/Rfl.lean b/Mathlib/Tactic/Relation/Rfl.lean index c81e3a024e888..5fe045dfabe5b 100644 --- a/Mathlib/Tactic/Relation/Rfl.lean +++ b/Mathlib/Tactic/Relation/Rfl.lean @@ -41,7 +41,7 @@ def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do if rel.isAppOf `Eq then -- No need to lift Eq to Eq return mvarId - for lem in ← (Std.Tactic.reflExt.getState (← getEnv)).getMatch rel do + for lem in ← (Std.Tactic.reflExt.getState (← getEnv)).getMatch rel Std.Tactic.reflExt.config do let res ← observing? do -- First create an equality relating the LHS and RHS -- and reduce the goal to proving that LHS is related to LHS. diff --git a/Mathlib/Tactic/Relation/Trans.lean b/Mathlib/Tactic/Relation/Trans.lean index fd92d2cea3d62..df0b91d4958f8 100644 --- a/Mathlib/Tactic/Relation/Trans.lean +++ b/Mathlib/Tactic/Relation/Trans.lean @@ -21,11 +21,14 @@ open Lean Meta Elab initialize registerTraceClass `Tactic.trans +/-- Discrimation tree settings for the `trans` extension. -/ +def transExt.config : WhnfCoreConfig := {} + /-- Environment extension storing transitivity lemmas -/ initialize transExt : - SimpleScopedEnvExtension (Name × Array (DiscrTree.Key true)) (DiscrTree Name true) ← + SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ← registerSimpleScopedEnvExtension { - addEntry := fun dt (n, ks) ↦ dt.insertCore ks n + addEntry := fun dt (n, ks) ↦ dt.insertCore ks n transExt.config initial := {} } @@ -43,7 +46,7 @@ initialize registerBuiltinAttribute { let some xyHyp := xs.pop.back? | fail let .app (.app _ _) _ ← inferType yzHyp | fail let .app (.app _ _) _ ← inferType xyHyp | fail - let key ← withReducible <| DiscrTree.mkPath rel + let key ← withReducible <| DiscrTree.mkPath rel transExt.config transExt.add (decl, key) kind } @@ -129,7 +132,9 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do let t'? ← t?.mapM (elabTermWithHoles · ty (← getMainTag)) let s ← saveState trace[Tactic.trans]"trying homogeneous case" - for lem in (← (transExt.getState (← getEnv)).getUnify rel).push ``Trans.simple do + let lemmas := + (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push ``Trans.simple + for lem in lemmas do trace[Tactic.trans]"trying lemma {lem}" try liftMetaTactic fun g ↦ do @@ -147,7 +152,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do trace[Tactic.trans]"trying heterogeneous case" let t'? ← t?.mapM (elabTermWithHoles · none (← getMainTag)) let s ← saveState - for lem in (← (transExt.getState (← getEnv)).getUnify rel).push + for lem in (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push ``HEq.trans |>.push ``HEq.trans do try liftMetaTactic fun g ↦ do diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean index b84c2348b1be5..bce7b0553c137 100644 --- a/Mathlib/Tactic/Rewrites.lean +++ b/Mathlib/Tactic/Rewrites.lean @@ -53,9 +53,12 @@ def forwardWeight := 2 /-- Weight to multiply the "specificity" of a rewrite lemma by when rewriting backwards. -/ def backwardWeight := 1 +/-- Configuration for `DiscrTree`. -/ +def discrTreeConfig : WhnfCoreConfig := {} + /-- Prepare the discrimination tree entries for a lemma. -/ def processLemma (name : Name) (constInfo : ConstantInfo) : - MetaM (Array (Array (DiscrTree.Key true) × (Name × Bool × Nat))) := do + MetaM (Array (Array DiscrTree.Key × (Name × Bool × Nat))) := do if constInfo.isUnsafe then return #[] if ← name.isBlackListed then return #[] -- We now remove some injectivity lemmas which are not useful to rewrite by. @@ -69,8 +72,8 @@ def processLemma (name : Name) (constInfo : ConstantInfo) : match type.getAppFnArgs with | (``Eq, #[_, lhs, rhs]) | (``Iff, #[lhs, rhs]) => do - let lhsKey ← DiscrTree.mkPath lhs - let rhsKey ← DiscrTree.mkPath rhs + let lhsKey ← DiscrTree.mkPath lhs discrTreeConfig + let rhsKey ← DiscrTree.mkPath rhs discrTreeConfig return #[(lhsKey, (name, false, forwardWeight * lhsKey.size)), (rhsKey, (name, true, backwardWeight * rhsKey.size))] | _ => return #[] @@ -85,8 +88,8 @@ def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool × match type.getAppFnArgs with | (``Eq, #[_, lhs, rhs]) | (``Iff, #[lhs, rhs]) => do - let lhsKey : Array (DiscrTree.Key true) ← DiscrTree.mkPath lhs - let rhsKey : Array (DiscrTree.Key true) ← DiscrTree.mkPath rhs + let lhsKey : Array DiscrTree.Key ← DiscrTree.mkPath lhs discrTreeConfig + let rhsKey : Array DiscrTree.Key ← DiscrTree.mkPath rhs discrTreeConfig result := result.push (h, false, forwardWeight * lhsKey.size) |>.push (h, true, backwardWeight * rhsKey.size) | _ => pure () @@ -98,15 +101,15 @@ def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool × -- `build/lib/MathlibExtras/Rewrites.extra` -- so that the cache is rebuilt. def addLemma (name : Name) (constInfo : ConstantInfo) - (lemmas : DiscrTree (Name × Bool × Nat) true) : MetaM (DiscrTree (Name × Bool × Nat) true) := do + (lemmas : DiscrTree (Name × Bool × Nat)) : MetaM (DiscrTree (Name × Bool × Nat)) := do let mut lemmas := lemmas for (key, value) in ← processLemma name constInfo do - lemmas := lemmas.insertIfSpecific key value + lemmas := lemmas.insertIfSpecific key value discrTreeConfig return lemmas /-- Construct the discrimination tree of all lemmas. -/ def buildDiscrTree : IO (DiscrTreeCache (Name × Bool × Nat)) := - DiscrTreeCache.mk "rw?: init cache" processLemma + DiscrTreeCache.mk "rw?: init cache" processLemma (config := discrTreeConfig) -- Sort so lemmas with longest names come first. -- This is counter-intuitive, but the way that `DiscrTree.getMatch` returns results -- means that the results come in "batches", with more specific matches *later*. @@ -130,9 +133,9 @@ Retrieve the current cache of lemmas. initialize rewriteLemmas : DiscrTreeCache (Name × Bool × Nat) ← unsafe do let path ← cachePath if (← path.pathExists) then - let (d, _r) ← unpickle (DiscrTree (Name × Bool × Nat) true) path + let (d, _r) ← unpickle (DiscrTree (Name × Bool × Nat)) path -- We can drop the `CompactedRegion` value; we do not plan to free it - DiscrTreeCache.mk "rw?: using cache" processLemma (init := some d) + DiscrTreeCache.mk "rw?: using cache" processLemma (init := some d) (config := discrTreeConfig) else buildDiscrTree @@ -213,12 +216,12 @@ See also `rewrites` for a more convenient interface. -- because `MLList.squash` executes lazily, -- so there is no opportunity for `← getMCtx` to record the context at the call site. def rewritesCore (hyps : Array (Expr × Bool × Nat)) - (lemmas : DiscrTree (Name × Bool × Nat) s × DiscrTree (Name × Bool × Nat) s) + (lemmas : DiscrTree (Name × Bool × Nat) × DiscrTree (Name × Bool × Nat)) (ctx : MetavarContext) (goal : MVarId) (target : Expr) (side : SideConditions := .solveByElim) : MLList MetaM RewriteResult := MLList.squash fun _ => do -- Get all lemmas which could match some subexpression - let candidates := (← lemmas.1.getSubexpressionMatches target) - ++ (← lemmas.2.getSubexpressionMatches target) + let candidates := (← lemmas.1.getSubexpressionMatches target discrTreeConfig) + ++ (← lemmas.2.getSubexpressionMatches target discrTreeConfig) -- Sort them by our preferring weighting -- (length of discriminant key, doubled for the forward implication) @@ -276,7 +279,7 @@ Find lemmas which can rewrite the goal, and deduplicate based on pretty-printed Note that this builds a `HashMap` containing the results, and so may consume significant memory. -/ def rewritesDedup (hyps : Array (Expr × Bool × Nat)) - (lemmas : DiscrTree (Name × Bool × Nat) s × DiscrTree (Name × Bool × Nat) s) + (lemmas : DiscrTree (Name × Bool × Nat) × DiscrTree (Name × Bool × Nat)) (mctx : MetavarContext) (goal : MVarId) (target : Expr) (side : SideConditions := .solveByElim) : MLList MetaM RewriteResult := MLList.squash fun _ => do @@ -289,7 +292,7 @@ def rewritesDedup (hyps : Array (Expr × Bool × Nat)) /-- Find lemmas which can rewrite the goal. -/ def rewrites (hyps : Array (Expr × Bool × Nat)) - (lemmas : DiscrTree (Name × Bool × Nat) s × DiscrTree (Name × Bool × Nat) s) + (lemmas : DiscrTree (Name × Bool × Nat) × DiscrTree (Name × Bool × Nat)) (goal : MVarId) (target : Expr) (side : SideConditions := .solveByElim) (stopAtRfl : Bool := false) (max : Nat := 20) (leavePercentHeartbeats : Nat := 10) : MetaM (List RewriteResult) := do diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean index 85a0de6f5af3f..634be8df3c637 100644 --- a/Mathlib/Tactic/Widget/Calc.lean +++ b/Mathlib/Tactic/Widget/Calc.lean @@ -21,7 +21,7 @@ open Lean Server RequestM /-- Code action to create a `calc` tactic from the current goal. -/ @[tactic_code_action calcTactic] -def createCalc : TacticCodeAction := fun params _snap ctx _stack node => do +def createCalc : TacticCodeAction := fun _params _snap ctx _stack node => do let .node (.ofTacticInfo info) _ := node | return #[] if info.goalsBefore.isEmpty then return #[] let eager := { @@ -37,7 +37,7 @@ def createCalc : TacticCodeAction := fun params _snap ctx _stack node => do let goal := info.goalsBefore[0]! let goalFmt ← ctx.runMetaM {} <| goal.withContext do Meta.ppExpr (← goal.getType) return { eager with - edit? := some <|.ofTextEdit params.textDocument.uri + edit? := some <|.ofTextEdit doc.versionedIdentifier { range := ⟨tacPos, endPos⟩, newText := s!"calc {goalFmt} := by sorry" } } }] diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index a44ee34ce7af2..5e9be1b2c6914 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -1029,7 +1029,7 @@ lemma IsClosedMap.restrictPreimage {f : α → β} (hcl : IsClosedMap f) (T : Se IsClosedMap (T.restrictPreimage f) := by rw [isClosedMap_iff_clusterPt] at hcl ⊢ intro A ⟨y, hyT⟩ hy - rw [restrictPreimage, MapClusterPt, ← inducing_subtype_val.mapClusterPt_iff, MapClusterPt, + rw [Set.restrictPreimage, MapClusterPt, ← inducing_subtype_val.mapClusterPt_iff, MapClusterPt, map_map, MapsTo.restrict_commutes, ← map_map, ← MapClusterPt, map_principal] at hy rcases hcl _ y hy with ⟨x, hxy, hx⟩ have hxT : f x ∈ T := hxy ▸ hyT diff --git a/Mathlib/Topology/DenseEmbedding.lean b/Mathlib/Topology/DenseEmbedding.lean index 07e58c1ace315..2e59f522668d0 100644 --- a/Mathlib/Topology/DenseEmbedding.lean +++ b/Mathlib/Topology/DenseEmbedding.lean @@ -201,8 +201,7 @@ theorem continuousAt_extend [T3Space γ] {b : β} {f : α → γ} (di : DenseInd have V₁_in : V₁ ∈ 𝓝 b := by filter_upwards [hf] rintro x ⟨c, hc⟩ - unfold_let φ - rwa [di.extend_eq_of_tendsto hc] + rwa [← di.extend_eq_of_tendsto hc] at hc obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by simpa [and_assoc] using ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in diff --git a/lake-manifest.json b/lake-manifest.json index f01e67b1d5d53..99a5e90a2ebf0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,6 +2,14 @@ "packagesDir": "lake-packages", "packages": [{"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "a71c160b1934814837d37f377efaf2964e55c433", + "opts": {}, + "name": "std", + "inputRev?": "main", + "inherited": false}}, + {"git": {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", @@ -9,6 +17,14 @@ "name": "Qq", "inputRev?": "master", "inherited": false}}, + {"git": + {"url": "https://github.com/leanprover-community/aesop", + "subDir?": null, + "rev": "ed733adcb79e54e157fafb805ce3518d4411ab70", + "opts": {}, + "name": "aesop", + "inputRev?": "master", + "inherited": false}}, {"git": {"url": "https://github.com/leanprover/lean4-cli", "subDir?": null, @@ -24,21 +40,5 @@ "opts": {}, "name": "proofwidgets", "inputRev?": "v0.0.21", - "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "6747f41f28627bed83e6d5891683538211caa2c1", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover-community/aesop", - "subDir?": null, - "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7", - "opts": {}, - "name": "aesop", - "inputRev?": "master", "inherited": false}}], "name": "mathlib"} diff --git a/lean-toolchain b/lean-toolchain index 2f868c67d035a..e8560170ab7d7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0 +leanprover/lean4:v4.3.0-rc1