diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean index 9329dbed30402..64d97d76cb021 100644 --- a/Mathlib/Algebra/BigOperators/Finprod.lean +++ b/Mathlib/Algebra/BigOperators/Finprod.lean @@ -277,7 +277,7 @@ theorem finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ i, p (f i)) : p (∏ᶠ i, f i) := by rw [finprod] split_ifs - exacts[Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀] + exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀] #align finprod_induction finprod_induction #align finsum_induction finsum_induction @@ -315,7 +315,7 @@ theorem MonoidHom.map_finprod_of_preimage_one (f : M →* N) (hf : ∀ x, f x = f (∏ᶠ i, g i) = ∏ᶠ i, f (g i) := by by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_pLift g hg rw [finprod, dif_neg, f.map_one, finprod, dif_neg] - exacts[Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg] + exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg] #align monoid_hom.map_finprod_of_preimage_one MonoidHom.map_finprod_of_preimage_one #align add_monoid_hom.map_finsum_of_preimage_zero AddMonoidHom.map_finsum_of_preimage_zero @@ -875,7 +875,7 @@ theorem finprod_mem_insert_of_eq_one_if_not_mem (h : a ∉ s → f a = 1) : (∏ᶠ i ∈ insert a s, f i) = ∏ᶠ i ∈ s, f i := by refine' finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨_, Or.inr⟩ rintro (rfl | hxs) - exacts[not_imp_comm.1 h hx, hxs] + exacts [not_imp_comm.1 h hx, hxs] #align finprod_mem_insert_of_eq_one_if_not_mem finprod_mem_insert_of_eq_one_if_not_mem #align finsum_mem_insert_of_eq_zero_if_not_mem finsum_mem_insert_of_eq_zero_if_not_mem @@ -903,7 +903,7 @@ theorem finprod_mem_dvd {f : α → N} (a : α) (hf : (mulSupport f).Finite) : f @[to_additive "The sum of `f i` over `i ∈ {a, b}`, `a ≠ b`, is equal to `f a + f b`."] theorem finprod_mem_pair (h : a ≠ b) : (∏ᶠ i ∈ ({a, b} : Set α), f i) = f a * f b := by rw [finprod_mem_insert, finprod_mem_singleton] - exacts[h, finite_singleton b] + exacts [h, finite_singleton b] #align finprod_mem_pair finprod_mem_pair #align finsum_mem_pair finsum_mem_pair @@ -1013,7 +1013,7 @@ theorem finprod_mem_inter_mul_diff' (t : Set α) (h : (s ∩ mulSupport f).Finit ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i := by rw [← finprod_mem_union', inter_union_diff] rw [disjoint_iff_inf_le] - exacts[fun x hx => hx.2.2 hx.1.2, h.subset fun x hx => ⟨hx.1.1, hx.2⟩, + exacts [fun x hx => hx.2.2 hx.1.2, h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩] #align finprod_mem_inter_mul_diff' finprod_mem_inter_mul_diff' #align finsum_mem_inter_add_diff' finsum_mem_inter_add_diff' @@ -1079,7 +1079,7 @@ theorem finprod_mem_biUnion {I : Set ι} {t : ι → Set α} (h : I.PairwiseDisj (ht : ∀ i ∈ I, (t i).Finite) : (∏ᶠ a ∈ ⋃ x ∈ I, t x, f a) = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j := by haveI := hI.fintype rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem] - exacts[fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2] + exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2] #align finprod_mem_bUnion finprod_mem_biUnion #align finsum_mem_bUnion finsum_mem_biUnion diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index 35805a529b536..ae7380da968a8 100644 --- a/Mathlib/Algebra/DirectLimit.lean +++ b/Mathlib/Algebra/DirectLimit.lean @@ -537,7 +537,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom dsimp only at this rw [this] exact sub_self _ - exacts[Or.inr rfl, Or.inl rfl] + exacts [Or.inr rfl, Or.inl rfl] · refine' ⟨i, {⟨i, 1⟩}, _, isSupported_sub (isSupported_of.2 rfl) isSupported_one, _⟩ · rintro k (rfl | h) rfl @@ -574,7 +574,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom exact sub_self _ all_goals tauto -- porting note: was - --exacts[sub_self _, Or.inl rfl, Or.inr (Or.inr rfl), Or.inr (Or.inl rfl)] + --exacts [sub_self _, Or.inl rfl, Or.inr (Or.inr rfl), Or.inr (Or.inl rfl)] · refine' Nonempty.elim (by infer_instance) fun ind : ι => _ refine' ⟨ind, ∅, fun _ => False.elim, isSupported_zero, _⟩ -- porting note: `RingHom.map_zero` was `(restriction _).map_zero` @@ -601,7 +601,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j have : ∀ z : Σi, G i, z ∈ ↑s ∪ t → z.1 ≤ k := by rintro z (hz | hz) - exacts[(hi z.1 <| Finset.mem_image.2 ⟨z, hz, rfl⟩).trans hik, (hj z hz).trans hjk] + exacts [(hi z.1 <| Finset.mem_image.2 ⟨z, hz, rfl⟩).trans hik, (hj z hz).trans hjk] refine' ⟨k, ↑s ∪ t, this, isSupported_mul (isSupported_upwards hxs <| Set.subset_union_left (↑s) t) diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean index 510eb7249c61b..c7bf0cf9f7a28 100644 --- a/Mathlib/Algebra/GroupPower/Order.lean +++ b/Mathlib/Algebra/GroupPower/Order.lean @@ -788,7 +788,7 @@ theorem pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := by theorem pow_lt_pow₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n := by induction' hmn with n _ ih - exacts[pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)] + exacts [pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)] #align pow_lt_pow₀ pow_lt_pow₀ end LinearOrderedCommGroupWithZero diff --git a/Mathlib/Algebra/Homology/QuasiIso.lean b/Mathlib/Algebra/Homology/QuasiIso.lean index c651506fbe7df..4094f11d2f510 100644 --- a/Mathlib/Algebra/Homology/QuasiIso.lean +++ b/Mathlib/Algebra/Homology/QuasiIso.lean @@ -79,7 +79,7 @@ theorem toQuasiIso {C D : HomologicalComplex W c} (e : HomotopyEquiv C D) : Quas refine' ⟨⟨(homologyFunctor W c i).map e.inv, _⟩⟩ simp only [← Functor.map_comp, ← (homologyFunctor W c i).map_id] constructor <;> apply homology_map_eq_of_homotopy - exacts[e.homotopyHomInvId, e.homotopyInvHomId]⟩ + exacts [e.homotopyHomInvId, e.homotopyInvHomId]⟩ #align homotopy_equiv.to_quasi_iso HomotopyEquiv.toQuasiIso theorem toQuasiIso_inv {C D : HomologicalComplex W c} (e : HomotopyEquiv C D) (i : ι) : diff --git a/Mathlib/Algebra/IndicatorFunction.lean b/Mathlib/Algebra/IndicatorFunction.lean index 7c56de0fcb0e4..2156900b9528d 100644 --- a/Mathlib/Algebra/IndicatorFunction.lean +++ b/Mathlib/Algebra/IndicatorFunction.lean @@ -357,7 +357,7 @@ theorem mulIndicator_rel_mulIndicator {r : M → M → Prop} (h1 : r 1 1) (ha : r (mulIndicator s f a) (mulIndicator s g a) := by simp only [mulIndicator] split_ifs with has - exacts[ha has, h1] + exacts [ha has, h1] #align set.mul_indicator_rel_mul_indicator Set.mulIndicator_rel_mulIndicator #align set.indicator_rel_indicator Set.indicator_rel_indicator @@ -493,7 +493,7 @@ theorem indicator_smul_apply (s : Set α) (r : α → M) (f : α → A) (x : α) indicator s (fun x => r x • f x) x = r x • indicator s f x := by dsimp only [indicator] split_ifs - exacts[rfl, (smul_zero (r x)).symm] + exacts [rfl, (smul_zero (r x)).symm] #align set.indicator_smul_apply Set.indicator_smul_apply theorem indicator_smul (s : Set α) (r : α → M) (f : α → A) : diff --git a/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean b/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean index 7d4c081b72333..b53b5b9044f14 100644 --- a/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean +++ b/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean @@ -100,7 +100,7 @@ theorem NoZeroDivisors.of_left_ordered [NoZeroDivisors R] [AddRightCancelSemigro refine' ⟨a + gmin, mem_support_iff.mpr _⟩ rw [mul_apply_add_eq_mul_of_forall_ne _] · refine' mul_ne_zero _ _ - exacts[mem_support_iff.mp ha, mem_support_iff.mp (Finset.min'_mem _ _)] + exacts [mem_support_iff.mp ha, mem_support_iff.mp (Finset.min'_mem _ _)] · rw [H] rintro b c bf cg (hb | hc) <;> refine' ne_of_gt _ · refine' lt_of_lt_of_le (_ : _ < b + gmin) _ @@ -139,7 +139,7 @@ theorem NoZeroDivisors.of_right_ordered [NoZeroDivisors R] [AddLeftCancelSemigro refine' ⟨fmin + a, mem_support_iff.mpr _⟩ rw [mul_apply_add_eq_mul_of_forall_ne _] · refine' mul_ne_zero _ _ - exacts[mem_support_iff.mp (Finset.min'_mem _ _), mem_support_iff.mp ha] + exacts [mem_support_iff.mp (Finset.min'_mem _ _), mem_support_iff.mp ha] · rw [H] rintro b c bf cg (hb | hc) <;> refine' ne_of_gt _ · refine' lt_of_le_of_lt (_ : _ ≤ fmin + c) _ diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean index 6fb0a61afaaec..532965bd8706a 100644 --- a/Mathlib/Algebra/Order/Ring/Defs.lean +++ b/Mathlib/Algebra/Order/Ring/Defs.lean @@ -1033,7 +1033,7 @@ instance (priority := 100) LinearOrderedRing.noZeroDivisors : NoZeroDivisors α intro a b hab refine' Decidable.or_iff_not_and_not.2 fun h => _; revert hab cases' lt_or_gt_of_ne h.1 with ha ha <;> cases' lt_or_gt_of_ne h.2 with hb hb - exacts[(mul_pos_of_neg_of_neg ha hb).ne.symm, (mul_neg_of_neg_of_pos ha hb).ne, + exacts [(mul_pos_of_neg_of_neg ha hb).ne.symm, (mul_neg_of_neg_of_pos ha hb).ne, (mul_neg_of_pos_of_neg ha hb).ne, (mul_pos ha hb).ne.symm] } #align linear_ordered_ring.no_zero_divisors LinearOrderedRing.noZeroDivisors @@ -1175,7 +1175,7 @@ theorem mul_self_pos {a : α} : 0 < a * a ↔ a ≠ 0 := by exact h.false · intro h cases' h.lt_or_lt with h h - exacts[mul_pos_of_neg_of_neg h h, mul_pos h h] + exacts [mul_pos_of_neg_of_neg h h, mul_pos h h] #align mul_self_pos mul_self_pos theorem mul_self_le_mul_self_of_le_of_neg_le {x y : α} (h₁ : x ≤ y) (h₂ : -x ≤ y) : x * x ≤ y * y := diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean index 7a9f9410cca81..e5aa78428e567 100644 --- a/Mathlib/Algebra/Star/Subalgebra.lean +++ b/Mathlib/Algebra/Star/Subalgebra.lean @@ -534,7 +534,7 @@ theorem adjoin_induction' {s : Set A} {p : adjoin R s → Prop} (a : adjoin R s) Subtype.recOn a fun b hb => by refine' Exists.elim _ fun (hb : b ∈ adjoin R s) (hc : p ⟨b, hb⟩) => hc apply adjoin_induction hb - exacts[fun x hx => ⟨subset_adjoin R s hx, Hs x hx⟩, fun r => + exacts [fun x hx => ⟨subset_adjoin R s hx, Hs x hx⟩, fun r => ⟨StarSubalgebra.algebraMap_mem _ r, Halg r⟩, fun x y hx hy => Exists.elim hx fun hx' hx => Exists.elim hy fun hy' hy => ⟨add_mem hx' hy', Hadd _ _ hx hy⟩, fun x y hx hy => diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index fddbc5595430d..ac93b0f1df2eb 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -764,7 +764,7 @@ theorem normalize_finite_fraction_representation (U : Opens (PrimeSpectrum.Top R all_goals rw [res_const]; apply const_ext; ring -- The remaining two goals were generated during the rewrite of `res_const` -- These can be solved immediately - exacts[PrimeSpectrum.basicOpen_mul_le_right _ _, PrimeSpectrum.basicOpen_mul_le_left _ _] + exacts [PrimeSpectrum.basicOpen_mul_le_right _ _, PrimeSpectrum.basicOpen_mul_le_left _ _] -- From the equality in the localization, we obtain for each `(i,j)` some power `(h i * h j) ^ n` -- which equalizes `a i * h j` and `h i * a j` have exists_power : diff --git a/Mathlib/Analysis/Asymptotics/Asymptotics.lean b/Mathlib/Analysis/Asymptotics/Asymptotics.lean index ba8dd90cb5fcf..41831a596735a 100644 --- a/Mathlib/Analysis/Asymptotics/Asymptotics.lean +++ b/Mathlib/Analysis/Asymptotics/Asymptotics.lean @@ -1393,7 +1393,7 @@ theorem isBigO_const_iff {c : F''} : (f'' =O[l] fun _x => c) ↔ refine' ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, _⟩ rintro ⟨hcf, hf⟩ rcases eq_or_ne c 0 with (hc | hc) - exacts[(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc] + exacts [(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc] #align asymptotics.is_O_const_iff Asymptotics.isBigO_const_iff theorem isBigO_iff_isBoundedUnder_le_div (h : ∀ᶠ x in l, g'' x ≠ 0) : diff --git a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean index cfc6a3dd21f5c..6ac9bf05fe9cb 100644 --- a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean @@ -178,7 +178,7 @@ theorem injective_coe : Injective ((↑) : Box ι → Set (ι → ℝ)) := by rintro ⟨l₁, u₁, h₁⟩ ⟨l₂, u₂, h₂⟩ h simp only [Subset.antisymm_iff, coe_subset_coe, le_iff_bounds] at h congr - exacts[le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2] + exacts [le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2] #align box_integral.box.injective_coe BoxIntegral.Box.injective_coe @[simp, norm_cast] diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean index 9cb8b8a1e3620..8994676eeebba 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean @@ -168,7 +168,7 @@ theorem sum_boxes_congr [Finite ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I _ = ∑ J in π₂.boxes, ∑ J' in (splitMany J s).boxes, f J' := (sum_biUnion_boxes _ _ _) _ = ∑ J in π₂.boxes, f J := Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _) - exacts[(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI, + exacts [(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI, (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI] #align box_integral.box_additive_map.sum_boxes_congr BoxIntegral.BoxAdditiveMap.sum_boxes_congr diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Filter.lean b/Mathlib/Analysis/BoxIntegral/Partition/Filter.lean index 492703e30d675..38306ae1bb896 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Filter.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Filter.lean @@ -410,10 +410,10 @@ protected theorem MemBaseSet.filter (hπ : l.MemBaseSet I c r π) (p : Box ι ext x fconstructor · rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩) - exacts[⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩] + exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩] · rintro ⟨hxI, hxp⟩ by_cases hxπ : x ∈ π.iUnion - exacts[Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩] + exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩] · have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD) simpa [hc] #align box_integral.integration_params.mem_base_set.filter BoxIntegral.IntegrationParams.MemBaseSet.filter diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean b/Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean index dc7e1471d9733..dafdc8e27f099 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean @@ -350,7 +350,7 @@ def disjUnion (π₁ π₂ : TaggedPrepartition I) (h : Disjoint π₁.iUnion π tag_mem_Icc J := by dsimp only [Finset.piecewise] split_ifs - exacts[π₁.tag_mem_Icc J, π₂.tag_mem_Icc J] + exacts [π₁.tag_mem_Icc J, π₂.tag_mem_Icc J] #align box_integral.tagged_prepartition.disj_union BoxIntegral.TaggedPrepartition.disjUnion @[simp] diff --git a/Mathlib/Analysis/Calculus/ContDiffDef.lean b/Mathlib/Analysis/Calculus/ContDiffDef.lean index 57fdfc667940a..932786d96e416 100644 --- a/Mathlib/Analysis/Calculus/ContDiffDef.lean +++ b/Mathlib/Analysis/Calculus/ContDiffDef.lean @@ -693,7 +693,7 @@ theorem contDiffOn_top : ContDiffOn 𝕜 ∞ f s ↔ ∀ n : ℕ, ContDiffOn theorem contDiffOn_all_iff_nat : (∀ n, ContDiffOn 𝕜 n f s) ↔ ∀ n : ℕ, ContDiffOn 𝕜 n f s := by refine' ⟨fun H n => H n, _⟩ rintro H (_ | n) - exacts[contDiffOn_top.2 H, H n] + exacts [contDiffOn_top.2 H, H n] #align cont_diff_on_all_iff_nat contDiffOn_all_iff_nat theorem ContDiffOn.continuousOn (h : ContDiffOn 𝕜 n f s) : ContinuousOn f s := fun x hx => @@ -1087,7 +1087,7 @@ theorem ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin {m : ℕ} simp only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter'] rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem, diff_eq_compl_inter] - exacts[rfl, mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)] + exacts [rfl, mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)] have B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t := iteratedFDerivWithin_eventually_congr_set' _ A.symm _ have C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) t x := diff --git a/Mathlib/Analysis/Calculus/LocalExtr.lean b/Mathlib/Analysis/Calculus/LocalExtr.lean index 596a80788cab2..c889e56c18128 100644 --- a/Mathlib/Analysis/Calculus/LocalExtr.lean +++ b/Mathlib/Analysis/Calculus/LocalExtr.lean @@ -97,7 +97,7 @@ theorem mem_posTangentConeAt_of_segment_subset {s : Set E} {x y : E} (h : segmen show x + d n ∈ segment ℝ x y · rw [segment_eq_image'] refine' ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩ - exacts[inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)] + exacts [inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)] show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x)) · exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm #align mem_pos_tangent_cone_at_of_segment_subset mem_posTangentConeAt_of_segment_subset @@ -282,9 +282,9 @@ theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (h refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩ simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl] · refine' ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt _ hC, lt_of_le_of_ne Cmem.2 <| mt _ hC⟩, Or.inr Cge⟩ - exacts[fun h => by rw [h], fun h => by rw [h, hfI]] + exacts [fun h => by rw [h], fun h => by rw [h, hfI]] · refine' ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt _ hc, lt_of_le_of_ne cmem.2 <| mt _ hc⟩, Or.inl cle⟩ - exacts[fun h => by rw [h], fun h => by rw [h, hfI]] + exacts [fun h => by rw [h], fun h => by rw [h, hfI]] #align exists_Ioo_extr_on_Icc exists_Ioo_extr_on_Icc /-- A continuous function on a closed interval with `f a = f b` has a local extremum at some diff --git a/Mathlib/Analysis/Convex/Combination.lean b/Mathlib/Analysis/Convex/Combination.lean index abe9167184d22..ce88530857d18 100644 --- a/Mathlib/Analysis/Convex/Combination.lean +++ b/Mathlib/Analysis/Convex/Combination.lean @@ -111,7 +111,7 @@ theorem Finset.centerMass_ite_eq (hi : i ∈ t) : trans ∑ j in t, if i = j then z i else 0 · congr with i split_ifs with h - exacts[h ▸ one_smul _ _, zero_smul _ _] + exacts [h ▸ one_smul _ _, zero_smul _ _] · rw [sum_ite_eq, if_pos hi] · rw [sum_ite_eq, if_pos hi] #align finset.center_mass_ite_eq Finset.centerMass_ite_eq @@ -332,7 +332,7 @@ theorem Finset.convexHull_eq (s : Finset E) : convexHull R ↑s = refine' ⟨_, _, _, Finset.centerMass_ite_eq _ _ _ hx⟩ · intros split_ifs - exacts[zero_le_one, le_refl 0] + exacts [zero_le_one, le_refl 0] · rw [Finset.sum_ite_eq, if_pos hx] · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab] diff --git a/Mathlib/Analysis/Convex/KreinMilman.lean b/Mathlib/Analysis/Convex/KreinMilman.lean index 19dd9cbad1d9c..77e8c9032383e 100644 --- a/Mathlib/Analysis/Convex/KreinMilman.lean +++ b/Mathlib/Analysis/Convex/KreinMilman.lean @@ -90,7 +90,7 @@ theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty) (fun t => isCompact_of_isClosed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t => (hFS t.mem).2.1 obtain htu | hut := hF.total t.mem u.mem - exacts[⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩] + exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩] #align is_compact.has_extreme_point IsCompact.has_extreme_point /-- **Krein-Milman theorem**: In a LCTVS, any compact convex set is the closure of the convex hull diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index cba752146c338..f1da1c5e9af51 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -343,7 +343,7 @@ theorem norm_eq_iInf_iff_real_inner_eq_zero (K : Submodule ℝ F) {u : F} {v : F have h₁ := h w' this exact le_of_eq h₁ rwa [norm_eq_iInf_iff_real_inner_le_zero] - exacts[Submodule.convex _, hv]) + exacts [Submodule.convex _, hv]) #align norm_eq_infi_iff_real_inner_eq_zero norm_eq_iInf_iff_real_inner_eq_zero /-- Characterization of minimizers in the projection on a subspace. diff --git a/Mathlib/Analysis/LocallyConvex/Basic.lean b/Mathlib/Analysis/LocallyConvex/Basic.lean index 82cc461e11bd1..7979a1f17c22a 100644 --- a/Mathlib/Analysis/LocallyConvex/Basic.lean +++ b/Mathlib/Analysis/LocallyConvex/Basic.lean @@ -361,7 +361,7 @@ theorem balanced_zero_union_interior (hA : Balanced 𝕜 A) : intro a ha obtain rfl | h := eq_or_ne a 0 · rw [zero_smul_set] - exacts[subset_union_left _ _, ⟨0, Or.inl rfl⟩] + exacts [subset_union_left _ _, ⟨0, Or.inl rfl⟩] · rw [← image_smul, image_union] apply union_subset_union · rw [image_zero, smul_zero] diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index dfc00fcab3ec1..0a7cc18afb4ab 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -506,7 +506,7 @@ theorem Lp_add_le_tsum {f g : ι → ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : Sum refine' le_trans (Lp_add_le s f g hp) (add_le_add _ _) <;> rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr pos)] <;> refine' sum_le_tsum _ (fun _ _ => zero_le _) _ - exacts[hf, hg] + exacts [hf, hg] have bdd : BddAbove (Set.range fun s => ∑ i in s, (f i + g i) ^ p) := by refine' ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, _⟩ rintro a ⟨s, rfl⟩ diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index c15ca40ee1bdd..9808adfe0ec6c 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/Mathlib/Analysis/Normed/Field/Basic.lean @@ -648,7 +648,7 @@ instance (priority := 100) NormedDivisionRing.to_topologicalDivisionRing : Topol theorem norm_map_one_of_pow_eq_one [Monoid β] (φ : β →* α) {x : β} {k : ℕ+} (h : x ^ (k : ℕ) = 1) : ‖φ x‖ = 1 := by rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow] - exacts[norm_nonneg _, zero_le_one, k.pos] + exacts [norm_nonneg _, zero_le_one, k.pos] #align norm_map_one_of_pow_eq_one norm_map_one_of_pow_eq_one theorem norm_one_of_pow_eq_one {x : α} {k : ℕ+} (h : x ^ (k : ℕ) = 1) : ‖x‖ = 1 := diff --git a/Mathlib/Analysis/Normed/Ring/Seminorm.lean b/Mathlib/Analysis/Normed/Ring/Seminorm.lean index c1a178fa77a8a..c2ebae282008a 100644 --- a/Mathlib/Analysis/Normed/Ring/Seminorm.lean +++ b/Mathlib/Analysis/Normed/Ring/Seminorm.lean @@ -133,7 +133,7 @@ instance [DecidableEq R] : One (RingSeminorm R) := refine' (if_pos h).trans_le (mul_nonneg _ _) <;> · change _ ≤ ite _ _ _ split_ifs - exacts[le_rfl, zero_le_one] + exacts [le_rfl, zero_le_one] · change ite _ _ _ ≤ ite _ _ _ * ite _ _ _ simp only [if_false, h, left_ne_zero_of_mul h, right_ne_zero_of_mul h, mul_one, le_refl] }⟩ diff --git a/Mathlib/Analysis/NormedSpace/Banach.lean b/Mathlib/Analysis/NormedSpace/Banach.lean index 141f4952ad684..921580ecd5653 100644 --- a/Mathlib/Analysis/NormedSpace/Banach.lean +++ b/Mathlib/Analysis/NormedSpace/Banach.lean @@ -99,7 +99,7 @@ theorem exists_approx_preimage_norm_le (surj : Surjective f) : rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩ refine' ⟨(ε / 2)⁻¹ * ‖c‖ * 2 * n, _, fun y => _⟩ · refine' mul_nonneg (mul_nonneg (mul_nonneg _ (norm_nonneg _)) (by norm_num)) _ - exacts[inv_nonneg.2 (div_nonneg (le_of_lt εpos) (by norm_num)), n.cast_nonneg] + exacts [inv_nonneg.2 (div_nonneg (le_of_lt εpos) (by norm_num)), n.cast_nonneg] · by_cases hy : y = 0 · use 0 simp [hy] diff --git a/Mathlib/Analysis/NormedSpace/Multilinear.lean b/Mathlib/Analysis/NormedSpace/Multilinear.lean index 671c3fe8d093c..8216d620d53b7 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear.lean @@ -494,7 +494,7 @@ theorem norm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [∀ i', N · refine' op_norm_le_bound _ (norm_nonneg f) fun m => _ dsimp rw [pi_norm_le_iff_of_nonneg] - exacts[fun i => (f i).le_of_op_norm_le m (norm_le_pi_norm f i), + exacts [fun i => (f i).le_of_op_norm_le m (norm_le_pi_norm f i), mul_nonneg (norm_nonneg f) (prod_nonneg fun _ _ => norm_nonneg _)] · refine' (pi_norm_le_iff_of_nonneg (norm_nonneg _)).2 fun i => _ refine' op_norm_le_bound _ (norm_nonneg _) fun m => _ diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean index ccf308ebe6f09..d90fc3f91a6ce 100644 --- a/Mathlib/Analysis/PSeries.lean +++ b/Mathlib/Analysis/PSeries.lean @@ -56,7 +56,7 @@ theorem le_sum_condensed' (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m suffices (∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k) ≤ 2 ^ n • f (2 ^ n) by rw [sum_range_succ, ← sum_Ico_consecutive] exact add_le_add ihn this - exacts[n.one_le_two_pow, Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ] + exacts [n.one_le_two_pow, Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ] have : ∀ k ∈ Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ f (2 ^ n) := fun k hk => hf (pow_pos zero_lt_two _) (mem_Ico.mp hk).1 convert sum_le_sum this diff --git a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean index 6aac6c4d7e75a..ada5654763f7d 100644 --- a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean +++ b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean @@ -147,7 +147,7 @@ theorem isLittleO_log_abs_re (hl : IsExpCmpFilter l) : (fun z => Real.log (abs z rw [one_mul, Real.norm_eq_abs, _root_.abs_of_nonneg (Real.log_nonneg hz')] refine' le_trans _ (le_abs_self _) rw [← Real.log_mul, Real.log_le_log, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)] - exacts[abs_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne'] + exacts [abs_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne'] _ =o[l] re := IsLittleO.add (isLittleO_const_left.2 <| Or.inr <| hl.tendsto_abs_re) <| isLittleO_iff_nat_mul_le.2 fun n => by diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean index d9ade4e8e59f7..cf4f56685d228 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean @@ -96,7 +96,7 @@ theorem arg_mul_cos_add_sin_mul_I {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ mk_eq_add_mul_I, neg_div, mul_div_cancel_left _ hr.ne', mul_nonneg_iff_right_nonneg_of_pos hr] by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2) · rw [if_pos] - exacts[Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁] + exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁] · rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁ cases' h₁ with h₁ h₁ · replace hθ := hθ.1 @@ -299,7 +299,7 @@ theorem arg_of_im_pos {z : ℂ} (hz : 0 < z.im) : arg z = Real.arccos (z.re / ab theorem arg_of_im_neg {z : ℂ} (hz : z.im < 0) : arg z = -Real.arccos (z.re / abs z) := by have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg] - exacts[neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le] + exacts [neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le] #align complex.arg_of_im_neg Complex.arg_of_im_neg theorem arg_conj (x : ℂ) : arg (conj x) = if arg x = π then π else -arg x := by @@ -335,7 +335,7 @@ theorem arg_le_pi_div_two_iff {z : ℂ} : arg z ≤ π / 2 ↔ 0 ≤ re z ∨ im rw [iff_false_iff, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub, Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ← _root_.abs_of_nonneg him, abs_im_lt_abs] - exacts[hre.ne, abs.pos <| ne_of_apply_ne re hre.ne] + exacts [hre.ne, abs.pos <| ne_of_apply_ne re hre.ne] · simp only [him] rw [iff_true_iff, arg_of_re_neg_of_im_neg hre him] exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _) @@ -353,7 +353,7 @@ theorem neg_pi_div_two_le_arg_iff {z : ℂ} : -(π / 2) ≤ arg z ↔ 0 ≤ re z rw [iff_false_iff, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ← sub_eq_add_neg, sub_half, Real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him, abs_im_lt_abs] - exacts[hre.ne, abs.pos <| ne_of_apply_ne re hre.ne] + exacts [hre.ne, abs.pos <| ne_of_apply_ne re hre.ne] #align complex.neg_pi_div_two_le_arg_iff Complex.neg_pi_div_two_le_arg_iff @[simp] @@ -545,7 +545,7 @@ theorem continuousAt_arg (h : 0 < x.re ∨ x.im ≠ 0) : ContinuousAt arg x := b simp at h rw [← lt_or_lt_iff_ne] at h rcases h with (hx_re | hx_im | hx_im) - exacts[(Real.continuousAt_arcsin.comp + exacts [(Real.continuousAt_arcsin.comp (continuous_im.continuousAt.div continuous_abs.continuousAt h₀)).congr (arg_eq_nhds_of_re_pos hx_re).symm, (Real.continuous_arccos.continuousAt.comp diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index dc0a546aea9f8..331a2effc6872 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -345,7 +345,7 @@ theorem zero_rpow_def (y : ℝ) : (0 : ℝ≥0∞) ^ y = if 0 < y then 0 else if theorem zero_rpow_mul_self (y : ℝ) : (0 : ℝ≥0∞) ^ y * (0 : ℝ≥0∞) ^ y = (0 : ℝ≥0∞) ^ y := by rw [zero_rpow_def] split_ifs - exacts[MulZeroClass.zero_mul _, one_mul _, top_mul_top] + exacts [MulZeroClass.zero_mul _, one_mul _, top_mul_top] #align ennreal.zero_rpow_mul_self ENNReal.zero_rpow_mul_self @[norm_cast] diff --git a/Mathlib/CategoryTheory/CommSq.lean b/Mathlib/CategoryTheory/CommSq.lean index 9a7f103ff036c..82cd0a776c2cd 100644 --- a/Mathlib/CategoryTheory/CommSq.lean +++ b/Mathlib/CategoryTheory/CommSq.lean @@ -203,7 +203,7 @@ variable (sq) theorem iff : HasLift sq ↔ Nonempty sq.LiftStruct := by constructor - exacts[fun h => h.exists_lift, fun h => mk h] + exacts [fun h => h.exists_lift, fun h => mk h] #align category_theory.comm_sq.has_lift.iff CategoryTheory.CommSq.HasLift.iff theorem iff_op : HasLift sq ↔ HasLift sq.op := by diff --git a/Mathlib/CategoryTheory/Extensive.lean b/Mathlib/CategoryTheory/Extensive.lean index cea7c9ad62cb9..929ac1d4dfe30 100644 --- a/Mathlib/CategoryTheory/Extensive.lean +++ b/Mathlib/CategoryTheory/Extensive.lean @@ -169,7 +169,7 @@ theorem BinaryCofan.isVanKampen_iff (c : BinaryCofan X Y) : · intro H exact ⟨H _, H _⟩ · rintro H ⟨⟨⟩⟩ - exacts[H.1, H.2] + exacts [H.1, H.2] · introv H F' hα h let X' := F'.obj ⟨WalkingPair.left⟩ let Y' := F'.obj ⟨WalkingPair.right⟩ @@ -184,7 +184,7 @@ theorem BinaryCofan.isVanKampen_iff (c : BinaryCofan X Y) : (NatTrans.congr_app hα ⟨WalkingPair.right⟩)] constructor · rintro H ⟨⟨⟩⟩ - exacts[H.1, H.2] + exacts [H.1, H.2] · intro H exact ⟨H _, H _⟩ #align category_theory.binary_cofan.is_van_kampen_iff CategoryTheory.BinaryCofan.isVanKampen_iff @@ -351,7 +351,7 @@ instance types.finitaryExtensive : FinitaryExtensive (Type u) := by have : ∀ x, f x = Sum.inl PUnit.unit ∨ f x = Sum.inr PUnit.unit := by intro x rcases f x with (⟨⟨⟩⟩ | ⟨⟨⟩⟩) - exacts[Or.inl rfl, Or.inr rfl] + exacts [Or.inl rfl, Or.inr rfl] let eX : { p : Z × PUnit // f p.fst = Sum.inl p.snd } ≃ { x : Z // f x = Sum.inl PUnit.unit } := ⟨fun p => ⟨p.1.1, by convert p.2⟩, fun x => ⟨⟨_, _⟩, x.2⟩, fun _ => by ext; rfl, fun _ => by ext; rfl⟩ @@ -392,7 +392,7 @@ noncomputable def finitaryExtensiveTopCatAux (Z : TopCat.{u}) have : ∀ x, f x = Sum.inl PUnit.unit ∨ f x = Sum.inr PUnit.unit := by intro x rcases f x with (⟨⟨⟩⟩ | ⟨⟨⟩⟩) - exacts[Or.inl rfl, Or.inr rfl] + exacts [Or.inl rfl, Or.inr rfl] letI eX : { p : Z × PUnit // f p.fst = Sum.inl p.snd } ≃ { x : Z // f x = Sum.inl PUnit.unit } := ⟨fun p => ⟨p.1.1, p.2.trans (congr_arg Sum.inl <| Subsingleton.elim _ _)⟩, fun x => ⟨⟨_, PUnit.unit⟩, x.2⟩, fun _ => by ext; rfl, fun _ => by ext; rfl⟩ diff --git a/Mathlib/CategoryTheory/GlueData.lean b/Mathlib/CategoryTheory/GlueData.lean index 01144c33d69bb..bbf572bcb9acd 100644 --- a/Mathlib/CategoryTheory/GlueData.lean +++ b/Mathlib/CategoryTheory/GlueData.lean @@ -389,7 +389,7 @@ def vPullbackConeIsLimitOfMap (i j : D.J) [ReflectsLimit (cospan (D.ι i) (D.ι NatIso.ofComponents (fun x => by cases x - exacts[D.gluedIso F, Iso.refl _]) + exacts [D.gluedIso F, Iso.refl _]) (by rintro (_ | _) (_ | _) (_ | _ | _) <;> simp) apply IsLimit.postcomposeHomEquiv e _ _ apply hc.ofIsoLimit diff --git a/Mathlib/CategoryTheory/LiftingProperties/Basic.lean b/Mathlib/CategoryTheory/LiftingProperties/Basic.lean index 10d46904bcef2..5b8c280659fdf 100644 --- a/Mathlib/CategoryTheory/LiftingProperties/Basic.lean +++ b/Mathlib/CategoryTheory/LiftingProperties/Basic.lean @@ -138,13 +138,13 @@ theorem iff_of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'} (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty i' p := by constructor <;> intro - exacts[of_arrow_iso_left e p, of_arrow_iso_left e.symm p] + exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p] #align category_theory.has_lifting_property.iff_of_arrow_iso_left CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left theorem iff_of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : Arrow.mk p ≅ Arrow.mk p') : HasLiftingProperty i p ↔ HasLiftingProperty i p' := by constructor <;> intro - exacts[of_arrow_iso_right i e, of_arrow_iso_right i e.symm] + exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm] #align category_theory.has_lifting_property.iff_of_arrow_iso_right CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right end HasLiftingProperty diff --git a/Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean index 8d74a7cebbe4a..bde168c5a89bf 100644 --- a/Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean +++ b/Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean @@ -49,7 +49,7 @@ def isBinaryProductOfIsTerminalIsPullback (F : Discrete WalkingPair ⥤ C) (c : dsimp; rw [← J, ← J] apply hc.hom_ext rintro (_ | (_ | _)) <;> simp only [PullbackCone.mk_π_app_one, PullbackCone.mk_π_app] - exacts[(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm, + exacts [(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm, (hc.fac c' WalkingCospan.left).symm, (hc.fac c' WalkingCospan.right).symm] #align is_binary_product_of_is_terminal_is_pullback isBinaryProductOfIsTerminalIsPullback @@ -147,7 +147,7 @@ def isBinaryCoproductOfIsInitialIsPushout (F : Discrete WalkingPair ⥤ C) (c : rintro (_ | (_ | _)) <;> simp only [PushoutCocone.mk_ι_app_zero, PushoutCocone.mk_ι_app, Category.assoc] congr 1 - exacts[(hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.left).symm, + exacts [(hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.right).symm] #align is_binary_coproduct_of_is_initial_is_pushout isBinaryCoproductOfIsInitialIsPushout diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean index 3057a06be5797..bb8a7d6e29d06 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean @@ -359,7 +359,7 @@ def BinaryFan.isLimitMk {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : ∀ s : { lift := lift fac := fun s j => by rcases j with ⟨⟨⟩⟩ - exacts[fac_left s, fac_right s] + exacts [fac_left s, fac_right s] uniq := fun s m w => uniq s m (w ⟨WalkingPair.left⟩) (w ⟨WalkingPair.right⟩) } #align category_theory.limits.binary_fan.is_limit_mk CategoryTheory.Limits.BinaryFan.isLimitMk @@ -377,7 +377,7 @@ def BinaryCofan.isColimitMk {W : C} {inl : X ⟶ W} {inr : Y ⟶ W} { desc := desc fac := fun s j => by rcases j with ⟨⟨⟩⟩ - exacts[fac_left s, fac_right s] + exacts [fac_left s, fac_right s] uniq := fun s m w => uniq s m (w ⟨WalkingPair.left⟩) (w ⟨WalkingPair.right⟩) } #align category_theory.limits.binary_cofan.is_colimit_mk CategoryTheory.Limits.BinaryCofan.isColimitMk diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean index 3e125e70ccaa3..634369a5a9f40 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean @@ -588,7 +588,7 @@ theorem biproduct.fromSubtype_π [DecidablePred p] (j : J) : by_cases h : p j · rw [dif_pos h, biproduct.ι_π] split_ifs with h₁ h₂ h₂ - exacts[rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] + exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] · rw [dif_neg h, dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero] #align category_theory.limits.biproduct.from_subtype_π CategoryTheory.Limits.biproduct.fromSubtype_π @@ -604,7 +604,7 @@ theorem biproduct.fromSubtype_π_subtype (j : Subtype p) : apply biproduct.hom_ext'; intro i rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π] split_ifs with h₁ h₂ h₂ - exacts[rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] + exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] #align category_theory.limits.biproduct.from_subtype_π_subtype CategoryTheory.Limits.biproduct.fromSubtype_π_subtype @[reassoc (attr := simp)] @@ -622,7 +622,7 @@ theorem biproduct.ι_toSubtype [DecidablePred p] (j : J) : by_cases h : p j · rw [dif_pos h, biproduct.ι_π] split_ifs with h₁ h₂ h₂ - exacts[rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] + exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp] #align category_theory.limits.biproduct.ι_to_subtype CategoryTheory.Limits.biproduct.ι_toSubtype @@ -638,7 +638,7 @@ theorem biproduct.ι_toSubtype_subtype (j : Subtype p) : apply biproduct.hom_ext; intro i rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π] split_ifs with h₁ h₂ h₂ - exacts[rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] + exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl] #align category_theory.limits.biproduct.ι_to_subtype_subtype CategoryTheory.Limits.biproduct.ι_toSubtype_subtype @[reassoc (attr := simp)] diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean index 8863a7e3ea6ee..1a324795c602e 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean @@ -131,10 +131,10 @@ theorem WalkingParallelPairHom.id.sizeOf_spec' (X : WalkingParallelPair) : right. -/ def walkingParallelPairOp : WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ where - obj x := op <| by cases x; exacts[one, zero] + obj x := op <| by cases x; exacts [one, zero] map f := by cases f <;> apply Quiver.Hom.op - exacts[left, right, WalkingParallelPairHom.id _] + exacts [left, right, WalkingParallelPairHom.id _] map_comp := by rintro _ _ _ (_|_|_) g <;> cases g <;> rfl #align category_theory.limits.walking_parallel_pair_op CategoryTheory.Limits.walkingParallelPairOp diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean index e5504827da686..07db76a8af490 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean @@ -740,7 +740,7 @@ def isLimitOfFactors (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ Z) [Mono h] (x : X simp only [PullbackCone.mk_fst, PullbackCone.mk_snd] at hr hr'⊢ <;> simp only [hr, hr'] <;> symm - exacts[hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right]⟩⟩ + exacts [hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right]⟩⟩ #align category_theory.limits.pullback_cone.is_limit_of_factors CategoryTheory.Limits.PullbackCone.isLimitOfFactors /-- If `W` is the pullback of `f, g`, diff --git a/Mathlib/CategoryTheory/MorphismProperty.lean b/Mathlib/CategoryTheory/MorphismProperty.lean index eac40034ef5ae..73c69b7983e9b 100644 --- a/Mathlib/CategoryTheory/MorphismProperty.lean +++ b/Mathlib/CategoryTheory/MorphismProperty.lean @@ -373,7 +373,7 @@ theorem RespectsIso.inverseImage {P : MorphismProperty D} (h : RespectsIso P) (F intro X Y Z e f hf dsimp [MorphismProperty.inverseImage] rw [F.map_comp] - exacts[h.1 (F.mapIso e) (F.map f) hf, h.2 (F.mapIso e) (F.map f) hf] + exacts [h.1 (F.mapIso e) (F.map f) hf, h.2 (F.mapIso e) (F.map f) hf] #align category_theory.morphism_property.respects_iso.inverse_image CategoryTheory.MorphismProperty.RespectsIso.inverseImage theorem StableUnderComposition.inverseImage {P : MorphismProperty D} (h : StableUnderComposition P) diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index dfa52eba46482..b981a514954b4 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -371,7 +371,7 @@ theorem exists_code {n} {f : Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : exact ⟨_, ⟨h, @(hm)⟩, rfl⟩ · refine' IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => _ obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h' - exacts[hm _ h, h] + exacts [hm _ h, h] · rintro ⟨n, ⟨hn, hm⟩, rfl⟩ refine' ⟨n.succ::v.1, _, rfl⟩ have : (n.succ::v.1 : List ℕ) ∈ diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean index 1cc98412a203d..ae5b20a11378c 100644 --- a/Mathlib/Computability/TuringMachine.lean +++ b/Mathlib/Computability/TuringMachine.lean @@ -1347,7 +1347,7 @@ theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₁} (h : q simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h hs iterate 3 rcases h with (rfl | h) <;> [exact hs; exact IH h hs] - case branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts[hs, IH₁ h hs.1, IH₂ h hs.2] + case branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2] case goto l => subst h; exact hs case halt => subst h; trivial #align turing.TM1.stmts₁_supports_stmt_mono Turing.TM1.stmts₁_supportsStmt_mono @@ -1920,7 +1920,7 @@ theorem tr_supports {S : Finset Λ} (ss : Supports M S) : Supports (tr enc dec M have := this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem hq⟩ rcases Finset.mem_insert.1 h with (rfl | h) - exacts[this.1, this.2 _ h] + exacts [this.1, this.2 _ h] intro q hs hw induction q case move d q IH => @@ -2217,7 +2217,7 @@ theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₂} (h : q simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h hs iterate 4 rcases h with (rfl | h) <;> [exact hs; exact IH h hs] - case branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts[hs, IH₁ h hs.1, IH₂ h hs.2] + case branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2] case goto l => subst h; exact hs case halt => subst h; trivial #align turing.TM2.stmts₁_supports_stmt_mono Turing.TM2.stmts₁_supportsStmt_mono diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean index 699be90757e07..e153a3f52a559 100644 --- a/Mathlib/Data/Bool/Basic.lean +++ b/Mathlib/Data/Bool/Basic.lean @@ -404,7 +404,7 @@ theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b := by theorem injective_iff {α : Sort _} {f : Bool → α} : Function.Injective f ↔ f false ≠ f true := ⟨fun Hinj Heq ↦ ff_ne_tt (Hinj Heq), fun H x y hxy ↦ by cases x <;> cases y - exacts[rfl, (H hxy).elim, (H hxy.symm).elim, rfl]⟩ + exacts [rfl, (H hxy).elim, (H hxy.symm).elim, rfl]⟩ #align bool.injective_iff Bool.injective_iff /-- **Kaminski's Equation** -/ diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean index 6e85bf126cbdd..8bae1155d2514 100644 --- a/Mathlib/Data/Complex/Module.lean +++ b/Mathlib/Data/Complex/Module.lean @@ -316,7 +316,7 @@ theorem real_algHom_eq_id_or_conj (f : ℂ →ₐ[ℝ] ℂ) : f = AlgHom.id ℝ refine' (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp _ _ <;> refine' fun h => algHom_ext _ - exacts[h, conj_I.symm ▸ h] + exacts [h, conj_I.symm ▸ h] #align complex.real_alg_hom_eq_id_or_conj Complex.real_algHom_eq_id_or_conj /-- The natural `AddEquiv` from `ℂ` to `ℝ × ℝ`. -/ diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 443464f028e36..345a2b5b482fe 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -1875,7 +1875,7 @@ theorem liftFun_iff_succ {α : Type _} (r : α → α → Prop) [IsTrans α r] { · intro j ihj hij rw [← le_castSucc_iff] at hij rcases hij.eq_or_lt with (rfl | hlt) - exacts[H j, _root_.trans (ihj hlt) (H j)] + exacts [H j, _root_.trans (ihj hlt) (H j)] #align fin.lift_fun_iff_succ Fin.liftFun_iff_succ /-- A function `f` on `Fin (n + 1)` is strictly monotone if and only if `f i < f (i + 1)` @@ -2154,7 +2154,7 @@ theorem pred_succAbove {x : Fin n} {y : Fin (n + 1)} (h : y ≤ castSucc x) theorem exists_succAbove_eq {x y : Fin (n + 1)} (h : x ≠ y) : ∃ z, y.succAbove z = x := by cases' h.lt_or_lt with hlt hlt - exacts[⟨_, succAbove_castLT hlt⟩, ⟨_, succAbove_pred hlt⟩] + exacts [⟨_, succAbove_castLT hlt⟩, ⟨_, succAbove_pred hlt⟩] #align fin.exists_succ_above_eq Fin.exists_succAbove_eq @[simp] diff --git a/Mathlib/Data/Fin/Tuple/Sort.lean b/Mathlib/Data/Fin/Tuple/Sort.lean index 2c9c74e672228..0c2c3e6aa9375 100644 --- a/Mathlib/Data/Fin/Tuple/Sort.lean +++ b/Mathlib/Data/Fin/Tuple/Sort.lean @@ -148,7 +148,7 @@ theorem eq_sort_iff : refine' ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => _⟩, fun h i j hij => _⟩ · exact (((Prod.Lex.lt_iff _ _).1 <| h hij).resolve_left hfij.not_lt).2 · obtain he | hl := (h.1 hij.le).eq_or_lt <;> apply (Prod.Lex.lt_iff _ _).2 - exacts[Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl] + exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl] #align tuple.eq_sort_iff Tuple.eq_sort_iff /-- The permutation that sorts `f` is the identity if and only if `f` is monotone. -/ diff --git a/Mathlib/Data/Fintype/Option.lean b/Mathlib/Data/Fintype/Option.lean index 0a6b61d52f358..55b615275558c 100644 --- a/Mathlib/Data/Fintype/Option.lean +++ b/Mathlib/Data/Fintype/Option.lean @@ -117,5 +117,5 @@ theorem Finite.induction_empty_option {P : Type u → Prop} (of_equiv : ∀ {α [Finite α] : P α := by cases nonempty_fintype α refine' Fintype.induction_empty_option _ _ _ α - exacts[fun α β _ => of_equiv, h_empty, @h_option] + exacts [fun α β _ => of_equiv, h_empty, @h_option] #align finite.induction_empty_option Finite.induction_empty_option diff --git a/Mathlib/Data/Fintype/Perm.lean b/Mathlib/Data/Fintype/Perm.lean index 64b28cd03ae89..57b0f18a33c85 100644 --- a/Mathlib/Data/Fintype/Perm.lean +++ b/Mathlib/Data/Fintype/Perm.lean @@ -69,7 +69,7 @@ theorem mem_permsOfList_of_mem {l : List α} {f : Perm α} (h : ∀ x, f x ≠ x refine' List.mem_of_ne_of_mem hxa (h x fun h => _) simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx split_ifs at hx with h_1 - exacts[hxa (h.symm.trans h_1), hx h] + exacts [hxa (h.symm.trans h_1), hx h] suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind] refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩ diff --git a/Mathlib/Data/List/BigOperators/Basic.lean b/Mathlib/Data/List/BigOperators/Basic.lean index ce61a12e26a60..d90f4da921d8e 100644 --- a/Mathlib/Data/List/BigOperators/Basic.lean +++ b/Mathlib/Data/List/BigOperators/Basic.lean @@ -386,7 +386,7 @@ theorem prod_eq_zero {L : List M₀} (h : (0 : M₀) ∈ L) : L.prod = 0 := by · exact absurd h (not_mem_nil _) · rw [prod_cons] cases' mem_cons.1 h with ha hL - exacts[mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)] + exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)] #align list.prod_eq_zero List.prod_eq_zero /-- Product of elements of a list `L` equals zero if and only if `0 ∈ L`. See also diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean index 717ec743051fe..78fead05eca8a 100644 --- a/Mathlib/Data/List/Sort.lean +++ b/Mathlib/Data/List/Sort.lean @@ -255,7 +255,7 @@ theorem Sorted.insertionSort_eq : ∀ {l : List α} (_ : Sorted r l), insertionS | [a], _ => rfl | a :: b :: l, h => by rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos] - exacts[rel_of_sorted_cons h _ (mem_cons_self _ _), h.tail] + exacts [rel_of_sorted_cons h _ (mem_cons_self _ _), h.tail] #align list.sorted.insertion_sort_eq List.Sorted.insertionSort_eq section TotalAndTransitive diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 813fecb1362b0..942b709bb39cf 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -140,7 +140,7 @@ theorem and_forall_succ {p : ℕ → Prop} : (p 0 ∧ ∀ n, p (n + 1)) ↔ ∀ theorem or_exists_succ {p : ℕ → Prop} : (p 0 ∨ ∃ n, p (n + 1)) ↔ ∃ n, p n := ⟨fun h => h.elim (fun h0 => ⟨0, h0⟩) fun ⟨n, hn⟩ => ⟨n + 1, hn⟩, by rintro ⟨_ | n, hn⟩ - exacts[Or.inl hn, Or.inr ⟨n, hn⟩]⟩ + exacts [Or.inl hn, Or.inr ⟨n, hn⟩]⟩ #align nat.or_exists_succ Nat.or_exists_succ /-! ### `succ` -/ @@ -862,7 +862,7 @@ theorem find_comp_succ (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬p 0 Nat.find h₁ = Nat.find h₂ + 1 := by refine' (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn => _⟩ cases' n with n - exacts[h0, @Nat.find_min (fun n => p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)] + exacts [h0, @Nat.find_min (fun n => p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)] #align nat.find_comp_succ Nat.find_comp_succ end Find diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean index 80a1969e84aa0..1ec103be9cbff 100644 --- a/Mathlib/Data/Nat/Log.lean +++ b/Mathlib/Data/Nat/Log.lean @@ -116,7 +116,7 @@ theorem pow_le_of_le_log {b x y : ℕ} (hy : y ≠ 0) (h : x ≤ log b y) : b ^ theorem le_log_of_pow_le {b x y : ℕ} (hb : 1 < b) (h : b ^ x ≤ y) : x ≤ log b y := by rcases ne_or_eq y 0 with (hy | rfl) - exacts[(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim] + exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim] #align nat.le_log_of_pow_le Nat.le_log_of_pow_le theorem pow_log_le_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : b ^ log b x ≤ x := diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean index e92c649c54dac..8273105d4f975 100644 --- a/Mathlib/Data/Nat/Order/Basic.lean +++ b/Mathlib/Data/Nat/Order/Basic.lean @@ -611,13 +611,13 @@ theorem findGreatest_eq_iff : exact ⟨le_rfl, fun _ => hk, fun n hlt hle => (hlt.not_le hle).elim⟩ · rintro ⟨hle, h0, hm⟩ rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt) - exacts[rfl, (hm hlt le_rfl hk).elim] + exacts [rfl, (hm hlt le_rfl hk).elim] · rw [findGreatest_of_not hk, ihk] constructor · rintro ⟨hle, hP, hm⟩ refine ⟨hle.trans k.le_succ, hP, fun n hlt hle => ?_⟩ rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt') - exacts[hk, hm hlt <| lt_succ_iff.1 hlt'] + exacts [hk, hm hlt <| lt_succ_iff.1 hlt'] · rintro ⟨hle, hP, hm⟩ refine ⟨lt_succ_iff.1 (hle.lt_of_ne ?_), hP, fun n hlt hle => hm hlt (hle.trans k.le_succ)⟩ rintro rfl diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean index 9ba05f333cc09..c50729069fbbd 100644 --- a/Mathlib/Data/Num/Lemmas.lean +++ b/Mathlib/Data/Num/Lemmas.lean @@ -327,7 +327,7 @@ theorem cmp_to_nat : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℕ) < n) (m = n | pos a, 0 => to_nat_pos _ | pos a, pos b => by have := PosNum.cmp_to_nat a b; revert this; dsimp [cmp]; cases PosNum.cmp a b - exacts[id, congr_arg pos, id] + exacts [id, congr_arg pos, id] #align num.cmp_to_nat Num.cmp_to_nat @[norm_cast] diff --git a/Mathlib/Data/Pi/Lex.lean b/Mathlib/Data/Pi/Lex.lean index 4b1a25bafcff6..de9e6da3e215f 100644 --- a/Mathlib/Data/Pi/Lex.lean +++ b/Mathlib/Data/Pi/Lex.lean @@ -89,7 +89,7 @@ theorem isTrichotomous_lex [∀ i, IsTrichotomous (β i) s] (wf : WellFounded r) exact fun h' => wf.not_lt_min _ _ h' have hne : a i ≠ b i := wf.min_mem _ hab cases' trichotomous_of s (a i) (b i) with hi hi - exacts[Or.inl ⟨i, hri, hi⟩, + exacts [Or.inl ⟨i, hri, hi⟩, Or.inr <| Or.inr <| ⟨i, fun j hj => (hri j hj).symm, hi.resolve_left hne⟩] } #align pi.is_trichotomous_lex Pi.isTrichotomous_lex @@ -102,7 +102,7 @@ instance Lex.isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] : trans := by rintro a b c ⟨N₁, lt_N₁, a_lt_b⟩ ⟨N₂, lt_N₂, b_lt_c⟩ rcases lt_trichotomy N₁ N₂ with (H | rfl | H) - exacts[⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩, + exacts [⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩, ⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩, ⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩] #align pi.lex.is_strict_order Pi.Lex.isStrictOrder diff --git a/Mathlib/Data/Polynomial/Degree/Definitions.lean b/Mathlib/Data/Polynomial/Degree/Definitions.lean index 00c4b1103e847..99e2fad85d339 100644 --- a/Mathlib/Data/Polynomial/Degree/Definitions.lean +++ b/Mathlib/Data/Polynomial/Degree/Definitions.lean @@ -334,7 +334,7 @@ theorem natDegree_monomial [DecidableEq R] (i : ℕ) (r : R) : theorem natDegree_monomial_le (a : R) {m : ℕ} : (monomial m a).natDegree ≤ m := by rw [Polynomial.natDegree_monomial] split_ifs - exacts[Nat.zero_le _, rfl.le] + exacts [Nat.zero_le _, rfl.le] #align polynomial.nat_degree_monomial_le Polynomial.natDegree_monomial_le theorem natDegree_monomial_eq (i : ℕ) {r : R} (r0 : r ≠ 0) : (monomial i r).natDegree = i := diff --git a/Mathlib/Data/Polynomial/Module.lean b/Mathlib/Data/Polynomial/Module.lean index c49a56835533a..9b74dd0cc345a 100644 --- a/Mathlib/Data/Polynomial/Module.lean +++ b/Mathlib/Data/Polynomial/Module.lean @@ -150,7 +150,7 @@ theorem monomial_smul_apply (i : ℕ) (r : R) (g : PolynomialModule R M) (n : · simp only [smul_zero, zero_apply, ite_self] · simp only [smul_add, add_apply, hp, hq] split_ifs - exacts[rfl, zero_add 0] + exacts [rfl, zero_add 0] · rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and] congr rw [eq_iff_iff] @@ -167,7 +167,7 @@ theorem smul_single_apply (i : ℕ) (f : R[X]) (m : M) (n : ℕ) : induction' f using Polynomial.induction_on' with p q hp hq · rw [add_smul, Finsupp.add_apply, hp, hq, coeff_add, add_smul] split_ifs - exacts[rfl, zero_add 0] + exacts [rfl, zero_add 0] · rw [monomial_smul_single, single_apply, coeff_monomial, ite_smul, zero_smul] by_cases h : i ≤ n · simp_rw [eq_tsub_iff_add_eq_of_le h, if_pos h] diff --git a/Mathlib/Data/Polynomial/Monic.lean b/Mathlib/Data/Polynomial/Monic.lean index 6d5e9771b2452..5460d95b4309c 100644 --- a/Mathlib/Data/Polynomial/Monic.lean +++ b/Mathlib/Data/Polynomial/Monic.lean @@ -286,7 +286,7 @@ theorem Monic.nextCoeff_multiset_prod (t : Multiset ι) (f : ι → R[X]) (h : rw [nextCoeff_C_eq_zero] · rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, Monic.nextCoeff_mul, ih] - exacts[fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _), + exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _), monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)] #align polynomial.monic.next_coeff_multiset_prod Polynomial.Monic.nextCoeff_multiset_prod diff --git a/Mathlib/Data/Polynomial/RingDivision.lean b/Mathlib/Data/Polynomial/RingDivision.lean index 268c10d1e3bd3..9e60686ec20a2 100644 --- a/Mathlib/Data/Polynomial/RingDivision.lean +++ b/Mathlib/Data/Polynomial/RingDivision.lean @@ -1112,7 +1112,7 @@ theorem exists_prod_multiset_X_sub_C_mul (p : R[X]) : rw [monic_prod_multiset_X_sub_C.natDegree_mul' hq, natDegree_multiset_prod_X_sub_C_eq_card] · replace he := congr_arg roots he.symm rw [roots_mul, roots_multiset_prod_X_sub_C] at he - exacts[add_right_eq_self.1 he, mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq] + exacts [add_right_eq_self.1 he, mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq] set_option linter.uppercaseLean3 false in #align polynomial.exists_prod_multiset_X_sub_C_mul Polynomial.exists_prod_multiset_X_sub_C_mul diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean index 312cf41c6c45d..f08b43bf67ded 100644 --- a/Mathlib/Data/Real/Basic.lean +++ b/Mathlib/Data/Real/Basic.lean @@ -895,7 +895,7 @@ bounded below by `0` to show that `0 ≤ sInf S`. -/ theorem sInf_nonneg (S : Set ℝ) (hS : ∀ x ∈ S, (0 : ℝ) ≤ x) : 0 ≤ sInf S := by rcases S.eq_empty_or_nonempty with (rfl | hS₂) - exacts[sInf_empty.ge, le_csInf hS₂ hS] + exacts [sInf_empty.ge, le_csInf hS₂ hS] #align real.Inf_nonneg Real.sInf_nonneg /-- As `0` is the default value for `Real.sInf` of the empty set, it suffices to show that `f i` is diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean index b510f8bb35c3a..7f692b12555be 100644 --- a/Mathlib/Data/Real/ENNReal.lean +++ b/Mathlib/Data/Real/ENNReal.lean @@ -1624,7 +1624,7 @@ theorem div_lt_of_lt_mul' (h : a < b * c) : a / b < c := theorem inv_le_iff_le_mul (h₁ : b = ∞ → a ≠ 0) (h₂ : a = ∞ → b ≠ 0) : a⁻¹ ≤ b ↔ 1 ≤ a * b := by rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm] - exacts[or_not_of_imp h₁, not_or_of_imp h₂] + exacts [or_not_of_imp h₁, not_or_of_imp h₂] #align ennreal.inv_le_iff_le_mul ENNReal.inv_le_iff_le_mul @[simp 900] @@ -1752,7 +1752,7 @@ protected theorem half_lt_self (hz : a ≠ 0) (ht : a ≠ ∞) : a / 2 < a := by lift a to ℝ≥0 using ht rw [coe_ne_zero] at hz rw [← coe_two, ← coe_div, coe_lt_coe] - exacts[NNReal.half_lt_self hz, two_ne_zero' _] + exacts [NNReal.half_lt_self hz, two_ne_zero' _] #align ennreal.half_lt_self ENNReal.half_lt_self protected theorem half_le_self : a / 2 ≤ a := diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean index cd87fa090d854..d31e23573b063 100644 --- a/Mathlib/Data/Real/Sqrt.lean +++ b/Mathlib/Data/Real/Sqrt.lean @@ -213,7 +213,7 @@ theorem sqrt_eq_cases : sqrt x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 · exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩ · exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩ · rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩) - exacts[sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le] + exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le] #align real.sqrt_eq_cases Real.sqrt_eq_cases theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x = y ↔ y * y = x := diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean index a7bfedcbd5722..27074d4a0f1c2 100644 --- a/Mathlib/Data/Seq/Computation.lean +++ b/Mathlib/Data/Seq/Computation.lean @@ -332,7 +332,7 @@ instance : Membership α (Computation α) := theorem le_stable (s : Computation α) {a m n} (h : m ≤ n) : s.1 m = some a → s.1 n = some a := by cases' s with f al induction' h with n _ IH - exacts[id, fun h2 => al (IH h2)] + exacts [id, fun h2 => al (IH h2)] #align computation.le_stable Computation.le_stable theorem mem_unique {s : Computation α} {a b : α} : a ∈ s → b ∈ s → a = b @@ -635,7 +635,7 @@ def memRecOn {C : Computation α → Sort v} {a s} (M : a ∈ s) (h1 : C (pure a haveI T := terminates_of_mem M rw [eq_thinkN' s, get_eq_of_mem s M] generalize length s = n - induction' n with n IH; exacts[h1, h2 _ IH] + induction' n with n IH; exacts [h1, h2 _ IH] #align computation.mem_rec_on Computation.memRecOn /-- Recursor based on assertion of `Terminates`-/ diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean index 974fddb8471de..3db661b361d7c 100644 --- a/Mathlib/Data/Seq/Seq.lean +++ b/Mathlib/Data/Seq/Seq.lean @@ -166,7 +166,7 @@ instance : Membership α (Seq α) := theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? n = none := by cases' s with f al induction' h with n _ IH - exacts[id, fun h2 => al (IH h2)] + exacts [id, fun h2 => al (IH h2)] #align stream.seq.le_stable Stream'.Seq.le_stable /-- If a sequence terminated at position `n`, it also terminated at `m ≥ n `. -/ @@ -216,7 +216,7 @@ theorem destruct_eq_nil {s : Seq α} : destruct s = none → s = nil := by · apply Subtype.eq funext n induction' n with n IH - exacts[f0, s.2 IH] + exacts [f0, s.2 IH] · contradiction #align stream.seq.destruct_eq_nil Stream'.Seq.destruct_eq_nil diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index c10fae94ddf1c..3e288ae234965 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1162,7 +1162,7 @@ theorem insert_subset_insert (h : s ⊆ t) : insert a s ⊆ insert a t := fun _ theorem insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t := by refine' ⟨fun h x hx => _, insert_subset_insert⟩ rcases h (subset_insert _ _ hx) with (rfl | hxt) - exacts[(ha hx).elim, hxt] + exacts [(ha hx).elim, hxt] #align set.insert_subset_insert_iff Set.insert_subset_insert_iff theorem subset_insert_iff_of_not_mem (ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t := diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index 803867f1c7e48..ec12fade98aba 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -143,7 +143,7 @@ theorem preimage_const_of_not_mem {b : β} {s : Set β} (h : b ∉ s) : (fun _ : theorem preimage_const (b : β) (s : Set β) [Decidable (b ∈ s)] : (fun _ : α => b) ⁻¹' s = if b ∈ s then univ else ∅ := by split_ifs with hb - exacts[preimage_const_of_mem hb, preimage_const_of_not_mem hb] + exacts [preimage_const_of_mem hb, preimage_const_of_not_mem hb] #align set.preimage_const Set.preimage_const theorem preimage_comp {s : Set γ} : g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s) := @@ -1498,7 +1498,7 @@ theorem injective_iff {α β} {f : Option α → β} : refine' ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, _⟩ rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab - exacts[rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)] + exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)] #align option.injective_iff Option.injective_iff theorem range_eq {α β} (f : Option α → β) : range f = insert (f none) (range (f ∘ some)) := diff --git a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean index 6755796207437..8a22ee3c6f3cd 100644 --- a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean +++ b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean @@ -225,7 +225,7 @@ lemma monotone_or_antitone_iff_uIcc : Monotone f ∨ Antitone f ↔ ∀ a b c, c ∈ [[a, b]] → f c ∈ [[f a, f b]] := by constructor · rintro (hf | hf) a b c <;> simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max] - exacts[fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩] + exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩] contrapose! rw [not_monotone_not_antitone_iff_exists_le_le] rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩ diff --git a/Mathlib/Data/Sum/Order.lean b/Mathlib/Data/Sum/Order.lean index 4422bac3214ce..7dd62745c0499 100644 --- a/Mathlib/Data/Sum/Order.lean +++ b/Mathlib/Data/Sum/Order.lean @@ -75,7 +75,7 @@ variable (r : α → α → Prop) (s : β → β → Prop) instance [IsRefl α r] [IsRefl β s] : IsRefl (Sum α β) (Lex r s) := ⟨by rintro (a | a) - exacts[Lex.inl (refl _), Lex.inr (refl _)]⟩ + exacts [Lex.inl (refl _), Lex.inr (refl _)]⟩ instance [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (Sum α β) (Lex r s) := ⟨by rintro _ (⟨h⟩ | ⟨h⟩) <;> exact irrefl _ h⟩ @@ -83,7 +83,7 @@ instance [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (Sum α β) (Lex r s) := instance [IsTrans α r] [IsTrans β s] : IsTrans (Sum α β) (Lex r s) := ⟨by rintro _ _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hbc⟩ | ⟨hbc⟩) - exacts[.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]⟩ + exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]⟩ instance [IsAntisymm α r] [IsAntisymm β s] : IsAntisymm (Sum α β) (Lex r s) := ⟨by rintro _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hba⟩ | ⟨hba⟩) <;> rw [antisymm hab hba]⟩ diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean index 7dc3e388aa794..a160fb03bea18 100644 --- a/Mathlib/Data/Sym/Sym2.lean +++ b/Mathlib/Data/Sym/Sym2.lean @@ -183,7 +183,7 @@ def lift : { f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ } toFun f := Quotient.lift (uncurry ↑f) <| by rintro _ _ ⟨⟩ - exacts[rfl, f.prop _ _] + exacts [rfl, f.prop _ _] invFun F := ⟨curry (F ∘ Quotient.mk''), fun a₁ a₂ => congr_arg F eq_swap⟩ left_inv f := Subtype.ext rfl right_inv F := funext <| Sym2.ind fun x y => rfl @@ -211,11 +211,11 @@ def lift₂ : Quotient.lift₂ (fun (a : α × α) (b : β × β) => f.1 a.1 a.2 b.1 b.2) (by rintro _ _ _ _ ⟨⟩ ⟨⟩ - exacts[rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]) + exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]) invFun F := ⟨fun a₁ a₂ b₁ b₂ => F ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧, fun a₁ a₂ b₁ b₂ => by constructor - exacts[congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]⟩ + exacts [congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]⟩ left_inv f := Subtype.ext rfl right_inv F := funext₂ fun a b => Sym2.inductionOn₂ a b fun _ _ _ _ => rfl #align sym2.lift₂ Sym2.lift₂ diff --git a/Mathlib/Data/Vector3.lean b/Mathlib/Data/Vector3.lean index 8592fd3696d20..a7c8a66772aee 100644 --- a/Mathlib/Data/Vector3.lean +++ b/Mathlib/Data/Vector3.lean @@ -287,7 +287,7 @@ theorem vectorAllP_iff_forall (p : α → Prop) (v : Vector3 α n) : (and_congr_right fun _ => IH).trans ⟨fun ⟨pa, h⟩ i => by refine' i.cases' _ _ - exacts[pa, h], fun h => ⟨_, fun i => _⟩⟩ + exacts [pa, h], fun h => ⟨_, fun i => _⟩⟩ · have h0 := h fz simp at h0 exact h0 diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index edf497ddcb334..bf2bbc89ca6a5 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/Mathlib/Data/ZMod/Basic.lean @@ -947,7 +947,7 @@ theorem valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) : a.valMinAbs * 2 = n apply iff_of_false _ (mt _ h) · intro he rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h - exacts[h (Nat.cast_nonneg _), zero_lt_two] + exacts [h (Nat.cast_nonneg _), zero_lt_two] · rw [mul_comm] exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le #align zmod.val_min_abs_mul_two_eq_iff ZMod.valMinAbs_mul_two_eq_iff @@ -956,7 +956,7 @@ theorem valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n := by simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]; split_ifs with h · refine' ⟨(neg_lt_zero.2 <| by exact_mod_cast NeZero.pos n).trans_le (mul_nonneg _ _), h⟩ - exacts[Nat.cast_nonneg _, zero_le_two] + exacts [Nat.cast_nonneg _, zero_le_two] · refine' ⟨_, le_trans (mul_nonpos_of_nonpos_of_nonneg _ zero_le_two) <| Nat.cast_nonneg _⟩ · linarith only [h] · rw [sub_nonpos, Int.ofNat_le] diff --git a/Mathlib/Dynamics/Minimal.lean b/Mathlib/Dynamics/Minimal.lean index 3715eeb5b3e4f..ad1de5c46371e 100644 --- a/Mathlib/Dynamics/Minimal.lean +++ b/Mathlib/Dynamics/Minimal.lean @@ -125,7 +125,7 @@ theorem isMinimal_iff_closed_smul_invariant [ContinuousConstSMul M α] : · intro _ _ exact eq_empty_or_univ_of_smul_invariant_closed M refine' fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ _ _).resolve_left _⟩ - exacts[isClosed_closure, fun _ ↦ smul_closure_orbit_subset _ _, + exacts [isClosed_closure, fun _ ↦ smul_closure_orbit_subset _ _, (orbit_nonempty _).closure.ne_empty] #align is_minimal_iff_closed_smul_invariant isMinimal_iff_closed_smul_invariant #align is_minimal_iff_closed_vadd_invariant isMinimal_iff_closed_vadd_invariant diff --git a/Mathlib/Dynamics/OmegaLimit.lean b/Mathlib/Dynamics/OmegaLimit.lean index 80d557dba79f8..2bf85745b8360 100644 --- a/Mathlib/Dynamics/OmegaLimit.lean +++ b/Mathlib/Dynamics/OmegaLimit.lean @@ -182,10 +182,10 @@ theorem omegaLimit_union : ω f ϕ (s₁ ∪ s₂) = ω f ϕ s₁ ∪ ω f ϕ s simp only [not_frequently, not_nonempty_iff_eq_empty, ← subset_empty_iff] rintro ⟨⟨n₁, hn₁, h₁⟩, ⟨n₂, hn₂, h₂⟩⟩ refine' ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ _, h₂.mono fun t ↦ _⟩ - exacts[Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_left _ _, + exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_left _ _, Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_right _ _] · rintro (hy | hy) - exacts[omegaLimit_mono_right _ _ (subset_union_left _ _) hy, + exacts [omegaLimit_mono_right _ _ (subset_union_left _ _) hy, omegaLimit_mono_right _ _ (subset_union_right _ _) hy] #align omega_limit_union omegaLimit_union diff --git a/Mathlib/Geometry/Euclidean/Sphere/Power.lean b/Mathlib/Geometry/Euclidean/Sphere/Power.lean index d3fbbbb6c952f..c72145f14994b 100644 --- a/Mathlib/Geometry/Euclidean/Sphere/Power.lean +++ b/Mathlib/Geometry/Euclidean/Sphere/Power.lean @@ -129,7 +129,7 @@ theorem mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero {a b c d p : P} obtain ⟨-, k₂, -, hcd₁⟩ := angle_eq_zero_iff.mp hcpd refine' mul_dist_eq_mul_dist_of_cospherical h ⟨k₁, _, hab₁⟩ ⟨k₂, _, hcd₁⟩ <;> by_contra hnot <;> simp_all only [Classical.not_not, one_smul] - exacts[hab (vsub_left_cancel hab₁).symm, hcd (vsub_left_cancel hcd₁).symm] + exacts [hab (vsub_left_cancel hab₁).symm, hcd (vsub_left_cancel hcd₁).symm] #align euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero end EuclideanGeometry diff --git a/Mathlib/GroupTheory/GroupAction/Option.lean b/Mathlib/GroupTheory/GroupAction/Option.lean index 49aded3aecae0..09f764a9e853f 100644 --- a/Mathlib/GroupTheory/GroupAction/Option.lean +++ b/Mathlib/GroupTheory/GroupAction/Option.lean @@ -59,7 +59,7 @@ theorem smul_some : a • some b = some (a • b) := instance [SMul M N] [IsScalarTower M N α] : IsScalarTower M N (Option α) := ⟨fun a b x => by cases x - exacts[rfl, congr_arg some (smul_assoc _ _ _)]⟩ + exacts [rfl, congr_arg some (smul_assoc _ _ _)]⟩ @[to_additive] instance [SMulCommClass M N α] : SMulCommClass M N (Option α) := @@ -69,7 +69,7 @@ instance [SMulCommClass M N α] : SMulCommClass M N (Option α) := instance [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M (Option α) := ⟨fun a x => by cases x - exacts[rfl, congr_arg some (op_smul_eq_smul _ _)]⟩ + exacts [rfl, congr_arg some (op_smul_eq_smul _ _)]⟩ @[to_additive] instance [FaithfulSMul M α] : FaithfulSMul M (Option α) := @@ -82,9 +82,9 @@ instance [Monoid M] [MulAction M α] : smul := (· • ·) one_smul b := by cases b - exacts[rfl, congr_arg some (one_smul _ _)] + exacts [rfl, congr_arg some (one_smul _ _)] mul_smul a₁ a₂ b := by cases b - exacts[rfl, congr_arg some (mul_smul _ _ _)] + exacts [rfl, congr_arg some (mul_smul _ _ _)] end Option diff --git a/Mathlib/GroupTheory/GroupAction/Sum.lean b/Mathlib/GroupTheory/GroupAction/Sum.lean index 3822517f90985..5ceea45ebcd91 100644 --- a/Mathlib/GroupTheory/GroupAction/Sum.lean +++ b/Mathlib/GroupTheory/GroupAction/Sum.lean @@ -63,20 +63,20 @@ theorem smul_swap : (a • x).swap = a • x.swap := by cases x <;> rfl instance [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] : IsScalarTower M N (Sum α β) := ⟨fun a b x => by cases x - exacts[congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]⟩ + exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]⟩ @[to_additive] instance [SMulCommClass M N α] [SMulCommClass M N β] : SMulCommClass M N (Sum α β) := ⟨fun a b x => by cases x - exacts[congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]⟩ + exacts [congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]⟩ @[to_additive] instance [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] : IsCentralScalar M (Sum α β) := ⟨fun a x => by cases x - exacts[congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]⟩ + exacts [congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]⟩ @[to_additive] instance FaithfulSMulLeft [FaithfulSMul M α] : FaithfulSMul M (Sum α β) := @@ -99,9 +99,9 @@ instance {m : Monoid M} [MulAction M α] [MulAction M β] : β) where mul_smul a b x := by cases x - exacts[congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)] + exacts [congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)] one_smul x := by cases x - exacts[congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)] + exacts [congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)] end Sum diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index 0860f12cf8d97..c5e50f9621e0a 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -438,7 +438,7 @@ theorem orderOf_mul_eq_right_of_forall_prime_mul_dvd (hy : IsOfFinOrder y) rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff hpy] refine' (orderOf_dvd_lcm_mul h).trans (lcm_dvd ((dvd_div_iff hpy).2 _) hd) by_cases h : p ∣ orderOf x - exacts[hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy] + exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy] #align commute.order_of_mul_eq_right_of_forall_prime_mul_dvd Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd #align add_commute.add_order_of_add_eq_right_of_forall_prime_mul_dvd AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 2495356baefea..11df6c1d7e952 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/Mathlib/GroupTheory/Subgroup/Basic.lean @@ -3159,7 +3159,7 @@ theorem sup_subgroupOf_eq {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) : theorem codisjoint_subgroupOf_sup (H K : Subgroup G) : Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)) := by rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self] - exacts[le_sup_left, le_sup_right] + exacts [le_sup_left, le_sup_right] #align subgroup.codisjoint_subgroup_of_sup Subgroup.codisjoint_subgroupOf_sup #align add_subgroup.codisjoint_add_subgroup_of_sup AddSubgroup.codisjoint_addSubgroupOf_sup diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index f745d0d1055a2..da2267710f3ed 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -362,7 +362,7 @@ theorem linearIndependent_comp_subtype {s : Set ι} : intros assumption · rwa [Finsupp.embDomain_eq_mapDomain, Finsupp.sum_mapDomain_index] - exacts[fun _ => zero_smul _ _, fun _ _ _ => add_smul _ _ _] + exacts [fun _ => zero_smul _ _, fun _ _ _ => add_smul _ _ _] #align linear_independent_comp_subtype linearIndependent_comp_subtype theorem linearDependent_comp_subtype' {s : Set ι} : diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean index bf2dddd5a142d..ba2b1cd444ca4 100644 --- a/Mathlib/Logic/Encodable/Basic.lean +++ b/Mathlib/Logic/Encodable/Basic.lean @@ -333,7 +333,7 @@ theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none := by rfl have : 1 ≤ n / 2 := by rw [Nat.le_div_iff_mul_le] - exacts[h, by decide] + exacts [h, by decide] cases' exists_eq_succ_of_ne_zero (_root_.ne_of_gt this) with m e simp [decodeSum, div2_val]; cases bodd n <;> simp [e] #align encodable.decode_ge_two Encodable.decode_ge_two diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index a6b1fcc4ff7fb..ba1a72a333c26 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/Mathlib/Logic/Equiv/Basic.lean @@ -1315,7 +1315,7 @@ def piSplitAt {α : Type _} [DecidableEq α] (i : α) (β : α → Type _) : invFun f j := if h : j = i then h.symm.rec f.1 else f.2 ⟨j, h⟩ right_inv f := by ext x - exacts[dif_pos rfl, (dif_neg x.2).trans (by cases x; rfl)] + exacts [dif_pos rfl, (dif_neg x.2).trans (by cases x; rfl)] left_inv f := by ext x dsimp only diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean index e892313efb4c8..3b011e7ad24e5 100644 --- a/Mathlib/Logic/Equiv/Set.lean +++ b/Mathlib/Logic/Equiv/Set.lean @@ -404,7 +404,7 @@ protected def unionSumInter {α : Type u} (s t : Set α) [DecidablePred (· ∈ sumCongr (Equiv.refl _) (by refine' (Set.union' (· ∉ s) _ _).symm - exacts[fun x hx => hx.2, fun x hx => not_not_intro hx.1]) + exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]) _ ≃ Sum s t := by { rw [(_ : t \ s ∪ s ∩ t = t)] rw [union_comm, inter_comm, inter_union_diff] } diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean index 31fde735707b7..0156183ee0593 100644 --- a/Mathlib/Logic/Relation.lean +++ b/Mathlib/Logic/Relation.lean @@ -440,7 +440,7 @@ theorem _root_.Acc.TransGen (h : Acc r a) : Acc (TransGen r) a := by induction' h with x _ H refine' Acc.intro x fun y hy ↦ _ cases' hy with _ hyx z _ hyz hzx - exacts[H y hyx, (H z hzx).inv hyz] + exacts [H y hyx, (H z hzx).inv hyz] #align acc.trans_gen Acc.TransGen theorem _root_.acc_transGen_iff : Acc (TransGen r) a ↔ Acc r a := diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index 1adb80d7e1a17..334ddbc6c5c9c 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -720,7 +720,7 @@ theorem ext_of_Ioc' {α : Type _} [TopologicalSpace α] {m : MeasurableSpace α} (μ ν : Measure α) (hμ : ∀ ⦃a b⦄, a < b → μ (Ioc a b) ≠ ∞) (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) : μ = ν := by refine' @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν _ _ <;> intro a b hab <;> erw [dual_Ico (α := α)] - exacts[hμ hab, h hab] + exacts [hμ hab, h hab] #align measure_theory.measure.ext_of_Ioc' MeasureTheory.Measure.ext_of_Ioc' /-- Two measures which are finite on closed-open intervals are equal if the agree on all diff --git a/Mathlib/MeasureTheory/Covering/VitaliFamily.lean b/Mathlib/MeasureTheory/Covering/VitaliFamily.lean index 71e9b8709ea56..cc193696b6d1c 100644 --- a/Mathlib/MeasureTheory/Covering/VitaliFamily.lean +++ b/Mathlib/MeasureTheory/Covering/VitaliFamily.lean @@ -190,10 +190,10 @@ def enlarge (v : VitaliFamily μ) (δ : ℝ) (δpos : 0 < δ) : VitaliFamily μ setsAt x := v.setsAt x ∪ { a | MeasurableSet a ∧ (interior a).Nonempty ∧ ¬a ⊆ closedBall x δ } MeasurableSet' x a ha := by cases' ha with ha ha - exacts[v.MeasurableSet' _ _ ha, ha.1] + exacts [v.MeasurableSet' _ _ ha, ha.1] nonempty_interior x a ha := by cases' ha with ha ha - exacts[v.nonempty_interior _ _ ha, ha.2.1] + exacts [v.nonempty_interior _ _ ha, ha.2.1] Nontrivial := by intro x ε εpos rcases v.Nontrivial x ε εpos with ⟨a, ha, h'a⟩ diff --git a/Mathlib/MeasureTheory/Decomposition/Jordan.lean b/Mathlib/MeasureTheory/Decomposition/Jordan.lean index d7113674e01f1..31576e15a0cb7 100644 --- a/Mathlib/MeasureTheory/Decomposition/Jordan.lean +++ b/Mathlib/MeasureTheory/Decomposition/Jordan.lean @@ -543,7 +543,7 @@ theorem totalVariation_absolutelyContinuous_iff (s : SignedMeasure α) (μ : Mea refine' Measure.AbsolutelyContinuous.mk fun S _ hS₂ => _ have := h hS₂ rw [totalVariation, Measure.add_apply, add_eq_zero_iff] at this - exacts[this.1, this.2] + exacts [this.1, this.2] · refine' Measure.AbsolutelyContinuous.mk fun S _ hS₂ => _ rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero] #align measure_theory.signed_measure.total_variation_absolutely_continuous_iff MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff diff --git a/Mathlib/MeasureTheory/Group/Pointwise.lean b/Mathlib/MeasureTheory/Group/Pointwise.lean index 98eb950a7680f..bc1a0eb7d6ca4 100644 --- a/Mathlib/MeasureTheory/Group/Pointwise.lean +++ b/Mathlib/MeasureTheory/Group/Pointwise.lean @@ -44,5 +44,5 @@ theorem MeasurableSet.const_smul₀ {G₀ α : Type _} [GroupWithZero G₀] [Zer [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : G₀) : MeasurableSet (a • s) := by rcases eq_or_ne a 0 with (rfl | ha) - exacts[(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha] + exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha] #align measurable_set.const_smul₀ MeasurableSet.const_smul₀ diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index e6924617064cc..457e4aaa3cd98 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -1254,7 +1254,7 @@ theorem set_lintegral_max {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Me (∫⁻ x in s, max (f x) (g x) ∂μ) = (∫⁻ x in s ∩ { x | f x ≤ g x }, g x ∂μ) + ∫⁻ x in s ∩ { x | g x < f x }, f x ∂μ := by rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s] - exacts[measurableSet_lt hg hf, measurableSet_le hf hg] + exacts [measurableSet_lt hg hf, measurableSet_le hf hg] #align measure_theory.set_lintegral_max MeasureTheory.set_lintegral_max theorem lintegral_map {mβ : MeasurableSpace β} {f : β → ℝ≥0∞} {g : α → β} (hf : Measurable f) diff --git a/Mathlib/MeasureTheory/MeasurableSpaceDef.lean b/Mathlib/MeasureTheory/MeasurableSpaceDef.lean index 5deb538118f8d..0deb01e39b9f1 100644 --- a/Mathlib/MeasureTheory/MeasurableSpaceDef.lean +++ b/Mathlib/MeasureTheory/MeasurableSpaceDef.lean @@ -225,14 +225,14 @@ protected theorem MeasurableSet.ite {t s₁ s₂ : Set α} (ht : MeasurableSet t theorem MeasurableSet.ite' {s t : Set α} {p : Prop} (hs : p → MeasurableSet s) (ht : ¬p → MeasurableSet t) : MeasurableSet (ite p s t) := by split_ifs with h - exacts[hs h, ht h] + exacts [hs h, ht h] #align measurable_set.ite' MeasurableSet.ite' @[simp, measurability] protected theorem MeasurableSet.cond {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) {i : Bool} : MeasurableSet (cond i s₁ s₂) := by cases i - exacts[h₂, h₁] + exacts [h₂, h₁] #align measurable_set.cond MeasurableSet.cond @[simp, measurability] diff --git a/Mathlib/MeasureTheory/Measure/Complex.lean b/Mathlib/MeasureTheory/Measure/Complex.lean index 67fc90f1d8f42..8a6cab38f9180 100644 --- a/Mathlib/MeasureTheory/Measure/Complex.lean +++ b/Mathlib/MeasureTheory/Measure/Complex.lean @@ -122,7 +122,7 @@ theorem absolutelyContinuous_eNNReal_iff (c : ComplexMeasure α) (μ : VectorMea · constructor <;> · intro i hi; simp [h hi] · intro i hi rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)] - exacts[by simp, h.2 hi, h.1 hi] + exacts [by simp, h.2 hi, h.1 hi] #align measure_theory.complex_measure.absolutely_continuous_ennreal_iff MeasureTheory.ComplexMeasure.absolutelyContinuous_eNNReal_iff end ComplexMeasure diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index 1658ea8141a64..9d60607ae791c 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -1771,7 +1771,7 @@ theorem restrict_iUnion_apply_eq_iSup [Countable ι] {s : ι → Set α} (hd : D {t : Set α} (ht : MeasurableSet t) : μ.restrict (⋃ i, s i) t = ⨆ i, μ.restrict (s i) t := by simp only [restrict_apply ht, inter_iUnion] rw [measure_iUnion_eq_iSup] - exacts[hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _] + exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _] #align measure_theory.measure.restrict_Union_apply_eq_supr MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup /-- The restriction of the pushforward measure is the pushforward of the restriction. For a version diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean index 98f87b4564f18..383428651bb03 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean @@ -598,7 +598,7 @@ irreducible_def toMeasurable (μ : Measure α) (s : Set α) : Set α := theorem subset_toMeasurable (μ : Measure α) (s : Set α) : s ⊆ toMeasurable μ s := by rw [toMeasurable_def]; split_ifs with hs h's - exacts[hs.choose_spec.fst, h's.choose_spec.fst, (exists_measurable_superset μ s).choose_spec.1] + exacts [hs.choose_spec.fst, h's.choose_spec.fst, (exists_measurable_superset μ s).choose_spec.1] #align measure_theory.subset_to_measurable MeasureTheory.subset_toMeasurable theorem ae_le_toMeasurable : s ≤ᵐ[μ] toMeasurable μ s := diff --git a/Mathlib/MeasureTheory/Measure/NullMeasurable.lean b/Mathlib/MeasureTheory/Measure/NullMeasurable.lean index 6c8e66b191108..36c39b541a2d4 100644 --- a/Mathlib/MeasureTheory/Measure/NullMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/NullMeasurable.lean @@ -295,7 +295,7 @@ theorem measure_iUnion₀ [Countable ι] {f : ι → Set α} (hd : Pairwise (AED theorem measure_union₀_aux (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) : μ (s ∪ t) = μ s + μ t := by rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond] - exacts[(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs] + exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs] #align measure_theory.measure_union₀_aux MeasureTheory.measure_union₀_aux /-- A null measurable set `t` is Carathéodory measurable: for any `s`, we have diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean index d4df9f5b90889..7a82eed332bd5 100644 --- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean @@ -1729,7 +1729,7 @@ theorem exists_measurable_superset_forall_eq_trim {ι} [Countable ι] (μ : ι replace hst := subset_iInter hst replace ht := MeasurableSet.iInter ht refine' ⟨⋂ i, t i, hst, ht, fun i => le_antisymm _ _⟩ - exacts[hμt i ▸ (μ i).mono (iInter_subset _ _), (mono' _ hst).trans_eq ((μ i).trim_eq ht)] + exacts [hμt i ▸ (μ i).mono (iInter_subset _ _), (mono' _ hst).trans_eq ((μ i).trim_eq ht)] #align measure_theory.outer_measure.exists_measurable_superset_forall_eq_trim MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim /-- If `m₁ s = op (m₂ s) (m₃ s)` for all `s`, then the same is true for `m₁.trim`, `m₂.trim`, diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean index ee39b36e6ef2e..58ec7331f4c8e 100644 --- a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean @@ -188,7 +188,7 @@ theorem of_disjoint_iUnion [Countable β] {f : β → Set α} (hf₁ : ∀ i, Me theorem of_union {A B : Set α} (h : Disjoint A B) (hA : MeasurableSet A) (hB : MeasurableSet B) : v (A ∪ B) = v A + v B := by rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond] - exacts[fun b => Bool.casesOn b hB hA, pairwise_disjoint_on_bool.2 h] + exacts [fun b => Bool.casesOn b hB hA, pairwise_disjoint_on_bool.2 h] #align measure_theory.vector_measure.of_union MeasureTheory.VectorMeasure.of_union theorem of_add_of_diff {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) : @@ -424,10 +424,10 @@ def toSignedMeasure (μ : Measure α) [hμ : IsFiniteMeasure μ] : SignedMeasure · refine' @summable_of_nonneg_of_le _ (ENNReal.toReal ∘ μ ∘ f) _ _ _ _ · intro split_ifs - exacts[ENNReal.toReal_nonneg, le_rfl] + exacts [ENNReal.toReal_nonneg, le_rfl] · intro split_ifs - exacts[le_rfl, ENNReal.toReal_nonneg] + exacts [le_rfl, ENNReal.toReal_nonneg] exact summable_measure_toReal hf₁ hf₂ · intro a ha apply ne_of_lt hμ.measure_univ_lt_top @@ -1224,7 +1224,7 @@ theorem add_left [T2Space N] [ContinuousAdd M] (h₁ : v₁ ⟂ᵥ w) (h₂ : v · by_cases hxu' : x ∈ uᶜ · exact Or.inl ⟨hxu', hx⟩ rcases ht hx with (hxu | hxv) - exacts[False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩] + exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩] · cases' hx with hx hx <;> exact hx.2 #align measure_theory.vector_measure.mutually_singular.add_left MeasureTheory.VectorMeasure.MutuallySingular.add_left diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 3d2eeac9b7443..d42689d62fa7a 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -439,7 +439,7 @@ theorem isPiSystem_piiUnionInter (π : ι → Set (Set α)) (hpi : ∀ x, IsPiSy simp only [inf_eq_inter, mem_inter_iff, mem_iInter, Finset.mem_union] refine' ⟨fun h i _ => _, fun h => ⟨fun i hi1 => _, fun i hi2 => _⟩⟩ · split_ifs with h_1 h_2 h_2 - exacts[⟨h.1 i h_1, h.2 i h_2⟩, ⟨h.1 i h_1, Set.mem_univ _⟩, ⟨Set.mem_univ _, h.2 i h_2⟩, + exacts [⟨h.1 i h_1, h.2 i h_2⟩, ⟨h.1 i h_1, Set.mem_univ _⟩, ⟨Set.mem_univ _, h.2 i h_2⟩, ⟨Set.mem_univ _, Set.mem_univ _⟩] · specialize h i (Or.inl hi1) rw [if_pos hi1] at h diff --git a/Mathlib/Order/Compare.lean b/Mathlib/Order/Compare.lean index 4a76ae8b9f3bd..4e4b16d187956 100644 --- a/Mathlib/Order/Compare.lean +++ b/Mathlib/Order/Compare.lean @@ -157,14 +157,14 @@ open Ordering OrderDual theorem toDual_compares_toDual [LT α] {a b : α} {o : Ordering} : Compares o (toDual a) (toDual b) ↔ Compares o b a := by cases o - exacts[Iff.rfl, eq_comm, Iff.rfl] + exacts [Iff.rfl, eq_comm, Iff.rfl] #align to_dual_compares_to_dual toDual_compares_toDual @[simp] theorem ofDual_compares_ofDual [LT α] {a b : αᵒᵈ} {o : Ordering} : Compares o (ofDual a) (ofDual b) ↔ Compares o b a := by cases o - exacts[Iff.rfl, eq_comm, Iff.rfl] + exacts [Iff.rfl, eq_comm, Iff.rfl] #align of_dual_compares_of_dual ofDual_compares_ofDual theorem cmp_compares [LinearOrder α] (a b : α) : (cmp a b).Compares a b := by diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index 6a8c6b932ed6d..131bfd674fd73 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -169,7 +169,7 @@ theorem wcovby_iff_le_and_eq_or_eq : a ⩿ b ↔ a ≤ b ∧ ∀ c, a ≤ c → theorem Wcovby.le_and_le_iff (h : a ⩿ b) : a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b := by refine' ⟨fun h2 => h.eq_or_eq h2.1 h2.2, _⟩; rintro (rfl | rfl); - exacts[⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩] + exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩] #align wcovby.le_and_le_iff Wcovby.le_and_le_iff theorem Wcovby.Icc_eq (h : a ⩿ b) : Icc a b = {a, b} := by diff --git a/Mathlib/Order/Directed.lean b/Mathlib/Order/Directed.lean index 521f660bb71fa..8d2834279b784 100644 --- a/Mathlib/Order/Directed.lean +++ b/Mathlib/Order/Directed.lean @@ -300,7 +300,7 @@ variable (β) [PartialOrder β] theorem exists_lt_of_directed_ge [IsDirected β (· ≥ ·)] [Nontrivial β] : ∃ a b : β, a < b := by rcases exists_pair_ne β with ⟨a, b, hne⟩ rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩) - exacts[⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩] + exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩] #align exists_lt_of_directed_ge exists_lt_of_directed_ge theorem exists_lt_of_directed_le [IsDirected β (· ≤ ·)] [Nontrivial β] : ∃ a b : β, a < b := diff --git a/Mathlib/Order/Filter/CountableInter.lean b/Mathlib/Order/Filter/CountableInter.lean index ae1d05ab1c55c..2d0da22f60f04 100644 --- a/Mathlib/Order/Filter/CountableInter.lean +++ b/Mathlib/Order/Filter/CountableInter.lean @@ -198,7 +198,7 @@ instance countableInterFilter_inf (l₁ l₂ : Filter α) [CountableInterFilter instance countableInterFilter_sup (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] : CountableInterFilter (l₁ ⊔ l₂) := by refine' ⟨fun S hSc hS => ⟨_, _⟩⟩ <;> refine' (countable_sInter_mem hSc).2 fun s hs => _ - exacts[(hS s hs).1, (hS s hs).2] + exacts [(hS s hs).1, (hS s hs).2] #align countable_Inter_filter_sup countableInterFilter_sup namespace Filter diff --git a/Mathlib/Order/GameAdd.lean b/Mathlib/Order/GameAdd.lean index e86e84f1ad4b9..7e4312ec8f173 100644 --- a/Mathlib/Order/GameAdd.lean +++ b/Mathlib/Order/GameAdd.lean @@ -62,10 +62,10 @@ theorem gameAdd_iff {rα rβ} {x y : α × β} : GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 := by constructor · rintro (@⟨a₁, a₂, b, h⟩ | @⟨a, b₁, b₂, h⟩) - exacts[Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩] + exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩] · revert x y rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨h, rfl : b₁ = b₂⟩ | ⟨h, rfl : a₁ = a₂⟩) - exacts[GameAdd.fst h, GameAdd.snd h] + exacts [GameAdd.fst h, GameAdd.snd h] #align prod.game_add_iff Prod.gameAdd_iff theorem gameAdd_mk_iff {rα rβ} {a₁ a₂ : α} {b₁ b₂ : β} : @@ -106,7 +106,7 @@ theorem Acc.prod_gameAdd (ha : Acc rα a) (hb : Acc rβ b) : induction' hb with b hb ihb refine' Acc.intro _ fun h => _ rintro (⟨ra⟩ | ⟨rb⟩) - exacts[iha _ ra (Acc.intro b hb), ihb _ rb] + exacts [iha _ ra (Acc.intro b hb), ihb _ rb] #align acc.prod_game_add Acc.prod_gameAdd /-- The `Prod.GameAdd` relation on well-founded inputs is well-founded. diff --git a/Mathlib/Order/Iterate.lean b/Mathlib/Order/Iterate.lean index ad0746a2dea4a..acb73eead9f48 100644 --- a/Mathlib/Order/Iterate.lean +++ b/Mathlib/Order/Iterate.lean @@ -70,7 +70,7 @@ theorem seq_pos_lt_seq_of_le_of_lt (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h theorem seq_lt_seq_of_lt_of_le (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0) (hx : ∀ k < n, x (k + 1) < f (x k)) (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n < y n := by cases n - exacts[h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy] + exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy] #align monotone.seq_lt_seq_of_lt_of_le Monotone.seq_lt_seq_of_lt_of_le theorem seq_lt_seq_of_le_of_lt (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0) diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean index 009aac5ac1c42..b43cd6e90a7ea 100644 --- a/Mathlib/Order/Lattice.lean +++ b/Mathlib/Order/Lattice.lean @@ -902,7 +902,7 @@ theorem sup_eq_maxDefault [SemilatticeSup α] [DecidableRel ((· ≤ ·) : α ext (x y) unfold maxDefault split_ifs with h' - exacts[sup_of_le_right h', sup_of_le_left $ (total_of (· ≤ ·) x y).resolve_left h'] + exacts [sup_of_le_right h', sup_of_le_left $ (total_of (· ≤ ·) x y).resolve_left h'] #align sup_eq_max_default sup_eq_maxDefault theorem inf_eq_minDefault [SemilatticeInf α] [DecidableRel ((· ≤ ·) : α → α → Prop)] @@ -911,7 +911,7 @@ theorem inf_eq_minDefault [SemilatticeInf α] [DecidableRel ((· ≤ ·) : α ext (x y) unfold minDefault split_ifs with h' - exacts[inf_of_le_left h', inf_of_le_right $ (total_of (· ≤ ·) x y).resolve_left h'] + exacts [inf_of_le_left h', inf_of_le_right $ (total_of (· ≤ ·) x y).resolve_left h'] #align inf_eq_min_default inf_eq_minDefault /-- A lattice with total order is a linear order. diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean index e88a3cdff5ae7..a3a3ab60c1029 100644 --- a/Mathlib/Order/Monotone/Basic.lean +++ b/Mathlib/Order/Monotone/Basic.lean @@ -968,7 +968,7 @@ theorem Nat.rel_of_forall_rel_succ_of_le_of_lt (r : β → β → Prop) [IsTrans (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a ≤ b) (hbc : b < c) : r (f b) (f c) := by induction' hbc with k b_lt_k r_b_k - exacts[h _ hab, _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)] + exacts [h _ hab, _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)] #align nat.rel_of_forall_rel_succ_of_le_of_lt Nat.rel_of_forall_rel_succ_of_le_of_lt theorem Nat.rel_of_forall_rel_succ_of_le_of_le (r : β → β → Prop) [IsRefl β r] [IsTrans β r] diff --git a/Mathlib/Order/OrderIsoNat.lean b/Mathlib/Order/OrderIsoNat.lean index 0bc53daa5efb3..d01738bde616a 100644 --- a/Mathlib/Order/OrderIsoNat.lean +++ b/Mathlib/Order/OrderIsoNat.lean @@ -160,7 +160,7 @@ theorem exists_subseq_of_forall_mem_union {s t : Set α} (e : ℕ → α) (he : simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union, Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ] cases this - exacts[⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩, + exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩, ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩] #align nat.exists_subseq_of_forall_mem_union Nat.exists_subseq_of_forall_mem_union diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean index 428d3828dfd8e..1e22cc454ce0a 100644 --- a/Mathlib/Order/WellFoundedSet.lean +++ b/Mathlib/Order/WellFoundedSet.lean @@ -350,7 +350,7 @@ theorem PartiallyWellOrderedOn.exists_monotone_subseq (h : s.PartiallyWellOrdere obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f · refine' ⟨g, fun m n hle => _⟩ obtain hlt | rfl := hle.lt_or_eq - exacts[h1 m n hlt, refl_of r _] + exacts [h1 m n hlt, refl_of r _] · exfalso obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g) fun n => hf _ exact h2 m n hlt hle diff --git a/Mathlib/Probability/CondCount.lean b/Mathlib/Probability/CondCount.lean index 3a8059cdd2c18..0af9ed4d5dc37 100644 --- a/Mathlib/Probability/CondCount.lean +++ b/Mathlib/Probability/CondCount.lean @@ -160,7 +160,7 @@ theorem condCount_union (hs : s.Finite) (htu : Disjoint t u) : condCount s (t ∪ u) = condCount s t + condCount s u := by rw [condCount, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add] - exacts[htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet] + exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet] #align probability_theory.cond_count_union ProbabilityTheory.condCount_union theorem condCount_compl (t : Set Ω) (hs : s.Finite) (hs' : s.Nonempty) : @@ -186,7 +186,7 @@ theorem condCount_disjoint_union (hs : s.Finite) (ht : t.Finite) (hst : Disjoint ← mul_assoc] rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union, Set.union_inter_distrib_right, mul_comm] - exacts[hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet, + exacts [hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet, Measure.count_ne_zero ht', (Measure.count_apply_lt_top.2 ht).ne, Measure.count_ne_zero hs', (Measure.count_apply_lt_top.2 hs).ne] #align probability_theory.cond_count_disjoint_union ProbabilityTheory.condCount_disjoint_union diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean index acc13ba1c8db9..1d165d093a338 100644 --- a/Mathlib/RingTheory/Ideal/Basic.lean +++ b/Mathlib/RingTheory/Ideal/Basic.lean @@ -179,7 +179,7 @@ theorem span_singleton_le_iff_mem {x : α} : span {x} ≤ I ↔ x ∈ I := theorem span_singleton_mul_left_unit {a : α} (h2 : IsUnit a) (x : α) : span ({a * x} : Set α) = span {x} := by apply le_antisymm <;> rw [span_singleton_le_iff_mem, mem_span_singleton'] - exacts[⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩] + exacts [⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩] #align ideal.span_singleton_mul_left_unit Ideal.span_singleton_mul_left_unit theorem span_insert (x) (s : Set α) : span (insert x s) = span ({x} : Set α) ⊔ span s := @@ -577,7 +577,7 @@ theorem IsPrime.mul_mem_iff_mem_or_mem {I : Ideal α} (hI : I.IsPrime) : ∀ {x y : α}, x * y ∈ I ↔ x ∈ I ∨ y ∈ I := @fun x y => ⟨hI.mem_or_mem, by rintro (h | h) - exacts[I.mul_mem_right y h, I.mul_mem_left x h]⟩ + exacts [I.mul_mem_right y h, I.mul_mem_left x h]⟩ #align ideal.is_prime.mul_mem_iff_mem_or_mem Ideal.IsPrime.mul_mem_iff_mem_or_mem theorem IsPrime.pow_mem_iff_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) : diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index b8db5754d8148..a393b79ddabd6 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -153,7 +153,7 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) · refine' ⟨inferInstance, (Ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩ · refine' (Ideal.comap_mono hq').trans _ rw [Ideal.comap_map_of_surjective] - exacts[sup_le rfl.le this, Ideal.Quotient.mk_surjective] + exacts [sup_le rfl.le this, Ideal.Quotient.mk_surjective] #align ideal.exists_comap_eq_of_mem_minimal_primes Ideal.exists_comap_eq_of_mem_minimalPrimes theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index c91bb0af86b87..dd835396bc150 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -1127,7 +1127,7 @@ theorem subset_union_prime' {R : Type u} [CommRing R] {s : Finset ι} {f : ι have hiu : i ∉ u := mt Finset.mem_insert_of_mem hit have hn' : (insert i u).card = n := by rwa [Finset.card_insert_of_not_mem] at hn⊢ - exacts[hiu, hju] + exacts [hiu, hju] have h' : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ k ∈ (↑(insert i u) : Set ι), f k := by rw [Finset.coe_insert] at h ⊢ rw [Finset.coe_insert] at h diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean index b14be87290384..3608333cdfabd 100644 --- a/Mathlib/RingTheory/PrincipalIdealDomain.lean +++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean @@ -371,7 +371,7 @@ theorem span_gcd (x y : R) : span ({gcd x y} : Set R) = span ({x, y} : Set R) := · obtain ⟨r, s, rfl⟩ : ∃ r s, r * x + s * y = d := by rw [← Ideal.mem_span_pair, hd, Ideal.mem_span_singleton] apply dvd_add <;> apply dvd_mul_of_dvd_right - exacts[gcd_dvd_left x y, gcd_dvd_right x y] + exacts [gcd_dvd_left x y, gcd_dvd_right x y] #align span_gcd span_gcd theorem gcd_dvd_iff_exists (a b : R) {z} : gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y := by diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean index ca5d8a00e0530..c4b8c274f3547 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean @@ -128,7 +128,7 @@ theorem not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) : classical refine' ⟨(f.erase b).cons (b * u), fun a ha => _, _, Multiset.cons_ne_zero⟩ · obtain rfl | ha := Multiset.mem_cons.1 ha - exacts[Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)] + exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)] · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm], fun ⟨f, hi, he, hne⟩ => let ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero hne diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 2edf99e2fa730..628d4a7ac0fb9 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -2248,7 +2248,7 @@ theorem mk_eq_two_iff' (x : α) : (#α) = 2 ↔ ∃! y, y ≠ x := by · rintro ⟨a, b, hne, h⟩ simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h rcases h x with (rfl | rfl) - exacts[⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩] + exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩] · rintro ⟨y, hne, hy⟩ exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩ #align cardinal.mk_eq_two_iff' Cardinal.mk_eq_two_iff' diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index d3e4b1870a57c..8b75c316a4035 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Ordinal.lean @@ -1057,7 +1057,7 @@ theorem mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [Nonempty α] [ · rw [mk_finsupp_lift_of_fintype] have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β) rw [max_eq_right (le_trans _ this), power_nat_eq this] - exacts[Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le] + exacts [Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le] · apply mk_finsupp_lift_of_infinite #align cardinal.mk_finsupp_lift_of_infinite' Cardinal.mk_finsupp_lift_of_infinite' diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index 2210951f5ef75..c8fc1eb33157c 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -1009,7 +1009,7 @@ theorem HasSum.int_rec {b : α} {f g : ℕ → α} (hf : HasSum f a) (hg : HasSu rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩ · rw [codisjoint_iff_le_sup] rintro (i | j) _ - exacts[Or.inl ⟨_, rfl⟩, Or.inr ⟨_, rfl⟩] + exacts [Or.inl ⟨_, rfl⟩, Or.inr ⟨_, rfl⟩] exact HasSum.add_isCompl this (h₁.hasSum_range_iff.mpr hf) (h₂.hasSum_range_iff.mpr hg) #align has_sum.int_rec HasSum.int_rec diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean index 4d8802aad7e85..1ff38af18191d 100644 --- a/Mathlib/Topology/Algebra/Order/Compact.lean +++ b/Mathlib/Topology/Algebra/Order/Compact.lean @@ -275,7 +275,7 @@ theorem ContinuousOn.exists_isMinOn' {s : Set β} {f : β → α} (hf : Continuo ((hK.inter_right hsc).insert x₀).exists_forall_le (insert_nonempty _ _) (hf.mono hsub) refine' ⟨x, hsub hx, fun y hy => _⟩ by_cases hyK : y ∈ K - exacts[hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)] + exacts [hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)] /-- The **extreme value theorem**: if a function `f` is continuous on a closed set `s` and it is larger than a value in its image away from compact sets, then it has a minimum on this set. -/ diff --git a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean index 4b79dff2f235c..141d31d7a1e32 100644 --- a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean @@ -129,7 +129,7 @@ variable [ConditionallyCompleteLattice α] [SupConvergenceClass α] {f : ι → theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) : Tendsto f atTop (𝓝 (⨆ i, f i)) := by cases isEmpty_or_nonempty ι - exacts[tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)] + exacts [tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)] #align tendsto_at_top_csupr tendsto_atTop_ciSup theorem tendsto_atBot_ciSup (h_anti : Antitone f) (hbdd : BddAbove <| range f) : diff --git a/Mathlib/Topology/Algebra/Semigroup.lean b/Mathlib/Topology/Algebra/Semigroup.lean index 2534556bf399e..7d314fe640965 100644 --- a/Mathlib/Topology/Algebra/Semigroup.lean +++ b/Mathlib/Topology/Algebra/Semigroup.lean @@ -73,7 +73,7 @@ theorem exists_idempotent_of_compact_t2_of_continuous_mul_left {M} [Nonempty M] · simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq] exact Set.sInter_eq_iInter · refine' DirectedOn.directed_val (IsChain.directedOn hc.symm) - exacts[fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1] + exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1] · rw [Set.mem_sInter] exact fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht) #align exists_idempotent_of_compact_t2_of_continuous_mul_left exists_idempotent_of_compact_t2_of_continuous_mul_left diff --git a/Mathlib/Topology/Algebra/StarSubalgebra.lean b/Mathlib/Topology/Algebra/StarSubalgebra.lean index e9e0e5c0177ba..148249f5487d7 100644 --- a/Mathlib/Topology/Algebra/StarSubalgebra.lean +++ b/Mathlib/Topology/Algebra/StarSubalgebra.lean @@ -232,7 +232,7 @@ theorem starAlgHomClass_ext [T2Space B] {F : Type _} {a : A} (hψ : Continuous ψ) (h : φ ⟨a, self_mem R a⟩ = ψ ⟨a, self_mem R a⟩) : φ = ψ := by refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_ apply adjoin_induction' x ?_ ?_ ?_ ?_ ?_ - exacts[fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by + exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by simp only [AlgHomClass.commutes], fun x y hx hy => by simp only [map_add, hx, hy], fun x y hx hy => by simp only [map_mul, hx, hy], fun x hx => by simp only [map_star, hx]] #align elemental_star_algebra.star_alg_hom_class_ext elementalStarAlgebra.starAlgHomClass_ext diff --git a/Mathlib/Topology/Algebra/UniformRing.lean b/Mathlib/Topology/Algebra/UniformRing.lean index e61e21f1b3e88..ef66123883823 100644 --- a/Mathlib/Topology/Algebra/UniformRing.lean +++ b/Mathlib/Topology/Algebra/UniformRing.lean @@ -291,7 +291,7 @@ noncomputable def DenseInducing.extendRingHom {i : α →+* β} {f : α →+* γ toFun := (ue.denseInducing dr).extend f map_one' := by convert DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous 1 - exacts[i.map_one.symm, f.map_one.symm] + exacts [i.map_one.symm, f.map_one.symm] map_zero' := by convert DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous 0 <;> simp only [map_zero] diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index e37433d08fc32..88cd40769a68e 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -521,7 +521,7 @@ theorem Dense.exists_countable_dense_subset_bot_top {α : Type _} [TopologicalSp ∀ x, IsTop x → x ∈ s → x ∈ t := by rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩ refine' ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, _, _, _, _, _⟩ - exacts[inter_subset_right _ _, + exacts [inter_subset_right _ _, (htc.union ((countable_isBot α).union (countable_isTop α))).mono (inter_subset_left _ _), htd.mono (subset_inter (subset_union_left _ _) hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩, fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩] diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index bd14ed7d88cd3..42ac17e5545a4 100644 --- a/Mathlib/Topology/Basic.lean +++ b/Mathlib/Topology/Basic.lean @@ -1284,7 +1284,7 @@ of a sequence is closed. -/ theorem isClosed_setOf_clusterPt {f : Filter α} : IsClosed { x | ClusterPt x f } := by simp only [ClusterPt, inf_neBot_iff_frequently_left, setOf_forall, imp_iff_not_or] refine' isClosed_iInter fun p => IsClosed.union _ _ <;> apply isClosed_compl_iff.2 - exacts[isOpen_setOf_eventually_nhds, isOpen_const] + exacts [isOpen_setOf_eventually_nhds, isOpen_const] #align is_closed_set_of_cluster_pt isClosed_setOf_clusterPt theorem mem_closure_iff_clusterPt {s : Set α} {a : α} : a ∈ closure s ↔ ClusterPt a (𝓟 s) := diff --git a/Mathlib/Topology/Category/Compactum.lean b/Mathlib/Topology/Category/Compactum.lean index 046bd791345f1..8bd5e9e2c213b 100644 --- a/Mathlib/Topology/Category/Compactum.lean +++ b/Mathlib/Topology/Category/Compactum.lean @@ -185,7 +185,7 @@ theorem isClosed_iff {X : Compactum} (S : Set X) : · intro h1 F h2 specialize h1 F cases' F.mem_or_compl_mem S with h h - exacts[absurd (h1 h) h2, h] + exacts [absurd (h1 h) h2, h] #align Compactum.is_closed_iff Compactum.isClosed_iff instance {X : Compactum} : CompactSpace X := by @@ -212,7 +212,7 @@ private theorem basic_inter {X : Compactum} (A B : Set X) : basic (A ∩ B) = ba constructor · intro hG constructor <;> filter_upwards [hG]with _ - exacts[And.left, And.right] + exacts [And.left, And.right] · rintro ⟨h1, h2⟩ exact inter_mem h1 h2 -- Porting note: removed #align declaration since it is a private lemma diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean index 50c01f62560cc..6961eef0c6833 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Products.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Products.lean @@ -312,7 +312,7 @@ def binaryCofanIsColimit (X Y : TopCat.{u}) : IsColimit (TopCat.binaryCofan X Y) rfl · intro s m h₁ h₂ ext (x | x) - exacts[(ConcreteCategory.congr_hom h₁ x : _), (ConcreteCategory.congr_hom h₂ x : _)] + exacts [(ConcreteCategory.congr_hom h₁ x : _), (ConcreteCategory.congr_hom h₂ x : _)] #align Top.binary_cofan_is_colimit TopCat.binaryCofanIsColimit theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) : @@ -394,5 +394,3 @@ theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) : change m x = dite _ _ _ split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm #align Top.binary_cofan_is_colimit_iff TopCat.binaryCofan_isColimit_iff - - diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean index ce85d8fd8f2b3..ec1d8b9ce80b7 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean @@ -141,7 +141,7 @@ theorem pullbackIsoProdSubtype_hom_apply {f : X ⟶ Z} {g : Y ⟶ Z} ⟨⟨(pullback.fst : pullback f g ⟶ _) x, (pullback.snd : pullback f g ⟶ _) x⟩, by simpa using ConcreteCategory.congr_hom pullback.condition x⟩ := by apply Subtype.ext; apply Prod.ext - exacts[ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_fst f g) x, + exacts [ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_fst f g) x, ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_snd f g) x] #align Top.pullback_iso_prod_subtype_hom_apply TopCat.pullbackIsoProdSubtype_hom_apply diff --git a/Mathlib/Topology/FiberBundle/Basic.lean b/Mathlib/Topology/FiberBundle/Basic.lean index 21d0db5ba2f93..b7bcb62bbb0ba 100644 --- a/Mathlib/Topology/FiberBundle/Basic.lean +++ b/Mathlib/Topology/FiberBundle/Basic.lean @@ -392,7 +392,7 @@ theorem FiberBundle.exists_trivialization_Icc_subset [ConditionallyCompleteLinea (ec.restrOpen (Iio d) isOpen_Iio).disjointUnion (ed.restrOpen (Ioi c) isOpen_Ioi) (he.mono (inter_subset_right _ _) (inter_subset_right _ _)), fun x hx => _⟩ rcases hx.2.eq_or_lt with (rfl | hxd) - exacts[Or.inr ⟨hed, hdcb.1⟩, Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩] + exacts [Or.inr ⟨hed, hdcb.1⟩, Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩] · /- If `(c, d)` is nonempty, then take `d' ∈ (c, d)`. Since the base set of `ec` includes `[a, d)`, it includes `[a, d'] ⊆ [a, d)` as well. -/ rw [disjoint_left] at he diff --git a/Mathlib/Topology/Homotopy/HSpaces.lean b/Mathlib/Topology/Homotopy/HSpaces.lean index 674fc3c99e766..9a9a0f53172ad 100644 --- a/Mathlib/Topology/Homotopy/HSpaces.lean +++ b/Mathlib/Topology/Homotopy/HSpaces.lean @@ -101,7 +101,7 @@ instance HSpace.prod (X : Type u) (Y : Type v) [TopologicalSpace X] [Topological -- porting note: was `use ⟨G, hG⟩` refine ⟨⟨⟨G, hG⟩, ?_, ?_⟩, ?_⟩ · rintro ⟨x, y⟩ - exacts[Prod.mk.inj_iff.mpr ⟨HSpace.eHmul.1.2 x, HSpace.eHmul.1.2 y⟩] + exacts [Prod.mk.inj_iff.mpr ⟨HSpace.eHmul.1.2 x, HSpace.eHmul.1.2 y⟩] · rintro ⟨x, y⟩ exact Prod.mk.inj_iff.mpr ⟨HSpace.eHmul.1.3 x, HSpace.eHmul.1.3 y⟩ · rintro t ⟨x, y⟩ h @@ -121,7 +121,7 @@ instance HSpace.prod (X : Type u) (Y : Type v) [TopologicalSpace X] [Topological -- porting note: was `use ⟨G, hG⟩` refine ⟨⟨⟨G, hG⟩, ?_, ?_⟩, ?_⟩ · rintro ⟨x, y⟩ - exacts[Prod.mk.inj_iff.mpr ⟨HSpace.hmulE.1.2 x, HSpace.hmulE.1.2 y⟩] + exacts [Prod.mk.inj_iff.mpr ⟨HSpace.hmulE.1.2 x, HSpace.hmulE.1.2 y⟩] · rintro ⟨x, y⟩ exact Prod.mk.inj_iff.mpr ⟨HSpace.hmulE.1.3 x, HSpace.hmulE.1.3 y⟩ · rintro t ⟨x, y⟩ h @@ -258,7 +258,7 @@ theorem delayReflRight_zero (γ : Path x y) : delayReflRight 0 γ = γ.trans (Pa refl_apply] split_ifs with h; swap; conv_rhs => rw [← γ.target] all_goals apply congr_arg γ; ext1; rw [qRight_zero_right] - exacts[if_neg h, if_pos h] + exacts [if_neg h, if_pos h] #align path.delay_refl_right_zero Path.delayReflRight_zero theorem delayReflRight_one (γ : Path x y) : delayReflRight 1 γ = γ := by diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index 669461bb22eb7..0441e98868daa 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -80,7 +80,7 @@ theorem continuous_right_toIcoMod : ContinuousWithinAt (toIcoMod hp a) (Ici x) x · rintro ⟨h, h'⟩ apply hIs rw [← toIcoMod_sub_zsmul, (toIcoMod_eq_self _).2] - exacts[⟨h.1, h.2.2⟩, ⟨hd.1.trans (sub_le_sub_right h' _), h.2.1⟩] + exacts [⟨h.1, h.2.2⟩, ⟨hd.1.trans (sub_le_sub_right h' _), h.2.1⟩] #align continuous_right_to_Ico_mod continuous_right_toIcoMod theorem continuous_left_toIocMod : ContinuousWithinAt (toIocMod hp a) (Iic x) x := by @@ -473,7 +473,7 @@ def setAddOrderOfEquiv {n : ℕ} (hn : 0 < n) : rw [← @Nat.cast_inj ℤ, ← sub_eq_zero] refine' Int.eq_zero_of_abs_lt_dvd ⟨_, hm.symm⟩ (abs_sub_lt_iff.2 ⟨_, _⟩) <;> apply (Int.sub_le_self _ <| Nat.cast_nonneg _).trans_lt (Nat.cast_lt.2 _) - exacts[m₁.2.1, m₂.2.1] + exacts [m₁.2.1, m₂.2.1] obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2 exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩) #align add_circle.set_add_order_of_equiv AddCircle.setAddOrderOfEquiv diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index f5725dd766c87..b8b80b43b1366 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -1134,7 +1134,7 @@ theorem not_summable_iff_tendsto_nat_atTop {f : ℕ → ℝ≥0} : constructor · intro h refine' ((tendsto_of_monotone _).resolve_right h).comp _ - exacts[Finset.sum_mono_set _, tendsto_finset_range] + exacts [Finset.sum_mono_set _, tendsto_finset_range] · rintro hnat ⟨r, hr⟩ exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr) #align nnreal.not_summable_iff_tendsto_nat_at_top NNReal.not_summable_iff_tendsto_nat_atTop diff --git a/Mathlib/Topology/MetricSpace/Metrizable.lean b/Mathlib/Topology/MetricSpace/Metrizable.lean index 1ea09e98dc9c6..564e438d6fba7 100644 --- a/Mathlib/Topology/MetricSpace/Metrizable.lean +++ b/Mathlib/Topology/MetricSpace/Metrizable.lean @@ -226,7 +226,7 @@ theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f := exact (f UV).continuous.tendsto x (closedBall_mem_nhds _ δ0) refine' this.mono fun y hy => (BoundedContinuousFunction.dist_le δ0.le).2 fun UV => _ cases' le_total δ (ε UV) with hle hle - exacts[hy _ hle, (Real.dist_le_of_mem_Icc (hf0ε _ _) (hf0ε _ _)).trans (by rwa [sub_zero])] + exacts [hy _ hle, (Real.dist_le_of_mem_Icc (hf0ε _ _) (hf0ε _ _)).trans (by rwa [sub_zero])] #align topological_space.exists_embedding_l_infty TopologicalSpace.exists_embedding_l_infty /-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 7bed1d4d29b1d..33dd5b3e4e5a1 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -485,7 +485,7 @@ theorem t1Space_TFAE (α : Type u) [ TopologicalSpace α ] : tfae_have 1 → 4 · simp only [continuous_def, CofiniteTopology.isOpen_iff'] rintro H s (rfl | hs) - exacts[isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl] + exacts [isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl] tfae_have 4 → 2 · exact fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h tfae_have 2 ↔ 10 @@ -1803,7 +1803,7 @@ theorem normalSpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] · simp only [disjoint_left, mem_iUnion, mem_diff, not_exists, not_and, not_forall, not_not] rintro a ⟨u, huU, hau, haV⟩ v hvV hav cases' le_total (Encodable.encode u) (Encodable.encode v) with hle hle - exacts[⟨u, huU, hle, subset_closure hau⟩, (haV _ hvV hle <| subset_closure hav).elim] + exacts [⟨u, huU, hle, subset_closure hau⟩, (haV _ hvV hle <| subset_closure hav).elim] #align normal_space_of_t3_second_countable normalSpaceOfT3SecondCountable end Normality @@ -1858,7 +1858,7 @@ instance [T5Space α] : T5Space (SeparationQuotient α) where completely_normal s t hd₁ hd₂ := by rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet] apply T5Space.completely_normal <;> rw [← preimage_mk_closure] - exacts[hd₁.preimage mk, hd₂.preimage mk] + exacts [hd₁.preimage mk, hd₂.preimage mk] end CompletelyNormal diff --git a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean index 8168ca44f42a9..40a6a3c9cd54f 100644 --- a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean +++ b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean @@ -356,9 +356,9 @@ def interUnionPullbackConeLift : s.pt ⟶ F.1.obj (op (U ⊔ V)) := by rw [Opens.coe_iSup, Set.mem_iUnion] constructor · rintro (h | h) - exacts[⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩] + exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩] · rintro ⟨⟨_ | _⟩, h⟩ - exacts[Or.inl h, Or.inr h] + exacts [Or.inl h, Or.inr h] refine' (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.lift ⟨s.pt, @@ -412,9 +412,9 @@ def isLimitPullbackCone : IsLimit (interUnionPullbackCone F U V) := by rw [Opens.coe_iSup, Set.mem_iUnion] constructor · rintro (h | h) - exacts[⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩] + exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩] · rintro ⟨⟨_ | _⟩, h⟩ - exacts[Or.inl h, Or.inr h] + exacts [Or.inl h, Or.inr h] apply PullbackCone.isLimitAux' intro s use interUnionPullbackConeLift F U V s diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean index c8018045c7643..8a659c90aec1b 100644 --- a/Mathlib/Topology/Sheaves/Stalks.lean +++ b/Mathlib/Topology/Sheaves/Stalks.lean @@ -444,7 +444,7 @@ theorem stalkFunctor_map_injective_of_app_injective {F G : Presheaf C X} (f : F rw [← comp_apply, ← comp_apply, ← f.naturality, ← f.naturality, comp_apply, comp_apply] at heq replace heq := h W heq convert congr_arg (F.germ ⟨x, hxW⟩) heq using 1 - exacts[(F.germ_res_apply iWU₁ ⟨x, hxW⟩ s).symm, (F.germ_res_apply iWU₂ ⟨x, hxW⟩ t).symm] + exacts [(F.germ_res_apply iWU₁ ⟨x, hxW⟩ s).symm, (F.germ_res_apply iWU₂ ⟨x, hxW⟩ t).symm] set_option linter.uppercaseLean3 false in #align Top.presheaf.stalk_functor_map_injective_of_app_injective TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective diff --git a/Mathlib/Topology/SubsetProperties.lean b/Mathlib/Topology/SubsetProperties.lean index a2c40ebb68b27..3187f3a60eafa 100644 --- a/Mathlib/Topology/SubsetProperties.lean +++ b/Mathlib/Topology/SubsetProperties.lean @@ -379,7 +379,7 @@ theorem IsCompact.eventually_forall_of_forall_eventually {x₀ : α} {K : Set β · intro s t hs ht filter_upwards [hs, ht] rintro x h1 h2 y (hys | hyt) - exacts[h1 y hys, h2 y hyt] + exacts [h1 y hys, h2 y hyt] · intro y hyK specialize hP y hyK rw [nhds_prod_eq, eventually_prod_iff] at hP @@ -562,7 +562,7 @@ theorem Tendsto.isCompact_insert_range_of_cocompact {f : α → β} {b} have : f '' K ∈ l := by filter_upwards [htl, le_principal_iff.1 hle]with y hyt hyf rcases hyf with (rfl | ⟨x, rfl⟩) - exacts[(hd.le_bot ⟨mem_of_mem_nhds hsb, hyt⟩).elim, + exacts [(hd.le_bot ⟨mem_of_mem_nhds hsb, hyt⟩).elim, mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)] rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩ exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩ @@ -1667,7 +1667,7 @@ theorem continuous_boolIndicator_iff_clopen (U : Set X) : exact ⟨(isOpen_discrete _).preimage hc, (isClosed_discrete _).preimage hc⟩ · refine' fun hU => ⟨fun s _ => _⟩ rcases U.preimage_boolIndicator s with (h | h | h | h) <;> rw [h] - exacts[isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty] + exacts [isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty] #align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_clopen theorem continuousOn_boolIndicator_iff_clopen (s U : Set X) : @@ -1969,7 +1969,7 @@ theorem IsPreirreducible.subset_irreducible {S U Z : Set α} (hZ : IsPreirreduci · intro U H simp only [Finset.mem_insert, Finset.mem_singleton] at H rcases H with (rfl | rfl | rfl) - exacts[⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩] + exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩] replace ha' : a ∈ U ∧ a ∈ u ∧ a ∈ v := by simpa using ha' exact ⟨a, h₁ ha'.1, ha'.2⟩ #align is_preirreducible.subset_irreducible IsPreirreducible.subset_irreducible diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean index 0d61de1cc6446..d8c1382598749 100644 --- a/Mathlib/Topology/Support.lean +++ b/Mathlib/Topology/Support.lean @@ -181,7 +181,7 @@ theorem hasCompactMulSupport_iff_eventuallyEq : theorem HasCompactMulSupport.isCompact_range [TopologicalSpace β] (h : HasCompactMulSupport f) (hf : Continuous f) : IsCompact (range f) := by cases' range_eq_image_mulTSupport_or f with h2 h2 <;> rw [h2] - exacts[h.image hf, (h.image hf).insert 1] + exacts [h.image hf, (h.image hf).insert 1] #align has_compact_mul_support.is_compact_range HasCompactMulSupport.isCompact_range #align has_compact_support.is_compact_range HasCompactSupport.isCompact_range diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 5beb6b0f8cd77..c23c4b589346c 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -880,7 +880,7 @@ theorem nhds_nhds_eq_uniformity_uniformity_prod {a b : α} : 𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s : Set (α × α) => (𝓤 α).lift' fun t => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ t } := by rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift'] - exacts[rfl, monotone_preimage, monotone_preimage] + exacts [rfl, monotone_preimage, monotone_preimage] #align nhds_nhds_eq_uniformity_uniformity_prod nhds_nhds_eq_uniformity_uniformity_prod theorem nhds_eq_uniformity_prod {a b : α} : diff --git a/Mathlib/Topology/UniformSpace/Compact.lean b/Mathlib/Topology/UniformSpace/Compact.lean index 03c04029daddb..649b5d3f9094e 100644 --- a/Mathlib/Topology/UniformSpace/Compact.lean +++ b/Mathlib/Topology/UniformSpace/Compact.lean @@ -201,7 +201,7 @@ theorem IsCompact.uniformContinuousAt_of_continuousAt {r : Set (β × β)} {s : obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁) apply htr refine' ⟨f a, htsymm.mk_mem_comm.1 (hb _ _ _ haU _), hb _ _ _ haU _⟩ - exacts[mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha] + exacts [mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha] #align is_compact.uniform_continuous_at_of_continuous_at IsCompact.uniformContinuousAt_of_continuousAt theorem Continuous.uniformContinuous_of_tendsto_cocompact {f : α → β} {x : β} diff --git a/Mathlib/Topology/VectorBundle/Constructions.lean b/Mathlib/Topology/VectorBundle/Constructions.lean index 73b50df6a1614..b8d258ee0ed0e 100644 --- a/Mathlib/Topology/VectorBundle/Constructions.lean +++ b/Mathlib/Topology/VectorBundle/Constructions.lean @@ -145,7 +145,7 @@ instance VectorBundle.prod [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ show (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) = (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂) rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply'] - exacts[rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩] + exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩] #align vector_bundle.prod VectorBundle.prod variable {𝕜 F₁ E₁ F₂ E₂}