diff --git a/Archive/Wiedijk100Theorems/BirthdayProblem.lean b/Archive/Wiedijk100Theorems/BirthdayProblem.lean index 37342bfe1bf1ca..33ceb56f834a8a 100644 --- a/Archive/Wiedijk100Theorems/BirthdayProblem.lean +++ b/Archive/Wiedijk100Theorems/BirthdayProblem.lean @@ -80,7 +80,10 @@ theorem birthday_measure : · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin] rfl rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff] - rotate_left; (iterate 2 right; norm_num); decide; (iterate 2 left; norm_num) + rotate_left + iterate 2 right; norm_num + · decide + iterate 2 left; norm_num simp only [Fintype.card_pi] norm_num #align theorems_100.birthday_measure Theorems100.birthday_measure diff --git a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean index 58aacf285f0710..a050098fc2ffc5 100644 --- a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean +++ b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean @@ -284,9 +284,9 @@ lemma integral_min_eq_two_mul : ∫ θ in (0)..π, min d (θ.sin * l) = 2 * ∫ θ in (0)..π / 2, min d (θ.sin * l) := by rw [← intervalIntegral.integral_add_adjacent_intervals (b := π / 2) (c := π)] conv => lhs; arg 2; arg 1; intro θ; rw [← neg_neg θ, Real.sin_neg] - simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi, - intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg, - (by ring : -(π / 2) + π = π / 2), two_mul] + · simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi, + intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg, + (by ring : -(π / 2) + π = π / 2), two_mul] all_goals exact intervalIntegrable_min_const_sin_mul d l _ _ /-- diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean index 6da0b8d8b70800..df5db7389bdc59 100644 --- a/Mathlib/Algebra/Lie/Weights/Basic.lean +++ b/Mathlib/Algebra/Lie/Weights/Basic.lean @@ -363,7 +363,8 @@ lemma mem_posFittingCompOf (x : L) (m : M) : obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k exact this n k intro m l - induction' l with l ih; simp + induction' l with l ih + · simp simp only [lowerCentralSeries_succ, pow_succ', LinearMap.mul_apply] exact LieSubmodule.lie_mem_lie _ ⊤ (LieSubmodule.mem_top x) ih @@ -602,7 +603,8 @@ lemma independent_weightSpace [NoZeroSMulDivisors R M] : simpa only [CompleteLattice.independent_iff_supIndep_of_injOn (injOn_weightSpace R L M), Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.not_mem_erase χ) intro χ₁ s - induction' s using Finset.induction_on with χ₂ s _ ih; simp + induction' s using Finset.induction_on with χ₂ s _ ih + · simp intro hχ₁₂ obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂ specialize ih hχ₁ diff --git a/Mathlib/Algebra/Module/Zlattice/Basic.lean b/Mathlib/Algebra/Module/Zlattice/Basic.lean index 48a5ee348150dd..bf578713a97e0a 100644 --- a/Mathlib/Algebra/Module/Zlattice/Basic.lean +++ b/Mathlib/Algebra/Module/Zlattice/Basic.lean @@ -518,8 +518,8 @@ theorem Zlattice.rank [hs : IsZlattice K L] : finrank ℤ L = finrank K E := by have h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ L) = (Set.range b).toFinset.card := by rw [Set.toFinset_range, Finset.univ.card_image_of_injective] - rfl - exact Subtype.coe_injective.comp (Basis.injective _) + · rfl + · exact Subtype.coe_injective.comp (Basis.injective _) rw [finrank_eq_card_chooseBasisIndex] -- We prove that `finrank ℤ L ≤ finrank K E` and `finrank K E ≤ finrank ℤ L` refine le_antisymm ?_ ?_ diff --git a/Mathlib/Algebra/Polynomial/UnitTrinomial.lean b/Mathlib/Algebra/Polynomial/UnitTrinomial.lean index 492cbabece4366..91ce67a0ebb844 100644 --- a/Mathlib/Algebra/Polynomial/UnitTrinomial.lean +++ b/Mathlib/Algebra/Polynomial/UnitTrinomial.lean @@ -273,10 +273,10 @@ theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k rw [this] at hp exact Or.inl (hq.trans hp.symm) rw [tsub_add_eq_add_tsub hmn.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm - rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm' - exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm) - exact hmn'.le.trans (Nat.le_add_right n k) - exact hmn.le.trans (Nat.le_add_right n k) + · rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm' + · exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm) + · exact hmn'.le.trans (Nat.le_add_right n k) + · exact hmn.le.trans (Nat.le_add_right n k) #align polynomial.is_unit_trinomial.irreducible_aux2 Polynomial.IsUnitTrinomial.irreducible_aux2 theorem irreducible_aux3 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n) diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 36b61391c47e68..b6ce412aa9ea59 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -267,7 +267,7 @@ theorem fromSpec_range : Set.range hU.fromSpec.1.base = (U : Set X) := by delta IsAffineOpen.fromSpec; dsimp rw [← Category.assoc, coe_comp, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ] - exact Subtype.range_coe + · exact Subtype.range_coe rw [← TopCat.epi_iff_surjective] infer_instance #align algebraic_geometry.is_affine_open.from_Spec_range AlgebraicGeometry.IsAffineOpen.fromSpec_range @@ -555,26 +555,26 @@ def _root_.AlgebraicGeometry.Scheme.affineBasicOpen theorem basicOpen_union_eq_self_iff (s : Set (X.presheaf.obj <| op U)) : ⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U) = U ↔ Ideal.span s = ⊤ := by trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ - trans - hU.fromSpec.1.base ⁻¹' (⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U)).1 = - hU.fromSpec.1.base ⁻¹' U.1 - · refine' ⟨fun h => by rw [h], _⟩ - intro h - apply_fun Set.image hU.fromSpec.1.base at h - rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.fromSpec_range] - at h - simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h - ext1 - refine' Set.Subset.antisymm _ h - simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup] - intro x _ - exact X.basicOpen_le x - · simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion] - congr! 1 - · refine congr_arg (Set.iUnion ·) ?_ - ext1 x - exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _) - · exact congr_arg Opens.carrier hU.fromSpec_base_preimage + · trans + hU.fromSpec.1.base ⁻¹' (⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U)).1 = + hU.fromSpec.1.base ⁻¹' U.1 + · refine' ⟨fun h => by rw [h], _⟩ + intro h + apply_fun Set.image hU.fromSpec.1.base at h + rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.fromSpec_range] + at h + simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h + ext1 + refine' Set.Subset.antisymm _ h + simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup] + intro x _ + exact X.basicOpen_le x + · simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion] + congr! 1 + · refine congr_arg (Set.iUnion ·) ?_ + ext1 x + exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _) + · exact congr_arg Opens.carrier hU.fromSpec_base_preimage · simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl] rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ← PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span] diff --git a/Mathlib/AlgebraicGeometry/FunctionField.lean b/Mathlib/AlgebraicGeometry/FunctionField.lean index 190882a2898f60..fe71ea653ff304 100644 --- a/Mathlib/AlgebraicGeometry/FunctionField.lean +++ b/Mathlib/AlgebraicGeometry/FunctionField.lean @@ -56,8 +56,9 @@ noncomputable instance [IsIntegral X] : Field X.functionField := by have hs : genericPoint X.carrier ∈ RingedSpace.basicOpen _ s := by rw [← SetLike.mem_coe, (genericPoint_spec X.carrier).mem_open_set_iff, Set.top_eq_univ, Set.univ_inter, Set.nonempty_iff_ne_empty, Ne, ← Opens.coe_bot, ← SetLike.ext'_iff] - erw [basicOpen_eq_bot_iff] - exacts [ha, (RingedSpace.basicOpen _ _).isOpen] + · erw [basicOpen_eq_bot_iff] + exact ha + · exact (RingedSpace.basicOpen _ _).isOpen have := (X.presheaf.germ ⟨_, hs⟩).isUnit_map (RingedSpace.isUnit_res_basicOpen _ s) rwa [TopCat.Presheaf.germ_res_apply] at this @@ -87,9 +88,9 @@ theorem genericPoint_eq_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsO symm rw [eq_top_iff, Set.top_eq_univ, Set.top_eq_univ] convert subset_closure_inter_of_isPreirreducible_of_isOpen _ H.base_open.isOpen_range _ - rw [Set.univ_inter, Set.image_univ] - apply PreirreducibleSpace.isPreirreducible_univ (X := Y.carrier) - exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩ + · rw [Set.univ_inter, Set.image_univ] + · apply PreirreducibleSpace.isPreirreducible_univ (X := Y.carrier) + · exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩ #align algebraic_geometry.generic_point_eq_of_is_open_immersion AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion noncomputable instance stalkFunctionFieldAlgebra [IrreducibleSpace X.carrier] (x : X.carrier) : diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean index 65495ac51f001d..6693d7b54698ad 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean @@ -301,8 +301,8 @@ theorem AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AffineTargetMo · introv hs hs' replace hs := ((topIsAffineOpen Y).basicOpen_union_eq_self_iff _).mpr hs have := H f ⟨Y.openCoverOfSuprEqTop _ hs, ?_, ?_⟩ (𝟙 _) - rwa [← Category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_isIso hP] - at this + · rwa [← Category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_isIso hP] + at this · intro i; exact (topIsAffineOpen Y).basicOpenIsAffine _ · rintro (i : s) specialize hs' i diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean index 693b75f6ab1e9b..aaafbddb325a4b 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean @@ -59,8 +59,9 @@ instance (priority := 900) quasiCompactOfIsIso {X Y : Scheme} (f : X ⟶ Y) [IsI intro U _ hU' convert hU'.image (inv f.1.base).continuous_toFun using 1 rw [Set.image_eq_preimage_of_inverse] - delta Function.LeftInverse - exacts [IsIso.inv_hom_id_apply f.1.base, IsIso.hom_inv_id_apply f.1.base] + · delta Function.LeftInverse + exact IsIso.inv_hom_id_apply f.1.base + · exact IsIso.hom_inv_id_apply f.1.base #align algebraic_geometry.quasi_compact_of_is_iso AlgebraicGeometry.quasiCompactOfIsIso instance quasiCompactComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCompact f] @@ -171,14 +172,14 @@ theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _). exact H · rintro X Y H f S hS hS' rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS - delta QuasiCompact.affineProperty - rw [← isCompact_univ_iff] - change IsCompact ((Opens.map f.val.base).obj ⊤).1 - rw [← hS] - dsimp [Opens.map] - simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion] - exacts [isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i), - topIsAffineOpen _] + · delta QuasiCompact.affineProperty + rw [← isCompact_univ_iff] + change IsCompact ((Opens.map f.val.base).obj ⊤).1 + rw [← hS] + dsimp [Opens.map] + simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion] + exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i) + · exact topIsAffineOpen _ #align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) : @@ -323,8 +324,8 @@ theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme convert congr_arg (X.presheaf.map (homOfLE _).op) H -- Note: the below was `simp only [← comp_apply]` · rw [← comp_apply, ← comp_apply] - simp only [← Functor.map_comp] - rfl + · simp only [← Functor.map_comp] + rfl · simp only [Scheme.basicOpen_res, ge_iff_le, inf_le_right] · rw [map_zero] choose n hn using H' diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean index 0512b44f6442d0..a4281091272328 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean @@ -393,12 +393,16 @@ theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U : replace hs : S ⊓ U.1 = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs have hs₁ : ∀ i : s, i.1.1 ≤ S := by intro i; change (i : Opens X.carrier) ≤ S - refine' le_trans _ inf_le_left; swap; exact U.1; erw [hs] + refine' le_trans _ inf_le_left; swap + · exact U.1 + erw [hs] -- Porting note: have to add argument explicitly exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i have hs₂ : ∀ i : s, i.1.1 ≤ U.1 := by intro i; change (i : Opens X.carrier) ≤ U - refine' le_trans _ inf_le_right; swap; exact S; erw [hs] + refine' le_trans _ inf_le_right; swap + · exact S + erw [hs] -- Porting note: have to add argument explicitly exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i -- On each affine open in the intersection, we have `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂` diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index 34a4bb7ef3262a..dd49d683a99524 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean @@ -180,25 +180,25 @@ theorem affineLocally_iff_affineOpens_le (hP : RingHom.RespectsIso @P) {X Y : Sc erw [Subtype.range_val] convert e have := H ⟨(Opens.map (X.ofRestrict U'.openEmbedding).1.base).obj V.1, ?h'⟩ - erw [← X.presheaf.map_comp] at this - rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc, - ← X.presheaf.map_comp] - convert this using 1 - dsimp only [Functor.op, unop_op] - rw [Opens.openEmbedding_obj_top] - congr 1 - exact e'.symm - case h' => - apply (X.ofRestrict U'.openEmbedding).isAffineOpen_iff_of_isOpenImmersion.mp - -- Porting note: was convert V.2 - erw [e'] - apply V.2 + · erw [← X.presheaf.map_comp] at this + · rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc, + ← X.presheaf.map_comp] + · convert this using 1 + dsimp only [Functor.op, unop_op] + rw [Opens.openEmbedding_obj_top] + congr 1 + exact e'.symm + case h' => + apply (X.ofRestrict U'.openEmbedding).isAffineOpen_iff_of_isOpenImmersion.mp + -- Porting note: was convert V.2 + erw [e'] + apply V.2 · intro H V specialize H ⟨_, V.2.imageIsOpenImmersion (X.ofRestrict _)⟩ (Subtype.coe_image_subset _ _) erw [← X.presheaf.map_comp] rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc, ← X.presheaf.map_comp] - convert H + · convert H · dsimp only [Functor.op, unop_op]; rw [Opens.openEmbedding_obj_top] #align algebraic_geometry.affine_locally_iff_affine_opens_le AlgebraicGeometry.affineLocally_iff_affineOpens_le @@ -230,16 +230,16 @@ theorem sourceAffineLocally_isLocal (h₁ : RingHom.RespectsIso @P) apply h₃ _ _ hs intro r have := hs' r ⟨(Opens.map (X.ofRestrict _).1.base).obj U.1, ?_⟩ - rwa [h₁.ofRestrict_morphismRestrict_iff] at this - · exact U.2 - · rfl - · suffices ∀ (V) (_ : V = (Opens.map f.val.base).obj (Y.basicOpen r.val)), - IsAffineOpen ((Opens.map (X.ofRestrict V.openEmbedding).1.base).obj U.1) by - exact this _ rfl - intro V hV - rw [Scheme.preimage_basicOpen] at hV - subst hV - exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1) + · rwa [h₁.ofRestrict_morphismRestrict_iff] at this + · exact U.2 + · rfl + · suffices ∀ (V) (_ : V = (Opens.map f.val.base).obj (Y.basicOpen r.val)), + IsAffineOpen ((Opens.map (X.ofRestrict V.openEmbedding).1.base).obj U.1) by + exact this _ rfl + intro V hV + rw [Scheme.preimage_basicOpen] at hV + subst hV + exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1) #align algebraic_geometry.source_affine_locally_is_local AlgebraicGeometry.sourceAffineLocally_isLocal variable (hP : RingHom.PropertyIsLocal @P) @@ -271,9 +271,9 @@ theorem isOpenImmersionCat_comp_of_sourceAffineLocally (h₁ : RingHom.RespectsI rw [← h₁.cancel_right_isIso _ (Scheme.Γ.map (IsOpenImmersion.isoOfRangeEq (Y.ofRestrict _) f _).hom.op), ← Functor.map_comp, ← op_comp] - convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3 - · rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc] - exact Subtype.range_coe + · convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3 + · rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc] + exact Subtype.range_coe #align algebraic_geometry.is_open_immersion_comp_of_source_affine_locally AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean index 230e713b2d4aad..b8ad8ecb9f967a 100644 --- a/Mathlib/AlgebraicGeometry/OpenImmersion.lean +++ b/Mathlib/AlgebraicGeometry/OpenImmersion.lean @@ -118,8 +118,8 @@ def affineCover (X : Scheme) : OpenCover X where intro x erw [coe_comp] rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ] - erw [Subtype.range_coe_subtype] - exact (X.local_affine x).choose.2 + · erw [Subtype.range_coe_subtype] + exact (X.local_affine x).choose.2 rw [← TopCat.epi_iff_surjective] change Epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forgetToSheafedSpace.map _)) infer_instance @@ -561,9 +561,9 @@ theorem range_pullback_snd_of_left : rw [Set.range_comp, Set.range_iff_surjective.mpr, ← @Set.preimage_univ _ _ (pullback.fst : pullback f.1.base g.1.base ⟶ _)] -- Porting note (#10691): was `rw` - erw [TopCat.pullback_snd_image_fst_preimage] - rw [Set.image_univ] - rfl + · erw [TopCat.pullback_snd_image_fst_preimage] + rw [Set.image_univ] + rfl rw [← TopCat.epi_iff_surjective] infer_instance #align algebraic_geometry.IsOpenImmersion.range_pullback_snd_of_left AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left @@ -578,9 +578,9 @@ theorem range_pullback_fst_of_right : rw [Set.range_comp, Set.range_iff_surjective.mpr, ← @Set.preimage_univ _ _ (pullback.snd : pullback g.1.base f.1.base ⟶ _)] -- Porting note (#10691): was `rw` - erw [TopCat.pullback_fst_image_snd_preimage] - rw [Set.image_univ] - rfl + · erw [TopCat.pullback_fst_image_snd_preimage] + rw [Set.image_univ] + rfl rw [← TopCat.epi_iff_surjective] infer_instance #align algebraic_geometry.IsOpenImmersion.range_pullback_fst_of_right AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right @@ -703,13 +703,13 @@ theorem image_basicOpen {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U -- Porting note (#10691): was `rw` erw [PresheafedSpace.IsOpenImmersion.invApp_app_apply] at e rw [Scheme.basicOpen_res, inf_eq_right.mpr _] at e - rw [← e] - ext1 - -- Porting note: this `dsimp` was not necessary - dsimp [Opens.map] - refine' Set.image_preimage_eq_inter_range.trans _ - erw [Set.inter_eq_left] - refine' Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _) + · rw [← e] + ext1 + -- Porting note: this `dsimp` was not necessary + dsimp [Opens.map] + refine' Set.image_preimage_eq_inter_range.trans _ + erw [Set.inter_eq_left] + refine' Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _) refine' le_trans (Scheme.basicOpen_le _ _) (le_of_eq _) ext1 exact (Set.preimage_image_eq _ H.base_open.inj).symm @@ -740,8 +740,8 @@ def Scheme.OpenCover.pullbackCover {X : Scheme} (𝒰 : X.OpenCover) {W : Scheme erw [coe_comp] rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ, TopCat.pullback_fst_range] - obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x) - exact ⟨y, h.symm⟩ + · obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x) + exact ⟨y, h.symm⟩ · rw [← TopCat.epi_iff_surjective]; infer_instance #align algebraic_geometry.Scheme.open_cover.pullback_cover AlgebraicGeometry.Scheme.OpenCover.pullbackCover @@ -763,8 +763,8 @@ def Scheme.OpenCover.pullbackCover' {X : Scheme} (𝒰 : X.OpenCover) {W : Schem erw [coe_comp] rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ, TopCat.pullback_snd_range] - obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x) - exact ⟨y, h⟩ + · obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x) + exact ⟨y, h⟩ · rw [← TopCat.epi_iff_surjective]; infer_instance theorem Scheme.OpenCover.iUnion_range {X : Scheme} (𝒰 : X.OpenCover) : diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean index c2442da3959d18..abb5fe4c471a4c 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean @@ -295,21 +295,21 @@ def toFun (x : Proj.T| pbo f) : Spec.T A⁰_ f := rw [Submonoid.coe_one, one_mul] at eq1 change f ^ _ * (_ * _) = f ^ _ * (f ^ _ * f ^ _ * _) at eq1 have that : a1 * a2 * f ^ N * f ^ M ∈ x.val.asHomogeneousIdeal.toIdeal := ?_ - rcases x.1.isPrime.mem_or_mem (show a1 * a2 * f ^ N * f ^ M ∈ _ from that) with (h1 | rid2) - rcases x.1.isPrime.mem_or_mem h1 with (h1 | rid1) - rcases x.1.isPrime.mem_or_mem h1 with (h1 | h2) - · left; - simp only [show (Localization.mk a1 ⟨f ^ n1, _⟩ : Away f) = - Localization.mk a1 1 * Localization.mk 1 (⟨f ^ n1, ⟨n1, rfl⟩⟩ : Submonoid.powers f) by - rw [Localization.mk_mul, mul_one, one_mul]] - exact Ideal.mul_mem_right _ _ (Ideal.subset_span ⟨_, h1, rfl⟩) - · right; - simp only [show (mk a2 ⟨f ^ n2, _⟩ : Away f) = - mk a2 1 * Localization.mk 1 (⟨f ^ n2, ⟨n2, rfl⟩⟩ : Submonoid.powers f) by - rw [Localization.mk_mul, mul_one, one_mul]] - exact Ideal.mul_mem_right _ _ (Ideal.subset_span ⟨_, h2, rfl⟩) - · exact False.elim (x.2 (x.1.isPrime.mem_of_pow_mem N rid1)) - · exact False.elim (x.2 (x.1.isPrime.mem_of_pow_mem M rid2)) + · rcases x.1.isPrime.mem_or_mem (show a1 * a2 * f ^ N * f ^ M ∈ _ from that) with (h1 | rid2) + · rcases x.1.isPrime.mem_or_mem h1 with (h1 | rid1) + · rcases x.1.isPrime.mem_or_mem h1 with (h1 | h2) + · left; + simp only [show (Localization.mk a1 ⟨f ^ n1, _⟩ : Away f) = + Localization.mk a1 1 * Localization.mk 1 (⟨f ^ n1, ⟨n1, rfl⟩⟩ : Submonoid.powers f) by + rw [Localization.mk_mul, mul_one, one_mul]] + exact Ideal.mul_mem_right _ _ (Ideal.subset_span ⟨_, h1, rfl⟩) + · right; + simp only [show (mk a2 ⟨f ^ n2, _⟩ : Away f) = + mk a2 1 * Localization.mk 1 (⟨f ^ n2, ⟨n2, rfl⟩⟩ : Submonoid.powers f) by + rw [Localization.mk_mul, mul_one, one_mul]] + exact Ideal.mul_mem_right _ _ (Ideal.subset_span ⟨_, h2, rfl⟩) + · exact False.elim (x.2 (x.1.isPrime.mem_of_pow_mem N rid1)) + · exact False.elim (x.2 (x.1.isPrime.mem_of_pow_mem M rid2)) · rw [← mul_comm (f ^ M), ← mul_comm (f ^ N), eq1] refine' mul_mem_left _ _ (mul_mem_left _ _ (sum_mem _ fun i _ => mul_mem_left _ _ _)) generalize_proofs h₁ h₂; exact (Classical.choose_spec h₂).1⟩ @@ -358,9 +358,9 @@ theorem preimage_eq (a b : A) (k : ℕ) (a_mem : a ∈ 𝒜 k) (b_mem1 : b ∈ refine' mul_mem_left _ _ (mul_mem_left _ _ (sum_mem _ fun i _ => mul_mem_left _ _ _)) generalize_proofs h₁ h₂; exact (Classical.choose_spec h₂).1 rcases y.1.isPrime.mem_or_mem this with (H1 | H3) - rcases y.1.isPrime.mem_or_mem H1 with (H1 | H2) - · exact hy2 H1 - · exact y.2 (y.1.isPrime.mem_of_pow_mem N H2) + · rcases y.1.isPrime.mem_or_mem H1 with (H1 | H2) + · exact hy2 H1 + · exact y.2 (y.1.isPrime.mem_of_pow_mem N H2) · exact y.2 (y.1.isPrime.mem_of_pow_mem M H3) #align algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.preimage_eq AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_eq @@ -524,18 +524,22 @@ theorem carrier.smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ ca let product : A⁰_ f := Mul.mul (Quotient.mk'' ⟨_, ⟨a ^ m, pow_mem_graded m ha⟩, ⟨_, ?_⟩, ⟨n, rfl⟩⟩ : A⁰_ f) (Quotient.mk'' ⟨_, ⟨proj 𝒜 (i - n) x ^ m, by mem_tac⟩, ⟨_, ?_⟩, ⟨i - n, rfl⟩⟩ : A⁰_ f) - split_ifs with h - · convert_to product ∈ q.1 - · dsimp [product] - erw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'', - HomogeneousLocalization.mul_val, HomogeneousLocalization.val_mk'', - HomogeneousLocalization.val_mk''] - simp_rw [mul_pow]; rw [Localization.mk_mul] - congr; erw [← pow_add, Nat.add_sub_of_le h] - · rw [(_ : m • n = _)]; mem_tac; simp only [smul_eq_mul, mul_comm] - · rw [(_ : m • (i - n) = _)]; mem_tac; simp only [smul_eq_mul, mul_comm] - · apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _) - · simpa only [map_zero, zero_pow hm.ne'] using zero_mem f_deg hm q i + · split_ifs with h + · convert_to product ∈ q.1 + · dsimp [product] + erw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'', + HomogeneousLocalization.mul_val, HomogeneousLocalization.val_mk'', + HomogeneousLocalization.val_mk''] + · simp_rw [mul_pow]; rw [Localization.mk_mul] + · congr; erw [← pow_add, Nat.add_sub_of_le h] + · rw [(_ : m • n = _)] + · mem_tac + · simp only [smul_eq_mul, mul_comm] + · rw [(_ : m • (i - n) = _)] + · mem_tac + · simp only [smul_eq_mul, mul_comm] + · apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _) + · simpa only [map_zero, zero_pow hm.ne'] using zero_mem f_deg hm q i · simp_rw [add_smul]; exact fun _ _ => carrier.add_mem f_deg q #align algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.smul_mem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.smul_mem diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean index b46aaea30e62a6..2f9fa600700052 100644 --- a/Mathlib/AlgebraicGeometry/Properties.lean +++ b/Mathlib/AlgebraicGeometry/Properties.lean @@ -187,8 +187,8 @@ theorem eq_zero_of_basicOpen_eq_bot {X : Scheme} [hX : IsReduced X] {U : Opens X replace hs := hs.map (SpecΓIdentity.app R).inv -- what the hell?! replace hs := @IsNilpotent.eq_zero _ _ _ _ (show _ from ?_) hs - rw [Iso.hom_inv_id_apply] at hs - rw [hs, map_zero] + · rw [Iso.hom_inv_id_apply] at hs + rw [hs, map_zero] exact @IsReduced.component_reduced _ hX ⊤ #align algebraic_geometry.eq_zero_of_basic_open_eq_bot AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot @@ -242,10 +242,10 @@ instance is_irreducible_of_isIntegral [IsIntegral X] : IrreducibleSpace X.carrie let e : X.presheaf.obj _ ≅ CommRingCat.of _ := (X.sheaf.isProductOfDisjoint ⟨_, hS.1⟩ ⟨_, hT.1⟩ ?_).conePointUniqueUpToIso (CommRingCat.prodFanIsLimit _ _) - apply (config := { allowSynthFailures := true }) false_of_nontrivial_of_product_domain - · exact e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _ - · apply X.toLocallyRingedSpace.component_nontrivial - · apply X.toLocallyRingedSpace.component_nontrivial + · apply (config := { allowSynthFailures := true }) false_of_nontrivial_of_product_domain + · exact e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _ + · apply X.toLocallyRingedSpace.component_nontrivial + · apply X.toLocallyRingedSpace.component_nontrivial · ext x constructor · rintro ⟨hS, hT⟩ diff --git a/Mathlib/AlgebraicGeometry/Pullbacks.lean b/Mathlib/AlgebraicGeometry/Pullbacks.lean index 10c5f8ecd3ed8d..a8b0b1b58616fe 100644 --- a/Mathlib/AlgebraicGeometry/Pullbacks.lean +++ b/Mathlib/AlgebraicGeometry/Pullbacks.lean @@ -59,8 +59,8 @@ def t (i j : 𝒰.J) : v 𝒰 f g i j ⟶ v 𝒰 f g j i := by refine' _ ≫ (pullbackSymmetry _ _).hom refine' _ ≫ (pullbackAssoc _ _ _ _).hom refine' pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) _ _ - rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id] - rw [Category.comp_id, Category.id_comp] + · rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id] + · rw [Category.comp_id, Category.id_comp] #align algebraic_geometry.Scheme.pullback.t AlgebraicGeometry.Scheme.Pullback.t @[simp, reassoc] @@ -105,9 +105,9 @@ theorem t_snd (i j : 𝒰.J) : t 𝒰 f g i j ≫ pullback.snd = pullback.fst theorem t_id (i : 𝒰.J) : t 𝒰 f g i i = 𝟙 _ := by apply pullback.hom_ext <;> rw [Category.id_comp] - apply pullback.hom_ext - · rw [← cancel_mono (𝒰.map i)]; simp only [pullback.condition, Category.assoc, t_fst_fst] - · simp only [Category.assoc, t_fst_snd] + · apply pullback.hom_ext + · rw [← cancel_mono (𝒰.map i)]; simp only [pullback.condition, Category.assoc, t_fst_fst] + · simp only [Category.assoc, t_fst_snd] · rw [← cancel_mono (𝒰.map i)]; simp only [pullback.condition, t_snd, Category.assoc] #align algebraic_geometry.Scheme.pullback.t_id AlgebraicGeometry.Scheme.Pullback.t_id @@ -257,7 +257,7 @@ def gluing : Scheme.GlueData.{u} where t' i j k := t' 𝒰 f g i j k t_fac i j k := by apply pullback.hom_ext - apply pullback.hom_ext + on_goal 1 => apply pullback.hom_ext all_goals simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd, Category.assoc] @@ -267,7 +267,7 @@ def gluing : Scheme.GlueData.{u} where /-- The first projection from the glued scheme into `X`. -/ def p1 : (gluing 𝒰 f g).glued ⟶ X := by fapply Multicoequalizer.desc - exact fun i => pullback.fst ≫ 𝒰.map i + · exact fun i => pullback.fst ≫ 𝒰.map i rintro ⟨i, j⟩ change pullback.fst ≫ _ ≫ 𝒰.map i = (_ ≫ _) ≫ _ ≫ 𝒰.map j -- Porting note (#11224): change `rw` to `erw` @@ -281,7 +281,7 @@ def p1 : (gluing 𝒰 f g).glued ⟶ X := by /-- The second projection from the glued scheme into `Y`. -/ def p2 : (gluing 𝒰 f g).glued ⟶ Y := by fapply Multicoequalizer.desc - exact fun i => pullback.snd + · exact fun i => pullback.snd rintro ⟨i, j⟩ change pullback.fst ≫ _ = (_ ≫ _) ≫ _ rw [Category.assoc] @@ -468,10 +468,10 @@ theorem lift_comp_ι (i : 𝒰.J) : `W` along `p1` is indeed `Uᵢ ×[X] Y`. -/ def pullbackP1Iso (i : 𝒰.J) : pullback (p1 𝒰 f g) (𝒰.map i) ≅ pullback (𝒰.map i ≫ f) g := by fconstructor - exact - pullback.lift pullback.snd (pullback.fst ≫ p2 𝒰 f g) - (by rw [← pullback.condition_assoc, Category.assoc, p_comm]) - refine' pullback.lift ((gluing 𝒰 f g).ι i) pullback.fst (by erw [Multicoequalizer.π_desc]) + · exact + pullback.lift pullback.snd (pullback.fst ≫ p2 𝒰 f g) + (by rw [← pullback.condition_assoc, Category.assoc, p_comm]) + · refine' pullback.lift ((gluing 𝒰 f g).ι i) pullback.fst (by erw [Multicoequalizer.π_desc]) · apply pullback.hom_ext · simpa using lift_comp_ι 𝒰 f g i · simp only [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp] diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean index 62ee811eb5266b..75e8510ab1ace7 100644 --- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean +++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean @@ -169,7 +169,7 @@ lemma unique_eventuallyEq_zpow_smul_nonzero {m n : ℤ} hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz exact hfz hz rw [frequently_eq_iff_eventually_eq hj_an] at this - rw [EventuallyEq.eq_of_nhds this, sub_self, zero_zpow _ (sub_ne_zero.mpr hj_ne), zero_smul] + · rw [EventuallyEq.eq_of_nhds this, sub_self, zero_zpow _ (sub_ne_zero.mpr hj_ne), zero_smul] conv => enter [2, z, 1]; rw [← Int.toNat_sub_of_le h_le, zpow_natCast] exact (((analyticAt_id _ _).sub analyticAt_const).pow _).smul hg_an diff --git a/Mathlib/Analysis/BoundedVariation.lean b/Mathlib/Analysis/BoundedVariation.lean index e0915415a96908..28239862efdaa0 100644 --- a/Mathlib/Analysis/BoundedVariation.lean +++ b/Mathlib/Analysis/BoundedVariation.lean @@ -337,16 +337,17 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ _ = (∑ i in Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) + edist (f (u N)) (f (u (N - 1))) + ∑ i in Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))) := by - congr 1; congr 1 - · apply Finset.sum_congr rfl fun i hi => ?_ - simp only [Finset.mem_Ico, zero_le', true_and_iff] at hi - dsimp only [w] - have A : i + 1 < N := Nat.lt_pred_iff.1 hi - have B : i < N := Nat.lt_of_succ_lt A - rw [if_pos A, if_pos B] - · have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos - have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A] - simp only [this, A, Finset.sum_singleton] + congr 1 + · congr 1 + · apply Finset.sum_congr rfl fun i hi => ?_ + simp only [Finset.mem_Ico, zero_le', true_and_iff] at hi + dsimp only [w] + have A : i + 1 < N := Nat.lt_pred_iff.1 hi + have B : i < N := Nat.lt_of_succ_lt A + rw [if_pos A, if_pos B] + · have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos + have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A] + simp only [this, A, Finset.sum_singleton] · apply Finset.sum_congr rfl fun i hi => ?_ rw [Finset.mem_Ico] at hi dsimp only [w] @@ -359,12 +360,13 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ _ = (∑ i in Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) + edist (f (w (N + 1))) (f (w (N - 1))) + ∑ i in Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i)) := by - congr 1; congr 1 - · dsimp only [w] - have A : ¬N + 1 < N := Nat.not_succ_lt_self - have B : N - 1 < N := Nat.pred_lt Npos.ne' - simp only [A, not_and, not_lt, Nat.succ_ne_self, Nat.add_succ_sub_one, add_zero, if_false, - B, if_true] + congr 1 + · congr 1 + · dsimp only [w] + have A : ¬N + 1 < N := Nat.not_succ_lt_self + have B : N - 1 < N := Nat.pred_lt Npos.ne' + simp only [A, not_and, not_lt, Nat.succ_ne_self, Nat.add_succ_sub_one, add_zero, + if_false, B, if_true] · exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) N n 1 _ ≤ ((∑ i in Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) + ∑ i in Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) + diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index b06dd3e2c38a81..9f7029cc70850e 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -607,19 +607,19 @@ private theorem ContDiffOn.comp_same_univ {Eu : Type u} [NormedAddCommGroup Eu] have wu : w ⊆ u := fun y hy => hy.2.1 have ws : w ⊆ s := fun y hy => hy.1 refine' ⟨w, _, fun y => (g' (f y)).comp (f' y), _, _⟩ - show w ∈ 𝓝[s] x - · apply Filter.inter_mem self_mem_nhdsWithin + · show w ∈ 𝓝[s] x + apply Filter.inter_mem self_mem_nhdsWithin apply Filter.inter_mem hu apply ContinuousWithinAt.preimage_mem_nhdsWithin' · rw [← continuousWithinAt_inter' hu] exact (hf' x xu).differentiableWithinAt.continuousWithinAt.mono (inter_subset_right _ _) · apply nhdsWithin_mono _ _ hv exact Subset.trans (image_subset_iff.mpr st) (subset_insert (f x) t) - show ∀ y ∈ w, HasFDerivWithinAt (g ∘ f) ((g' (f y)).comp (f' y)) w y - · rintro y ⟨-, yu, yv⟩ + · show ∀ y ∈ w, HasFDerivWithinAt (g ∘ f) ((g' (f y)).comp (f' y)) w y + rintro y ⟨-, yu, yv⟩ exact (hg' (f y) yv).comp y ((hf' y yu).mono wu) wv - show ContDiffOn 𝕜 n (fun y => (g' (f y)).comp (f' y)) w - · have A : ContDiffOn 𝕜 n (fun y => g' (f y)) w := + · show ContDiffOn 𝕜 n (fun y => (g' (f y)).comp (f' y)) w + have A : ContDiffOn 𝕜 n (fun y => g' (f y)) w := IH g'_diff ((hf.of_le (WithTop.coe_le_coe.2 (Nat.le_succ n))).mono ws) wv have B : ContDiffOn 𝕜 n f' w := f'_diff.mono wu have C : ContDiffOn 𝕜 n (fun y => (g' (f y), f' y)) w := A.prod B diff --git a/Mathlib/Analysis/Calculus/FDeriv/Extend.lean b/Mathlib/Analysis/Calculus/FDeriv/Extend.lean index e55e37067803ea..c75ead2ea3d734 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Extend.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Extend.lean @@ -81,10 +81,10 @@ theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : Set E} {x : exact le_of_lt (h z_in.2 z_in.1) simpa using conv.norm_image_sub_le_of_norm_fderivWithin_le' diff bound u_in v_in rintro ⟨u, v⟩ uv_in - refine' ContinuousWithinAt.closure_le uv_in _ _ key have f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y := by intro y y_in exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt + refine' ContinuousWithinAt.closure_le uv_in _ _ key all_goals -- common start for both continuity proofs have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by mono <;> exact inter_subset_right _ _ @@ -92,8 +92,8 @@ theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : Set E} {x : simpa [closure_prod_eq] using closure_mono this uv_in apply ContinuousWithinAt.mono _ this simp only [ContinuousWithinAt] - rw [nhdsWithin_prod_eq] - · have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel + · rw [nhdsWithin_prod_eq] + have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel simp only [this] exact Tendsto.comp continuous_norm.continuousAt diff --git a/Mathlib/Analysis/Complex/AbsMax.lean b/Mathlib/Analysis/Complex/AbsMax.lean index e91a75346f22bc..f72aca855c3a3d 100644 --- a/Mathlib/Analysis/Complex/AbsMax.lean +++ b/Mathlib/Analysis/Complex/AbsMax.lean @@ -125,11 +125,11 @@ theorem norm_max_aux₁ [CompleteSpace F] {f : ℂ → F} {z w : ℂ} this inequality is strict at `ζ = w`. -/ have hsub : sphere z r ⊆ closedBall z r := sphere_subset_closedBall refine' circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr _ _ ⟨w, rfl, _⟩ - show ContinuousOn (fun ζ : ℂ => (ζ - z)⁻¹ • f ζ) (sphere z r) - · refine ((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub) + · show ContinuousOn (fun ζ : ℂ => (ζ - z)⁻¹ • f ζ) (sphere z r) + refine ((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub) exact fun ζ hζ => sub_ne_zero.2 (ne_of_mem_sphere hζ hr.ne') - show ∀ ζ ∈ sphere z r, ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r - · rintro ζ (hζ : abs (ζ - z) = r) + · show ∀ ζ ∈ sphere z r, ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r + rintro ζ (hζ : abs (ζ - z) = r) rw [le_div_iff hr, norm_smul, norm_inv, norm_eq_abs, hζ, mul_comm, mul_inv_cancel_left₀ hr.ne'] exact hz (hsub hζ) show ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r diff --git a/Mathlib/Analysis/Complex/Angle.lean b/Mathlib/Analysis/Complex/Angle.lean index 2cf2509ff8c1a5..063d48f81fcec0 100644 --- a/Mathlib/Analysis/Complex/Angle.lean +++ b/Mathlib/Analysis/Complex/Angle.lean @@ -90,20 +90,20 @@ lemma norm_sub_mem_Icc_angle (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : rw [norm_eq_abs, abs_eq_one_iff'] at hx obtain ⟨θ, hθ, rfl⟩ := hx rw [angle_exp_one, exp_mul_I, add_sub_right_comm, (toIocMod_eq_self _).2] - norm_cast - rw [norm_eq_abs, abs_add_mul_I] - refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩ - · rw [mul_pow, ← _root_.abs_pow, abs_sq] - calc - _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring - _ ≤ 2 * (1 - θ.cos) := by - gcongr; exact Real.cos_quadratic_upper_bound <| abs_le.2 <| Ioc_subset_Icc_self hθ - _ = _ := by linear_combination -θ.cos_sq_add_sin_sq - · rw [Real.sqrt_le_left (by positivity), ← _root_.abs_pow, abs_sq] - calc - _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq - _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos - _ = _ := by ring + · norm_cast + rw [norm_eq_abs, abs_add_mul_I] + refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩ + · rw [mul_pow, ← _root_.abs_pow, abs_sq] + calc + _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring + _ ≤ 2 * (1 - θ.cos) := by + gcongr; exact Real.cos_quadratic_upper_bound <| abs_le.2 <| Ioc_subset_Icc_self hθ + _ = _ := by linear_combination -θ.cos_sq_add_sin_sq + · rw [Real.sqrt_le_left (by positivity), ← _root_.abs_pow, abs_sq] + calc + _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq + _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos + _ = _ := by ring · convert hθ ring diff --git a/Mathlib/Analysis/ConstantSpeed.lean b/Mathlib/Analysis/ConstantSpeed.lean index 30357c53ccadae..3eda2d4ec88794 100644 --- a/Mathlib/Analysis/ConstantSpeed.lean +++ b/Mathlib/Analysis/ConstantSpeed.lean @@ -118,11 +118,11 @@ theorem HasConstantSpeedOnWith.union {t : Set ℝ} (hfs : HasConstantSpeedOnWith · rintro (⟨ws, zw, wx⟩ | ⟨wt, xw, wy⟩) exacts [⟨Or.inl ws, zw, wx.trans (ht.2 yt)⟩, ⟨Or.inr wt, (hs.2 zs).trans xw, wy⟩] rw [this, @eVariationOn.union _ _ _ _ f _ _ x, hfs zs hs.1 (hs.2 zs), hft ht.1 yt (ht.2 yt)] - have q := ENNReal.ofReal_add (mul_nonneg l.prop (sub_nonneg.mpr (hs.2 zs))) - (mul_nonneg l.prop (sub_nonneg.mpr (ht.2 yt))) - simp only [NNReal.val_eq_coe] at q - rw [← q] - ring_nf + · have q := ENNReal.ofReal_add (mul_nonneg l.prop (sub_nonneg.mpr (hs.2 zs))) + (mul_nonneg l.prop (sub_nonneg.mpr (ht.2 yt))) + simp only [NNReal.val_eq_coe] at q + rw [← q] + ring_nf exacts [⟨⟨hs.1, hs.2 zs, le_rfl⟩, fun w ⟨_, _, wx⟩ => wx⟩, ⟨⟨ht.1, le_rfl, ht.2 yt⟩, fun w ⟨_, xw, _⟩ => xw⟩] · cases le_antisymm zy ((hs.2 ys).trans (ht.2 zt)) @@ -140,13 +140,13 @@ theorem HasConstantSpeedOnWith.union {t : Set ℝ} (hfs : HasConstantSpeedOnWith theorem HasConstantSpeedOnWith.Icc_Icc {x y z : ℝ} (hfs : HasConstantSpeedOnWith f (Icc x y) l) (hft : HasConstantSpeedOnWith f (Icc y z) l) : HasConstantSpeedOnWith f (Icc x z) l := by rcases le_total x y with (xy | yx) - rcases le_total y z with (yz | zy) - · rw [← Set.Icc_union_Icc_eq_Icc xy yz] - exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz) - · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩ - rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ← - hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu, - inf_of_le_right (vz.trans zy)] + · rcases le_total y z with (yz | zy) + · rw [← Set.Icc_union_Icc_eq_Icc xy yz] + exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz) + · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩ + rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ← + hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu, + inf_of_le_right (vz.trans zy)] · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩ rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ← hft ⟨yx.trans xu, uz⟩ ⟨yx.trans xv, vz⟩, Icc_inter_Icc, sup_of_le_right (yx.trans xu), diff --git a/Mathlib/Analysis/Convex/Cone/Pointed.lean b/Mathlib/Analysis/Convex/Cone/Pointed.lean index 035ea28699643a..290eca806ef993 100644 --- a/Mathlib/Analysis/Convex/Cone/Pointed.lean +++ b/Mathlib/Analysis/Convex/Cone/Pointed.lean @@ -70,8 +70,8 @@ def _root_.ConvexCone.toPointedCone {S : ConvexCone 𝕜 E} (hS : S.Pointed) : P convert hS simp [← hzero] · apply ConvexCone.smul_mem - convert hpos - exact hx + · convert hpos + · exact hx @[simp] lemma _root_.ConvexCone.mem_toPointedCone {S : ConvexCone 𝕜 E} (hS : S.Pointed) (x : E) : diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 7cd344d0066691..bbb0ee983fb11c 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -368,10 +368,10 @@ theorem fourierCoeff_liftIoc_eq {a : ℝ} (f : ℝ → ℂ) (n : ℤ) : fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn (lt_add_of_pos_right a hT.out) f n := by rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel_left a T] - congr 1 - refine' intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => _) - rw [liftIoc_coe_apply] - rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx + · congr 1 + refine' intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => _) + rw [liftIoc_coe_apply] + rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx #align fourier_coeff_lift_Ioc_eq fourierCoeff_liftIoc_eq theorem fourierCoeff_liftIco_eq {a : ℝ} (f : ℝ → ℂ) (n : ℤ) : diff --git a/Mathlib/Analysis/Fourier/PoissonSummation.lean b/Mathlib/Analysis/Fourier/PoissonSummation.lean index 5c0ac8b3b10ab5..ebba87516ed614 100644 --- a/Mathlib/Analysis/Fourier/PoissonSummation.lean +++ b/Mathlib/Analysis/Fourier/PoissonSummation.lean @@ -174,9 +174,9 @@ theorem isBigO_norm_Icc_restrict_atBot {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b) rintro ⟨x, hx⟩ rw [ContinuousMap.restrict_apply_mk] refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, _⟩) - rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk, - ContinuousMap.coe_mk, neg_neg] - exact ⟨by linarith [hx.2], by linarith [hx.1]⟩ + · rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk, + ContinuousMap.coe_mk, neg_neg] + exact ⟨by linarith [hx.2], by linarith [hx.1]⟩ set_option linter.uppercaseLean3 false in #align is_O_norm_Icc_restrict_at_bot isBigO_norm_Icc_restrict_atBot diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index cbbaaf46ca8fb1..b46e0d3603e523 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -99,7 +99,7 @@ theorem fourierIntegral_eq_half_sub_half_period_translate {w : V} (hw : w ≠ 0) simp_rw [smul_sub] rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ← two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul] - norm_num + · norm_num exacts [(Real.fourierIntegral_convergent_iff w).2 hf, (Real.fourierIntegral_convergent_iff w).2 (hf.comp_add_right _)] #align fourier_integral_eq_half_sub_half_period_translate fourierIntegral_eq_half_sub_half_period_translate diff --git a/Mathlib/Analysis/InnerProductSpace/Orientation.lean b/Mathlib/Analysis/InnerProductSpace/Orientation.lean index 25ac73d0ac7c79..60d9a5605f7dc0 100644 --- a/Mathlib/Analysis/InnerProductSpace/Orientation.lean +++ b/Mathlib/Analysis/InnerProductSpace/Orientation.lean @@ -292,8 +292,8 @@ theorem abs_volumeForm_apply_of_pairwise_orthogonal {v : Fin n → E} have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim v rw [o.volumeForm_robust' b, hb, Finset.abs_prod] by_cases h : ∃ i, v i = 0 - obtain ⟨i, hi⟩ := h - · rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)] <;> + · obtain ⟨i, hi⟩ := h + rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)] <;> simp [hi] push_neg at h congr diff --git a/Mathlib/Analysis/NormedSpace/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Spectrum.lean index dee055e3bdf6e6..8b495d9258443c 100644 --- a/Mathlib/Analysis/NormedSpace/Spectrum.lean +++ b/Mathlib/Analysis/NormedSpace/Spectrum.lean @@ -188,8 +188,8 @@ theorem spectralRadius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) : have hn : 0 < ((n + 1 : ℕ) : ℝ) := mod_cast Nat.succ_pos' convert monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le using 1 all_goals dsimp - rw [one_div, pow_rpow_inv_natCast] - positivity + · rw [one_div, pow_rpow_inv_natCast] + positivity rw [Nat.cast_succ, ENNReal.coe_mul_rpow] #align spectrum.spectral_radius_le_pow_nnnorm_pow_one_div spectrum.spectralRadius_le_pow_nnnorm_pow_one_div @@ -489,8 +489,8 @@ theorem exp_mem_exp [RCLike 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [Complet have h₃ : exp 𝕜 (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b := by rw [exp_eq_tsum] convert tsum_eq_zero_add (expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)) - simp only [Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, one_smul] - exact h₀.symm + · simp only [Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, one_smul] + · exact h₀.symm rw [spectrum.mem_iff, IsUnit.sub_iff, ← one_mul (↑ₐ (exp 𝕜 z)), hexpmul, ← _root_.sub_mul, Commute.isUnit_mul_iff (Algebra.commutes (exp 𝕜 z) (exp 𝕜 (a - ↑ₐ z) - 1)).symm, sub_eq_iff_eq_add'.mpr h₃, Commute.isUnit_mul_iff (h₀ ▸ h₁ : (a - ↑ₐ z) * b = b * (a - ↑ₐ z))] diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index 53af57c8d416c0..a75a7eb2fb663b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -323,7 +323,9 @@ theorem Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = Ga by_cases h : 0 ≤ 1 - s.re · apply Nat.le_of_lt_succ exact_mod_cast lt_of_le_of_lt (Nat.floor_le h) (by linarith : 1 - s.re < n + 1) - · rw [Nat.floor_of_nonpos]; omega; linarith + · rw [Nat.floor_of_nonpos] + · omega + · linarith #align complex.Gamma_eq_Gamma_aux Complex.Gamma_eq_GammaAux /-- The recurrence relation for the `Γ` function. -/ @@ -611,7 +613,8 @@ is mathematically undefined and we set it to `0` by convention). -/ theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 := by suffices ∀ {n : ℕ}, -(n : ℝ) < s → Gamma s ≠ 0 by apply this - swap; exact ⌊-s⌋₊ + 1 + swap + · exact ⌊-s⌋₊ + 1 rw [neg_lt, Nat.cast_add, Nat.cast_one] exact Nat.lt_floor_add_one _ intro n diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index eaabfefffa69a7..37cdac0311c5be 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -174,8 +174,8 @@ theorem betaIntegral_recurrence {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) : intro x hx have U : HasDerivAt (fun y : ℂ => y ^ u) (u * (x : ℂ) ^ (u - 1)) ↑x := by have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_) - simp only [id_eq, mul_one] at this - · exact this + · simp only [id_eq, mul_one] at this + exact this · rw [id_eq, ofReal_re]; exact hx.1 have V : HasDerivAt (fun y : ℂ => (1 - y) ^ v) (-v * (1 - (x : ℂ)) ^ (v - 1)) ↑x := by have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_) @@ -313,8 +313,8 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) : Tendsto (fun n : ℕ => f n x) atTop (𝓝 <| ↑(Real.exp (-x)) * (x : ℂ) ^ (s - 1)) := by intro x hx apply Tendsto.congr' - show ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x - · filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn + · show ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x + filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn rw [Nat.ceil_le] at hn dsimp only [f] rw [indicator_of_mem] diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean index a84c005d2b110e..f528650e37689c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean @@ -216,9 +216,9 @@ theorem f_add_nat_eq (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) · simp · have : x + n.succ = x + n + 1 := by push_cast; ring rw [this, hf_feq, hn] - rw [Finset.range_succ, Finset.sum_insert Finset.not_mem_range_self] - abel - linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))] + · rw [Finset.range_succ, Finset.sum_insert Finset.not_mem_range_self] + abel + · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))] #align real.bohr_mollerup.f_add_nat_eq Real.BohrMollerup.f_add_nat_eq /-- Linear upper bound for `f (x + n)` on unit interval -/ @@ -293,13 +293,13 @@ theorem tendsto_logGammaSeq_of_le_one (hf_conv : ConvexOn ℝ (Ioi 0) f) refine' tendsto_of_tendsto_of_tendsto_of_le_of_le' _ tendsto_const_nhds _ _ -- Porting note: `show` no longer reorders goals pick_goal 4 - show ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1 - · filter_upwards [eventually_ne_atTop 0] with n hn using + · show ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1 + filter_upwards [eventually_ne_atTop 0] with n hn using le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn) -- Porting note: `show` no longer reorders goals pick_goal 3 - show ∀ᶠ n : ℕ in atTop, f x - f 1 - x * (log (n + 1) - log n) ≤ logGammaSeq x n - · filter_upwards with n + · show ∀ᶠ n : ℕ in atTop, f x - f 1 - x * (log (n + 1) - log n) ≤ logGammaSeq x n + filter_upwards with n rw [sub_le_iff_le_add', sub_le_iff_le_add'] convert le_logGammaSeq hf_conv (@hf_feq) hx hx' n using 1 ring diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean index e90cdc6d11bd95..36008c1dfe7ed5 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean @@ -293,8 +293,8 @@ theorem integral_gaussian_complex {b : ℂ} (hb : 0 < re b) : · rw [← ofReal_one, ← ofReal_div] · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div] rw [← ofReal_cpow, ofReal_inj] - convert integral_gaussian (1 : ℝ) using 1 - · rw [sqrt_eq_rpow] + · convert integral_gaussian (1 : ℝ) using 1 + rw [sqrt_eq_rpow] · rw [div_one]; exact pi_pos.le · -- squares of both sides agree dsimp only [Pi.pow_apply] @@ -338,15 +338,15 @@ theorem integral_gaussian_Ioi (b : ℝ) : ∫ x in Ioi (0 : ℝ), exp (-b * x ^ 2) = √(π / b) / 2 := by rcases le_or_lt b 0 with (hb | hb) · rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div] - exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb - rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt] + · exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb + · rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt] rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal, coe_algebraMap] convert integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re) · simp · rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow] - norm_num - exact (div_pos pi_pos hb).le + · norm_num + · exact (div_pos pi_pos hb).le #align integral_gaussian_Ioi integral_gaussian_Ioi /-- The special-value formula `Γ(1/2) = √π`, which is equivalent to the Gaussian integral. -/ diff --git a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean index 64222a787d8182..35b5932ff26a30 100644 --- a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean @@ -119,9 +119,9 @@ theorem integral_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) : theorem integrableOn_Ioi_cpow_of_lt {a : ℂ} (ha : a.re < -1) {c : ℝ} (hc : 0 < c) : IntegrableOn (fun t : ℝ => (t : ℂ) ^ a) (Ioi c) := by rw [IntegrableOn, ← integrable_norm_iff, ← IntegrableOn] - refine' (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => _) measurableSet_Ioi - · dsimp only - rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos (hc.trans hx)] + · refine' (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => _) measurableSet_Ioi + · dsimp only + rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos (hc.trans hx)] · refine' ContinuousOn.aestronglyMeasurable (fun t ht => _) measurableSet_Ioi exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean index 2822b56e2a855a..b8097660db1724 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrals.lean @@ -390,7 +390,8 @@ theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a, · simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul] · -- Porting note: was `change ... with ...` have : Complex.re = RCLike.re := rfl - rw [this, ← integral_re]; rfl + rw [this, ← integral_re] + · rfl refine' intervalIntegrable_iff.mp _ cases' h' with h' h' · exact intervalIntegrable_cpow' h' @@ -652,13 +653,13 @@ theorem integral_sin_pow_aux : have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by simpa only [neg_neg] using (hasDerivAt_cos x).neg have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_ - calc - (∫ x in a..b, sin x ^ (n + 2)) = ∫ x in a..b, sin x ^ (n + 1) * sin x := by - simp only [_root_.pow_succ] - _ = C + (↑n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n := by simp [H, h, sq]; ring - _ = C + (↑n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) := by - simp [cos_sq', sub_mul, ← pow_add, add_comm] - _ = (C + (↑n + 1) * ∫ x in a..b, sin x ^ n) - (↑n + 1) * ∫ x in a..b, sin x ^ (n + 2) := by + · calc + (∫ x in a..b, sin x ^ (n + 2)) = ∫ x in a..b, sin x ^ (n + 1) * sin x := by + simp only [_root_.pow_succ] + _ = C + (↑n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n := by simp [H, h, sq]; ring + _ = C + (↑n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) := by + simp [cos_sq', sub_mul, ← pow_add, add_comm] + _ = (C + (↑n + 1) * ∫ x in a..b, sin x ^ n) - (↑n + 1) * ∫ x in a..b, sin x ^ (n + 2) := by rw [integral_sub, mul_sub, add_sub_assoc] <;> apply Continuous.intervalIntegrable <;> continuity all_goals apply Continuous.intervalIntegrable; continuity @@ -731,15 +732,15 @@ theorem integral_cos_pow_aux : simpa only [mul_right_comm, neg_mul, mul_neg] using (hasDerivAt_cos x).pow (n + 1) have hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x := fun x _ => hasDerivAt_sin x have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_ - calc - (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by - simp only [_root_.pow_succ] - _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [H, h, sq, -neg_add_rev] - _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by - simp [sin_sq, sub_mul, ← pow_add, add_comm] - _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) := by - rw [integral_sub, mul_sub, add_sub_assoc] <;> - apply Continuous.intervalIntegrable <;> continuity + · calc + (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by + simp only [_root_.pow_succ] + _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [H, h, sq, -neg_add_rev] + _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by + simp [sin_sq, sub_mul, ← pow_add, add_comm] + _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) := by + rw [integral_sub, mul_sub, add_sub_assoc] <;> + apply Continuous.intervalIntegrable <;> continuity all_goals apply Continuous.intervalIntegrable; continuity #align integral_cos_pow_aux integral_cos_pow_aux diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean index 355cbf3d40eb49..789a2e529344df 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean @@ -269,8 +269,8 @@ theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) : theorem hasSum_pow_div_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) : HasSum (fun n : ℕ => x ^ (n + 1) / (n + 1)) (-log (1 - x)) := by rw [Summable.hasSum_iff_tendsto_nat] - show Tendsto (fun n : ℕ => ∑ i : ℕ in range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x))) - · rw [tendsto_iff_norm_sub_tendsto_zero] + · show Tendsto (fun n : ℕ => ∑ i : ℕ in range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x))) + rw [tendsto_iff_norm_sub_tendsto_zero] simp only [norm_eq_abs, sub_neg_eq_add] refine' squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) _ suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by diff --git a/Mathlib/CategoryTheory/Preadditive/Schur.lean b/Mathlib/CategoryTheory/Preadditive/Schur.lean index bd427367f5c85c..ab2db4fdff78a2 100644 --- a/Mathlib/CategoryTheory/Preadditive/Schur.lean +++ b/Mathlib/CategoryTheory/Preadditive/Schur.lean @@ -206,8 +206,8 @@ open scoped Classical theorem finrank_hom_simple_simple (X Y : C) [∀ X Y : C, FiniteDimensional 𝕜 (X ⟶ Y)] [Simple X] [Simple Y] : finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0 := by split_ifs with h - exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h - exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h) + · exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h + · exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h) #align category_theory.finrank_hom_simple_simple CategoryTheory.finrank_hom_simple_simple end CategoryTheory diff --git a/Mathlib/Combinatorics/Additive/Behrend.lean b/Mathlib/Combinatorics/Additive/Behrend.lean index 5d057809d4d39a..225dd8ddf54725 100644 --- a/Mathlib/Combinatorics/Additive/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/Behrend.lean @@ -293,7 +293,7 @@ theorem log_two_mul_two_le_sqrt_log_eight : log 2 * 2 ≤ √(log 8) := by rw [mul_pow, sq (log 2), mul_assoc, mul_comm] refine' mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two) rw [← le_div_iff] - apply log_two_lt_d9.le.trans + on_goal 1 => apply log_two_lt_d9.le.trans all_goals norm_num1 #align behrend.log_two_mul_two_le_sqrt_log_eight Behrend.log_two_mul_two_le_sqrt_log_eight @@ -428,9 +428,9 @@ theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dV apply div_lt_floor _ rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv] · apply le_trans _ (div_le_div_of_nonneg_left _ _ (ceil_lt_mul _).le) - rw [mul_comm, ← div_div, div_sqrt, le_div_iff] - · set_option tactic.skipAssignedInstances false in norm_num; exact le_sqrt_log hN - · norm_num1 + · rw [mul_comm, ← div_div, div_sqrt, le_div_iff] + · set_option tactic.skipAssignedInstances false in norm_num; exact le_sqrt_log hN + · norm_num1 · apply log_nonneg rw [one_le_cast] exact hN.trans' (by norm_num1) @@ -491,8 +491,8 @@ theorem roth_lower_bound_explicit (hN : 4096 ≤ N) : theorem exp_four_lt : exp 4 < 64 := by rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1, ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff'] - exact log_two_gt_d9.trans_le' (by norm_num1) - norm_num + · exact log_two_gt_d9.trans_le' (by norm_num1) + · norm_num #align behrend.exp_four_lt Behrend.exp_four_lt theorem four_zero_nine_six_lt_exp_sixteen : 4096 < exp 16 := by diff --git a/Mathlib/Data/Complex/ExponentialBounds.lean b/Mathlib/Data/Complex/ExponentialBounds.lean index b784b59dbae00c..84126d845afabe 100644 --- a/Mathlib/Data/Complex/ExponentialBounds.lean +++ b/Mathlib/Data/Complex/ExponentialBounds.lean @@ -43,14 +43,16 @@ theorem exp_one_lt_d9 : exp 1 < 2.7182818286 := theorem exp_neg_one_gt_d9 : 0.36787944116 < exp (-1) := by rw [exp_neg, lt_inv _ (exp_pos _)] - refine' lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) _ - all_goals norm_num + · refine' lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) _ + norm_num + · norm_num #align real.exp_neg_one_gt_d9 Real.exp_neg_one_gt_d9 theorem exp_neg_one_lt_d9 : exp (-1) < 0.3678794412 := by rw [exp_neg, inv_lt (exp_pos _)] - refine' lt_of_lt_of_le _ (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2) - all_goals norm_num + · refine' lt_of_lt_of_le _ (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2) + norm_num + · norm_num #align real.exp_neg_one_lt_d9 Real.exp_neg_one_lt_d9 set_option tactic.skipAssignedInstances false in diff --git a/Mathlib/Data/Rat/Cast/Defs.lean b/Mathlib/Data/Rat/Cast/Defs.lean index ba11da9369e766..d59f0048f469ee 100644 --- a/Mathlib/Data/Rat/Cast/Defs.lean +++ b/Mathlib/Data/Rat/Cast/Defs.lean @@ -64,8 +64,8 @@ lemma cast_comm (q : ℚ≥0) (a : α) : q * a = a * q := cast_commute _ _ rw [cast_def] dsimp rw [Commute.div_eq_div_iff _ hd hb] - norm_cast - rw [e] + · norm_cast + rw [e] exact b.commute_cast _ @[norm_cast] @@ -73,8 +73,8 @@ lemma cast_add_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ↑(q + r) = (q + r : α) := by rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den, (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr] - push_cast - rfl + · push_cast + rfl · push_cast exact mul_ne_zero hq hr @@ -83,8 +83,8 @@ lemma cast_mul_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ↑(q * r) = (q * r : α) := by rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)] - push_cast - rfl + · push_cast + rfl · push_cast exact mul_ne_zero hq hr @@ -97,8 +97,8 @@ lemma cast_div_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.num : α) ≠ 0) : ↑(q / r) = (q / r : α) := by rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)] - push_cast - rfl + · push_cast + rfl · push_cast exact mul_ne_zero hq hr diff --git a/Mathlib/Data/Real/Pi/Bounds.lean b/Mathlib/Data/Real/Pi/Bounds.lean index b5e3b7b69506ed..1588eb16e270de 100644 --- a/Mathlib/Data/Real/Pi/Bounds.lean +++ b/Mathlib/Data/Real/Pi/Bounds.lean @@ -28,7 +28,10 @@ namespace Real theorem pi_gt_sqrtTwoAddSeries (n : ℕ) : (2 : ℝ) ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π := by have : √(2 - sqrtTwoAddSeries 0 n) / (2 : ℝ) * (2 : ℝ) ^ (n + 2) < π := by - rw [← lt_div_iff, ← sin_pi_over_two_pow_succ]; apply sin_lt; apply div_pos pi_pos + rw [← lt_div_iff, ← sin_pi_over_two_pow_succ] + focus + apply sin_lt + apply div_pos pi_pos all_goals apply pow_pos; norm_num apply lt_of_le_of_lt (le_of_eq _) this rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]; norm_num @@ -39,29 +42,32 @@ theorem pi_lt_sqrtTwoAddSeries (n : ℕ) : have : π < (√(2 - sqrtTwoAddSeries 0 n) / (2 : ℝ) + (1 : ℝ) / ((2 : ℝ) ^ n) ^ 3 / 4) * (2 : ℝ) ^ (n + 2) := by - rw [← div_lt_iff, ← sin_pi_over_two_pow_succ] + rw [← div_lt_iff (by norm_num), ← sin_pi_over_two_pow_succ] refine' lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _ · apply div_pos pi_pos; apply pow_pos; norm_num · rw [div_le_iff'] · refine' le_trans pi_le_four _ simp only [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, mul_one] - apply pow_le_pow_right; norm_num; apply le_add_of_nonneg_left; apply Nat.zero_le + apply pow_le_pow_right (by norm_num) + apply le_add_of_nonneg_left; apply Nat.zero_le · apply pow_pos; norm_num - apply add_le_add_left; rw [div_le_div_right] - rw [le_div_iff, ← mul_pow] + apply add_le_add_left; rw [div_le_div_right (by norm_num)] + rw [le_div_iff (by norm_num), ← mul_pow] refine' le_trans _ (le_of_eq (one_pow 3)); apply pow_le_pow_left - · apply le_of_lt; apply mul_pos; apply div_pos pi_pos; apply pow_pos; norm_num; apply pow_pos - norm_num - rw [← le_div_iff] - refine' le_trans ((div_le_div_right _).mpr pi_le_four) _; apply pow_pos; norm_num - simp only [pow_succ', ← div_div, one_div] - -- Porting note: removed `convert le_rfl` - all_goals (repeat' apply pow_pos); norm_num + · apply le_of_lt; apply mul_pos + · apply div_pos pi_pos; apply pow_pos; norm_num + · apply pow_pos; norm_num + · rw [← le_div_iff (by norm_num)] + refine' le_trans ((div_le_div_right _).mpr pi_le_four) _ + · apply pow_pos; norm_num + · simp only [pow_succ', ← div_div, one_div] + -- Porting note: removed `convert le_rfl` + norm_num apply lt_of_lt_of_le this (le_of_eq _); rw [add_mul]; congr 1 · ring simp only [show (4 : ℝ) = 2 ^ 2 by norm_num, ← pow_mul, div_div, ← pow_add] rw [one_div, one_div, inv_mul_eq_iff_eq_mul₀, eq_comm, mul_inv_eq_iff_eq_mul₀, ← pow_add] - rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n] + · rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n] all_goals norm_num #align real.pi_lt_sqrt_two_add_series Real.pi_lt_sqrtTwoAddSeries diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean index f72a8800c397ae..7ee66b6bcdfe84 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -510,11 +510,11 @@ theorem oangle_add {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : o.oangle x y + o.oangle y z = o.oangle x z := by simp_rw [oangle] rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z] - congr 1 - convert Complex.arg_real_mul _ (_ : 0 < ‖y‖ ^ 2) using 2 - · norm_cast - · have : 0 < ‖y‖ := by simpa using hy - positivity + · congr 1 + convert Complex.arg_real_mul _ (_ : 0 < ‖y‖ ^ 2) using 2 + · norm_cast + · have : 0 < ‖y‖ := by simpa using hy + positivity · exact o.kahler_ne_zero hx hy · exact o.kahler_ne_zero hy hz #align orientation.oangle_add Orientation.oangle_add diff --git a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean index a9beee9ef85de2..fc25dc4f808b45 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean @@ -199,17 +199,18 @@ theorem dist_div_cos_oangle_center_div_two_eq_radius {s : Sphere P} {p₁ p₂ : div_mul_cancel₀ _ (two_ne_zero' ℝ), @dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, vadd_vsub_assoc, add_comm, o.oangle_add_right_smul_rotation_pi_div_two, Real.Angle.cos_coe, Real.cos_arctan] - norm_cast - rw [one_div, div_inv_eq_mul, ← - mul_self_inj (mul_nonneg (norm_nonneg _) (Real.sqrt_nonneg _)) (norm_nonneg _), - norm_add_sq_eq_norm_sq_add_norm_sq_real (o.inner_smul_rotation_pi_div_two_right _ _), ← - mul_assoc, mul_comm, mul_comm _ (√_), ← mul_assoc, ← mul_assoc, - Real.mul_self_sqrt (add_nonneg zero_le_one (sq_nonneg _)), norm_smul, - LinearIsometryEquiv.norm_map] - swap; · simpa using h.symm - conv_rhs => - rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, abs_mul_abs_self] - ring + · norm_cast + rw [one_div, div_inv_eq_mul, ← + mul_self_inj (mul_nonneg (norm_nonneg _) (Real.sqrt_nonneg _)) (norm_nonneg _), + norm_add_sq_eq_norm_sq_add_norm_sq_real (o.inner_smul_rotation_pi_div_two_right _ _), ← + mul_assoc, mul_comm, mul_comm _ (√_), ← mul_assoc, ← mul_assoc, + Real.mul_self_sqrt (add_nonneg zero_le_one (sq_nonneg _)), norm_smul, + LinearIsometryEquiv.norm_map] + conv_rhs => + rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, + abs_mul_abs_self] + ring + · simpa using h.symm #align euclidean_geometry.sphere.dist_div_cos_oangle_center_div_two_eq_radius EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius /-- Given two points on a circle, twice the radius of that circle may be expressed explicitly as diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean index dda4737a25a610..bed5df183e054a 100644 --- a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean +++ b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean @@ -380,10 +380,10 @@ theorem ContMDiffOn.contMDiffOn_tangentMapWithin (hf : ContMDiffOn I I' n f s) ( rcases continuousOn_iff'.1 hf'.1 r.source r.open_source with ⟨o, o_open, ho⟩ suffices h : ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) s'_lift by refine' ⟨π E (TangentSpace I) ⁻¹' (o ∩ l.source), _, _, _⟩ - show IsOpen (π E (TangentSpace I) ⁻¹' (o ∩ l.source)); - exact (o_open.inter l.open_source).preimage (FiberBundle.continuous_proj E _) - show p ∈ π E (TangentSpace I) ⁻¹' (o ∩ l.source) - · simp only [l, preimage_inter, mem_inter_iff, mem_preimage, mem_chart_source, and_true] + · show IsOpen (π E (TangentSpace I) ⁻¹' (o ∩ l.source)); + exact (o_open.inter l.open_source).preimage (FiberBundle.continuous_proj E _) + · show p ∈ π E (TangentSpace I) ⁻¹' (o ∩ l.source) + simp only [l, preimage_inter, mem_inter_iff, mem_preimage, mem_chart_source, and_true] have : p.proj ∈ f ⁻¹' r.source ∩ s := by simp [r, hp] rw [ho] at this exact this.1 @@ -573,8 +573,8 @@ theorem tangentMap_tangentBundle_pure (p : TangentBundle I M) : rcases p with ⟨x, v⟩ have N : I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (I ((chartAt H x) x)) := by apply IsOpen.mem_nhds - apply (PartialHomeomorph.open_target _).preimage I.continuous_invFun - simp only [mfld_simps] + · apply (PartialHomeomorph.open_target _).preimage I.continuous_invFun + · simp only [mfld_simps] have A : MDifferentiableAt I I.tangent (fun x => @TotalSpace.mk M E (TangentSpace I) x 0) x := haveI : Smooth I (I.prod 𝓘(𝕜, E)) (zeroSection E (TangentSpace I : M → Type _)) := Bundle.smooth_zeroSection 𝕜 (TangentSpace I : M → Type _) diff --git a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean index c546d5bb379682..f172877b85f720 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean @@ -140,7 +140,8 @@ theorem inf_iSup_generalizedEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, suffices ∀ μ, (m μ : V) ∈ p by exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩ intro μ - by_cases hμ : μ ∈ m.support; swap; simp only [Finsupp.not_mem_support_iff.mp hμ, p.zero_mem] + by_cases hμ : μ ∈ m.support; swap + · simp only [Finsupp.not_mem_support_iff.mp hμ, p.zero_mem] have h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - algebraMap K (End K V) μ₁) ^ finrank K V) ((f - algebraMap K (End K V) μ₂) ^ finrank K V) := fun μ₁ μ₂ ↦ diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean index 950816a3c33e3a..fce33059e767b7 100644 --- a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean +++ b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean @@ -255,14 +255,14 @@ lemma rnDeriv_add_right_of_mutuallySingular {ν' : Measure α} have h₂ := rnDeriv_add' (μ.singularPart ν') (ν'.withDensity (μ.rnDeriv ν')) ν refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm have h₃ := rnDeriv_add_right_of_mutuallySingular' (?_ : μ.singularPart ν' ⟂ₘ ν') hνν' - have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 := by - refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac - exact hνν'.symm.withDensity - have h₅ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv ν =ᵐ[ν] 0 := by - rw [rnDeriv_eq_zero] - exact hνν'.symm.withDensity - filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅ - rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅] + · have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 := by + refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac + exact hνν'.symm.withDensity + have h₅ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv ν =ᵐ[ν] 0 := by + rw [rnDeriv_eq_zero] + exact hνν'.symm.withDensity + filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅ + rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅] exact mutuallySingular_singularPart μ ν' lemma rnDeriv_withDensity_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) : diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index 63e22c84d81c40..734e30079c9306 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -336,8 +336,8 @@ theorem tendsto_lintegral_norm_of_dominated_convergence {F : ℕ → α → β} calc ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by rw [← ENNReal.ofReal_add] - apply ofReal_le_ofReal - · apply norm_sub_le + · apply ofReal_le_ofReal + apply norm_sub_le · exact norm_nonneg _ · exact norm_nonneg _ _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂ diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean index c88e216b8fdcaa..826a6e88ee5efe 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean @@ -78,7 +78,7 @@ theorem norm_approxOn_y₀_le [OpensMeasurableSpace E] {f : β → E} (hf : Meas {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] (x : β) (n : ℕ) : ‖approxOn f hf s y₀ h₀ n x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖ := by have := edist_approxOn_y0_le hf h₀ x n - repeat' rw [edist_comm y₀, edist_eq_coe_nnnorm_sub] at this + repeat rw [edist_comm y₀, edist_eq_coe_nnnorm_sub] at this exact mod_cast this #align measure_theory.simple_func.norm_approx_on_y₀_le MeasureTheory.SimpleFunc.norm_approxOn_y₀_le diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean index f4e680320dc72f..594cb092211e7c 100644 --- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean @@ -234,23 +234,23 @@ theorem Memℒp.snormEssSup_indicator_norm_ge_eq_zero (hf : Memℒp f ∞ μ) have hbdd : snormEssSup f μ < ∞ := hf.snorm_lt_top refine' ⟨(snorm f ∞ μ + 1).toReal, _⟩ rw [snormEssSup_indicator_eq_snormEssSup_restrict] - have : μ.restrict { x : α | (snorm f ⊤ μ + 1).toReal ≤ ‖f x‖₊ } = 0 := by - simp only [coe_nnnorm, snorm_exponent_top, Measure.restrict_eq_zero] - have : { x : α | (snormEssSup f μ + 1).toReal ≤ ‖f x‖ } ⊆ - { x : α | snormEssSup f μ < ‖f x‖₊ } := by - intro x hx - rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne, - ENNReal.coe_toReal, coe_nnnorm] - refine' lt_of_lt_of_le _ hx - rw [ENNReal.toReal_lt_toReal hbdd.ne] - · exact ENNReal.lt_add_right hbdd.ne one_ne_zero - · exact (ENNReal.add_lt_top.2 ⟨hbdd, ENNReal.one_lt_top⟩).ne - rw [← nonpos_iff_eq_zero] - refine' (measure_mono this).trans _ - have hle := coe_nnnorm_ae_le_snormEssSup f μ - simp_rw [ae_iff, not_le] at hle - exact nonpos_iff_eq_zero.2 hle - rw [this, snormEssSup_measure_zero] + · have : μ.restrict { x : α | (snorm f ⊤ μ + 1).toReal ≤ ‖f x‖₊ } = 0 := by + simp only [coe_nnnorm, snorm_exponent_top, Measure.restrict_eq_zero] + have : { x : α | (snormEssSup f μ + 1).toReal ≤ ‖f x‖ } ⊆ + { x : α | snormEssSup f μ < ‖f x‖₊ } := by + intro x hx + rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne, + ENNReal.coe_toReal, coe_nnnorm] + refine' lt_of_lt_of_le _ hx + rw [ENNReal.toReal_lt_toReal hbdd.ne] + · exact ENNReal.lt_add_right hbdd.ne one_ne_zero + · exact (ENNReal.add_lt_top.2 ⟨hbdd, ENNReal.one_lt_top⟩).ne + rw [← nonpos_iff_eq_zero] + refine' (measure_mono this).trans _ + have hle := coe_nnnorm_ae_le_snormEssSup f μ + simp_rw [ae_iff, not_le] at hle + exact nonpos_iff_eq_zero.2 hle + rw [this, snormEssSup_measure_zero] exact measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe #align measure_theory.mem_ℒp.snorm_ess_sup_indicator_norm_ge_eq_zero MeasureTheory.Memℒp.snormEssSup_indicator_norm_ge_eq_zero @@ -284,7 +284,8 @@ theorem Memℒp.snorm_indicator_norm_ge_le (hf : Memℒp f p μ) (hmeas : Strong (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _), mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one] by_cases hx : x ∈ { x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊ } - · rw [Set.indicator_of_mem hx, Set.indicator_of_mem, Real.nnnorm_of_nonneg]; rfl + · rw [Set.indicator_of_mem hx, Set.indicator_of_mem, Real.nnnorm_of_nonneg] + · rfl rw [Set.mem_setOf_eq] rwa [← hiff] · rw [Set.indicator_of_not_mem hx, Set.indicator_of_not_mem] @@ -351,8 +352,8 @@ theorem Memℒp.snorm_indicator_le' (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf snorm_indicator_le_of_bound (f := { x | ‖f x‖ < M }.indicator f) hp_top hε (by intro x rw [norm_indicator_eq_indicator_norm, Set.indicator_apply] - split_ifs with h - exacts [h, hMpos]) + · split_ifs with h + exacts [h, hMpos]) · refine' ⟨δ, hδpos, fun s hs hμs => _⟩ rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)] · rw [snorm_indicator_eq_snorm_restrict hs] diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index 9e93e5fd8c9677..0aa5011cbaf6ca 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -1907,7 +1907,7 @@ theorem integral_countable [MeasurableSingletonClass α] (f : α → E) {s : Set have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs have hf' : Integrable (fun (x : s) => f x) (Measure.comap Subtype.val μ) := by rw [← map_comap_subtype_coe, integrable_map_measure] at hf - apply hf + · apply hf · exact Integrable.aestronglyMeasurable hf · exact Measurable.aemeasurable measurable_subtype_coe · exact Countable.measurableSet hs diff --git a/Mathlib/MeasureTheory/Integral/CircleTransform.lean b/Mathlib/MeasureTheory/Integral/CircleTransform.lean index b32739f05212b6..65d8383eb30b8d 100644 --- a/Mathlib/MeasureTheory/Integral/CircleTransform.lean +++ b/Mathlib/MeasureTheory/Integral/CircleTransform.lean @@ -76,8 +76,8 @@ theorem continuous_circleTransform {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z w : (hf : ContinuousOn f <| sphere z R) (hw : w ∈ ball z R) : Continuous (circleTransform R z w f) := by apply_rules [Continuous.smul, continuous_const] - simp_rw [deriv_circleMap] - apply_rules [Continuous.mul, continuous_circleMap 0 R, continuous_const] + · simp_rw [deriv_circleMap] + apply_rules [Continuous.mul, continuous_circleMap 0 R, continuous_const] · exact continuous_circleMap_inv hw · apply ContinuousOn.comp_continuous hf (continuous_circleMap z R) exact fun _ => (circleMap_mem_sphere _ hR.le) _ diff --git a/Mathlib/MeasureTheory/Integral/Gamma.lean b/Mathlib/MeasureTheory/Integral/Gamma.lean index 78e4045a690812..3347d2428cc2db 100644 --- a/Mathlib/MeasureTheory/Integral/Gamma.lean +++ b/Mathlib/MeasureTheory/Integral/Gamma.lean @@ -53,7 +53,7 @@ theorem integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 0 < p) (hq : - 1 _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by rw [integral_mul_left, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc, ← rpow_neg_one, ← rpow_mul, ← rpow_add] - congr; ring + · congr; ring all_goals positivity theorem integral_exp_neg_rpow {p : ℝ} (hp : 0 < p) : diff --git a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean index 2aa716b05c4585..3efbc4a5d7de93 100644 --- a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean +++ b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean @@ -816,7 +816,7 @@ theorem _root_.HasCompactSupport.integral_Ioi_deriv_eq (hf : ContDiff ℝ 1 f) (h2f : HasCompactSupport f) (b : ℝ) : ∫ x in Ioi b, deriv f x = - f b := by have := fun x (_ : x ∈ Ioi b) ↦ hf.differentiable le_rfl x |>.hasDerivAt rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub] - refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn + · refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f exact h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto @@ -1019,7 +1019,7 @@ theorem _root_.HasCompactSupport.integral_Iic_deriv_eq (hf : ContDiff ℝ 1 f) (h2f : HasCompactSupport f) (b : ℝ) : ∫ x in Iic b, deriv f x = f b := by have := fun x (_ : x ∈ Iio b) ↦ hf.differentiable le_rfl x |>.hasDerivAt rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero] - refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn + · refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f exact h2f.filter_mono _root_.atBot_le_cocompact |>.tendsto diff --git a/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean b/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean index fb1d07b989f50d..2dd76343e5ba38 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean @@ -138,8 +138,8 @@ lemma ae_ae_add_linearMap_mem_iff [LocallyCompactSpace F] {s : Set F} (hs : Meas have A : ∀ x, M x ∈ s ↔ x ∈ M ⁻¹' s := fun x ↦ Iff.rfl simp_rw [← ae_comp_linearMap_mem_iff M (ν.prod μ) ν hM hs, A] rw [Measure.ae_prod_mem_iff_ae_ae_mem] - simp only [M, mem_preimage, LinearMap.coprod_apply, LinearMap.id_coe, id_eq] - exact M_cont.measurable hs + · simp only [M, mem_preimage, LinearMap.coprod_apply, LinearMap.id_coe, id_eq] + · exact M_cont.measurable hs /-- To check that a property holds almost everywhere with respect to an additive Haar measure, it suffices to check it almost everywhere along all translates of a given vector subspace. This is an diff --git a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean index 023ebc9c58ac0e..c7557936e49ed5 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean @@ -365,12 +365,12 @@ lemma _root_.MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map intro s s_meas hs rw [map_apply meas_π s_meas] at hs ⊢ rw [Measure.restrict_apply] at hs - apply h𝓕.measure_zero_of_invariant _ _ hs - · intro γ - ext g - rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage] - congr! 1 - convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1 + · apply h𝓕.measure_zero_of_invariant _ _ hs + · intro γ + ext g + rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage] + congr! 1 + convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1 exact MeasurableSet.preimage s_meas meas_π attribute [-instance] Quotient.instMeasurableSpace diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index 503ec9d3651045..7159602d76a950 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -519,7 +519,7 @@ theorem mkMetric_apply (m : ℝ≥0∞ → ℝ≥0∞) (s : Set X) : push_neg at htr; rcases htr with ⟨n, hn⟩ refine' ENNReal.tsum_eq_top_of_eq_top ⟨n, _⟩ rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg] - exact hn.not_le + · exact hn.not_le rcases diam_pos_iff.1 ((zero_le r).trans_lt hn) with ⟨x, hx, -⟩ exact ⟨x, hx⟩ #align measure_theory.measure.mk_metric_apply MeasureTheory.Measure.mkMetric_apply @@ -799,10 +799,10 @@ theorem MeasureTheory.Measure.hausdorffMeasure_smul₀ {𝕜 E : Type*} [NormedA suffices ∀ {r : 𝕜}, r ≠ 0 → ∀ s : Set E, μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s by refine' le_antisymm (this hr s) _ rw [← le_inv_smul_iff_of_pos] - dsimp - rw [← NNReal.inv_rpow, ← nnnorm_inv] - · refine' Eq.trans_le _ (this (inv_ne_zero hr) (r • s)) - rw [inv_smul_smul₀ hr] + · dsimp + rw [← NNReal.inv_rpow, ← nnnorm_inv] + · refine' Eq.trans_le _ (this (inv_ne_zero hr) (r • s)) + rw [inv_smul_smul₀ hr] · simp [pos_iff_ne_zero, hr] intro r _ s simp only [NNReal.rpow_eq_pow, ENNReal.smul_def, ← ENNReal.coe_rpow_of_nonneg _ hd, smul_eq_mul] diff --git a/Mathlib/MeasureTheory/Measure/Tilted.lean b/Mathlib/MeasureTheory/Measure/Tilted.lean index d5570572cc0b15..e35bdb7e197e29 100644 --- a/Mathlib/MeasureTheory/Measure/Tilted.lean +++ b/Mathlib/MeasureTheory/Measure/Tilted.lean @@ -139,8 +139,8 @@ lemma isProbabilityMeasure_tilted [NeZero μ] (hf : Integrable (fun x ↦ exp (f rw [lintegral_mul_const'' _ hf.1.aemeasurable.ennreal_ofReal, ← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ fun _ ↦ (exp_pos _).le), ENNReal.mul_inv_cancel] - simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le] - · exact integral_exp_pos hf + · simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le] + exact integral_exp_pos hf · simp section lintegral diff --git a/Mathlib/NumberTheory/Bertrand.lean b/Mathlib/NumberTheory/Bertrand.lean index 347ee23e1bfbf9..e5d6822adc9129 100644 --- a/Mathlib/NumberTheory/Bertrand.lean +++ b/Mathlib/NumberTheory/Bertrand.lean @@ -69,20 +69,20 @@ theorem real_main_inequality {x : ℝ} (x_large : (512 : ℝ) ≤ x) : -- porting note (#11083): the proof was rewritten, because it was too slow have h : ConcaveOn ℝ (Set.Ioi 0.5) f := by apply ConcaveOn.sub - apply ConcaveOn.add - exact strictConcaveOn_log_Ioi.concaveOn.subset - (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5) - convert ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap - ((2 : ℝ) • LinearMap.id))) using 1 - · ext x + · apply ConcaveOn.add + · exact strictConcaveOn_log_Ioi.concaveOn.subset + (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5) + convert ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap + ((2 : ℝ) • LinearMap.id))) using 1 + ext x simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply, LinearMap.id_coe, id_eq, smul_eq_mul] rw [← mul_lt_mul_left (two_pos)] norm_num1 rfl apply ConvexOn.smul - refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1) - exact convexOn_id (convex_Ioi (0.5 : ℝ)) + · refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1) + · exact convexOn_id (convex_Ioi (0.5 : ℝ)) suffices ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0 by obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4 @@ -100,7 +100,7 @@ theorem real_main_inequality {x : ℝ} (x_large : (512 : ℝ) ≤ x) : rw [rpow_natCast, ← pow_mul, ← pow_add] conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1 rw [← rpow_mul, ← rpow_natCast] - apply rpow_le_rpow_of_exponent_le + on_goal 1 => apply rpow_le_rpow_of_exponent_le all_goals norm_num1 #align bertrand.real_main_inequality Bertrand.real_main_inequality diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 8a04f9352e2621..13007fc15441ee 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -673,8 +673,8 @@ instance [IsDomain A] [NeZero ((n : ℕ) : A)] : map_units' := fun ⟨x, hx⟩ => by rw [isUnit_iff_ne_zero] apply map_ne_zero_of_mem_nonZeroDivisors - apply adjoin_algebra_injective - exact hx + · apply adjoin_algebra_injective + · exact hx surj' x := by letI : NeZero ((n : ℕ) : K) := NeZero.nat_of_injective (IsFractionRing.injective A K) refine diff --git a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean index a00769716ca65e..9db05ca5344968 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean @@ -81,7 +81,7 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two] cases k · simp - · norm_num; simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow, + · simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow, ((even_two.mul_right _).mul_right _).neg_one_pow] · replace hp2 : (p : ℕ) ≠ 2 := by rwa [Ne, ← coe_two, PNat.coe_inj] have hpo : Odd (p : ℕ) := hp.out.odd_of_ne_two hp2 diff --git a/Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean b/Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean index deeae25da0302d..e190bd5f3287e8 100644 --- a/Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean +++ b/Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean @@ -105,7 +105,7 @@ lemma eulerMascheroniSeq'_six_lt_two_thirds : eulerMascheroniSeq' 6 < 2 / 3 := b refine lt_trans this ?_ rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat, ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast] - norm_num + · norm_num all_goals positivity lemma eulerMascheroniSeq_lt_eulerMascheroniSeq' (m n : ℕ) : @@ -127,8 +127,8 @@ noncomputable def eulerMascheroniConstant : ℝ := limUnder atTop eulerMascheron lemma tendsto_eulerMascheroniSeq : Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant) := by have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_ - rwa [eulerMascheroniConstant, this.limUnder_eq] - exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩ + · rwa [eulerMascheroniConstant, this.limUnder_eq] + · exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩ lemma tendsto_harmonic_sub_log_add_one : Tendsto (fun n : ℕ ↦ harmonic n - log (n + 1)) atTop (𝓝 eulerMascheroniConstant) := diff --git a/Mathlib/NumberTheory/KummerDedekind.lean b/Mathlib/NumberTheory/KummerDedekind.lean index fc2a6d4e93a313..a82decd893f1d5 100644 --- a/Mathlib/NumberTheory/KummerDedekind.lean +++ b/Mathlib/NumberTheory/KummerDedekind.lean @@ -140,9 +140,9 @@ theorem prod_mem_ideal_map_of_mem_conductor {p : R} {z : S} rfl refine Finset.sum_induction _ (fun u => u ∈ algebraMap R S '' I.map (algebraMap R R)) (fun a b => ?_) ?_ ?_ - rintro ⟨z, hz, rfl⟩ ⟨y, hy, rfl⟩ - rw [← RingHom.map_add] - exact ⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, rfl⟩ + · rintro ⟨z, hz, rfl⟩ ⟨y, hy, rfl⟩ + rw [← RingHom.map_add] + exact ⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, rfl⟩ · exact ⟨0, SetLike.mem_coe.mpr <| Ideal.zero_mem _, RingHom.map_zero _⟩ · intro y hy exact lem ((Finsupp.mem_supported _ l).mp H hy) @@ -217,10 +217,10 @@ noncomputable def quotAdjoinEquivQuotMap (hx : (conductor R x).comap (algebraMap from Ideal.map_comap_le) (le_refl (I.map (algebraMap R S)))) hx rw [← Ideal.mem_quotient_iff_mem_sup, hz, Ideal.mem_map_iff_of_surjective] at this - obtain ⟨u, hu, hu'⟩ := this - use ⟨u, conductor_subset_adjoin hu⟩ - simp only [← hu'] - rfl + · obtain ⟨u, hu, hu'⟩ := this + use ⟨u, conductor_subset_adjoin hu⟩ + simp only [← hu'] + rfl · exact Ideal.Quotient.mk_surjective #align quot_adjoin_equiv_quot_map quotAdjoinEquivQuotMap @@ -304,20 +304,20 @@ theorem normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map (hI : I rw [multiplicity_eq_count_normalizedFactors, multiplicity_eq_count_normalizedFactors, UniqueFactorizationMonoid.normalize_normalized_factor _ hJ, UniqueFactorizationMonoid.normalize_normalized_factor, PartENat.natCast_inj] at this - refine' this.trans _ - -- Get rid of the `map` by applying the equiv to both sides. - generalize hJ' : - (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J' - have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) = - J := - by rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk] - subst this - -- Get rid of the `attach` by applying the subtype `coe` to both sides. - rw [Multiset.count_map_eq_count' fun f => - ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f : - Ideal S), - Multiset.count_attach] - · exact Subtype.coe_injective.comp (Equiv.injective _) + · refine' this.trans _ + -- Get rid of the `map` by applying the equiv to both sides. + generalize hJ' : + (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J' + have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) = + J := + by rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk] + subst this + -- Get rid of the `attach` by applying the subtype `coe` to both sides. + rw [Multiset.count_map_eq_count' fun f => + ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f : + Ideal S), + Multiset.count_attach] + · exact Subtype.coe_injective.comp (Equiv.injective _) · exact (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop · exact irreducible_of_normalized_factor _ (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean b/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean index e75ffec1c52728..91966a5085cb5d 100644 --- a/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean +++ b/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean @@ -148,9 +148,10 @@ theorem aux_calc (n : ℕ) {m : ℝ} (hm : 2 ≤ m) : -- I solve all extraneous goals at once with `exact pow_pos (zero_lt_two.trans_le hm) _`.] -- Clear denominators and massage* apply (div_le_div_iff _ _).mpr - conv_rhs => rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul] - -- the second factors coincide, so we prove the inequality of the first factors* - refine' (mul_le_mul_right _).mpr _ + focus + conv_rhs => rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul] + -- the second factors coincide, so we prove the inequality of the first factors* + refine' (mul_le_mul_right _).mpr _ -- solve all the inequalities `0 < m ^ ??` any_goals exact pow_pos (zero_lt_two.trans_le hm) _ -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`. diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index fdc04ff3f066a6..bbf8223e7a65c3 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -661,7 +661,8 @@ lemma comap_surjective [Algebra k K] (h : Algebra.IsAlgebraic k K) : lemma mult_comap_le (f : k →+* K) (w : InfinitePlace K) : mult (w.comap f) ≤ mult w := by rw [mult, mult] split_ifs with h₁ h₂ h₂ - pick_goal 3; exact (h₁ (h₂.comap _)).elim + pick_goal 3 + · exact (h₁ (h₂.comap _)).elim all_goals decide variable [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] @@ -956,18 +957,18 @@ lemma card_isUnramified [NumberField k] [IsGalois k K] : rw [← IsGalois.card_aut_eq_finrank, Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K))) (t := (univ.filter <| IsUnramifiedIn K (k := k))), ← smul_eq_mul, ← sum_const] - refine sum_congr rfl (fun w hw ↦ ?_) - obtain ⟨w, rfl⟩ := comap_surjective (Normal.isAlgebraic' (K := K)) w - simp only [mem_univ, forall_true_left, mem_filter, true_and] at hw - trans Finset.card (MulAction.orbit (K ≃ₐ[k] K) w).toFinset - · congr; ext w' - simp only [mem_univ, forall_true_left, filter_congr_decidable, mem_filter, true_and, - Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _), and_iff_right_iff_imp] - intro e; rwa [← isUnramifiedIn_comap, ← e] - · rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w, - ← Nat.card_eq_fintype_card (α := Stab w), card_stabilizer, if_pos, - mul_one, Set.toFinset_card] - rwa [← isUnramifiedIn_comap] + · refine sum_congr rfl (fun w hw ↦ ?_) + obtain ⟨w, rfl⟩ := comap_surjective (Normal.isAlgebraic' (K := K)) w + simp only [mem_univ, forall_true_left, mem_filter, true_and] at hw + trans Finset.card (MulAction.orbit (K ≃ₐ[k] K) w).toFinset + · congr; ext w' + simp only [mem_univ, forall_true_left, filter_congr_decidable, mem_filter, true_and, + Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _), and_iff_right_iff_imp] + intro e; rwa [← isUnramifiedIn_comap, ← e] + · rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w, + ← Nat.card_eq_fintype_card (α := Stab w), card_stabilizer, if_pos, + mul_one, Set.toFinset_card] + rwa [← isUnramifiedIn_comap] · simp [isUnramifiedIn_comap] open Finset BigOperators in @@ -978,18 +979,18 @@ lemma card_isUnramified_compl [NumberField k] [IsGalois k K] : rw [← IsGalois.card_aut_eq_finrank, Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K))) (t := (univ.filter <| IsUnramifiedIn K (k := k))ᶜ), ← smul_eq_mul, ← sum_const] - refine sum_congr rfl (fun w hw ↦ ?_) - obtain ⟨w, rfl⟩ := comap_surjective (Normal.isAlgebraic' (K := K)) w - simp only [mem_univ, forall_true_left, compl_filter, not_not, mem_filter, true_and] at hw - trans Finset.card (MulAction.orbit (K ≃ₐ[k] K) w).toFinset - · congr; ext w' - simp only [compl_filter, filter_congr_decidable, mem_filter, mem_univ, true_and, - @eq_comm _ (comap w' _), Set.mem_toFinset, mem_orbit_iff, and_iff_right_iff_imp] - intro e; rwa [← isUnramifiedIn_comap, ← e] - · rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w, - ← Nat.card_eq_fintype_card (α := Stab w), InfinitePlace.card_stabilizer, if_neg, - Nat.mul_div_cancel _ zero_lt_two, Set.toFinset_card] - rwa [← isUnramifiedIn_comap] + · refine sum_congr rfl (fun w hw ↦ ?_) + obtain ⟨w, rfl⟩ := comap_surjective (Normal.isAlgebraic' (K := K)) w + simp only [mem_univ, forall_true_left, compl_filter, not_not, mem_filter, true_and] at hw + trans Finset.card (MulAction.orbit (K ≃ₐ[k] K) w).toFinset + · congr; ext w' + simp only [compl_filter, filter_congr_decidable, mem_filter, mem_univ, true_and, + @eq_comm _ (comap w' _), Set.mem_toFinset, mem_orbit_iff, and_iff_right_iff_imp] + intro e; rwa [← isUnramifiedIn_comap, ← e] + · rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w, + ← Nat.card_eq_fintype_card (α := Stab w), InfinitePlace.card_stabilizer, if_neg, + Nat.mul_div_cancel _ zero_lt_two, Set.toFinset_card] + rwa [← isUnramifiedIn_comap] · simp [isUnramifiedIn_comap] lemma card_eq_card_isUnramifiedIn [NumberField k] [IsGalois k K] : diff --git a/Mathlib/NumberTheory/ZetaValues.lean b/Mathlib/NumberTheory/ZetaValues.lean index 4cc35523b68522..677e7d3ab40299 100644 --- a/Mathlib/NumberTheory/ZetaValues.lean +++ b/Mathlib/NumberTheory/ZetaValues.lean @@ -217,11 +217,11 @@ theorem hasSum_one_div_pow_mul_fourier_mul_bernoulliFun {k : ℕ} (hk : 2 ≤ k) ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y simp_rw [step1] at step2 convert step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n - rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ), - ← div_div, div_self] - · rw [Ne, pow_eq_zero_iff', not_and_or] - exact Or.inl two_pi_I_ne_zero - · exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _) + · rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ), + ← div_div, div_self] + · rw [Ne, pow_eq_zero_iff', not_and_or] + exact Or.inl two_pi_I_ne_zero + · exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _) · rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli, AddCircle.liftIco_coe_apply (show y ∈ Ico 0 (0 + 1) by rwa [zero_add])] #align has_sum_one_div_pow_mul_fourier_mul_bernoulli_fun hasSum_one_div_pow_mul_fourier_mul_bernoulliFun @@ -361,7 +361,8 @@ theorem hasSum_zeta_two : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) (π theorem hasSum_zeta_four : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 4) (π ^ 4 / 90) := by convert hasSum_zeta_nat two_ne_zero using 1; norm_num rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four] - norm_num [Nat.factorial]; field_simp; ring; decide + · norm_num [Nat.factorial]; field_simp; ring + · decide #align has_sum_zeta_four hasSum_zeta_four theorem Polynomial.bernoulli_three_eval_one_quarter : @@ -392,7 +393,9 @@ theorem hasSum_L_function_mod_four_eval_three : rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3), Polynomial.bernoulli_three_eval_one_quarter] norm_num [Nat.factorial]; field_simp; ring - · rw [mem_Icc]; constructor; linarith; linarith + · rw [mem_Icc]; constructor + · linarith + · linarith set_option linter.uppercaseLean3 false in #align has_sum_L_function_mod_four_eval_three hasSum_L_function_mod_four_eval_three diff --git a/Mathlib/Probability/Distributions/Exponential.lean b/Mathlib/Probability/Distributions/Exponential.lean index e080e5e42c6616..e67d27882572ce 100644 --- a/Mathlib/Probability/Distributions/Exponential.lean +++ b/Mathlib/Probability/Distributions/Exponential.lean @@ -140,21 +140,21 @@ lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) : (by intro a ⟨(hle : _ ≤ a), _⟩; rw [if_pos hle]))] rw [← ENNReal.toReal_eq_toReal _ ENNReal.ofReal_ne_top, ← integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun _ ↦ le_of_lt (mul_pos hr (exp_pos _)))] - have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in (0)..x, r * rexp (-(r * a)) := by - rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul] - rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this] - rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h - (f := fun a ↦ -1 * rexp (-(r * a))) _ _] - rw [ENNReal.toReal_ofReal_eq_iff.2 - (by set_option tactic.skipAssignedInstances false in norm_num; positivity)] - · norm_num; ring - · simp only [intervalIntegrable_iff, uIoc_of_le h] - exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _ - · have : Continuous (fun a ↦ rexp (-(r * a))) := by - simp only [← neg_mul]; exact (continuous_mul_left (-r)).exp - exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this) - · simp only [neg_mul, one_mul] - exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp + · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in (0)..x, r * rexp (-(r * a)) := by + rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul] + rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this] + rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h + (f := fun a ↦ -1 * rexp (-(r * a))) _ _] + · rw [ENNReal.toReal_ofReal_eq_iff.2 + (by set_option tactic.skipAssignedInstances false in norm_num; positivity)] + · norm_num; ring + · simp only [intervalIntegrable_iff, uIoc_of_le h] + exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _ + · have : Continuous (fun a ↦ rexp (-(r * a))) := by + simp only [← neg_mul]; exact (continuous_mul_left (-r)).exp + exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this) + · simp only [neg_mul, one_mul] + exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp · apply Integrable.aestronglyMeasurable (Integrable.const_mul _ _) rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc] exact exp_neg_integrableOn_Ioc hr diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean index dcf300bcb21e69..9524202aa9c6d5 100644 --- a/Mathlib/Probability/Kernel/Basic.lean +++ b/Mathlib/Probability/Kernel/Basic.lean @@ -296,7 +296,10 @@ class _root_.ProbabilityTheory.IsSFiniteKernel (κ : kernel α β) : Prop where instance (priority := 100) IsFiniteKernel.isSFiniteKernel [h : IsFiniteKernel κ] : IsSFiniteKernel κ := - ⟨⟨fun n => if n = 0 then κ else 0, fun n => by simp only; split_ifs; exact h; infer_instance, by + ⟨⟨fun n => if n = 0 then κ else 0, fun n => by + simp only; split_ifs + · exact h + · infer_instance, by ext a s hs rw [kernel.sum_apply' _ _ hs] have : (fun i => ((ite (i = 0) κ 0) a) s) = fun i => ite (i = 0) (κ a s) 0 := by diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index b4c0dbddbaef89..43cb16faff4c02 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -361,12 +361,14 @@ theorem compProd_restrict {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : theorem compProd_restrict_left {s : Set β} (hs : MeasurableSet s) : kernel.restrict κ hs ⊗ₖ η = kernel.restrict (κ ⊗ₖ η) (hs.prod MeasurableSet.univ) := by - rw [← compProd_restrict]; congr; exact kernel.restrict_univ.symm + rw [← compProd_restrict] + · congr; exact kernel.restrict_univ.symm #align probability_theory.kernel.comp_prod_restrict_left ProbabilityTheory.kernel.compProd_restrict_left theorem compProd_restrict_right {t : Set γ} (ht : MeasurableSet t) : κ ⊗ₖ kernel.restrict η ht = kernel.restrict (κ ⊗ₖ η) (MeasurableSet.univ.prod ht) := by - rw [← compProd_restrict]; congr; exact kernel.restrict_univ.symm + rw [← compProd_restrict] + · congr; exact kernel.restrict_univ.symm #align probability_theory.kernel.comp_prod_restrict_right ProbabilityTheory.kernel.compProd_restrict_right end Restrict diff --git a/Mathlib/Probability/Kernel/RadonNikodym.lean b/Mathlib/Probability/Kernel/RadonNikodym.lean index 9806bcd609578c..fcfa1e6a6223d8 100644 --- a/Mathlib/Probability/Kernel/RadonNikodym.lean +++ b/Mathlib/Probability/Kernel/RadonNikodym.lean @@ -115,7 +115,8 @@ lemma withDensity_rnDerivAux (κ η : kernel α γ) [IsFiniteKernel κ] [IsFinit withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)) = κ := by ext a s hs rw [kernel.withDensity_apply'] - swap; exact (measurable_rnDerivAux _ _).ennreal_ofReal + swap + · exact (measurable_rnDerivAux _ _).ennreal_ofReal have : ∀ b, (Real.toNNReal b : ℝ≥0∞) = ENNReal.ofReal b := fun _ ↦ rfl simp_rw [this] exact set_lintegral_rnDerivAux κ η a hs diff --git a/Mathlib/Probability/Martingale/Convergence.lean b/Mathlib/Probability/Martingale/Convergence.lean index bd042eec57061b..a9427d73c4cc4d 100644 --- a/Mathlib/Probability/Martingale/Convergence.lean +++ b/Mathlib/Probability/Martingale/Convergence.lean @@ -173,10 +173,10 @@ theorem Submartingale.upcrossings_ae_lt_top' [IsFiniteMeasure μ] (hf : Submarti fun n => le_trans _ (hR' n)⟩) refine' lintegral_mono fun ω => _ rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm] - by_cases hnonneg : 0 ≤ f n ω - a - · rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg] - · rw [posPart_eq_zero.2 (not_le.1 hnonneg).le] - exact norm_nonneg _ + · by_cases hnonneg : 0 ≤ f n ω - a + · rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg] + · rw [posPart_eq_zero.2 (not_le.1 hnonneg).le] + exact norm_nonneg _ · simp only [Ne, ENNReal.coe_ne_top, not_false_iff] · simp only [hab, Ne, ENNReal.ofReal_eq_zero, sub_nonpos, not_le] · simp only [hab, Ne, ENNReal.ofReal_eq_zero, sub_nonpos, not_le, true_or_iff] diff --git a/Mathlib/Probability/Martingale/Upcrossing.lean b/Mathlib/Probability/Martingale/Upcrossing.lean index 85d58930a0f5e8..584ef9bdf4315c 100644 --- a/Mathlib/Probability/Martingale/Upcrossing.lean +++ b/Mathlib/Probability/Martingale/Upcrossing.lean @@ -498,16 +498,18 @@ theorem crossing_eq_crossing_of_lowerCrossingTime_lt {M : ℕ} (hNM : N ≤ M) lowerCrossingTime_zero, true_and_iff, eq_comm] refine' hitting_eq_hitting_of_exists hNM _ rw [lowerCrossingTime, hitting_lt_iff] at h - obtain ⟨j, hj₁, hj₂⟩ := h - exacts [⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl] + · obtain ⟨j, hj₁, hj₂⟩ := h + exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩ + · exact le_rfl · specialize ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h) (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h') have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω := by rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h' - simp only [upperCrossingTime_succ_eq] - obtain ⟨j, hj₁, hj₂⟩ := h' - rw [eq_comm, ih.2] - exacts [hitting_eq_hitting_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl] + · simp only [upperCrossingTime_succ_eq] + obtain ⟨j, hj₁, hj₂⟩ := h' + rw [eq_comm, ih.2] + exact hitting_eq_hitting_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩ + · exact le_rfl refine' ⟨this, _⟩ simp only [lowerCrossingTime, eq_comm, this] refine' hitting_eq_hitting_of_exists hNM _ @@ -526,8 +528,9 @@ theorem crossing_eq_crossing_of_upperCrossingTime_lt {M : ℕ} (hNM : N ≤ M) rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this] refine' hitting_eq_hitting_of_exists hNM _ rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h - obtain ⟨j, hj₁, hj₂⟩ := h - exacts [⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl] + · obtain ⟨j, hj₁, hj₂⟩ := h + exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩ + · exact le_rfl #align measure_theory.crossing_eq_crossing_of_upper_crossing_time_lt MeasureTheory.crossing_eq_crossing_of_upperCrossingTime_lt theorem upperCrossingTime_eq_upperCrossingTime_of_lt {M : ℕ} (hNM : N ≤ M) diff --git a/Mathlib/Probability/Process/Filtration.lean b/Mathlib/Probability/Process/Filtration.lean index 63bc542af7417c..6a2df726b9551b 100644 --- a/Mathlib/Probability/Process/Filtration.lean +++ b/Mathlib/Probability/Process/Filtration.lean @@ -299,10 +299,10 @@ theorem filtrationOfSet_eq_natural [MulZeroOneClass β] [Nontrivial β] {s : ι refine' generateFrom_le _ rintro t ⟨hn, u, _, hu'⟩ obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β) - pick_goal 4; rw [Set.mem_singleton_iff] at heq + on_goal 4 => rw [Set.mem_singleton_iff] at heq all_goals rw [heq] at hu'; rw [← hu'] - exacts [measurableSet_empty _, MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩, - MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩)] + exacts [MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩, + MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩), measurableSet_empty _] #align measure_theory.filtration.filtration_of_set_eq_natural MeasureTheory.Filtration.filtrationOfSet_eq_natural end diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean index a61fcfdff9edba..5f2d924a91708e 100644 --- a/Mathlib/Probability/Process/Stopping.lean +++ b/Mathlib/Probability/Process/Stopping.lean @@ -1207,7 +1207,8 @@ theorem condexp_min_stopping_time_ae_eq_restrict_le [MeasurableSpace ι] [Second have : SigmaFinite (μ.trim hτ.measurableSpace_le) := haveI h_le : (hτ.min hσ).measurableSpace ≤ hτ.measurableSpace := by rw [IsStoppingTime.measurableSpace_min] - exact inf_le_left; simp_all only + · exact inf_le_left + · simp_all only sigmaFiniteTrim_mono _ h_le refine' (condexp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => _).symm diff --git a/Mathlib/Probability/Variance.lean b/Mathlib/Probability/Variance.lean index 44e65d8e4ca07b..2109e0867211b3 100644 --- a/Mathlib/Probability/Variance.lean +++ b/Mathlib/Probability/Variance.lean @@ -221,12 +221,12 @@ theorem variance_le_expectation_sq [@IsProbabilityMeasure Ω _ ℙ] {X : Ω → · rw [variance_def' hX] simp only [sq_nonneg, sub_le_self_iff] rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae] - by_cases hint : Integrable X; swap - · simp only [integral_undef hint, Pi.pow_apply, Pi.sub_apply, sub_zero] - exact le_rfl - · rw [integral_undef] - · exact integral_nonneg fun a => sq_nonneg _ - · intro h + · by_cases hint : Integrable X; swap + · simp only [integral_undef hint, Pi.pow_apply, Pi.sub_apply, sub_zero] + exact le_rfl + · rw [integral_undef] + · exact integral_nonneg fun a => sq_nonneg _ + intro h have A : Memℒp (X - fun ω : Ω => 𝔼[X]) 2 ℙ := (memℒp_two_iff_integrable_sq (hint.aestronglyMeasurable.sub aestronglyMeasurable_const)).2 h have B : Memℒp (fun _ : Ω => 𝔼[X]) 2 ℙ := memℒp_const _ diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean index a8f4fda6949b54..94e1f9f6ffbdc9 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean @@ -380,14 +380,14 @@ theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1) -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [diagonalSucc_hom_single] erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index] - simp only [one_smul] - erw [Representation.linHom_apply] - simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply] - erw [Finsupp.llift_apply] - rw [Finsupp.lift_apply] - erw [Finsupp.sum_single_index] - rw [one_smul] - · rw [zero_smul] + · simp only [one_smul] + erw [Representation.linHom_apply] + simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply] + erw [Finsupp.llift_apply] + rw [Finsupp.lift_apply] + erw [Finsupp.sum_single_index] + · rw [one_smul] + · rw [zero_smul] · rw [zero_smul] set_option linter.uppercaseLean3 false in #align Rep.diagonal_hom_equiv_symm_apply Rep.diagonalHomEquiv_symm_apply diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean index a4fc84cfab1603..21580ea3399b98 100644 --- a/Mathlib/RepresentationTheory/Rep.lean +++ b/Mathlib/RepresentationTheory/Rep.lean @@ -373,9 +373,9 @@ noncomputable def leftRegularHomEquiv (A : Rep k G) : (Rep.ofMulAction k G G ⟶ simp only [LinearMap.comp_apply, Finsupp.lsingle_apply, leftRegularHom_hom] erw [Finsupp.lift_apply] rw [Finsupp.sum_single_index, ← this, of_ρ_apply] - erw [Representation.ofMulAction_single x (1 : G) (1 : k)] - simp only [one_smul, smul_eq_mul, mul_one] - · -- This goal didn't exist before leanprover/lean4#2644 + · erw [Representation.ofMulAction_single x (1 : G) (1 : k)] + simp only [one_smul, smul_eq_mul, mul_one] + -- This goal didn't exist before leanprover/lean4#2644 rfl · rw [zero_smul] right_inv x := leftRegularHom_apply x diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean index 5cfc21b0b89557..3e4acbc3e01e77 100644 --- a/Mathlib/RingTheory/DedekindDomain/Different.lean +++ b/Mathlib/RingTheory/DedekindDomain/Different.lean @@ -318,8 +318,8 @@ variable {I} lemma dual_div_dual : dual A K J / dual A K I = I / J := by rw [dual_eq_mul_inv A K J, dual_eq_mul_inv A K I, mul_div_mul_comm, div_self, one_mul] - exact inv_div_inv J I - simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true] + · exact inv_div_inv J I + · simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true] lemma dual_mul_self : dual A K I * I = dual A K 1 := by @@ -385,7 +385,7 @@ lemma coeSubmodule_differentIdeal_fractionRing simp only [← one_div, FractionalIdeal.val_eq_coe] at this rw [FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _), FractionalIdeal.coe_dual] at this - simpa only [FractionalIdeal.coe_one] using this + · simpa only [FractionalIdeal.coe_one] using this · exact one_ne_zero · exact one_ne_zero @@ -479,7 +479,8 @@ lemma traceForm_dualSubmodule_adjoin · rintro _ ⟨i, rfl⟩ by_cases hi : i < pb.dim · exact Submodule.subset_span ⟨⟨i, hi⟩, rfl⟩ - · rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero]; exact zero_mem _ + · rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero] + · exact zero_mem _ rw [← pb.natDegree_minpoly, pbgen, ← natDegree_minpolyDiv_succ hKx, ← Nat.succ_eq_add_one] at hi exact le_of_not_lt hi @@ -497,7 +498,8 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton] rw [coeIdeal_differentIdeal A K L B, mul_inv_eq_iff_eq_mul₀] - swap; exact FractionalIdeal.dual_ne_zero A K one_ne_zero + swap + · exact FractionalIdeal.dual_ne_zero A K one_ne_zero apply FractionalIdeal.coeToSubmodule_injective simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul, FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_mul] @@ -509,7 +511,8 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁ rw [Submodule.mem_smul_iff_inv_mul_mem this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual, mem_coeSubmodule_conductor] - swap; exact one_ne_zero + swap + · exact one_ne_zero have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 := by rwa [ne_eq, inv_eq_zero] have : IsIntegral A (algebraMap B L x) := IsIntegral.map (IsScalarTower.toAlgHom A B L) hAx diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean index 8e579b803a7908..cc2179dd14a74c 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean @@ -75,7 +75,9 @@ theorem inv_nonzero {J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) : theorem coe_inv_of_nonzero {J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) : (↑J⁻¹ : Submodule R₁ K) = IsLocalization.coeSubmodule K ⊤ / (J : Submodule R₁ K) := by - rw [inv_nonzero]; rfl; assumption + rw [inv_nonzero] + · rfl + · assumption #align fractional_ideal.coe_inv_of_nonzero FractionalIdeal.coe_inv_of_nonzero variable {K} diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index 23524a76eb14fc..92788345621d59 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -127,13 +127,13 @@ theorem exists_integral_multiples (s : Finset L) : have := exists_integral_multiple ((IsFractionRing.isAlgebraic_iff A K L).mpr (.of_finite _ x)) ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_) - rcases this with ⟨x', y', hy', hx'⟩ - refine' ⟨y * y', mul_ne_zero hy hy', fun x'' hx'' => _⟩ - rcases Finset.mem_insert.mp hx'' with (rfl | hx'') - · rw [mul_smul, Algebra.smul_def, Algebra.smul_def, mul_comm _ x'', hx'] - exact isIntegral_algebraMap.mul x'.2 - · rw [mul_comm, mul_smul, Algebra.smul_def] - exact isIntegral_algebraMap.mul (hs _ hx'') + · rcases this with ⟨x', y', hy', hx'⟩ + refine' ⟨y * y', mul_ne_zero hy hy', fun x'' hx'' => _⟩ + rcases Finset.mem_insert.mp hx'' with (rfl | hx'') + · rw [mul_smul, Algebra.smul_def, Algebra.smul_def, mul_comm _ x'', hx'] + exact isIntegral_algebraMap.mul x'.2 + · rw [mul_comm, mul_smul, Algebra.smul_def] + exact isIntegral_algebraMap.mul (hs _ hx'') · rw [IsScalarTower.algebraMap_eq A K L] apply (algebraMap K L).injective.comp exact IsFractionRing.injective _ _ diff --git a/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean b/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean index ffc5ff1279652a..c93532d0cd5261 100644 --- a/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean +++ b/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean @@ -97,7 +97,7 @@ theorem valuationOfNeZeroToFun_eq (x : Kˣ) : change _ = ite _ _ _ * (ite _ _ _)⁻¹ rw [IsLocalization.toLocalizationMap_sec] rw [if_neg <| IsLocalization.sec_fst_ne_zero le_rfl x.ne_zero, if_neg ?_] - rfl + · rfl exact nonZeroDivisors.coe_ne_zero _ #align is_dedekind_domain.height_one_spectrum.valuation_of_ne_zero_to_fun_eq IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq diff --git a/Mathlib/RingTheory/Nilpotent/Basic.lean b/Mathlib/RingTheory/Nilpotent/Basic.lean index fc0b92c31213db..aeb24bf2137605 100644 --- a/Mathlib/RingTheory/Nilpotent/Basic.lean +++ b/Mathlib/RingTheory/Nilpotent/Basic.lean @@ -122,7 +122,7 @@ theorem add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero {m n k : ℕ} rintro ⟨i, j⟩ hij suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero] by_cases hi : m ≤ i - rw [pow_eq_zero_of_le hi hx, zero_mul] + · rw [pow_eq_zero_of_le hi hx, zero_mul] rw [pow_eq_zero_of_le ?_ hy, mul_zero] linarith [Finset.mem_antidiagonal.mp hij] diff --git a/Mathlib/RingTheory/Norm.lean b/Mathlib/RingTheory/Norm.lean index 95d48fe6a89173..ed47c1c034c50a 100644 --- a/Mathlib/RingTheory/Norm.lean +++ b/Mathlib/RingTheory/Norm.lean @@ -153,7 +153,7 @@ theorem norm_zero [Nontrivial S] [Module.Free R S] [Module.Finite R S] : norm R theorem norm_eq_zero_iff [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] {x : S} : norm R x = 0 ↔ x = 0 := by constructor - let b := Module.Free.chooseBasis R S + on_goal 1 => let b := Module.Free.chooseBasis R S swap · rintro rfl; exact norm_zero · letI := Classical.decEq (Module.Free.ChooseBasisIndex R S) @@ -252,10 +252,10 @@ theorem norm_eq_prod_embeddings_gen [Algebra R F] (pb : PowerBasis R S) rw [PowerBasis.norm_gen_eq_prod_roots pb hE] rw [@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv' (fun σ => σ pb.gen) (fun x => x) ?_] - rw [Finset.prod_mem_multiset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val, - Multiset.dedup_eq_self.mpr, Multiset.map_id] - · exact nodup_roots hfx.map - · intro x; rfl + · rw [Finset.prod_mem_multiset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val, + Multiset.dedup_eq_self.mpr, Multiset.map_id] + · exact nodup_roots hfx.map + · intro x; rfl · intro σ; simp only [PowerBasis.liftEquiv'_apply_coe] #align algebra.norm_eq_prod_embeddings_gen Algebra.norm_eq_prod_embeddings_gen @@ -274,11 +274,10 @@ theorem prod_embeddings_eq_finrank_pow [Algebra L F] [IsScalarTower K L F] [IsAl haveI : FiniteDimensional L F := FiniteDimensional.right K L F haveI : IsSeparable L F := isSeparable_tower_top_of_isSeparable K L F letI : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb - letI : ∀ f : L →ₐ[K] E, Fintype (@AlgHom L F E _ _ _ _ f.toRingHom.toAlgebra) := ?_ rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen, ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow] - refine Finset.prod_congr rfl fun σ _ => ?_ - · letI : Algebra L E := σ.toRingHom.toAlgebra + · refine Finset.prod_congr rfl fun σ _ => ?_ + letI : Algebra L E := σ.toRingHom.toAlgebra simp_rw [Finset.prod_const] congr exact AlgHom.card L F E @@ -308,8 +307,8 @@ theorem norm_eq_prod_automorphisms [FiniteDimensional K L] [IsGalois K L] (x : L rw [map_prod (algebraMap L (AlgebraicClosure L))] rw [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)] · rw [← norm_eq_prod_embeddings] - simp only [algebraMap_eq_smul_one, smul_one_smul] - rfl + · simp only [algebraMap_eq_smul_one, smul_one_smul] + rfl · intro σ simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk, AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, id.map_eq_id, RingHom.id_apply] @@ -355,10 +354,10 @@ lemma norm_eq_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [Ring (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) (x) : Algebra.norm A₁ x = e₁.symm (Algebra.norm A₂ (e₂ x)) := by letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra' ?_ - let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl } - rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e', - RingEquiv.symm_apply_apply] - rfl + · let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl } + rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e', + RingEquiv.symm_apply_apply] + rfl intros c x apply e₂.symm.injective simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, _root_.map_mul, diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index d28203799b9098..204915fff2e64a 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -155,18 +155,18 @@ theorem eval_one_cyclotomic_not_prime_pow {R : Type*} [Ring R] {n : ℕ} apply_fun eval 1 at this rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ← Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _, Finset.prod_image] at this - simp_rw [eval_one_cyclotomic_prime_pow, Finset.prod_const, Finset.card_range, mul_comm] at this - rw [← Finset.prod_sdiff <| show {n} ⊆ _ from _] at this - swap - · simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne, mem_divisors, dvd_refl, - true_and_iff, mem_image, mem_range, exists_prop, not_exists, not_and] - exact ⟨⟨hn.ne', hn'.ne'⟩, fun t _ => h hp _⟩ - rw [← Int.natAbs_ofNat p, Int.natAbs_dvd_natAbs] at hpe - obtain ⟨t, ht⟩ := hpe - rw [Finset.prod_singleton, ht, mul_left_comm, mul_comm, ← mul_assoc, mul_assoc] at this - have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩ - simp only [← _root_.pow_succ, ← Int.natAbs_dvd_natAbs, Int.natAbs_ofNat, Int.natAbs_pow] at this - exact pow_succ_padicValNat_not_dvd hn'.ne' this + · simp_rw [eval_one_cyclotomic_prime_pow, Finset.prod_const, Finset.card_range, mul_comm] at this + rw [← Finset.prod_sdiff <| show {n} ⊆ _ from _] at this + swap + · simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne, mem_divisors, dvd_refl, + true_and_iff, mem_image, mem_range, exists_prop, not_exists, not_and] + exact ⟨⟨hn.ne', hn'.ne'⟩, fun t _ => h hp _⟩ + rw [← Int.natAbs_ofNat p, Int.natAbs_dvd_natAbs] at hpe + obtain ⟨t, ht⟩ := hpe + rw [Finset.prod_singleton, ht, mul_left_comm, mul_comm, ← mul_assoc, mul_assoc] at this + have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩ + simp only [← _root_.pow_succ, ← Int.natAbs_dvd_natAbs, Int.natAbs_ofNat, Int.natAbs_pow] at this + exact pow_succ_padicValNat_not_dvd hn'.ne' this · rintro x - y - hxy apply Nat.succ_injective exact Nat.pow_right_injective hp.two_le hxy @@ -260,9 +260,9 @@ theorem cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ rintro rfl exact hn.ne' (hζ.unique IsPrimitiveRoot.zero) have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩ - rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this - rw [this] at hζ - linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm] + · rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this + rw [this] at hζ + linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm] · contrapose! hζ₀ apply Complex.ext <;> simp [hζ₀, h.2] have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean index ea36864e5729d0..4b719fdf6bb32d 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean @@ -156,9 +156,9 @@ theorem cyclotomic_mul_prime_pow_eq (R : Type*) {p m : ℕ} [Fact (Nat.Prime p)] have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ']⟩ rw [pow_succ', mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv, cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ← pow_mul] - congr 1 - simp only [tsub_zero, Nat.succ_sub_succ_eq_sub] - rwa [Nat.mul_sub_right_distrib, mul_comm, pow_succ] + · simp only [tsub_zero, Nat.succ_sub_succ_eq_sub] + rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ] + · assumption #align polynomial.cyclotomic_mul_prime_pow_eq Polynomial.cyclotomic_mul_prime_pow_eq /-- If `R` is of characteristic `p` and `¬p ∣ m`, then `ζ` is a root of `cyclotomic (p ^ k * m) R` diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean index 764b1dc2df8277..b57400a84dfb47 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean @@ -272,7 +272,7 @@ theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis exact dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt hp hBint hQ hzint hei · intro hj convert hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd _ hndiv - exact n + · exact n -- Two technical results we will need about `P.natDegree` and `Q.natDegree`. have H := degree_modByMonic_lt Q₁ (minpoly.monic hBint) rw [← hQ₁, ← hP] at H diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean b/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean index 7cd35c359ac5d3..abd104558a3e7d 100644 --- a/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean +++ b/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean @@ -50,7 +50,7 @@ theorem deriv_gaussian_eq_hermite_mul_gaussian (n : ℕ) (x : ℝ) : rw [deriv_exp (by simp)]; simp; ring rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_mul, pow_succ (-1 : ℝ), deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval] - ring + · ring · apply Polynomial.differentiable_aeval · apply DifferentiableAt.exp; simp -- Porting note: was just `simp` #align polynomial.deriv_gaussian_eq_hermite_mul_gaussian Polynomial.deriv_gaussian_eq_hermite_mul_gaussian diff --git a/Mathlib/RingTheory/Polynomial/Selmer.lean b/Mathlib/RingTheory/Polynomial/Selmer.lean index 8907a4673d5646..cd41ad3bceff32 100644 --- a/Mathlib/RingTheory/Polynomial/Selmer.lean +++ b/Mathlib/RingTheory/Polynomial/Selmer.lean @@ -56,7 +56,7 @@ theorem X_pow_sub_X_sub_one_irreducible (hn1 : n ≠ 1) : Irreducible (X ^ n - X rw [hp] apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩ rintro z ⟨h1, h2⟩ - apply X_pow_sub_X_sub_one_irreducible_aux z + apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2 simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C, Units.val_neg, Units.val_one, map_neg, map_one] at h1 h2 diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean index 137796f0ff0804..6152d9aa25897b 100644 --- a/Mathlib/RingTheory/Trace.lean +++ b/Mathlib/RingTheory/Trace.lean @@ -395,18 +395,18 @@ theorem sum_embeddings_eq_finrank_mul [FiniteDimensional K F] [IsSeparable K F] haveI : IsSeparable L F := isSeparable_tower_top_of_isSeparable K L F letI : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb letI : ∀ f : L →ₐ[K] E, Fintype (haveI := f.toRingHom.toAlgebra; AlgHom L F E) := ?_ - rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen, ← - Finset.univ_sigma_univ, Finset.sum_sigma, ← Finset.sum_nsmul] - refine' Finset.sum_congr rfl fun σ _ => _ - · letI : Algebra L E := σ.toRingHom.toAlgebra - -- Porting note: `Finset.card_univ` was inside `simp only`. - simp only [Finset.sum_const] - congr - rw [← AlgHom.card L F E] - exact Finset.card_univ (α := F →ₐ[L] E) - · intro σ - simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply, - IsScalarTower.coe_toAlgHom'] + · rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen, ← + Finset.univ_sigma_univ, Finset.sum_sigma, ← Finset.sum_nsmul] + · refine' Finset.sum_congr rfl fun σ _ => _ + letI : Algebra L E := σ.toRingHom.toAlgebra + -- Porting note: `Finset.card_univ` was inside `simp only`. + simp only [Finset.sum_const] + congr + rw [← AlgHom.card L F E] + exact Finset.card_univ (α := F →ₐ[L] E) + · intro σ + simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply, + IsScalarTower.coe_toAlgHom'] #align sum_embeddings_eq_finrank_mul sum_embeddings_eq_finrank_mul theorem trace_eq_sum_embeddings [FiniteDimensional K L] [IsSeparable K L] {x : L} : @@ -591,13 +591,13 @@ theorem det_traceMatrix_ne_zero' [IsSeparable K L] : det (traceMatrix K pb.basis rw [ht, RingHom.map_zero] haveI : FiniteDimensional K L := pb.finiteDimensional let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm - rw [RingHom.map_det, RingHom.mapMatrix_apply, - traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e, - embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose] - refine mt mul_self_eq_zero.mp ?_ - · simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero] - rintro i ⟨_, j, hij, h⟩ - exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h) + · rw [RingHom.map_det, RingHom.mapMatrix_apply, + traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e, + embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose] + refine mt mul_self_eq_zero.mp ?_ + · simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero] + rintro i ⟨_, j, hij, h⟩ + exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h) · rw [AlgHom.card, pb.finrank] #align det_trace_matrix_ne_zero' det_traceMatrix_ne_zero'