From ee18bf38f103b6c314be9e23f073eacb81e6872e Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 13 Mar 2024 11:52:17 +0000 Subject: [PATCH] chore: remove useless tactics (#11333) The removal of some pointless tactics flagged by #11308. --- Mathlib/AlgebraicTopology/SimplexCategory.lean | 2 -- Mathlib/CategoryTheory/Action.lean | 2 -- Mathlib/CategoryTheory/Adjunction/Reflective.lean | 1 - Mathlib/CategoryTheory/Closed/Cartesian.lean | 1 - .../CategoryTheory/ConcreteCategory/ReflectsIso.lean | 4 +--- Mathlib/CategoryTheory/EssentiallySmall.lean | 7 +------ Mathlib/CategoryTheory/Functor/Flat.lean | 5 ++--- Mathlib/CategoryTheory/Limits/FunctorCategory.lean | 4 ++-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean | 1 - Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean | 12 ++++-------- Mathlib/CategoryTheory/Types.lean | 1 - Mathlib/Computability/Halting.lean | 11 ++--------- Mathlib/Data/DFinsupp/Basic.lean | 5 +---- Mathlib/Data/Matrix/Basis.lean | 3 +-- Mathlib/Data/Ordmap/Ordset.lean | 2 +- Mathlib/Data/Seq/WSeq.lean | 3 +-- Mathlib/GroupTheory/Perm/Sign.lean | 1 - Mathlib/LinearAlgebra/LinearIndependent.lean | 3 +-- Mathlib/LinearAlgebra/Matrix/Symmetric.lean | 3 +-- Mathlib/SetTheory/Cardinal/Cofinality.lean | 5 ++--- Mathlib/SetTheory/Cardinal/Divisibility.lean | 3 ++- Mathlib/SetTheory/Cardinal/Ordinal.lean | 3 +-- Mathlib/SetTheory/Game/Basic.lean | 3 +-- Mathlib/SetTheory/Game/Short.lean | 4 +--- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 2 +- Mathlib/SetTheory/Ordinal/Basic.lean | 4 ++-- Mathlib/SetTheory/Ordinal/Notation.lean | 4 ++-- Mathlib/Topology/StoneCech.lean | 2 -- 28 files changed, 30 insertions(+), 71 deletions(-) diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean index 4032b060ebaaf..9f2b14d85f27d 100644 --- a/Mathlib/AlgebraicTopology/SimplexCategory.lean +++ b/Mathlib/AlgebraicTopology/SimplexCategory.lean @@ -752,8 +752,6 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ erw [Fin.predAbove_of_castSucc_lt _ _ (by rwa [Fin.castSucc_castPred])] dsimp [δ] rw [Fin.succAbove_of_le_castSucc i _] - -- This was not needed before leanprover/lean4#2644 - conv_rhs => dsimp erw [Fin.succ_pred] simpa only [Fin.le_iff_val_le_val, Fin.coe_castSucc, Fin.coe_pred] using Nat.le_sub_one_of_lt (Fin.lt_iff_val_lt_val.mp h') diff --git a/Mathlib/CategoryTheory/Action.lean b/Mathlib/CategoryTheory/Action.lean index 338e529b01d81..9d2c6dc848bcd 100644 --- a/Mathlib/CategoryTheory/Action.lean +++ b/Mathlib/CategoryTheory/Action.lean @@ -199,7 +199,6 @@ def curry (F : ActionCategory G X ⥤ SingleObj H) : G →* (X → H) ⋊[mulAut rfl { toFun := fun g => ⟨fun b => F.map (homOfPair b g), g⟩ map_one' := by - congr dsimp ext1 ext b @@ -207,7 +206,6 @@ def curry (F : ActionCategory G X ⥤ SingleObj H) : G →* (X → H) ⋊[mulAut rfl map_mul' := by intro g h - congr ext b exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g)) rfl } diff --git a/Mathlib/CategoryTheory/Adjunction/Reflective.lean b/Mathlib/CategoryTheory/Adjunction/Reflective.lean index 80cc2176eaa17..a30ac87046b22 100644 --- a/Mathlib/CategoryTheory/Adjunction/Reflective.lean +++ b/Mathlib/CategoryTheory/Adjunction/Reflective.lean @@ -97,7 +97,6 @@ theorem mem_essImage_of_unit_isSplitMono [Reflective i] {A : C} refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_ rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))] apply epi_comp (η.app (i.obj ((leftAdjoint i).obj A))) - skip haveI := isIso_of_epi_of_isSplitMono (η.app A) exact mem_essImage_of_unit_isIso A #align category_theory.mem_ess_image_of_unit_is_split_mono CategoryTheory.mem_essImage_of_unit_isSplitMono diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean index fa23c6602fe5f..36889277ff909 100644 --- a/Mathlib/CategoryTheory/Closed/Cartesian.lean +++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean @@ -433,7 +433,6 @@ def cartesianClosedOfEquiv (e : C ≌ D) [h : CartesianClosed C] : CartesianClos apply isoWhiskerRight e.counitIso (prod.functor.obj X ⋙ e.inverse ⋙ e.functor) ≪≫ _ change prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X apply isoWhiskerLeft (prod.functor.obj X) e.counitIso - skip apply Adjunction.leftAdjointOfNatIso this } #align category_theory.cartesian_closed_of_equiv CategoryTheory.cartesianClosedOfEquiv diff --git a/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean b/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean index 048f12f17c2be..437d4fbe8db4c 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean @@ -32,12 +32,10 @@ where `forget C` reflects isomorphisms, itself reflects isomorphisms. theorem reflectsIsomorphisms_forget₂ [HasForget₂ C D] [ReflectsIsomorphisms (forget C)] : ReflectsIsomorphisms (forget₂ C D) := { reflects := fun X Y f {i} => by - skip haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _ haveI : IsIso ((forget C).map f) := by have := @HasForget₂.forget_comp C D - rw [← this] - exact i' + rwa [← this] apply isIso_of_reflects_iso f (forget C) } #align category_theory.reflects_isomorphisms_forget₂ CategoryTheory.reflectsIsomorphisms_forget₂ diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean index 5d659410c66ec..0f66423aee2ae 100644 --- a/Mathlib/CategoryTheory/EssentiallySmall.lean +++ b/Mathlib/CategoryTheory/EssentiallySmall.lean @@ -72,10 +72,8 @@ theorem essentiallySmall_congr {C : Type u} [Category.{v} C] {D : Type u'} [Cate (e : C ≌ D) : EssentiallySmall.{w} C ↔ EssentiallySmall.{w} D := by fconstructor · rintro ⟨S, 𝒮, ⟨f⟩⟩ - skip exact EssentiallySmall.mk' (e.symm.trans f) · rintro ⟨S, 𝒮, ⟨f⟩⟩ - skip exact EssentiallySmall.mk' (e.trans f) #align category_theory.essentially_small_congr CategoryTheory.essentiallySmall_congr @@ -222,13 +220,10 @@ theorem essentiallySmall_iff (C : Type u) [Category.{v} C] : · intro h fconstructor · rcases h with ⟨S, 𝒮, ⟨e⟩⟩ - skip refine' ⟨⟨Skeleton S, ⟨_⟩⟩⟩ exact e.skeletonEquiv - · skip - infer_instance + · infer_instance · rintro ⟨⟨S, ⟨e⟩⟩, L⟩ - skip let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm letI : Category S := InducedCategory.category (e'.trans e).symm refine' ⟨⟨S, this, ⟨_⟩⟩⟩ diff --git a/Mathlib/CategoryTheory/Functor/Flat.lean b/Mathlib/CategoryTheory/Functor/Flat.lean index 38328621f39fd..0b09f68d6f854 100644 --- a/Mathlib/CategoryTheory/Functor/Flat.lean +++ b/Mathlib/CategoryTheory/Functor/Flat.lean @@ -314,7 +314,7 @@ variable [PreservesLimits (forget E)] noncomputable instance lanPreservesFiniteLimitsOfFlat (F : C ⥤ D) [RepresentablyFlat F] : PreservesFiniteLimits (lan F.op : _ ⥤ Dᵒᵖ ⥤ E) := by apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁} - intro J _ _; skip + intro J _ _ apply preservesLimitsOfShapeOfEvaluation (lan F.op : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J intro K haveI : IsFiltered (CostructuredArrow F.op K) := @@ -341,11 +341,10 @@ set_option linter.uppercaseLean3 false in theorem flat_iff_lan_flat (F : C ⥤ D) : RepresentablyFlat F ↔ RepresentablyFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁) := ⟨fun H => inferInstance, fun H => by - skip haveI := preservesFiniteLimitsOfFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁) haveI : PreservesFiniteLimits F := by apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁} - intros; skip; apply preservesLimitOfLanPreservesLimit + intros; apply preservesLimitOfLanPreservesLimit apply flat_of_preservesFiniteLimits⟩ set_option linter.uppercaseLean3 false in #align category_theory.flat_iff_Lan_flat CategoryTheory.flat_iff_lan_flat diff --git a/Mathlib/CategoryTheory/Limits/FunctorCategory.lean b/Mathlib/CategoryTheory/Limits/FunctorCategory.lean index bf81e69df7daf..7c62b7d4675fb 100644 --- a/Mathlib/CategoryTheory/Limits/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Limits/FunctorCategory.lean @@ -321,7 +321,7 @@ theorem colimit_obj_ext {H : J ⥤ K ⥤ C} [HasColimitsOfShape J C] {k : K} {W instance evaluationPreservesLimits [HasLimits C] (k : K) : PreservesLimits ((evaluation K C).obj k) where - preservesLimitsOfShape {J} 𝒥 := by skip; infer_instance + preservesLimitsOfShape {_} _𝒥 := inferInstance #align category_theory.limits.evaluation_preserves_limits CategoryTheory.Limits.evaluationPreservesLimits /-- `F : D ⥤ K ⥤ C` preserves the limit of some `G : J ⥤ D` if it does for each `k : K`. -/ @@ -358,7 +358,7 @@ instance preservesLimitsConst : PreservesLimitsOfSize.{w', w} (const D : C ⥤ _ instance evaluationPreservesColimits [HasColimits C] (k : K) : PreservesColimits ((evaluation K C).obj k) where - preservesColimitsOfShape := by skip; infer_instance + preservesColimitsOfShape := inferInstance #align category_theory.limits.evaluation_preserves_colimits CategoryTheory.Limits.evaluationPreservesColimits /-- `F : D ⥤ K ⥤ C` preserves the colimit of some `G : J ⥤ D` if it does for each `k : K`. -/ diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean index 1b0f60026af19..77082e3b817b1 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean @@ -465,7 +465,6 @@ instance [HasImage f] [∀ {Z : C} (g h : image f ⟶ Z), HasLimit (parallelPair theorem epi_image_of_epi {X Y : C} (f : X ⟶ Y) [HasImage f] [E : Epi f] : Epi (image.ι f) := by rw [← image.fac f] at E - skip exact epi_of_epi (factorThruImage f) (image.ι f) #align category_theory.limits.epi_image_of_epi CategoryTheory.Limits.epi_image_of_epi diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean index 730f78f368121..4eaa8e5cf8a8c 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean @@ -423,10 +423,8 @@ theorem kernel_not_epi_of_nonzero (w : f ≠ 0) : ¬Epi (kernel.ι f) := fun _ = w (eq_zero_of_epi_kernel f) #align category_theory.limits.kernel_not_epi_of_nonzero CategoryTheory.Limits.kernel_not_epi_of_nonzero -theorem kernel_not_iso_of_nonzero (w : f ≠ 0) : IsIso (kernel.ι f) → False := fun I => - kernel_not_epi_of_nonzero w <| by - skip - infer_instance +theorem kernel_not_iso_of_nonzero (w : f ≠ 0) : IsIso (kernel.ι f) → False := fun _ => + kernel_not_epi_of_nonzero w inferInstance #align category_theory.limits.kernel_not_iso_of_nonzero CategoryTheory.Limits.kernel_not_iso_of_nonzero instance hasKernel_comp_mono {X Y Z : C} (f : X ⟶ Y) [HasKernel f] (g : Y ⟶ Z) [Mono g] : @@ -926,10 +924,8 @@ theorem cokernel_not_mono_of_nonzero (w : f ≠ 0) : ¬Mono (cokernel.π f) := f w (eq_zero_of_mono_cokernel f) #align category_theory.limits.cokernel_not_mono_of_nonzero CategoryTheory.Limits.cokernel_not_mono_of_nonzero -theorem cokernel_not_iso_of_nonzero (w : f ≠ 0) : IsIso (cokernel.π f) → False := fun I => - cokernel_not_mono_of_nonzero w <| by - skip - infer_instance +theorem cokernel_not_iso_of_nonzero (w : f ≠ 0) : IsIso (cokernel.π f) → False := fun _ => + cokernel_not_mono_of_nonzero w inferInstance #align category_theory.limits.cokernel_not_iso_of_nonzero CategoryTheory.Limits.cokernel_not_iso_of_nonzero -- TODO the remainder of this section has obvious generalizations to `HasCoequalizer f g`. diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean index 11ba117582696..2118f70f4640d 100644 --- a/Mathlib/CategoryTheory/Types.lean +++ b/Mathlib/CategoryTheory/Types.lean @@ -258,7 +258,6 @@ See . theorem mono_iff_injective {X Y : Type u} (f : X ⟶ Y) : Mono f ↔ Function.Injective f := by constructor · intro H x x' h - skip rw [← homOfElement_eq_iff] at h ⊢ exact (cancel_mono f).mp h · exact fun H => ⟨fun g g' h => H.comp_left h⟩ diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean index 1ef51be0121ed..ca99f38692e86 100644 --- a/Mathlib/Computability/Halting.lean +++ b/Mathlib/Computability/Halting.lean @@ -203,19 +203,12 @@ theorem to_re {p : α → Prop} (hp : ComputablePred p) : RePred p := by /-- **Rice's Theorem** -/ theorem rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => eval c ∈ C) {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C := by - cases' h with _ h; skip + cases' h with _ h obtain ⟨c, e⟩ := fixed_point₂ (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂ ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂ - simp? at e says simp only [Bool.cond_decide] at e - by_cases H : eval c ∈ C - · simp only [H, if_true] at e - change (fun b => g b) ∈ C - rwa [← e] - · simp only [H, if_false] at e - rw [e] at H - contradiction + aesop #align computable_pred.rice ComputablePred.rice theorem rice₂ (C : Set Code) (H : ∀ cf cg, eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)) : diff --git a/Mathlib/Data/DFinsupp/Basic.lean b/Mathlib/Data/DFinsupp/Basic.lean index cf1cb3fc49e10..f91bd99b8b6c9 100644 --- a/Mathlib/Data/DFinsupp/Basic.lean +++ b/Mathlib/Data/DFinsupp/Basic.lean @@ -1136,10 +1136,7 @@ theorem mem_support_toFun (f : Π₀ i, β i) (i) : i ∈ f.support ↔ f i ≠ exact and_iff_right_of_imp (s.prop i).resolve_right #align dfinsupp.mem_support_to_fun DFinsupp.mem_support_toFun -theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support fun i => f i := by - change f = mk f.support fun i => f i.1 - ext i - by_cases h : f i ≠ 0 <;> [skip; rw [not_not] at h] <;> simp [h] +theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support fun i => f i := by aesop #align dfinsupp.eq_mk_support DFinsupp.eq_mk_support /-- Equivalence between dependent functions with finite support `s : Finset ι` and functions diff --git a/Mathlib/Data/Matrix/Basis.lean b/Mathlib/Data/Matrix/Basis.lean index cddfd795a97bc..94f70f8ae71da 100644 --- a/Mathlib/Data/Matrix/Basis.lean +++ b/Mathlib/Data/Matrix/Basis.lean @@ -251,8 +251,7 @@ theorem mem_range_scalar_of_commute_stdBasisMatrix {M : Matrix n n α} obtain rfl | hij := Decidable.eq_or_ne i j · rfl · exact diag_eq_of_commute_stdBasisMatrix (hM hij) - · push_neg at hkl - rw [diagonal_apply_ne _ hkl] + · rw [diagonal_apply_ne _ hkl] obtain rfl | hij := Decidable.eq_or_ne i j · rw [col_eq_zero_of_commute_stdBasisMatrix (hM hkl.symm) hkl] · rw [row_eq_zero_of_commute_stdBasisMatrix (hM hij) hkl.symm] diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean index 5be1da868ef1f..fc3b4920e3ca7 100644 --- a/Mathlib/Data/Ordmap/Ordset.lean +++ b/Mathlib/Data/Ordmap/Ordset.lean @@ -395,7 +395,7 @@ theorem node3R_size {l x m y r} : size (@node3R α l x m y r) = size l + size m theorem node4L_size {l x m y r} (hm : Sized m) : size (@node4L α l x m y r) = size l + size m + size r + 2 := by - cases m <;> simp [node4L, node3L, node'] <;> [skip; simp [size, hm.1]] <;> abel + cases m <;> simp [node4L, node3L, node'] <;> [abel; (simp [size, hm.1]; abel)] #align ordnode.node4_l_size Ordnode.node4L_size theorem Sized.dual : ∀ {t : Ordnode α}, Sized t → Sized (dual t) diff --git a/Mathlib/Data/Seq/WSeq.lean b/Mathlib/Data/Seq/WSeq.lean index ae716453f64b4..fb1c60b18fe5f 100644 --- a/Mathlib/Data/Seq/WSeq.lean +++ b/Mathlib/Data/Seq/WSeq.lean @@ -545,8 +545,7 @@ theorem LiftRel.refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (Lif theorem LiftRelO.swap (R : α → β → Prop) (C) : swap (LiftRelO R C) = LiftRelO (swap R) (swap C) := by funext x y - cases' x with x <;> [skip; cases x] <;> - (cases' y with y <;> [skip; cases y] <;> rfl) + rcases x with ⟨⟩ | ⟨hx, jx⟩ <;> rcases y with ⟨⟩ | ⟨hy, jy⟩ <;> rfl #align stream.wseq.lift_rel_o.swap Stream'.WSeq.LiftRelO.swap theorem LiftRel.swap_lem {R : α → β → Prop} {s1 s2} (h : LiftRel R s1 s2) : diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean index f4ba7add61a8f..9872709def04f 100644 --- a/Mathlib/GroupTheory/Perm/Sign.lean +++ b/Mathlib/GroupTheory/Perm/Sign.lean @@ -493,7 +493,6 @@ theorem sign_subtypePerm (f : Perm α) {p : α → Prop} [DecidablePred p] (h₁ conv => congr rw [← l.2.1] - skip simp_rw [← hl'₂] rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map] #align equiv.perm.sign_subtype_perm Equiv.Perm.sign_subtypePerm diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index 9ef74e1f4fb34..f7126365d81c5 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -518,8 +518,7 @@ theorem linearIndependent_iUnion_of_directed {η : Type*} {s : η → Set M} (hs (h : ∀ i, LinearIndependent R (fun x => x : s i → M)) : LinearIndependent R (fun x => x : (⋃ i, s i) → M) := by by_cases hη : Nonempty η - · skip - refine' linearIndependent_of_finite (⋃ i, s i) fun t ht ft => _ + · refine' linearIndependent_of_finite (⋃ i, s i) fun t ht ft => _ rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩ rcases hs.finset_le fi.toFinset with ⟨i, hi⟩ exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj)) diff --git a/Mathlib/LinearAlgebra/Matrix/Symmetric.lean b/Mathlib/LinearAlgebra/Matrix/Symmetric.lean index 14f6f68ee388b..d53e1f1f43d7c 100644 --- a/Mathlib/LinearAlgebra/Matrix/Symmetric.lean +++ b/Mathlib/LinearAlgebra/Matrix/Symmetric.lean @@ -140,8 +140,7 @@ theorem IsSymm.fromBlocks {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n rw [← hBC] simp unfold Matrix.IsSymm - rw [fromBlocks_transpose] - congr; rw [hA, hCB, hBC, hD] + rw [fromBlocks_transpose, hA, hCB, hBC, hD] #align matrix.is_symm.from_blocks Matrix.IsSymm.fromBlocks /-- This is the `iff` version of `Matrix.isSymm.fromBlocks`. -/ diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index dfec40874fc60..7e5337c0ff459 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -516,7 +516,6 @@ theorem cof_succ (o) : cof (succ o) = 1 := by @[simp] theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a := ⟨inductionOn o fun α r _ z => by - skip rcases cof_eq r with ⟨S, hl, e⟩; rw [z] at e cases' mk_ne_zero_iff.1 (by rw [e]; exact one_ne_zero) with a refine' @@ -976,7 +975,7 @@ theorem isRegular_succ {c : Cardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c succ_le_of_lt (by cases' Quotient.exists_rep (@succ Cardinal _ _ c) with α αe; simp at αe - rcases ord_eq α with ⟨r, wo, re⟩; skip + rcases ord_eq α with ⟨r, wo, re⟩ have := ord_isLimit (h.trans (le_succ _)) rw [← αe, re] at this ⊢ rcases cof_eq' r this with ⟨S, H, Se⟩ @@ -1222,7 +1221,7 @@ theorem univ_inaccessible : IsInaccessible univ.{u, v} := theorem lt_power_cof {c : Cardinal.{u}} : ℵ₀ ≤ c → c < (c^cof c.ord) := Quotient.inductionOn c fun α h => by - rcases ord_eq α with ⟨r, wo, re⟩; skip + rcases ord_eq α with ⟨r, wo, re⟩ have := ord_isLimit h rw [mk'_def, re] at this ⊢ rcases cof_eq' r this with ⟨S, H, Se⟩ diff --git a/Mathlib/SetTheory/Cardinal/Divisibility.lean b/Mathlib/SetTheory/Cardinal/Divisibility.lean index e3ad71bf49f26..6ae203c88cc2c 100644 --- a/Mathlib/SetTheory/Cardinal/Divisibility.lean +++ b/Mathlib/SetTheory/Cardinal/Divisibility.lean @@ -80,7 +80,8 @@ theorem prime_of_aleph0_le (ha : ℵ₀ ≤ a) : Prime a := by rcases eq_or_ne (b * c) 0 with hz | hz · rcases mul_eq_zero.mp hz with (rfl | rfl) <;> simp wlog h : c ≤ b - · cases le_total c b <;> [skip; rw [or_comm]] <;> apply_assumption + · cases le_total c b <;> [solve_by_elim; rw [or_comm]] + apply_assumption assumption' all_goals rwa [mul_comm] left diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index 5347d67a624c0..1374e22275d43 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Ordinal.lean @@ -500,7 +500,6 @@ theorem mul_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c := by refine' Acc.recOn (Cardinal.lt_wf.apply c) (fun c _ => Quotient.inductionOn c fun α IH ol => _) h -- consider the minimal well-order `r` on `α` (a type with cardinality `c`). rcases ord_eq α with ⟨r, wo, e⟩ - skip letI := linearOrderOfSTO r haveI : IsWellOrder α (· < ·) := wo -- Define an order `s` on `α × α` by writing `(a, b) < (c, d)` if `max a b < max c d`, or @@ -1354,7 +1353,7 @@ theorem mk_compl_eq_mk_compl_finite_same {α : Type u} [Finite α] {s t : Set α theorem extend_function {α β : Type*} {s : Set α} (f : s ↪ β) (h : Nonempty ((sᶜ : Set α) ≃ ((range f)ᶜ : Set β))) : ∃ g : α ≃ β, ∀ x : s, g x = f x := by - intros; have := h; cases' this with g + have := h; cases' this with g let h : α ≃ β := (Set.sumCompl (s : Set α)).symm.trans ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f))) diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean index 0340a48017df7..3be6de9d52e7e 100644 --- a/Mathlib/SetTheory/Game/Basic.lean +++ b/Mathlib/SetTheory/Game/Basic.lean @@ -660,8 +660,7 @@ def mulOneRelabelling : ∀ x : PGame.{u}, x * 1 ≡r x refine ⟨(Equiv.sumEmpty _ _).trans (Equiv.prodPUnit _), (Equiv.emptySum _ _).trans (Equiv.prodPUnit _), ?_, ?_⟩ <;> (try rintro (⟨i, ⟨⟩⟩ | ⟨i, ⟨⟩⟩)) <;> - { (try intro i) - dsimp + { dsimp apply (Relabelling.subCongr (Relabelling.refl _) (mulZeroRelabelling _)).trans rw [sub_zero] exact (addZeroRelabelling _).trans <| diff --git a/Mathlib/SetTheory/Game/Short.lean b/Mathlib/SetTheory/Game/Short.lean index f7e1be3f87d51..afa2609b6c918 100644 --- a/Mathlib/SetTheory/Game/Short.lean +++ b/Mathlib/SetTheory/Game/Short.lean @@ -205,9 +205,7 @@ instance listShortGet : ∀ (L : List PGame.{u}) [ListShort L] (i : Fin (List.length L)), Short (List.get L i) | [], _, n => by exfalso - rcases n with ⟨_, ⟨⟩⟩ - -- Porting note: The proof errors unless `done` or a `;` is added after `rcases` - done + rcases n with ⟨_, ⟨⟩⟩; | _::_, ListShort.cons' S _, ⟨0, _⟩ => S | hd::tl, ListShort.cons' _ S, ⟨n + 1, h⟩ => @listShortGet tl S ⟨n, (add_lt_add_iff_right 1).mp h⟩ diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index 3180ae04f4a42..5c22953cb2aa1 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -379,7 +379,7 @@ theorem type_subrel_lt (o : Ordinal.{u}) : type (Subrel ((· < ·) : Ordinal → Ordinal → Prop) { o' : Ordinal | o' < o }) = Ordinal.lift.{u + 1} o := by refine' Quotient.inductionOn o _ - rintro ⟨α, r, wo⟩; skip; apply Quotient.sound + rintro ⟨α, r, wo⟩; apply Quotient.sound -- Porting note: `symm; refine' [term]` → `refine' [term].symm` constructor; refine' ((RelIso.preimage Equiv.ulift r).trans (enumIso r).symm).symm #align ordinal.type_subrel_lt Ordinal.type_subrel_lt diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 045cd8aad6d20..98c856dad7ab1 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -550,7 +550,7 @@ theorem relIso_enum' {α β : Type u} {r : α → α → Prop} {s : β → β [IsWellOrder β s] (f : r ≃r s) (o : Ordinal) : ∀ (hr : o < type r) (hs : o < type s), f (enum r o hr) = enum s o hs := by refine' inductionOn o _; rintro γ t wo ⟨g⟩ ⟨h⟩ - skip; rw [enum_type g, enum_type (PrincipalSeg.ltEquiv g f)]; rfl + rw [enum_type g, enum_type (PrincipalSeg.ltEquiv g f)]; rfl #align ordinal.rel_iso_enum' Ordinal.relIso_enum' theorem relIso_enum {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] @@ -1340,7 +1340,7 @@ theorem ord_le {c o} : ord c ≤ o ↔ c ≤ o.card := inductionOn c fun α => Ordinal.inductionOn o fun β s _ => by let ⟨r, _, e⟩ := ord_eq α - skip; simp only [card_type]; constructor <;> intro h + simp only [card_type]; constructor <;> intro h · rw [e] at h exact let ⟨f⟩ := h diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index 7a8213fda97fa..2049b700e6bb5 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -784,7 +784,7 @@ theorem repr_scale (x) [NF x] (o) [NF o] : repr (scale x o) = ω ^ repr x * repr theorem nf_repr_split {o o' m} [NF o] (h : split o = (o', m)) : NF o' ∧ repr o = repr o' + m := by cases' e : split' o with a n - cases' nf_repr_split' e with s₁ s₂; skip + cases' nf_repr_split' e with s₁ s₂ rw [split_eq_scale_split' e] at h injection h; substs o' n simp only [repr_scale, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, @@ -796,7 +796,7 @@ theorem split_dvd {o o' m} [NF o] (h : split o = (o', m)) : ω ∣ repr o' := by cases' e : split' o with a n rw [split_eq_scale_split' e] at h injection h; subst o' - cases nf_repr_split' e; skip; simp + cases nf_repr_split' e; simp #align onote.split_dvd ONote.split_dvd theorem split_add_lt {o e n a m} [NF o] (h : split o = (oadd e n a, m)) : diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean index 7e06f1c96d38b..8f190359e728a 100644 --- a/Mathlib/Topology/StoneCech.lean +++ b/Mathlib/Topology/StoneCech.lean @@ -297,7 +297,6 @@ end Extension theorem convergent_eqv_pure {u : Ultrafilter α} {x : α} (ux : ↑u ≤ 𝓝 x) : u ≈ pure x := fun γ tγ h₁ h₂ f hf => by - skip trans f x; swap; symm all_goals refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _)) · apply pure_le_nhds @@ -319,7 +318,6 @@ instance StoneCech.t2Space : T2Space (StoneCech α) := by rintro ⟨x⟩ ⟨y⟩ g gx gy apply Quotient.sound intro γ tγ h₁ h₂ f hf - skip let ff := stoneCechExtend hf change ff ⟦x⟧ = ff ⟦y⟧ have lim := fun (z : Ultrafilter α) (gz : (g : Filter (StoneCech α)) ≤ 𝓝 ⟦z⟧) =>