diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean index 8a023b47a692f..e3eb8a8116504 100644 --- a/Mathlib/Algebra/Exact.lean +++ b/Mathlib/Algebra/Exact.lean @@ -323,19 +323,17 @@ theorem Exact.split_tfae' (h : Function.Exact f g) : Function.Surjective g ∧ ∃ l, l ∘ₗ f = LinearMap.id, ∃ e : N ≃ₗ[R] M × P, f = e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ e] := by tfae_have 1 → 3 - · rintro ⟨hf, l, hl⟩ - exact ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩ + | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩ tfae_have 2 → 3 - · rintro ⟨hg, l, hl⟩ - exact ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩ + | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩ tfae_have 3 → 1 - · rintro ⟨e, e₁, e₂⟩ + | ⟨e, e₁, e₂⟩ => by have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective - refine ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩ + exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩ tfae_have 3 → 2 - · rintro ⟨e, e₁, e₂⟩ + | ⟨e, e₁, e₂⟩ => by have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective - refine ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩ + exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩ tfae_finish /-- Equivalent characterizations of split exact sequences. Also known as the **Splitting lemma**. -/ @@ -347,10 +345,10 @@ theorem Exact.split_tfae ∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id, ∃ e : N ≃ₗ[R] M × P, f = e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ e] := by - tfae_have 1 ↔ 3 - · simpa using (h.splitSurjectiveEquiv hf).nonempty_congr - tfae_have 2 ↔ 3 - · simpa using (h.splitInjectiveEquiv hg).nonempty_congr + tfae_have 1 ↔ 3 := by + simpa using (h.splitSurjectiveEquiv hf).nonempty_congr + tfae_have 2 ↔ 3 := by + simpa using (h.splitInjectiveEquiv hg).nonempty_congr tfae_finish end split diff --git a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean index 974a1c8685585..d61079ee62930 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean @@ -116,7 +116,7 @@ lemma preservesFiniteLimits_tfae : List.TFAE Nonempty <| PreservesFiniteLimits F ] := by tfae_have 1 → 2 - · rintro hF S ⟨hS, hf⟩ + | hF, S, ⟨hS, hf⟩ => by have := preservesMonomorphisms_of_preserves_shortExact_left F hF refine ⟨?_, inferInstance⟩ let T := ShortComplex.mk S.f (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero) @@ -129,7 +129,7 @@ lemma preservesFiniteLimits_tfae : List.TFAE exact (exact_iff_of_epi_of_isIso_of_mono φ).1 (hF T ⟨(S.exact_iff_exact_coimage_π).1 hS⟩).1 tfae_have 2 → 3 - · intro hF X Y f + | hF, X, Y, f => by refine ⟨preservesLimitOfPreservesLimitCone (kernelIsKernel f) ?_⟩ apply (KernelFork.isLimitMapConeEquiv _ F).2 let S := ShortComplex.mk _ _ (kernel.condition f) @@ -138,13 +138,13 @@ lemma preservesFiniteLimits_tfae : List.TFAE exact hS.1.fIsKernel tfae_have 3 → 4 - · intro hF + | hF => by have := fun X Y (f : X ⟶ Y) ↦ (hF f).some exact ⟨preservesFiniteLimitsOfPreservesKernels F⟩ tfae_have 4 → 1 - · rintro ⟨_⟩ S hS - exact (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩ + | ⟨_⟩, S, hS => + (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩ tfae_finish @@ -175,7 +175,7 @@ lemma preservesFiniteColimits_tfae : List.TFAE Nonempty <| PreservesFiniteColimits F ] := by tfae_have 1 → 2 - · rintro hF S ⟨hS, hf⟩ + | hF, S, ⟨hS, hf⟩ => by have := preservesEpimorphisms_of_preserves_shortExact_right F hF refine ⟨?_, inferInstance⟩ let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero) @@ -188,7 +188,7 @@ lemma preservesFiniteColimits_tfae : List.TFAE exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1 tfae_have 2 → 3 - · intro hF X Y f + | hF, X, Y, f => by refine ⟨preservesColimitOfPreservesColimitCocone (cokernelIsCokernel f) ?_⟩ apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2 let S := ShortComplex.mk _ _ (cokernel.condition f) @@ -197,14 +197,13 @@ lemma preservesFiniteColimits_tfae : List.TFAE exact hS.1.gIsCokernel tfae_have 3 → 4 - · intro hF + | hF => by have := fun X Y (f : X ⟶ Y) ↦ (hF f).some exact ⟨preservesFiniteColimitsOfPreservesCokernels F⟩ tfae_have 4 → 1 - · rintro ⟨_⟩ S hS - exact (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2 - ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩ + | ⟨_⟩, S, hS => (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2 + ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩ tfae_finish @@ -224,7 +223,7 @@ lemma exact_tfae : List.TFAE Nonempty (PreservesFiniteLimits F) ∧ Nonempty (PreservesFiniteColimits F) ] := by tfae_have 1 → 3 - · intro hF + | hF => by refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩ · have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦ And.intro (hF S hS).exact (hF S hS).mono_f) @@ -234,7 +233,7 @@ lemma exact_tfae : List.TFAE exact h f |>.some tfae_have 2 → 1 - · intro hF S hS + | hF, S, hS => by have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <| hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f) have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <| @@ -242,13 +241,11 @@ lemma exact_tfae : List.TFAE exact ⟨hF S hS.exact⟩ tfae_have 3 → 4 - · rintro ⟨h⟩ - exact ⟨⟨preservesFiniteLimitsOfPreservesHomology F⟩, - ⟨preservesFiniteColimitsOfPreservesHomology F⟩⟩ + | ⟨h⟩ => ⟨⟨preservesFiniteLimitsOfPreservesHomology F⟩, + ⟨preservesFiniteColimitsOfPreservesHomology F⟩⟩ tfae_have 4 → 2 - · rintro ⟨⟨h1⟩, ⟨h2⟩⟩ - exact fun _ h ↦ h.map F + | ⟨⟨h1⟩, ⟨h2⟩⟩, _, h => h.map F tfae_finish diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean index 686d38e4a5a1b..260764b5fe69c 100644 --- a/Mathlib/Algebra/Order/ToIntervalMod.lean +++ b/Mathlib/Algebra/Order/ToIntervalMod.lean @@ -517,23 +517,23 @@ theorem tfae_modEq : [a ≡ b [PMOD p], ∀ z : ℤ, b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b, toIcoMod hp a b + p = toIocMod hp a b] := by rw [modEq_iff_toIcoMod_eq_left hp] - tfae_have 3 → 2 - · rw [← not_exists, not_imp_not] + tfae_have 3 → 2 := by + rw [← not_exists, not_imp_not] exact fun ⟨i, hi⟩ => ((toIcoMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans ((toIocMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm tfae_have 4 → 3 - · intro h + | h => by rw [← h, Ne, eq_comm, add_right_eq_self] exact hp.ne' tfae_have 1 → 4 - · intro h + | h => by rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc] refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩ rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero] conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h] - tfae_have 2 → 1 - · rw [← not_exists, not_imp_comm] + tfae_have 2 → 1 := by + rw [← not_exists, not_imp_comm] have h' := toIcoMod_mem_Ico hp a b exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩ tfae_finish diff --git a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean index 91269631ab2c4..551320c2187d8 100644 --- a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean @@ -140,15 +140,12 @@ theorem le_def : I ≤ J ↔ ∀ x ∈ I, x ∈ J := Iff.rfl theorem le_TFAE : List.TFAE [I ≤ J, (I : Set (ι → ℝ)) ⊆ J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper] := by - tfae_have 1 ↔ 2 - · exact Iff.rfl + tfae_have 1 ↔ 2 := Iff.rfl tfae_have 2 → 3 - · intro h - simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h - tfae_have 3 ↔ 4 - · exact Icc_subset_Icc_iff I.lower_le_upper + | h => by simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h + tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper tfae_have 4 → 2 - · exact fun h x hx i ↦ Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i) + | h, x, hx, i => Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i) tfae_finish variable {I J} diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean index 2e4adbdbee16f..aff60c1cd6250 100644 --- a/Mathlib/Analysis/InnerProductSpace/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Basic.lean @@ -1671,8 +1671,8 @@ theorem norm_inner_eq_norm_tfae (x y : E) : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ r : 𝕜, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x] := by - tfae_have 1 → 2 - · refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_ + tfae_have 1 → 2 := by + refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_ have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀) rw [← sq_eq_sq, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h <;> try positivity @@ -1682,13 +1682,12 @@ theorem norm_inner_eq_norm_tfae (x y : E) : sub_eq_zero] at h rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀] rwa [inner_self_ne_zero] - tfae_have 2 → 3 - · exact fun h => h.imp_right fun h' => ⟨_, h'⟩ - tfae_have 3 → 1 - · rintro (rfl | ⟨r, rfl⟩) <;> + tfae_have 2 → 3 := fun h => h.imp_right fun h' => ⟨_, h'⟩ + tfae_have 3 → 1 := by + rintro (rfl | ⟨r, rfl⟩) <;> simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K, inner_self_eq_norm_mul_norm, sq, mul_left_comm] - tfae_have 3 ↔ 4; · simp only [Submodule.mem_span_singleton, eq_comm] + tfae_have 3 ↔ 4 := by simp only [Submodule.mem_span_singleton, eq_comm] tfae_finish /-- If the inner product of two vectors is equal to the product of their norms, then the two vectors diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean index c562e61f2eae3..ae6a4a37290bc 100644 --- a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean +++ b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean @@ -623,14 +623,11 @@ protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*} clear u hu hq -- Now we can prove the equivalence in this setting simp only [List.map] - tfae_have 1 → 3 - · exact uniformEquicontinuous_of_equicontinuousAt_zero f - tfae_have 3 → 2 - · exact UniformEquicontinuous.equicontinuous - tfae_have 2 → 1 - · exact fun H ↦ H 0 + tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f + tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous + tfae_have 2 → 1 := fun H ↦ H 0 tfae_have 3 → 5 - · intro H + | H => by have : ∀ᶠ x in 𝓝 0, ∀ k, q i (f k x) ≤ 1 := by filter_upwards [Metric.equicontinuousAt_iff_right.mp (H.equicontinuous 0) 1 one_pos] with x hx k @@ -642,11 +639,10 @@ protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*} refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩ filter_upwards [this] with x hx simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using hx - tfae_have 5 → 4 - · exact fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩ + tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩ tfae_have 4 → 1 -- This would work over any `NormedField` - · intro ⟨p, hp, hfp⟩ - exact Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <| + | ⟨p, hp, hfp⟩ => + Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <| Eventually.of_forall fun x k ↦ by simpa using hfp k x tfae_finish diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean index 8530ba797f7ed..85edc3f7a843e 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean @@ -313,33 +313,30 @@ protected theorem NormedSpace.equicontinuous_TFAE : List.TFAE BddAbove (Set.range (‖f ·‖)), (⨆ i, (‖f i‖₊ : ENNReal)) < ⊤ ] := by -- `1 ↔ 2 ↔ 3` follows from `uniformEquicontinuous_of_equicontinuousAt_zero` - tfae_have 1 → 3 - · exact uniformEquicontinuous_of_equicontinuousAt_zero f - tfae_have 3 → 2 - · exact UniformEquicontinuous.equicontinuous - tfae_have 2 → 1 - · exact fun H ↦ H 0 + tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f + tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous + tfae_have 2 → 1 := fun H ↦ H 0 -- `4 ↔ 5 ↔ 6 ↔ 7 ↔ 8 ↔ 9` is morally trivial, we just have to use a lot of rewriting -- and `congr` lemmas - tfae_have 4 ↔ 5 - · rw [exists_ge_and_iff_exists] + tfae_have 4 ↔ 5 := by + rw [exists_ge_and_iff_exists] exact fun C₁ C₂ hC ↦ forall₂_imp fun i x ↦ le_trans' <| by gcongr - tfae_have 5 ↔ 7 - · refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_) + tfae_have 5 ↔ 7 := by + refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_) rw [ContinuousLinearMap.opNorm_le_iff hC] - tfae_have 7 ↔ 8 - · simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range] - tfae_have 6 ↔ 8 - · simp_rw [bddAbove_def, Set.forall_mem_range] - tfae_have 8 ↔ 9 - · rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp] + tfae_have 7 ↔ 8 := by + simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range] + tfae_have 6 ↔ 8 := by + simp_rw [bddAbove_def, Set.forall_mem_range] + tfae_have 8 ↔ 9 := by + rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp] rfl -- `3 ↔ 4` is the interesting part of the result. It is essentially a combination of -- `WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm` which turns -- equicontinuity into existence of some continuous seminorm and -- `Seminorm.bound_of_continuous_normedSpace` which characterize such seminorms. - tfae_have 3 ↔ 4 - · refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans + tfae_have 3 ↔ 4 := by + refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans ?_ rw [forall_const] constructor diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean index 66edd002bd1e6..869aa9fe0a463 100644 --- a/Mathlib/Analysis/RCLike/Basic.lean +++ b/Mathlib/Analysis/RCLike/Basic.lean @@ -317,16 +317,14 @@ open List in /-- There are several equivalent ways to say that a number `z` is in fact a real number. -/ theorem is_real_TFAE (z : K) : TFAE [conj z = z, ∃ r : ℝ, (r : K) = z, ↑(re z) = z, im z = 0] := by tfae_have 1 → 4 - · intro h + | h => by rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div, ofReal_zero] tfae_have 4 → 3 - · intro h + | h => by conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero] - tfae_have 3 → 2 - · exact fun h => ⟨_, h⟩ - tfae_have 2 → 1 - · exact fun ⟨r, hr⟩ => hr ▸ conj_ofReal _ + tfae_have 3 → 2 := fun h => ⟨_, h⟩ + tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _ tfae_finish theorem conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) := diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index b1303cc470be5..d15e75afada5e 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -130,29 +130,24 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) : fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩ have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A -- First we prove that 1-4 are equivalent using 2 → 3 → 4, 1 → 3, and 2 → 1 - tfae_have 1 → 3 - · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩ - tfae_have 2 → 1 - · exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩ + tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩ + tfae_have 2 → 1 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩ tfae_have 3 → 2 - · rintro ⟨a, ha, H⟩ + | ⟨a, ha, H⟩ => by rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩ exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩, H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩ - tfae_have 2 → 4 - · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩ - tfae_have 4 → 3 - · exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩ + tfae_have 2 → 4 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩ + tfae_have 4 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩ -- Add 5 and 6 using 4 → 6 → 5 → 3 tfae_have 4 → 6 - · rintro ⟨a, ha, H⟩ + | ⟨a, ha, H⟩ => by rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩ refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩ simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne') - tfae_have 6 → 5 - · exact fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩ + tfae_have 6 → 5 := fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩ tfae_have 5 → 3 - · rintro ⟨a, ha, C, h₀, H⟩ + | ⟨a, ha, C, h₀, H⟩ => by rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩) · obtain rfl : f = 0 := by ext n @@ -163,19 +158,15 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) : isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩ -- Add 7 and 8 using 2 → 8 → 7 → 3 tfae_have 2 → 8 - · rintro ⟨a, ha, H⟩ + | ⟨a, ha, H⟩ => by refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩ rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn - tfae_have 8 → 7 - · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩ + tfae_have 8 → 7 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩ tfae_have 7 → 3 - · rintro ⟨a, ha, H⟩ + | ⟨a, ha, H⟩ => by have : 0 ≤ a := nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans) refine ⟨a, A ⟨this, ha⟩, IsBigO.of_bound 1 ?_⟩ simpa only [Real.norm_eq_abs, one_mul, abs_pow, abs_of_nonneg this] - -- Porting note: used to work without explicitly having 6 → 7 - tfae_have 6 → 7 - · exact fun h ↦ tfae_8_to_7 <| tfae_2_to_8 <| tfae_3_to_2 <| tfae_5_to_3 <| tfae_6_to_5 h tfae_finish /-- For any natural `k` and a real `r > 1` we have `n ^ k = o(r ^ n)` as `n → ∞`. -/ diff --git a/Mathlib/CategoryTheory/Abelian/Exact.lean b/Mathlib/CategoryTheory/Abelian/Exact.lean index 85352b81dbb61..04967ba6b7f80 100644 --- a/Mathlib/CategoryTheory/Abelian/Exact.lean +++ b/Mathlib/CategoryTheory/Abelian/Exact.lean @@ -169,25 +169,19 @@ section open List in theorem Abelian.tfae_mono {X Y : C} (f : X ⟶ Y) (Z : C) : TFAE [Mono f, kernel.ι f = 0, (ShortComplex.mk (0 : Z ⟶ X) f zero_comp).Exact] := by - tfae_have 2 → 1 - · exact mono_of_kernel_ι_eq_zero _ + tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _ tfae_have 1 → 2 - · intro - rw [← cancel_mono f, kernel.condition, zero_comp] - tfae_have 3 ↔ 1 - · exact ShortComplex.exact_iff_mono _ (by simp) + | _ => by rw [← cancel_mono f, kernel.condition, zero_comp] + tfae_have 3 ↔ 1 := ShortComplex.exact_iff_mono _ (by simp) tfae_finish open List in theorem Abelian.tfae_epi {X Y : C} (f : X ⟶ Y) (Z : C ) : TFAE [Epi f, cokernel.π f = 0, (ShortComplex.mk f (0 : Y ⟶ Z) comp_zero).Exact] := by - tfae_have 2 → 1 - · exact epi_of_cokernel_π_eq_zero _ + tfae_have 2 → 1 := epi_of_cokernel_π_eq_zero _ tfae_have 1 → 2 - · intro - rw [← cancel_epi f, cokernel.condition, comp_zero] - tfae_have 3 ↔ 1 - · exact ShortComplex.exact_iff_epi _ (by simp) + | _ => by rw [← cancel_epi f, cokernel.condition, comp_zero] + tfae_have 3 ↔ 1 := ShortComplex.exact_iff_epi _ (by simp) tfae_finish end diff --git a/Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean b/Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean index d4ec2116851e0..ac3e11be6fb37 100644 --- a/Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean +++ b/Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean @@ -106,14 +106,11 @@ theorem isLeftAdjoint_TFAE (f : a ⟶ b) : HasAbsLeftKanExtension f (𝟙 a), ∃ _ : HasLeftKanExtension f (𝟙 a), Lan.CommuteWith f (𝟙 a) f] := by tfae_have 1 → 2 - · intro h - exact IsAbsKan.hasAbsLeftKanExtension (Adjunction.ofIsLeftAdjoint f).isAbsoluteLeftKan + | h => IsAbsKan.hasAbsLeftKanExtension (Adjunction.ofIsLeftAdjoint f).isAbsoluteLeftKan tfae_have 2 → 3 - · intro h - exact ⟨inferInstance, inferInstance⟩ + | h => ⟨inferInstance, inferInstance⟩ tfae_have 3 → 1 - · intro ⟨h, h'⟩ - exact .mk <| (lanIsKan f (𝟙 a)).adjunction <| Lan.CommuteWith.isKan f (𝟙 a) f + | ⟨h, h'⟩ => .mk <| (lanIsKan f (𝟙 a)).adjunction <| Lan.CommuteWith.isKan f (𝟙 a) f tfae_finish end LeftExtension @@ -188,14 +185,11 @@ theorem isRightAdjoint_TFAE (u : b ⟶ a) : HasAbsLeftKanLift u (𝟙 a), ∃ _ : HasLeftKanLift u (𝟙 a), LanLift.CommuteWith u (𝟙 a) u] := by tfae_have 1 → 2 - · intro h - exact IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift + | h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift tfae_have 2 → 3 - · intro h - exact ⟨inferInstance, inferInstance⟩ + | h => ⟨inferInstance, inferInstance⟩ tfae_have 3 → 1 - · intro ⟨h, h'⟩ - exact .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u + | ⟨h, h'⟩ => .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u tfae_finish end LeftLift diff --git a/Mathlib/FieldTheory/Galois.lean b/Mathlib/FieldTheory/Galois.lean index 259a8533aa662..868454440fa9b 100644 --- a/Mathlib/FieldTheory/Galois.lean +++ b/Mathlib/FieldTheory/Galois.lean @@ -391,18 +391,12 @@ theorem tfae [FiniteDimensional F E] : List.TFAE [ IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E, ∃ p : F[X], p.Separable ∧ p.IsSplittingField F E] := by - tfae_have 1 → 2 - · exact fun h => OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm - tfae_have 1 → 3 - · intro; exact card_aut_eq_finrank F E - tfae_have 1 → 4 - · intro; exact is_separable_splitting_field F E - tfae_have 2 → 1 - · exact of_fixedField_eq_bot F E - tfae_have 3 → 1 - · exact of_card_aut_eq_finrank F E - tfae_have 4 → 1 - · rintro ⟨h, hp1, _⟩; exact of_separable_splitting_field hp1 + tfae_have 1 → 2 := fun h ↦ OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm + tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E + tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E + tfae_have 2 → 1 := of_fixedField_eq_bot F E + tfae_have 3 → 1 := of_card_aut_eq_finrank F E + tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1 tfae_finish end IsGalois diff --git a/Mathlib/FieldTheory/KummerExtension.lean b/Mathlib/FieldTheory/KummerExtension.lean index 65eb3d88e45c4..18680d5a83dd6 100644 --- a/Mathlib/FieldTheory/KummerExtension.lean +++ b/Mathlib/FieldTheory/KummerExtension.lean @@ -638,14 +638,11 @@ lemma isCyclic_tfae (K L) [Field K] [Field L] [Algebra K L] [FiniteDimensional K IsSplittingField K L (X ^ (finrank K L) - C a), ∃ (α : L), α ^ (finrank K L) ∈ Set.range (algebraMap K L) ∧ K⟮α⟯ = ⊤] := by tfae_have 1 → 3 - · intro ⟨inst₁, inst₂⟩ - exact exists_root_adjoin_eq_top_of_isCyclic K L hK + | ⟨inst₁, inst₂⟩ => exists_root_adjoin_eq_top_of_isCyclic K L hK tfae_have 3 → 2 - · intro ⟨α, ⟨a, ha⟩, hα⟩ - exact ⟨a, irreducible_X_pow_sub_C_of_root_adjoin_eq_top ha.symm hα, + | ⟨α, ⟨a, ha⟩, hα⟩ => ⟨a, irreducible_X_pow_sub_C_of_root_adjoin_eq_top ha.symm hα, isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top hK ha.symm hα⟩ tfae_have 2 → 1 - · intro ⟨a, H, inst⟩ - exact ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L, + | ⟨a, H, inst⟩ => ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L, isCyclic_of_isSplittingField_X_pow_sub_C hK H L⟩ tfae_finish diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean index 5e2d9a0bdeadd..90196dde62882 100644 --- a/Mathlib/GroupTheory/Nilpotent.lean +++ b/Mathlib/GroupTheory/Nilpotent.lean @@ -811,16 +811,15 @@ theorem isNilpotent_of_finite_tfae : ∀ (p : ℕ) (_hp : Fact p.Prime) (P : Sylow p G), (↑P : Subgroup G).Normal, Nonempty ((∀ p : (Nat.card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)] := by - tfae_have 1 → 2 - · exact @normalizerCondition_of_isNilpotent _ _ + tfae_have 1 → 2 := @normalizerCondition_of_isNilpotent _ _ tfae_have 2 → 3 - · exact fun h H => NormalizerCondition.normal_of_coatom H h + | h, H => NormalizerCondition.normal_of_coatom H h tfae_have 3 → 4 - · intro h p _ P; exact Sylow.normal_of_all_max_subgroups_normal h _ + | h, p, _, P => Sylow.normal_of_all_max_subgroups_normal h _ tfae_have 4 → 5 - · exact fun h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP) + | h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP) tfae_have 5 → 1 - · rintro ⟨e⟩; exact isNilpotent_of_product_of_sylow_group e + | ⟨e⟩ => isNilpotent_of_product_of_sylow_group e tfae_finish @[deprecated (since := "2024-06-05")] alias isNilpotent_of_finite_tFAE := isNilpotent_of_finite_tfae diff --git a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean index 53ceb99c2ae29..7830bfb5e4d7f 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean @@ -52,15 +52,14 @@ lemma charpoly_nilpotent_tfae [IsNoetherian R M] (φ : Module.End R M) : φ.charpoly = X ^ finrank R M, ∀ m : M, ∃ (n : ℕ), (φ ^ n) m = 0, natTrailingDegree φ.charpoly = finrank R M ] := by - tfae_have 1 → 2 - · apply IsNilpotent.charpoly_eq_X_pow_finrank + tfae_have 1 → 2 := IsNilpotent.charpoly_eq_X_pow_finrank _ tfae_have 2 → 3 - · intro h m + | h, m => by use finrank R M suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply] simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly tfae_have 3 → 1 - · intro h + | h => by obtain ⟨n, hn⟩ := Filter.eventually_atTop.mp <| φ.eventually_iSup_ker_pow_eq use n ext x @@ -68,8 +67,8 @@ lemma charpoly_nilpotent_tfae [IsNoetherian R M] (φ : Module.End R M) : obtain ⟨k, hk⟩ := h x rw [← mem_ker] at hk exact Submodule.mem_iSup_of_mem _ hk - tfae_have 2 ↔ 4 - · rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree] + tfae_have 2 ↔ 4 := by + rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree] tfae_finish lemma charpoly_eq_X_pow_iff [IsNoetherian R M] (φ : Module.End R M) : @@ -85,27 +84,25 @@ lemma hasEigenvalue_zero_tfae (φ : Module.End K M) : LinearMap.det φ = 0, ⊥ < ker φ, ∃ (m : M), m ≠ 0 ∧ φ m = 0 ] := by - tfae_have 1 ↔ 2 - · exact Module.End.hasEigenvalue_iff_isRoot - tfae_have 2 → 3 - · obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ + tfae_have 1 ↔ 2 := Module.End.hasEigenvalue_iff_isRoot + tfae_have 2 → 3 := by + obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ simp only [IsRoot.def, constantCoeff_apply, coeff_zero_eq_eval_zero, hF, eval_mul] intro h; rw [h, zero_mul] - tfae_have 3 → 4 - · rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff, + tfae_have 3 → 4 := by + rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff, constantCoeff_apply, charpoly] intro h; rw [h, mul_zero] - tfae_have 4 → 5 - · exact bot_lt_ker_of_det_eq_zero - tfae_have 5 → 6 - · contrapose! + tfae_have 4 → 5 := bot_lt_ker_of_det_eq_zero + tfae_have 5 → 6 := by + contrapose! simp only [not_bot_lt_iff, eq_bot_iff] intro h x simp only [mem_ker, Submodule.mem_bot] contrapose! apply h tfae_have 6 → 1 - · rintro ⟨x, h1, h2⟩ + | ⟨x, h1, h2⟩ => by apply Module.End.hasEigenvalue_of_hasEigenvector ⟨_, h1⟩ simpa only [Module.End.eigenspace_zero, mem_ker] using h2 tfae_finish diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean index 28b06957d5abb..04f432bce67b9 100644 --- a/Mathlib/MeasureTheory/Group/Action.lean +++ b/Mathlib/MeasureTheory/Group/Action.lean @@ -226,23 +226,17 @@ theorem smulInvariantMeasure_tfae : ∀ (c : G) (s), μ (c • s) = μ s, ∀ c : G, Measure.map (c • ·) μ = μ, ∀ c : G, MeasurePreserving (c • ·) μ μ] := by - tfae_have 1 ↔ 2 - · exact ⟨fun h => h.1, fun h => ⟨h⟩⟩ - tfae_have 1 → 6 - · intro h c - exact (measurePreserving_smul c μ).map_eq - tfae_have 6 → 7 - · exact fun H c => ⟨measurable_const_smul c, H c⟩ - tfae_have 7 → 4 - · exact fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c) + tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩ + tfae_have 1 → 6 := fun h c => (measurePreserving_smul c μ).map_eq + tfae_have 6 → 7 := fun H c => ⟨measurable_const_smul c, H c⟩ + tfae_have 7 → 4 := fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c) tfae_have 4 → 5 - · exact fun H c s => by - rw [← preimage_smul_inv] - apply H - tfae_have 5 → 3 - · exact fun H c s _ => H c s + | H, c, s => by + rw [← preimage_smul_inv] + apply H + tfae_have 5 → 3 := fun H c s _ => H c s tfae_have 3 → 2 - · intro H c s hs + | H, c, s, hs => by rw [preimage_smul] exact H c⁻¹ s hs tfae_finish diff --git a/Mathlib/NumberTheory/FLT/Basic.lean b/Mathlib/NumberTheory/FLT/Basic.lean index 3d9712d21923c..3630dbe1368d9 100644 --- a/Mathlib/NumberTheory/FLT/Basic.lean +++ b/Mathlib/NumberTheory/FLT/Basic.lean @@ -83,7 +83,7 @@ lemma FermatLastTheoremFor.mono (hmn : m ∣ n) (hm : FermatLastTheoremFor m) : lemma fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : TFAE [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n] := by tfae_have 1 → 2 - · rintro h a b c ha hb hc habc + | h, a, b, c, ha, hb, hc, habc => by obtain hn | hn := n.even_or_odd · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_) @@ -123,7 +123,7 @@ lemma fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : push_cast simp only [abs_of_pos, habc, *] tfae_have 2 → 3 - · rintro h a b c ha hb hc habc + | h, a, b, c, ha, hb, hc, habc => by rw [← Rat.num_ne_zero] at ha hb hc refine h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num) (by positivity) (by positivity) (by positivity) ?_ @@ -134,8 +134,7 @@ lemma fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0), one_mul, mul_one, Rat.num_div_den, habc] tfae_have 3 → 1 - · rintro h a b c - exact mod_cast h a b c + | h, a, b, c => mod_cast h a b c tfae_finish lemma fermatLastTheoremFor_iff_nat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n := @@ -189,14 +188,14 @@ lemma fermatLastTheoremWith'_iff_fermatLastTheoremWith {α : Type*} [CommSemirin lemma fermatLastTheoremWith'_nat_int_tfae (n : ℕ) : TFAE [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n] := by - tfae_have 2 ↔ 1 - · apply fermatLastTheoremWith'_iff_fermatLastTheoremWith + tfae_have 2 ↔ 1 := by + apply fermatLastTheoremWith'_iff_fermatLastTheoremWith simp only [Nat.isUnit_iff] intro _ _ _ ha hb hc rw [ha, hb, hc] simp only [one_pow, Nat.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true] - tfae_have 3 ↔ 1 - · rw [fermatLastTheoremFor_iff_int] + tfae_have 3 ↔ 1 := by + rw [fermatLastTheoremFor_iff_int] apply fermatLastTheoremWith'_iff_fermatLastTheoremWith intro a b c ha hb hc by_cases hn : n = 0 diff --git a/Mathlib/Order/CompactlyGenerated/Basic.lean b/Mathlib/Order/CompactlyGenerated/Basic.lean index 1d5c2b6ad6f39..60620cc7187cf 100644 --- a/Mathlib/Order/CompactlyGenerated/Basic.lean +++ b/Mathlib/Order/CompactlyGenerated/Basic.lean @@ -250,14 +250,10 @@ open List in theorem wellFounded_characterisations : List.TFAE [WellFounded ((· > ·) : α → α → Prop), IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k] := by - tfae_have 1 → 2 - · exact WellFounded.isSupFiniteCompact α - tfae_have 2 → 3 - · exact IsSupFiniteCompact.isSupClosedCompact α - tfae_have 3 → 1 - · exact IsSupClosedCompact.wellFounded α - tfae_have 2 ↔ 4 - · exact isSupFiniteCompact_iff_all_elements_compact α + tfae_have 1 → 2 := WellFounded.isSupFiniteCompact α + tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α + tfae_have 3 → 1 := IsSupClosedCompact.wellFounded α + tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α tfae_finish theorem wellFounded_iff_isSupFiniteCompact : diff --git a/Mathlib/Order/Height.lean b/Mathlib/Order/Height.lean index 531157c49d046..22b9697c5dd05 100644 --- a/Mathlib/Order/Height.lean +++ b/Mathlib/Order/Height.lean @@ -100,9 +100,9 @@ theorem exists_chain_of_le_chainHeight {n : ℕ} (hn : ↑n ≤ s.chainHeight) : theorem le_chainHeight_TFAE (n : ℕ) : TFAE [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, length l = n, ∃ l ∈ s.subchain, n ≤ length l] := by - tfae_have 1 → 2; · exact s.exists_chain_of_le_chainHeight - tfae_have 2 → 3; · rintro ⟨l, hls, he⟩; exact ⟨l, hls, he.ge⟩ - tfae_have 3 → 1; · rintro ⟨l, hs, hn⟩; exact le_iSup₂_of_le l hs (WithTop.coe_le_coe.2 hn) + tfae_have 1 → 2 := s.exists_chain_of_le_chainHeight + tfae_have 2 → 3 := fun ⟨l, hls, he⟩ ↦ ⟨l, hls, he.ge⟩ + tfae_have 3 → 1 := fun ⟨l, hs, hn⟩ ↦ le_iSup₂_of_le l hs (WithTop.coe_le_coe.2 hn) tfae_finish variable {s t} @@ -169,10 +169,10 @@ theorem chainHeight_add_le_chainHeight_add (s : Set α) (t : Set β) (n m : ℕ) theorem chainHeight_le_chainHeight_TFAE (s : Set α) (t : Set β) : TFAE [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l = length l', ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l ≤ length l'] := by - tfae_have 1 ↔ 3 - · convert ← chainHeight_add_le_chainHeight_add s t 0 0 <;> apply add_zero - tfae_have 2 ↔ 3 - · refine forall₂_congr fun l hl ↦ ?_ + tfae_have 1 ↔ 3 := by + convert ← chainHeight_add_le_chainHeight_add s t 0 0 <;> apply add_zero + tfae_have 2 ↔ 3 := by + refine forall₂_congr fun l _ ↦ ?_ simp_rw [← (le_chainHeight_TFAE t l.length).out 1 2, eq_comm] tfae_finish diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean index af6576042206c..5c7e684d6af00 100644 --- a/Mathlib/Order/WellFoundedSet.lean +++ b/Mathlib/Order/WellFoundedSet.lean @@ -134,16 +134,15 @@ theorem acc_iff_wellFoundedOn {α} {r : α → α → Prop} {a : α} : TFAE [Acc r a, WellFoundedOn { b | ReflTransGen r b a } r, WellFoundedOn { b | TransGen r b a } r] := by - tfae_have 1 → 2 - · refine fun h => ⟨fun b => InvImage.accessible _ ?_⟩ + tfae_have 1 → 2 := by + refine fun h => ⟨fun b => InvImage.accessible _ ?_⟩ rw [← acc_transGen_iff] at h ⊢ obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2 · rwa [h'] at h · exact h.inv h' - tfae_have 2 → 3 - · exact fun h => h.subset fun _ => TransGen.to_reflTransGen - tfae_have 3 → 1 - · refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_) + tfae_have 2 → 3 := fun h => h.subset fun _ => TransGen.to_reflTransGen + tfae_have 3 → 1 := by + refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_) exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩ tfae_finish diff --git a/Mathlib/RingTheory/Bezout.lean b/Mathlib/RingTheory/Bezout.lean index 4ef7731887a6d..37aef0df9ae66 100644 --- a/Mathlib/RingTheory/Bezout.lean +++ b/Mathlib/RingTheory/Bezout.lean @@ -51,13 +51,13 @@ theorem TFAE [IsBezout R] [IsDomain R] : [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R] := by classical tfae_have 1 → 2 - · intro H; exact ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩ + | H => ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩ tfae_have 2 → 3 - · intro; infer_instance + | _ => inferInstance tfae_have 3 → 4 - · intro; infer_instance + | _ => inferInstance tfae_have 4 → 1 - · rintro ⟨h⟩ + | ⟨h⟩ => by rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded] refine ⟨RelEmbedding.wellFounded ?_ h⟩ have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} := diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean index 48cab27dd47c2..b3171e5b848cd 100644 --- a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean +++ b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean @@ -166,23 +166,17 @@ theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain (maximalIdeal R).IsPrincipal, finrank (ResidueField R) (CotangentSpace R) ≤ 1, ∀ (I) (_ : I ≠ ⊥), ∃ n : ℕ, I = maximalIdeal R ^ n] := by - tfae_have 1 → 2 - · exact fun _ ↦ inferInstance - tfae_have 2 → 1 - · exact fun _ ↦ ((IsBezout.TFAE (R := R)).out 0 1).mp ‹_› + tfae_have 1 → 2 := fun _ ↦ inferInstance + tfae_have 2 → 1 := fun _ ↦ ((IsBezout.TFAE (R := R)).out 0 1).mp ‹_› tfae_have 1 → 4 - · intro H - exact ⟨inferInstance, fun P hP hP' ↦ eq_maximalIdeal (hP'.isMaximal hP)⟩ - tfae_have 4 → 3 - · exact fun ⟨h₁, h₂⟩ ↦ { h₁ with maximalOfPrime := (h₂ _ · · ▸ maximalIdeal.isMaximal R) } - tfae_have 3 → 5 - · exact fun h ↦ maximalIdeal_isPrincipal_of_isDedekindDomain R - tfae_have 6 ↔ 5 - · exact finrank_cotangentSpace_le_one_iff - tfae_have 5 → 7 - · exact exists_maximalIdeal_pow_eq_of_principal R - tfae_have 7 → 2 - · rw [ValuationRing.iff_ideal_total] + | H => ⟨inferInstance, fun P hP hP' ↦ eq_maximalIdeal (hP'.isMaximal hP)⟩ + tfae_have 4 → 3 := + fun ⟨h₁, h₂⟩ ↦ { h₁ with maximalOfPrime := (h₂ _ · · ▸ maximalIdeal.isMaximal R) } + tfae_have 3 → 5 := fun h ↦ maximalIdeal_isPrincipal_of_isDedekindDomain R + tfae_have 6 ↔ 5 := finrank_cotangentSpace_le_one_iff + tfae_have 5 → 7 := exists_maximalIdeal_pow_eq_of_principal R + tfae_have 7 → 2 := by + rw [ValuationRing.iff_ideal_total] intro H constructor intro I J diff --git a/Mathlib/RingTheory/Flat/EquationalCriterion.lean b/Mathlib/RingTheory/Flat/EquationalCriterion.lean index bef434517f9b0..e90cd0987d45c 100644 --- a/Mathlib/RingTheory/Flat/EquationalCriterion.lean +++ b/Mathlib/RingTheory/Flat/EquationalCriterion.lean @@ -125,14 +125,12 @@ theorem tfae_equational_criterion : List.TFAE [ ∃ (κ : Type u) (_ : Fintype κ) (a : N →ₗ[R] (κ →₀ R)) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0] := by classical - tfae_have 1 ↔ 2 - · exact iff_rTensor_injective' R M - tfae_have 3 ↔ 2 - · exact forall_vanishesTrivially_iff_forall_rTensor_injective R - tfae_have 3 ↔ 4 - · simp [(TensorProduct.lid R M).injective.eq_iff.symm, isTrivialRelation_iff_vanishesTrivially] + tfae_have 1 ↔ 2 := iff_rTensor_injective' R M + tfae_have 3 ↔ 2 := forall_vanishesTrivially_iff_forall_rTensor_injective R + tfae_have 3 ↔ 4 := by + simp [(TensorProduct.lid R M).injective.eq_iff.symm, isTrivialRelation_iff_vanishesTrivially] tfae_have 4 → 5 - · intro h₄ ι hι f x hfx + | h₄, ι, hι, f, x, hfx => by let f' : ι → R := f let x' : ι → M := fun i ↦ x (single i 1) have := calc @@ -154,7 +152,7 @@ theorem tfae_equational_criterion : List.TFAE [ simp only [linearCombination_apply, zero_smul, implies_true, sum_fintype, finset_sum_apply] exact ha' j tfae_have 5 → 4 - · intro h₅ ι hi f x hfx + | h₅, ι, hi, f, x, hfx => by let f' : ι →₀ R := equivFunOnFinite.symm f let x' : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R x have : x' f' = 0 := by simpa [x', f', linearCombination_apply, sum_fintype] using hfx @@ -167,7 +165,7 @@ theorem tfae_equational_criterion : List.TFAE [ ← (fun _ ↦ equivFunOnFinite_symm_apply_toFun _ _ : ∀ x, f' x = f x), univ_sum_single] simpa using DFunLike.congr_fun ha' j tfae_have 5 → 6 - · intro h₅ N _ _ _ _ f x hfx + | h₅, N, _, _, _, _, f, x, hfx => by have ϕ := Module.Free.repr R N have : (x ∘ₗ ϕ.symm) (ϕ f) = 0 := by simpa obtain ⟨κ, hκ, a', y, ha'y, ha'⟩ := h₅ this @@ -175,8 +173,7 @@ theorem tfae_equational_criterion : List.TFAE [ · simpa [LinearMap.comp_assoc] using congrArg (fun g ↦ (g ∘ₗ ϕ : N →ₗ[R] M)) ha'y · simpa using ha' tfae_have 6 → 5 - · intro h₆ _ _ _ _ hfx - exact h₆ hfx + | h₆, _, _, _, _, hfx => h₆ hfx tfae_finish /-- **Equational criterion for flatness** [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK). diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean index 18e8607dbc93a..ab874dcea2329 100644 --- a/Mathlib/RingTheory/Henselian.lean +++ b/Mathlib/RingTheory/Henselian.lean @@ -121,10 +121,9 @@ theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [LocalRing R] : ∀ (φ : R →+* K), Surjective φ → ∀ f : R[X], f.Monic → ∀ a₀ : K, f.eval₂ φ a₀ = 0 → f.derivative.eval₂ φ a₀ ≠ 0 → ∃ a : R, f.IsRoot a ∧ φ a = a₀] := by tfae_have 3 → 2 - · intro H - exact H (residue R) Ideal.Quotient.mk_surjective + | H => H (residue R) Ideal.Quotient.mk_surjective tfae_have 2 → 1 - · intro H + | H => by constructor intro f hf a₀ h₁ h₂ specialize H f hf (residue R a₀) @@ -136,7 +135,7 @@ theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [LocalRing R] : rw [← Ideal.Quotient.eq_zero_iff_mem] rwa [← sub_eq_zero, ← RingHom.map_sub] at ha₂ tfae_have 1 → 3 - · intro hR K _K φ hφ f hf a₀ h₁ h₂ + | hR, K, _K, φ, hφ, f, hf, a₀, h₁, h₂ => by obtain ⟨a₀, rfl⟩ := hφ a₀ have H := HenselianLocalRing.is_henselian f hf a₀ simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker φ] at H h₁ h₂ diff --git a/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean b/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean index fc9ea8c3bc6a3..7dd4c8dade367 100644 --- a/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean +++ b/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean @@ -97,22 +97,13 @@ theorem local_hom_TFAE (f : R →+* S) : (maximalIdeal R).map f ≤ maximalIdeal S, maximalIdeal R ≤ (maximalIdeal S).comap f, (maximalIdeal S).comap f = maximalIdeal R] := by tfae_have 1 → 2 - · rintro _ _ ⟨a, ha, rfl⟩ - exact map_nonunit f a ha - tfae_have 2 → 4 - · exact Set.image_subset_iff.1 - tfae_have 3 ↔ 4 - · exact Ideal.map_le_iff_le_comap - tfae_have 4 → 1 - · intro h - constructor - exact fun x => not_imp_not.1 (@h x) + | _, _, ⟨a, ha, rfl⟩ => map_nonunit f a ha + tfae_have 2 → 4 := Set.image_subset_iff.1 + tfae_have 3 ↔ 4 := Ideal.map_le_iff_le_comap + tfae_have 4 → 1 := fun h ↦ ⟨fun x => not_imp_not.1 (@h x)⟩ tfae_have 1 → 5 - · intro - ext - exact not_iff_not.2 (isUnit_map_iff f _) - tfae_have 5 → 4 - · exact fun h => le_of_eq h.symm + | _ => by ext; exact not_iff_not.2 (isUnit_map_iff f _) + tfae_have 5 → 4 := fun h ↦ le_of_eq h.symm tfae_finish end diff --git a/Mathlib/RingTheory/Valuation/Basic.lean b/Mathlib/RingTheory/Valuation/Basic.lean index c64c33a0023cf..77bb5ceacdaaf 100644 --- a/Mathlib/RingTheory/Valuation/Basic.lean +++ b/Mathlib/RingTheory/Valuation/Basic.lean @@ -506,10 +506,10 @@ theorem isEquiv_tfae [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGr (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) : [v.IsEquiv v', ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x}, v x = 1 ↔ v' x = 1, ∀ {x}, v x < 1 ↔ v' x < 1, ∀ {x}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE := by - tfae_have 1 ↔ 2; · apply isEquiv_iff_val_le_one - tfae_have 1 ↔ 3; · apply isEquiv_iff_val_eq_one - tfae_have 1 ↔ 4; · apply isEquiv_iff_val_lt_one - tfae_have 1 ↔ 5; · apply isEquiv_iff_val_sub_one_lt_one + tfae_have 1 ↔ 2 := isEquiv_iff_val_le_one .. + tfae_have 1 ↔ 3 := isEquiv_iff_val_eq_one .. + tfae_have 1 ↔ 4 := isEquiv_iff_val_lt_one .. + tfae_have 1 ↔ 5 := isEquiv_iff_val_sub_one_lt_one .. tfae_finish end diff --git a/Mathlib/RingTheory/Valuation/ValuationRing.lean b/Mathlib/RingTheory/Valuation/ValuationRing.lean index 3aa7cd60c9a41..864d73e5b39e6 100644 --- a/Mathlib/RingTheory/Valuation/ValuationRing.lean +++ b/Mathlib/RingTheory/Valuation/ValuationRing.lean @@ -363,10 +363,10 @@ protected theorem TFAE (R : Type u) [CommRing R] [IsDomain R] : [ValuationRing R, ∀ x : FractionRing R, IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹, IsTotal R (· ∣ ·), IsTotal (Ideal R) (· ≤ ·), LocalRing R ∧ IsBezout R] := by - tfae_have 1 ↔ 2; · exact iff_isInteger_or_isInteger R _ - tfae_have 1 ↔ 3; · exact iff_dvd_total - tfae_have 1 ↔ 4; · exact iff_ideal_total - tfae_have 1 ↔ 5; · exact iff_local_bezout_domain + tfae_have 1 ↔ 2 := iff_isInteger_or_isInteger R _ + tfae_have 1 ↔ 3 := iff_dvd_total + tfae_have 1 ↔ 4 := iff_ideal_total + tfae_have 1 ↔ 5 := iff_local_bezout_domain tfae_finish end diff --git a/Mathlib/SetTheory/Ordinal/Topology.lean b/Mathlib/SetTheory/Ordinal/Topology.lean index 3f648546cba25..73e5ab814961e 100644 --- a/Mathlib/SetTheory/Ordinal/Topology.lean +++ b/Mathlib/SetTheory/Ordinal/Topology.lean @@ -87,19 +87,19 @@ theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) : ∃ (o : Ordinal.{u}), o ≠ 0 ∧ ∃ (f : ∀ x < o, Ordinal), (∀ x hx, f x hx ∈ s) ∧ bsup.{u, u} o f = a, ∃ (ι : Type u), Nonempty ι ∧ ∃ f : ι → Ordinal, (∀ i, f i ∈ s) ∧ ⨆ i, f i = a] := by - tfae_have 1 → 2 - · simp only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', nhds_left_eq_nhds] + tfae_have 1 → 2 := by + simp only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', nhds_left_eq_nhds] exact id tfae_have 2 → 3 - · intro h + | h => by rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne · simp [he] at h · refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩ exact fun x hx => hx.2 tfae_have 3 → 4 - · exact fun h => ⟨_, inter_subset_left, h.1, bddAbove_Iic.mono inter_subset_right, h.2⟩ - tfae_have 4 → 5 - · rintro ⟨t, hts, hne, hbdd, rfl⟩ + | h => ⟨_, inter_subset_left, h.1, bddAbove_Iic.mono inter_subset_right, h.2⟩ + tfae_have 4 → 5 := by + rintro ⟨t, hts, hne, hbdd, rfl⟩ have hlub : IsLUB t (sSup t) := isLUB_csSup hne hbdd let ⟨y, hyt⟩ := hne classical @@ -109,11 +109,11 @@ theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) : · refine le_antisymm (bsup_le fun x _ => ?_) (csSup_le hne fun x hx => ?_) · split_ifs <;> exact hlub.1 ‹_› · refine (if_pos hx).symm.trans_le (le_bsup _ _ <| (hlub.1 hx).trans_lt (lt_succ _)) - tfae_have 5 → 6 - · rintro ⟨o, h₀, f, hfs, rfl⟩ + tfae_have 5 → 6 := by + rintro ⟨o, h₀, f, hfs, rfl⟩ exact ⟨_, toType_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩ - tfae_have 6 → 1 - · rintro ⟨ι, hne, f, hfs, rfl⟩ + tfae_have 6 → 1 := by + rintro ⟨ι, hne, f, hfs, rfl⟩ exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f) (bddAbove_range.{u, u} f) tfae_finish diff --git a/Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean b/Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean index 1b86b845e840f..ae23b4d9c3b9b 100644 --- a/Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean +++ b/Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean @@ -61,15 +61,15 @@ theorem mapClusterPt_atTop_pow_tfae (x y : G) : x ∈ closure (range (y ^ · : ℕ → G)), x ∈ closure (range (y ^ · : ℤ → G)), ] := by - tfae_have 2 ↔ 1; exact mapClusterPt_atTop_zpow_iff_pow - tfae_have 3 → 4 - · refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h + tfae_have 2 ↔ 1 := mapClusterPt_atTop_zpow_iff_pow + tfae_have 3 → 4 := by + refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h exact ⟨n, zpow_natCast _ _⟩ - tfae_have 4 → 1 - · refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h + tfae_have 4 → 1 := by + refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h exact range_subset_iff.2 (mapClusterPt_self_zpow_atTop_pow _) - tfae_have 1 → 3 - · rw [mem_closure_iff_clusterPt] + tfae_have 1 → 3 := by + rw [mem_closure_iff_clusterPt] exact (ClusterPt.mono · (le_principal_iff.2 range_mem_map)) tfae_finish diff --git a/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean b/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean index c6517bf9f086a..11338ba0c53d7 100644 --- a/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean +++ b/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean @@ -41,12 +41,9 @@ theorem effectiveEpi_tfae , Epi π , Function.Surjective π ] := by - tfae_have 1 → 2 - · intro; infer_instance - tfae_have 2 ↔ 3 - · exact epi_iff_surjective π - tfae_have 3 → 1 - · exact fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩ + tfae_have 1 → 2 := fun _ ↦ inferInstance + tfae_have 2 ↔ 3 := epi_iff_surjective π + tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩ tfae_finish instance : Preregular CompHaus := @@ -65,12 +62,12 @@ theorem effectiveEpiFamily_tfae , ∀ b : B, ∃ (a : α) (x : X a), π a x = b ] := by tfae_have 2 → 1 - · intro + | _ => by simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1] tfae_have 1 → 2 - · intro; infer_instance + | _ => inferInstance tfae_have 3 → 2 - · intro e + | e => by rw [epi_iff_surjective] intro b obtain ⟨t, x, h⟩ := e b @@ -78,7 +75,8 @@ theorem effectiveEpiFamily_tfae change (Sigma.ι X t ≫ Sigma.desc π) x = _ simpa using h tfae_have 2 → 3 - · intro e; rw [epi_iff_surjective] at e + | e => by + rw [epi_iff_surjective] at e let i : ∐ X ≅ finiteCoproduct X := (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _) intro b diff --git a/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean b/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean index 251da0eb75003..f6a2c77737320 100644 --- a/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean +++ b/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean @@ -37,12 +37,9 @@ theorem effectiveEpi_tfae , Epi π , Function.Surjective π ] := by - tfae_have 1 → 2 - · intro; infer_instance - tfae_have 2 ↔ 3 - · exact epi_iff_surjective π - tfae_have 3 → 1 - · exact fun hπ ↦ ⟨⟨CompHausLike.effectiveEpiStruct π hπ⟩⟩ + tfae_have 1 → 2 := fun _ ↦ inferInstance + tfae_have 2 ↔ 3 := epi_iff_surjective π + tfae_have 3 → 1 := fun hπ ↦ ⟨⟨CompHausLike.effectiveEpiStruct π hπ⟩⟩ tfae_finish instance : profiniteToCompHaus.PreservesEffectiveEpis where @@ -80,12 +77,11 @@ theorem effectiveEpiFamily_tfae , ∀ b : B, ∃ (a : α) (x : X a), π a x = b ] := by tfae_have 2 → 1 - · intro + | _ => by simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1] - tfae_have 1 → 2 - · intro; infer_instance - tfae_have 3 ↔ 1 - · erw [((CompHaus.effectiveEpiFamily_tfae + tfae_have 1 → 2 := fun _ ↦ inferInstance + tfae_have 3 ↔ 1 := by + erw [((CompHaus.effectiveEpiFamily_tfae (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 : )] exact ⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h, fun _ ↦ inferInstance⟩ diff --git a/Mathlib/Topology/Category/Stonean/EffectiveEpi.lean b/Mathlib/Topology/Category/Stonean/EffectiveEpi.lean index ff4d234dae338..1901963fcc1a9 100644 --- a/Mathlib/Topology/Category/Stonean/EffectiveEpi.lean +++ b/Mathlib/Topology/Category/Stonean/EffectiveEpi.lean @@ -36,12 +36,9 @@ theorem effectiveEpi_tfae , Epi π , Function.Surjective π ] := by - tfae_have 1 → 2 - · intro; infer_instance - tfae_have 2 ↔ 3 - · exact epi_iff_surjective π - tfae_have 3 → 1 - · exact fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩ + tfae_have 1 → 2 := fun _ ↦ inferInstance + tfae_have 2 ↔ 3 := epi_iff_surjective π + tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩ tfae_finish instance : Stonean.toCompHaus.PreservesEffectiveEpis where @@ -81,12 +78,11 @@ theorem effectiveEpiFamily_tfae , ∀ b : B, ∃ (a : α) (x : X a), π a x = b ] := by tfae_have 2 → 1 - · intro + | _ => by simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1] - tfae_have 1 → 2 - · intro; infer_instance - tfae_have 3 ↔ 1 - · erw [((CompHaus.effectiveEpiFamily_tfae + tfae_have 1 → 2 := fun _ ↦ inferInstance + tfae_have 3 ↔ 1 := by + erw [((CompHaus.effectiveEpiFamily_tfae (fun a ↦ Stonean.toCompHaus.obj (X a)) (fun a ↦ Stonean.toCompHaus.map (π a))).out 2 0 : )] exact ⟨fun h ↦ Stonean.toCompHaus.finite_effectiveEpiFamily_of_map _ _ h, fun _ ↦ inferInstance⟩ diff --git a/Mathlib/Topology/Inseparable.lean b/Mathlib/Topology/Inseparable.lean index f4f888556c776..392ac4f52c773 100644 --- a/Mathlib/Topology/Inseparable.lean +++ b/Mathlib/Topology/Inseparable.lean @@ -53,20 +53,15 @@ theorem specializes_TFAE (x y : X) : y ∈ closure ({ x } : Set X), closure ({ y } : Set X) ⊆ closure { x }, ClusterPt y (pure x)] := by - tfae_have 1 → 2 - · exact (pure_le_nhds _).trans - tfae_have 2 → 3 - · exact fun h s hso hy => h (hso.mem_nhds hy) - tfae_have 3 → 4 - · exact fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx - tfae_have 4 → 5 - · exact fun h => h _ isClosed_closure (subset_closure <| mem_singleton _) - tfae_have 6 ↔ 5 - · exact isClosed_closure.closure_subset_iff.trans singleton_subset_iff - tfae_have 5 ↔ 7 - · rw [mem_closure_iff_clusterPt, principal_singleton] - tfae_have 5 → 1 - · refine fun h => (nhds_basis_opens _).ge_iff.2 ?_ + tfae_have 1 → 2 := (pure_le_nhds _).trans + tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy) + tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx + tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _) + tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff + tfae_have 5 ↔ 7 := by + rw [mem_closure_iff_clusterPt, principal_singleton] + tfae_have 5 → 1 := by + refine fun h => (nhds_basis_opens _).ge_iff.2 ?_ rintro s ⟨hy, ho⟩ rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩ exact ho.mem_nhds hxs diff --git a/Mathlib/Topology/LocallyClosed.lean b/Mathlib/Topology/LocallyClosed.lean index 2cb3f5399de36..fd260f0e11c03 100644 --- a/Mathlib/Topology/LocallyClosed.lean +++ b/Mathlib/Topology/LocallyClosed.lean @@ -150,8 +150,8 @@ lemma isLocallyClosed_tfae (s : Set X) : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s), ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)] := by - tfae_have 1 → 2 - · rintro ⟨U, Z, hU, hZ, rfl⟩ + tfae_have 1 → 2 := by + rintro ⟨U, Z, hU, hZ, rfl⟩ have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by nth_rw 1 [← hZ.closure_eq] rw [← compl_subset_iff_union, compl_subset_compl] @@ -160,23 +160,23 @@ lemma isLocallyClosed_tfae (s : Set X) : inter_univ] exact hU.union isClosed_frontier.isOpen_compl tfae_have 2 → 3 - · exact fun h x ↦ (⟨coborder s, h.mem_nhds <| subset_coborder ·, isClosed_preimage_val_coborder⟩) + | h, x => (⟨coborder s, h.mem_nhds <| subset_coborder ·, isClosed_preimage_val_coborder⟩) tfae_have 3 → 4 - · intro h x hx + | h, x, hx => by obtain ⟨t, ht, ht'⟩ := h x hx obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht rw [isClosed_preimage_val] at ht' exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩ tfae_have 4 → 5 - · intro H + | H => by choose U hxU hU e using H refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩ · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩ exact e y hy ⟨hxU, x.2⟩ · exact (subset_iUnion₂ _ _ <| hxU x ·) tfae_have 5 → 1 - · intro H + | H => by convert H.isLocallyClosed.image inducing_subtype_val (by simpa using isClosed_closure.isLocallyClosed) simpa using subset_closure diff --git a/Mathlib/Topology/LocallyConstant/Basic.lean b/Mathlib/Topology/LocallyConstant/Basic.lean index bc918bf4803b5..401cf78da5d19 100644 --- a/Mathlib/Topology/LocallyConstant/Basic.lean +++ b/Mathlib/Topology/LocallyConstant/Basic.lean @@ -39,18 +39,15 @@ protected theorem tfae (f : X → Y) : ∀ x, IsOpen { x' | f x' = f x }, ∀ y, IsOpen (f ⁻¹' {y}), ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x] := by - tfae_have 1 → 4 - · exact fun h y => h {y} - tfae_have 4 → 3 - · exact fun h x => h (f x) - tfae_have 3 → 2 - · exact fun h x => IsOpen.mem_nhds (h x) rfl + tfae_have 1 → 4 := fun h y => h {y} + tfae_have 4 → 3 := fun h x => h (f x) + tfae_have 3 → 2 := fun h x => IsOpen.mem_nhds (h x) rfl tfae_have 2 → 5 - · intro h x + | h, x => by rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩ exact ⟨U, hU, hx, eq⟩ tfae_have 5 → 1 - · intro h s + | h, s => by refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_ rcases h x with ⟨U, hU, hxU, eq⟩ exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩ diff --git a/Mathlib/Topology/NoetherianSpace.lean b/Mathlib/Topology/NoetherianSpace.lean index 74d4532b5976c..88d07a7493deb 100644 --- a/Mathlib/Topology/NoetherianSpace.lean +++ b/Mathlib/Topology/NoetherianSpace.lean @@ -81,15 +81,12 @@ theorem noetherianSpace_TFAE : WellFounded fun s t : Closeds α => s < t, ∀ s : Set α, IsCompact s, ∀ s : Opens α, IsCompact (s : Set α)] := by - tfae_have 1 ↔ 2 - · refine (noetherianSpace_iff α).trans (Opens.compl_bijective.2.wellFounded_iff ?_) + tfae_have 1 ↔ 2 := by + refine (noetherianSpace_iff α).trans (Opens.compl_bijective.2.wellFounded_iff ?_) exact (@OrderIso.compl (Set α)).lt_iff_lt.symm - tfae_have 1 ↔ 4 - · exact noetherianSpace_iff_opens α - tfae_have 1 → 3 - · exact @NoetherianSpace.isCompact α _ - tfae_have 3 → 4 - · exact fun h s => h s + tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α + tfae_have 1 → 3 := @NoetherianSpace.isCompact α _ + tfae_have 3 → 4 := fun h s => h s tfae_finish variable {α} diff --git a/Mathlib/Topology/Order/LeftRightNhds.lean b/Mathlib/Topology/Order/LeftRightNhds.lean index c44a1895b3c19..c6f61ba355838 100644 --- a/Mathlib/Topology/Order/LeftRightNhds.lean +++ b/Mathlib/Topology/Order/LeftRightNhds.lean @@ -43,17 +43,15 @@ theorem TFAE_mem_nhdsWithin_Ioi {a b : α} (hab : a < b) (s : Set α) : s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s] := by - tfae_have 1 ↔ 2 - · rw [nhdsWithin_Ioc_eq_nhdsWithin_Ioi hab] - tfae_have 1 ↔ 3 - · rw [nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab] - tfae_have 4 → 5 - · exact fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩ + tfae_have 1 ↔ 2 := by + rw [nhdsWithin_Ioc_eq_nhdsWithin_Ioi hab] + tfae_have 1 ↔ 3 := by + rw [nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab] + tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩ tfae_have 5 → 1 - · rintro ⟨u, hau, hu⟩ - exact mem_of_superset (Ioo_mem_nhdsWithin_Ioi ⟨le_refl a, hau⟩) hu + | ⟨u, hau, hu⟩ => mem_of_superset (Ioo_mem_nhdsWithin_Ioi ⟨le_refl a, hau⟩) hu tfae_have 1 → 4 - · intro h + | h => by rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩ rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩ exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩ @@ -183,19 +181,15 @@ theorem TFAE_mem_nhdsWithin_Ici {a b : α} (hab : a < b) (s : Set α) : s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a , Ico a u ⊆ s] := by - tfae_have 1 ↔ 2 - · rw [nhdsWithin_Icc_eq_nhdsWithin_Ici hab] - tfae_have 1 ↔ 3 - · rw [nhdsWithin_Ico_eq_nhdsWithin_Ici hab] - tfae_have 1 ↔ 5 - · exact (nhdsWithin_Ici_basis' ⟨b, hab⟩).mem_iff - tfae_have 4 → 5 - · exact fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩ + tfae_have 1 ↔ 2 := by + rw [nhdsWithin_Icc_eq_nhdsWithin_Ici hab] + tfae_have 1 ↔ 3 := by + rw [nhdsWithin_Ico_eq_nhdsWithin_Ici hab] + tfae_have 1 ↔ 5 := (nhdsWithin_Ici_basis' ⟨b, hab⟩).mem_iff + tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩ tfae_have 5 → 4 - · rintro ⟨u, hua, hus⟩ - exact - ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩, - (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩ + | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩, + (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩ tfae_finish theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : Set α} (hu' : a < u') : diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index b87d9628b0774..500bae87ab25c 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -576,30 +576,28 @@ theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] : ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y] := by - tfae_have 1 ↔ 2 - · exact ⟨fun h => h.1, fun h => ⟨h⟩⟩ - tfae_have 2 ↔ 3 - · simp only [isOpen_compl_iff] - tfae_have 5 ↔ 3 - · refine forall_swap.trans ?_ + tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩ + tfae_have 2 ↔ 3 := by + simp only [isOpen_compl_iff] + tfae_have 5 ↔ 3 := by + refine forall_swap.trans ?_ simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff] - tfae_have 5 ↔ 6 - · simp only [← subset_compl_singleton_iff, exists_mem_subset_iff] - tfae_have 5 ↔ 7 - · simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, exists_prop, and_assoc, + tfae_have 5 ↔ 6 := by + simp only [← subset_compl_singleton_iff, exists_mem_subset_iff] + tfae_have 5 ↔ 7 := by + simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, exists_prop, and_assoc, and_left_comm] - tfae_have 5 ↔ 8 - · simp only [← principal_singleton, disjoint_principal_right] - tfae_have 8 ↔ 9 - · exact forall_swap.trans (by simp only [disjoint_comm, ne_comm]) - tfae_have 1 → 4 - · simp only [continuous_def, CofiniteTopology.isOpen_iff'] + tfae_have 5 ↔ 8 := by + simp only [← principal_singleton, disjoint_principal_right] + tfae_have 8 ↔ 9 := forall_swap.trans (by simp only [disjoint_comm, ne_comm]) + tfae_have 1 → 4 := by + 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] - tfae_have 4 → 2 - · exact fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h - tfae_have 2 ↔ 10 - · simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def, + tfae_have 4 → 2 := + fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h + tfae_have 2 ↔ 10 := by + simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def, mem_singleton_iff, eq_comm] tfae_finish @@ -1890,30 +1888,28 @@ theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] : ∀ (x : X) (s : Set X), s ∈ 𝓝 x → ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s, ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x, ∀ x : X , (𝓝 x).lift' closure = 𝓝 x] := by - tfae_have 1 ↔ 5 - · rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_swap] + tfae_have 1 ↔ 5 := by + rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_swap] simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _), (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp, (nhds_basis_opens _).disjoint_iff_right, exists_prop, ← subset_interior_iff_mem_nhdsSet, interior_compl, compl_subset_compl] - tfae_have 5 → 6 - · exact fun h a => (h a).antisymm (𝓝 _).le_lift'_closure + tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure tfae_have 6 → 4 - · intro H a s hs + | H, a, s, hs => by rw [← H] at hs rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩ exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩ tfae_have 4 → 2 - · intro H s a ha + | H, s, a, ha => by have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl] rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩ refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm] - tfae_have 2 → 3 - · refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩ + tfae_have 2 → 3 := by + refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩ exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot - tfae_have 3 → 1 - · exact fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩ + tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩ tfae_finish theorem RegularSpace.of_lift'_closure_le (h : ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x) : diff --git a/Mathlib/Topology/UniformSpace/UniformConvergence.lean b/Mathlib/Topology/UniformSpace/UniformConvergence.lean index b01801362aefe..4d216ca50a3ca 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergence.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergence.lean @@ -680,14 +680,14 @@ theorem tendstoLocallyUniformlyOn_TFAE [LocallyCompactSpace α] (G : ι → α ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K, ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v] := by tfae_have 1 → 2 - · rintro h K hK1 hK2 - exact (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1) + | h, K, hK1, hK2 => + (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1) tfae_have 2 → 3 - · rintro h x hx + | h, x, hx => by obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx) exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩ tfae_have 3 → 1 - · rintro h u hu x hx + | h, u, hu, x, hx => by obtain ⟨v, hv1, hv2⟩ := h x hx exact ⟨v, hv1, hv2 u hu⟩ tfae_finish