diff --git a/Archive/Arithcc.lean b/Archive/Arithcc.lean index fc77d0c0749f0..557ee58d825ae 100644 --- a/Archive/Arithcc.lean +++ b/Archive/Arithcc.lean @@ -303,23 +303,21 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State} Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit. -/ -theorem compiler_correctness : - ∀ (map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register), - (∀ x, read (loc x map) η = ξ x) → - (∀ x, loc x map < t) → outcome (compile map e t) η ≃[t] { η with ac := value e ξ } := by - intro map e ξ η t hmap ht - revert η t - induction e <;> intro η t hmap ht +theorem compiler_correctness + (map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register) + (hmap : ∀ x, read (loc x map) η = ξ x) (ht : ∀ x, loc x map < t) : + outcome (compile map e t) η ≃[t] { η with ac := value e ξ } := by + induction e generalizing η t with -- 5.I - case const => simp [StateEq, step]; rfl + | const => simp [StateEq, step]; rfl -- 5.II - case var => + | var => simp [hmap, StateEq, step] -- Porting note: was `finish [hmap, StateEq, step]` constructor · simp_all only [read, loc] · rfl -- 5.III - case sum => + | sum => rename_i e_s₁ e_s₂ e_ih_s₁ e_ih_s₂ simp generalize value e_s₁ ξ = ν₁ at e_ih_s₁ ⊢ diff --git a/Archive/Imo/Imo1962Q1.lean b/Archive/Imo/Imo1962Q1.lean index 6a05b328784b8..bd440259d1147 100644 --- a/Archive/Imo/Imo1962Q1.lean +++ b/Archive/Imo/Imo1962Q1.lean @@ -145,11 +145,11 @@ theorem satisfied_by_153846 : ProblemPredicate 153846 := by #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by - cases' without_digits h1 with c h2 + have ⟨c, h2⟩ := without_digits h1 have h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6 := by apply lt_or_ge - cases' h3 with h3 h3 - case inr => exact case_more_digits h3 h2 - case inl => + cases h3 with + | inr h3 => exact case_more_digits h3 h2 + | inl h3 => interval_cases h : (digits 10 c).length · exfalso; exact case_0_digit h h2 · exfalso; exact case_1_digit h h2 diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean index 1952ca46bbb9d..278d05db08d66 100644 --- a/Mathlib/Algebra/Associated.lean +++ b/Mathlib/Algebra/Associated.lean @@ -1143,25 +1143,23 @@ theorem one_or_eq_of_le_of_prime : ∀ p m : Associates α, Prime p → m ≤ p rw [r] match h m d dvd_rfl' with | Or.inl h' => - by_cases h : m = 0 - case pos => + if h : m = 0 then simp [h, zero_mul] - case neg => + else rw [r] at h' have : m * d ≤ m * 1 := by simpa using h' have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this have : d = 1 := bot_unique this simp [this] | Or.inr h' => - by_cases h : d = 0 - case pos => - rw [r] at hp0 - have : m * d = 0 := by rw [h]; simp - contradiction - case neg => - rw [r] at h' - have : d * m ≤ d * 1 := by simpa [mul_comm] using h' - exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this + if h : d = 0 then + rw [r] at hp0 + have : m * d = 0 := by rw [h]; simp + contradiction + else + rw [r] at h' + have : d * m ≤ d * 1 := by simpa [mul_comm] using h' + exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this #align associates.one_or_eq_of_le_of_prime Associates.one_or_eq_of_le_of_prime instance : CanonicallyOrderedCommMonoid (Associates α) where diff --git a/Mathlib/Algebra/CharP/ExpChar.lean b/Mathlib/Algebra/CharP/ExpChar.lean index 94d248dd17670..9ea5a40c02362 100644 --- a/Mathlib/Algebra/CharP/ExpChar.lean +++ b/Mathlib/Algebra/CharP/ExpChar.lean @@ -102,9 +102,9 @@ theorem char_prime_of_ne_zero {p : ℕ} [hp : CharP R p] (p_ne_zero : p ≠ 0) : /-- The exponential characteristic is a prime number or one. -/ theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 := by - cases hq - case zero => exact .inr rfl - case prime hp _ => exact .inl hp + cases hq with + | zero => exact .inr rfl + | prime hp => exact .inl hp #align exp_char_is_prime_or_one expChar_is_prime_or_one /-- The exponential characteristic is positive. -/ diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean index f8a78987127d1..60e16e7d3946b 100644 --- a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean @@ -68,12 +68,12 @@ of great interest for the end user. /-- Shows that the fractional parts of the stream are in `[0,1)`. -/ theorem nth_stream_fr_nonneg_lt_one {ifp_n : IntFractPair K} (nth_stream_eq : IntFractPair.stream v n = some ifp_n) : 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1 := by - cases n - case zero => + cases n with + | zero => have : IntFractPair.of v = ifp_n := by injection nth_stream_eq rw [← this, IntFractPair.of] exact ⟨fract_nonneg _, fract_lt_one _⟩ - case succ => + | succ => rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩ rw [← ifp_of_eq_ifp_n, IntFractPair.of] exact ⟨fract_nonneg _, fract_lt_one _⟩ @@ -238,9 +238,9 @@ theorem succ_nth_fib_le_of_nth_denom (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - (fib (n + 1) : K) ≤ (of v).denominators n := by rw [denom_eq_conts_b, nth_cont_eq_succ_nth_cont_aux] have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by - cases' n with n - case zero => exact Or.inl <| le_refl 1 - case succ => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero) + cases n with + | zero => exact Or.inl <| le_refl 1 + | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero) exact fib_le_of_continuantsAux_b this #align generalized_continued_fraction.succ_nth_fib_le_of_nth_denom GeneralizedContinuedFraction.succ_nth_fib_le_of_nth_denom @@ -249,9 +249,9 @@ theorem succ_nth_fib_le_of_nth_denom (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - theorem zero_le_of_continuantsAux_b : 0 ≤ ((of v).continuantsAux n).b := by let g := of v - induction' n with n IH - case zero => rfl - case succ => + induction n with + | zero => rfl + | succ n IH => cases' Decidable.em <| g.TerminatedAt (n - 1) with terminated not_terminated · -- terminating case cases' n with n @@ -320,9 +320,9 @@ Next we prove the so-called *determinant formula* for `GeneralizedContinuedFract theorem determinant_aux (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)) : ((of v).continuantsAux n).a * ((of v).continuantsAux (n + 1)).b - ((of v).continuantsAux n).b * ((of v).continuantsAux (n + 1)).a = (-1) ^ n := by - induction' n with n IH - case zero => simp [continuantsAux] - case succ => + induction n with + | zero => simp [continuantsAux] + | succ n IH => -- set up some shorthand notation let g := of v let conts := continuantsAux g (n + 2) diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean b/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean index db29aa94d4722..3e664efb3e999 100644 --- a/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean +++ b/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean @@ -175,16 +175,16 @@ theorem coe_of_rat_eq : ((IntFractPair.of q).mapFr (↑) : IntFractPair K) = Int theorem coe_stream_nth_rat_eq : ((IntFractPair.stream q n).map (mapFr (↑)) : Option <| IntFractPair K) = IntFractPair.stream v n := by - induction' n with n IH - case zero => + induction n with + | zero => -- Porting note: was -- simp [IntFractPair.stream, coe_of_rat_eq v_eq_q] simp only [IntFractPair.stream, Option.map_some', coe_of_rat_eq v_eq_q] - case succ => + | succ n IH => rw [v_eq_q] at IH - cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n - case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq] - case some => + cases stream_q_nth_eq : IntFractPair.stream q n with + | none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq] + | some ifp_n => cases' ifp_n with b fr cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero] @@ -296,12 +296,12 @@ theorem stream_succ_nth_fr_num_lt_nth_fr_num_rat {ifp_n ifp_succ_n : IntFractPai theorem stream_nth_fr_num_le_fr_num_sub_n_rat : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - n := by - induction' n with n IH - case zero => + induction n with + | zero => intro ifp_zero stream_zero_eq have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq simp [le_refl, this.symm] - case succ => + | succ n IH => intro ifp_succ_n stream_succ_nth_eq suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by rw [Int.ofNat_succ, sub_add_eq_sub_sub] diff --git a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean index 715b3210257fe..23322b4bfb910 100644 --- a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean +++ b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean @@ -120,9 +120,9 @@ theorem squashSeq_nth_of_not_terminated {gp_n gp_succ_n : Pair K} (s_nth_eq : s. /-- The values before the squashed position stay the same. -/ theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m = s.get? m := by - cases s_succ_nth_eq : s.get? (n + 1) - case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq] - case some => + cases s_succ_nth_eq : s.get? (n + 1) with + | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq] + | some => obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n exact s.ge_stable n.le_succ s_succ_nth_eq obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m @@ -134,11 +134,11 @@ theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m sequence at position `n`. -/ theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n : (squashSeq s (n + 1)).tail = squashSeq s.tail n := by - cases' s_succ_succ_nth_eq : s.get? (n + 2) with gp_succ_succ_n - case none => + cases s_succ_succ_nth_eq : s.get? (n + 2) with + | none => cases s_succ_nth_eq : s.get? (n + 1) <;> simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq] - case some => + | some gp_succ_succ_n => obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n; exact s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq -- apply extensionality with `m` and continue by cases `m = n`. @@ -155,19 +155,19 @@ theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n : corresponding squashed sequence at the squashed position. -/ theorem succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq : convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1) := by - cases' s_succ_nth_eq : s.get? <| n + 1 with gp_succ_n - case none => + cases s_succ_nth_eq : s.get? <| n + 1 with + | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq, convergents'Aux_stable_step_of_terminated s_succ_nth_eq] - case some => - induction' n with m IH generalizing s gp_succ_n - case zero => + | some gp_succ_n => + induction n generalizing s gp_succ_n with + | zero => obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head exact s.ge_stable zero_le_one s_succ_nth_eq have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ := squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail] - case succ => + | succ m IH => obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head exact s.ge_stable (m + 2).zero_le s_succ_nth_eq suffices @@ -204,11 +204,11 @@ squashed gcf. -/ /-- If the gcf already terminated at position `n`, nothing gets squashed. -/ theorem squashGCF_eq_self_of_terminated (terminated_at_n : TerminatedAt g n) : squashGCF g n = g := by - cases n - case zero => + cases n with + | zero => change g.s.get? 0 = none at terminated_at_n simp only [convergents', squashGCF, convergents'Aux, terminated_at_n] - case succ => + | succ => cases g simp only [squashGCF, mk.injEq, true_and] exact squashSeq_eq_self_of_terminated terminated_at_n @@ -224,11 +224,11 @@ theorem squashGCF_nth_of_lt {m : ℕ} (m_lt_n : m < n) : squashed position. -/ theorem succ_nth_convergent'_eq_squashGCF_nth_convergent' : g.convergents' (n + 1) = (squashGCF g n).convergents' n := by - cases n - case zero => + cases n with + | zero => cases g_s_head_eq : g.s.get? 0 <;> simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head] - case succ => + | succ => simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents', squashGCF] #align generalized_continued_fraction.succ_nth_convergent'_eq_squash_gcf_nth_convergent' GeneralizedContinuedFraction.succ_nth_convergent'_eq_squashGCF_nth_convergent' @@ -270,8 +270,8 @@ theorem succ_nth_convergent_eq_squashGCF_nth_convergent [Field K] · obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n exact Option.ne_none_iff_exists'.mp not_terminated_at_n have b_ne_zero : b ≠ 0 := nth_part_denom_ne_zero (part_denom_eq_s_b s_nth_eq) - cases' n with n' - case zero => + cases n with + | zero => suffices (b * g.h + a) / b = g.h + a / b by simpa [squashGCF, s_nth_eq, convergent_eq_conts_a_div_conts_b, continuants_recurrenceAux s_nth_eq zeroth_continuant_aux_eq_one_zero @@ -280,7 +280,7 @@ theorem succ_nth_convergent_eq_squashGCF_nth_convergent [Field K] (b * g.h + a) / b = b * g.h / b + a / b := by ring -- requires `Field`, not `DivisionRing` _ = g.h + a / b := by rw [mul_div_cancel_left _ b_ne_zero] - case succ => + | succ n' => obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' := g.s.ge_stable n'.le_succ s_nth_eq -- Notations @@ -342,9 +342,9 @@ positivity criterion required here. The analogous result for them theorem convergents_eq_convergents' [LinearOrderedField K] (s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) : g.convergents n = g.convergents' n := by - induction' n with n IH generalizing g - case zero => simp - case succ => + induction n generalizing g with + | zero => simp + | succ n IH => let g' := squashGCF g n -- first replace the rhs with the squashed computation suffices g.convergents (n + 1) = g'.convergents' n by diff --git a/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean b/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean index bfc48c04ba1fb..0f37a957af95c 100644 --- a/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean +++ b/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean @@ -45,12 +45,12 @@ theorem continuantsAux_stable_of_terminated (n_lt_m : n < m) (terminated_at_n : theorem convergents'Aux_stable_step_of_terminated {s : Stream'.Seq <| Pair K} (terminated_at_n : s.TerminatedAt n) : convergents'Aux s (n + 1) = convergents'Aux s n := by change s.get? n = none at terminated_at_n - induction' n with n IH generalizing s - case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head] - case succ => - cases' s_head_eq : s.head with gp_head - case none => simp only [convergents'Aux, s_head_eq] - case some => + induction n generalizing s with + | zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head] + | succ n IH => + cases s_head_eq : s.head with + | none => simp only [convergents'Aux, s_head_eq] + | some gp_head => have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n] have := IH this diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean index f7d8be0a962fd..c0a84fc39b2e0 100644 --- a/Mathlib/Algebra/FreeAlgebra.lean +++ b/Mathlib/Algebra/FreeAlgebra.lean @@ -371,21 +371,21 @@ def lift : (X → A) ≃ (FreeAlgebra R X →ₐ[R] A) := right_inv := fun F ↦ by ext t rcases t with ⟨x⟩ - induction x - case of => + induction x with + | of => change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _ simp only [Function.comp_apply, ι_def] - case ofScalar x => + | ofScalar x => change algebraMap _ _ x = F (algebraMap _ _ x) rw [AlgHom.commutes F _] - case add a b ha hb => + | add a b ha hb => -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X let fa : FreeAlgebra R X := Quot.mk (Rel R X) a let fb : FreeAlgebra R X := Quot.mk (Rel R X) b change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb) rw [AlgHom.map_add, AlgHom.map_add, ha, hb] - case mul a b ha hb => + | mul a b ha hb => let fa : FreeAlgebra R X := Quot.mk (Rel R X) a let fb : FreeAlgebra R X := Quot.mk (Rel R X) b change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb) diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean index 8c326e4887858..7e2e718de4be1 100644 --- a/Mathlib/Algebra/GroupPower/Lemmas.lean +++ b/Mathlib/Algebra/GroupPower/Lemmas.lean @@ -213,10 +213,10 @@ theorem zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ := @[to_additive add_zsmul] theorem zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by - induction' n using Int.induction_on with n ihn n ihn - case hz => simp - · simp only [← add_assoc, zpow_add_one, ihn, mul_assoc] - · rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, add_sub_assoc] + induction n using Int.induction_on with + | hz => simp + | hp n ihn => simp only [← add_assoc, zpow_add_one, ihn, mul_assoc] + | hn n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, add_sub_assoc] #align zpow_add zpow_add #align add_zsmul add_zsmul diff --git a/Mathlib/Algebra/Lie/Free.lean b/Mathlib/Algebra/Lie/Free.lean index 66ab1f4a5235b..ed701c023455d 100644 --- a/Mathlib/Algebra/Lie/Free.lean +++ b/Mathlib/Algebra/Lie/Free.lean @@ -201,14 +201,14 @@ theorem liftAux_map_mul (f : X → L) (a b : lib R X) : theorem liftAux_spec (f : X → L) (a b : lib R X) (h : FreeLieAlgebra.Rel R X a b) : liftAux R f a = liftAux R f b := by - induction h - case lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self] - case leibniz_lie a' b' c' => + induction h with + | lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self] + | leibniz_lie a' b' c' => simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie] - case smul t a' b' _ h₂ => simp only [liftAux_map_smul, h₂] - case add_right a' b' c' _ h₂ => simp only [liftAux_map_add, h₂] - case mul_left a' b' c' _ h₂ => simp only [liftAux_map_mul, h₂] - case mul_right a' b' c' _ h₂ => simp only [liftAux_map_mul, h₂] + | smul b' _ h₂ => simp only [liftAux_map_smul, h₂] + | add_right c' _ h₂ => simp only [liftAux_map_add, h₂] + | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂] + | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂] #align free_lie_algebra.lift_aux_spec FreeLieAlgebra.liftAux_spec /-- The quotient map as a `NonUnitalAlgHom`. -/ diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index 07f886c18f078..e543896ee0add 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -645,10 +645,10 @@ protected theorem map_sub (x y : M) : f (x - y) = f x - f y := instance CompatibleSMul.intModule {S : Type*} [Semiring S] [Module S M] [Module S M₂] : CompatibleSMul M M₂ ℤ S := ⟨fun fₗ c x ↦ by - induction c using Int.induction_on - case hz => simp - case hp n ih => simp [add_smul, ih] - case hn n ih => simp [sub_smul, ih]⟩ + induction c using Int.induction_on with + | hz => simp + | hp n ih => simp [add_smul, ih] + | hn n ih => simp [sub_smul, ih]⟩ #align linear_map.compatible_smul.int_module LinearMap.CompatibleSMul.intModule instance CompatibleSMul.units {R S : Type*} [Monoid R] [MulAction R M] [MulAction R M₂] diff --git a/Mathlib/Analysis/Calculus/Deriv/Polynomial.lean b/Mathlib/Analysis/Calculus/Deriv/Polynomial.lean index 1efb4b91a9b20..8d32cb227257e 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Polynomial.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Polynomial.lean @@ -66,9 +66,9 @@ variable (p : 𝕜[X]) (q : R[X]) /-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`. -/ protected theorem hasStrictDerivAt (x : 𝕜) : HasStrictDerivAt (fun x => p.eval x) (p.derivative.eval x) x := by - induction p using Polynomial.induction_on' - case h_add p q hp hq => simpa using hp.add hq - case h_monomial n a => simpa [mul_assoc] using (hasStrictDerivAt_pow n x).const_mul a + induction p using Polynomial.induction_on' with + | h_add p q hp hq => simpa using hp.add hq + | h_monomial n a => simpa [mul_assoc] using (hasStrictDerivAt_pow n x).const_mul a #align polynomial.has_strict_deriv_at Polynomial.hasStrictDerivAt protected theorem hasStrictDerivAt_aeval (x : 𝕜) : @@ -195,4 +195,3 @@ protected theorem fderivWithin_aeval (hxs : UniqueDiffWithinAt 𝕜 s x) : #align polynomial.fderiv_within_aeval Polynomial.fderivWithin_aeval end Polynomial - diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean index 0f573fc5f8eff..acb7850df8d66 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean @@ -47,13 +47,13 @@ lemma strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : lemma concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : ConcaveOn ℝ≥0 univ fun x : ℝ≥0 ↦ x ^ p := by - by_cases hp : p = 0 - case pos => exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩ - case neg => + if hp : p = 0 then + exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩ + else push_neg at hp - by_cases hp' : p = 1 - case pos => exact ⟨convex_univ, by simp [hp']⟩ - case neg => + if hp' : p = 1 then + exact ⟨convex_univ, by simp [hp']⟩ + else push_neg at hp' exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn @@ -86,13 +86,13 @@ lemma strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : lemma concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : ConcaveOn ℝ (Set.Ici 0) fun x : ℝ ↦ x ^ p := by - by_cases hp : p = 0 - case pos => exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩ - case neg => + if hp : p = 0 then + exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩ + else push_neg at hp - by_cases hp' : p = 1 - case pos => exact ⟨convex_Ici 0, by simp [hp']⟩ - case neg => + if hp' : p = 1 then + exact ⟨convex_Ici 0, by simp [hp']⟩ + else push_neg at hp' exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index 24ba679fa2b05..a33fb9175e3e9 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -220,9 +220,9 @@ theorem log_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : log x ≤ 0 := #align real.log_nonpos Real.log_nonpos theorem log_nat_cast_nonneg (n : ℕ) : 0 ≤ log n := by - by_cases hn : n = 0 - case pos => simp [hn] - case neg => + if hn : n = 0 then + simp [hn] + else have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn exact log_nonneg this diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 9a4f0606447eb..598828dcdd8ff 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -594,9 +594,9 @@ theorem coe_mul_rpow (x y : ℝ≥0) (z : ℝ) : ((x : ℝ≥0∞) * y) ^ z = (x theorem prod_coe_rpow {ι} (s : Finset ι) (f : ι → ℝ≥0) (r : ℝ) : ∏ i in s, (f i : ℝ≥0∞) ^ r = ((∏ i in s, f i : ℝ≥0) : ℝ≥0∞) ^ r := by - induction s using Finset.induction - case empty => simp - case insert i s hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul] + induction s using Finset.induction with + | empty => simp + | insert hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul] theorem mul_rpow_of_ne_zero {x y : ℝ≥0∞} (hx : x ≠ 0) (hy : y ≠ 0) (z : ℝ) : (x * y) ^ z = x ^ z * y ^ z := by simp [*, mul_rpow_eq_ite] @@ -608,18 +608,18 @@ theorem mul_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x * y) theorem prod_rpow_of_ne_top {ι} {s : Finset ι} {f : ι → ℝ≥0∞} (hf : ∀ i ∈ s, f i ≠ ∞) (r : ℝ) : ∏ i in s, f i ^ r = (∏ i in s, f i) ^ r := by - induction s using Finset.induction - case empty => simp - case insert i s hi ih => + induction s using Finset.induction with + | empty => simp + | @insert i s hi ih => have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..] apply prod_lt_top h2f |>.ne theorem prod_rpow_of_nonneg {ι} {s : Finset ι} {f : ι → ℝ≥0∞} {r : ℝ} (hr : 0 ≤ r) : ∏ i in s, f i ^ r = (∏ i in s, f i) ^ r := by - induction s using Finset.induction - case empty => simp - case insert i s hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr] + induction s using Finset.induction with + | empty => simp + | insert hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr] theorem inv_rpow (x : ℝ≥0∞) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹ := by rcases eq_or_ne y 0 with (rfl | hy); · simp only [rpow_zero, inv_one] diff --git a/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean b/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean index 5d666c3a85a6f..8ca0ebd62812c 100644 --- a/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean +++ b/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean @@ -145,17 +145,17 @@ theorem Concrete.isColimit_exists_of_rep_eq {D : Cocone F} {i j : J} (hD : IsCol ∃ (k : _) (f : a.1 ⟶ k) (g : b.1 ⟶ k), F.map f a.2 = F.map g b.2 by exact this ⟨i, x⟩ ⟨j, y⟩ h intro a b h - induction h - case rel x y hh => + induction h with + | rel x y hh => obtain ⟨e, he⟩ := hh use y.1, e, 𝟙 _ simpa using he.symm - case refl x => + | refl x => exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩ - case symm x y _ hh => + | symm x y _ hh => obtain ⟨k, f, g, hh⟩ := hh exact ⟨k, g, f, hh.symm⟩ - case trans x y z _ _ hh1 hh2 => + | trans x y z _ _ hh1 hh2 => obtain ⟨k1, f1, g1, h1⟩ := hh1 obtain ⟨k2, f2, g2, h2⟩ := hh2 let k0 : J := IsFiltered.max k1 k2 diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean index 0a473c1a2426d..d6c4fdc578dfe 100644 --- a/Mathlib/CategoryTheory/Limits/Final.lean +++ b/Mathlib/CategoryTheory/Limits/Final.lean @@ -395,18 +395,18 @@ namespace Final theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : ΣX, d ⟶ F.obj X} (t : EqvGen (Types.Quot.Rel.{v, v} (F ⋙ coyoneda.obj (op d))) f₁ f₂) : Zigzag (StructuredArrow.mk f₁.2) (StructuredArrow.mk f₂.2) := by - induction t - case rel x y r => + induction t with + | rel x y r => obtain ⟨f, w⟩ := r fconstructor swap; fconstructor left; fconstructor exact StructuredArrow.homMk f - case refl => fconstructor - case symm x y _ ih => + | refl => fconstructor + | symm x y _ ih => apply zigzag_symmetric exact ih - case trans x y z _ _ ih₁ ih₂ => + | trans x y z _ _ ih₁ ih₂ => apply Relation.ReflTransGen.trans exact ih₁; exact ih₂ #align category_theory.functor.final.zigzag_of_eqv_gen_quot_rel CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index 8a595d5a9522b..1c4adb124c365 100644 --- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean +++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean @@ -259,11 +259,11 @@ lemma eventually_log_b_mul_pos : ∀ᶠ (n:ℕ) in atTop, ∀ i, 0 < log (b i * exact h.eventually_gt_atTop 0 @[aesop safe apply] lemma T_pos (n : ℕ) : 0 < T n := by - induction n using Nat.strongInductionOn - case ind n h_ind => - rcases lt_or_le n R.n₀ with hn|hn - case inl => exact R.T_gt_zero' n hn -- n < R.n₀ - case inr => -- R.n₀ ≤ n + induction n using Nat.strongInductionOn with + | ind n h_ind => + cases lt_or_le n R.n₀ with + | inl hn => exact R.T_gt_zero' n hn -- n < R.n₀ + | inr hn => -- R.n₀ ≤ n rw [R.h_rec n hn] have := R.g_nonneg refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by aesop) @@ -614,8 +614,8 @@ lemma eventually_atTop_sumTransform_le : intro i have hrpos_i := hrpos i have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity) - rcases le_or_lt 0 (p a b + 1) with hp|hp - case h.inl => -- 0 ≤ p a b + 1 + cases le_or_lt 0 (p a b + 1) with + | inl hp => -- 0 ≤ p a b + 1 calc sumTransform (p a b) g (r i n) n = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl _ ≤ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by @@ -647,7 +647,7 @@ lemma eventually_atTop_sumTransform_le : _ = c₂ * g n / c₁ ^ ((p a b) + 1) := by rw [div_self (by positivity), mul_one] _ = (c₂ / c₁ ^ ((p a b) + 1)) * g n := by ring _ ≤ max c₂ (c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact le_max_right _ _ - case h.inr => -- p a b + 1 < 0 + | inr hp => -- p a b + 1 < 0 calc sumTransform (p a b) g (r i n) n = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl _ ≤ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by @@ -693,8 +693,8 @@ lemma eventually_atTop_sumTransform_ge : intro i have hrpos_i := hrpos i have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity) - rcases le_or_gt 0 (p a b + 1) with hp|hp - case h.inl => -- 0 ≤ (p a b) + 1 + cases le_or_gt 0 (p a b + 1) with + | inl hp => -- 0 ≤ (p a b) + 1 calc sumTransform (p a b) g (r i n) n = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl _ ≥ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u^((p a b) + 1)) := by @@ -728,7 +728,7 @@ lemma eventually_atTop_sumTransform_ge : _ = c₂ * (1 - c₃) * g n := by rw [div_self (by positivity), mul_one] _ ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact min_le_left _ _ - case h.inr => -- (p a b) + 1 < 0 + | inr hp => -- (p a b) + 1 < 0 calc sumTransform (p a b) g (r i n) n = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u^((p a b) + 1)) := by rfl _ ≥ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by @@ -910,8 +910,8 @@ lemma isTheta_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) : lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖ := by - rcases eq_or_ne p 0 with hp|hp - case inl => -- p = 0 + cases eq_or_ne p 0 with + | inl hp => -- p = 0 have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by filter_upwards [eventually_deriv_one_sub_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos @@ -924,7 +924,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : (GrowsPolynomially.pow 2 growsPolynomially_log ?_) filter_upwards [eventually_ge_atTop 1] with _ hx exact log_nonneg hx - case inr => -- p ≠ 0 + | inr hp => -- p ≠ 0 refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1)) (isTheta_deriv_rpow_p_mul_one_sub_smoothingFn hp) ?_ filter_upwards [eventually_gt_atTop 0] with _ _ @@ -932,8 +932,8 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ := by - rcases eq_or_ne p 0 with hp|hp - case inl => -- p = 0 + cases eq_or_ne p 0 with + | inl hp => -- p = 0 have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos @@ -947,8 +947,8 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : (GrowsPolynomially.pow 2 growsPolynomially_log ?_) filter_upwards [eventually_ge_atTop 1] with x hx exact log_nonneg hx - case inr => -- p ≠ 0 - refine GrowsPolynomially.of_isTheta ((growsPolynomially_rpow (p-1))) + | inr hp => -- p ≠ 0 + refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1)) (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_ filter_upwards [eventually_gt_atTop 0] with _ _ positivity @@ -1212,8 +1212,8 @@ lemma T_isBigO_smoothingFn_mul_asympBound : have h_one_sub_smoothingFn_pos' : 0 < 1 - ε n := h_smoothing_pos n hn rw [Real.norm_of_nonneg (R.T_nonneg n), Real.norm_of_nonneg (by positivity)] -- We now prove all other cases by induction - induction n using Nat.strongInductionOn - case ind n h_ind => + induction n using Nat.strongInductionOn with + | ind n h_ind => have b_mul_n₀_le_ri i : ⌊b' * ↑n₀⌋₊ ≤ r i n := by exact_mod_cast calc ⌊b' * (n₀ : ℝ)⌋₊ ≤ b' * n₀ := Nat.floor_le <| by positivity _ ≤ b' * n := by gcongr @@ -1225,9 +1225,9 @@ lemma T_isBigO_smoothingFn_mul_asympBound : -- Apply the induction hypothesis, or use the base case depending on how large n is gcongr (∑ i, a i * ?_) + g n with i _ · exact le_of_lt <| R.a_pos _ - · by_cases ri_lt_n₀ : r i n < n₀ - case pos => exact h_base _ <| by aesop - case neg => + · if ri_lt_n₀ : r i n < n₀ then + exact h_base _ <| by aesop + else push_neg at ri_lt_n₀ exact h_ind (r i n) (R.r_lt_n _ _ (n₀_ge_Rn₀.trans hn)) ri_lt_n₀ (h_asympBound_r_pos _ hn _) (h_smoothing_r_pos n hn i) @@ -1358,8 +1358,8 @@ lemma smoothingFn_mul_asympBound_isBigO_T : have h_one_sub_smoothingFn_pos' : 0 < 1 + ε n := h_smoothing_pos n hn rw [Real.norm_of_nonneg (R.T_nonneg n), Real.norm_of_nonneg (by positivity)] -- We now prove all other cases by induction - induction n using Nat.strongInductionOn - case ind n h_ind => + induction n using Nat.strongInductionOn with + | ind n h_ind => have b_mul_n₀_le_ri i : ⌊b' * ↑n₀⌋₊ ≤ r i n := by exact_mod_cast calc ⌊b' * ↑n₀⌋₊ ≤ b' * n₀ := Nat.floor_le <| by positivity _ ≤ b' * n := by gcongr @@ -1371,9 +1371,9 @@ lemma smoothingFn_mul_asympBound_isBigO_T : -- Apply the induction hypothesis, or use the base case depending on how large `n` is gcongr (∑ i, a i * ?_) + g n with i _ · exact le_of_lt <| R.a_pos _ - · rcases lt_or_le (r i n) n₀ with ri_lt_n₀ | n₀_le_ri - case inl => exact h_base _ <| Finset.mem_Ico.mpr ⟨b_mul_n₀_le_ri i, ri_lt_n₀⟩ - case inr => + · cases lt_or_le (r i n) n₀ with + | inl ri_lt_n₀ => exact h_base _ <| Finset.mem_Ico.mpr ⟨b_mul_n₀_le_ri i, ri_lt_n₀⟩ + | inr n₀_le_ri => exact h_ind (r i n) (R.r_lt_n _ _ (n₀_ge_Rn₀.trans hn)) n₀_le_ri (h_asympBound_r_pos _ hn _) (h_smoothing_r_pos n hn i) _ = (∑ i, a i * (C * ((1 + ε (r i n)) * ((r i n) ^ (p a b) diff --git a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean index 889bd9b1aa119..cccf395c85a0b 100644 --- a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean +++ b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean @@ -95,15 +95,15 @@ lemma eventually_zero_of_frequently_zero (hf : GrowsPolynomially f) (hf' : ∃ have hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc ((2:ℝ)^(-(m:ℤ) -1) * x₀) ((2:ℝ)^(-(m:ℤ)) * x₀) → f z = 0 := by intro m - induction m - case zero => + induction m with + | zero => simp only [Nat.zero_eq, CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at * specialize hx x₀ (le_of_max_le_left hx₀_ge) simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx refine fun z _ hz => hx _ ?_ simp only [zpow_neg, zpow_one] at hz simp only [one_div, hz] - case succ k ih => + | succ k ih => intro z hxz hz simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one] at * have hx' : x ≤ (2:ℝ)^(-(k:ℤ) - 1) * x₀ := by @@ -154,8 +154,8 @@ lemma eventually_zero_of_frequently_zero (hf : GrowsPolynomially f) (hf' : ∃ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) : (∀ᶠ x in atTop, 0 ≤ f x) ∨ (∀ᶠ x in atTop, f x ≤ 0) := by obtain ⟨c₁, _, c₂, _, h⟩ := hf (1/2) (by norm_num) - rcases lt_trichotomy c₁ c₂ with hlt|heq|hgt - case inl => -- c₁ < c₂ + match lt_trichotomy c₁ c₂ with + | .inl hlt => -- c₁ < c₂ left filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by @@ -166,7 +166,7 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) : rw [Set.nonempty_Icc] at hu have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith exact nonneg_of_mul_nonneg_right hu' (by linarith) - case inr.inr => -- c₂ < c₁ + | .inr (.inr hgt) => -- c₂ < c₁ right filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by @@ -177,7 +177,7 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) : rw [Set.nonempty_Icc] at hu have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith exact nonpos_of_mul_nonpos_right hu' (by linarith) - case inr.inl => -- c₁ = c₂ + | .inr (.inl heq) => -- c₁ = c₂ have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by simp only [heq, Set.Icc_self, Set.mem_singleton_iff, one_mul] at h rw [eventually_atTop] at h @@ -225,28 +225,28 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) : exact_mod_cast hz.2 rw [← z_to_half_z, half_z_to_base] obtain ⟨c, hc⟩ := hmain - rcases le_or_lt 0 c with hpos|hneg - case inl => + cases le_or_lt 0 c with + | inl hpos => exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc] - case inr => + | inr hneg => right filter_upwards [hc] with x hc exact le_of_lt <| by simpa only [hc] lemma eventually_atTop_zero_or_pos_or_neg (hf : GrowsPolynomially f) : (∀ᶠ x in atTop, f x = 0) ∨ (∀ᶠ x in atTop, 0 < f x) ∨ (∀ᶠ x in atTop, f x < 0) := by - by_cases h : ∃ᶠ x in atTop, f x = 0 - case pos => exact Or.inl <| eventually_zero_of_frequently_zero hf h - case neg => + if h : ∃ᶠ x in atTop, f x = 0 then + exact Or.inl <| eventually_zero_of_frequently_zero hf h + else rw [not_frequently] at h push_neg at h - rcases eventually_atTop_nonneg_or_nonpos hf with h'|h' - case inl => + cases eventually_atTop_nonneg_or_nonpos hf with + | inl h' => refine Or.inr (Or.inl ?_) simp only [lt_iff_le_and_ne] rw [eventually_and] exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩ - case inr => + | inr h' => refine Or.inr (Or.inr ?_) simp only [lt_iff_le_and_ne] rw [eventually_and] @@ -265,14 +265,14 @@ protected lemma neg_iff {f : ℝ → ℝ} : GrowsPolynomially f ↔ GrowsPolynom ⟨fun hf => hf.neg, fun hf => by rw [← neg_neg f]; exact hf.neg⟩ protected lemma abs (hf : GrowsPolynomially f) : GrowsPolynomially (fun x => |f x|) := by - rcases eventually_atTop_nonneg_or_nonpos hf with hf'|hf' - case inl => + cases eventually_atTop_nonneg_or_nonpos hf with + | inl hf' => have hmain : f =ᶠ[atTop] fun x => |f x| := by filter_upwards [hf'] with x hx rw [abs_of_nonneg hx] rw [← iff_eventuallyEq hmain] exact hf - case inr => + | inr hf' => have hmain : -f =ᶠ[atTop] fun x => |f x| := by filter_upwards [hf'] with x hx simp only [Pi.neg_apply, abs_of_nonpos hx] @@ -304,29 +304,29 @@ lemma growsPolynomially_id : GrowsPolynomially (fun x => x) := by protected lemma GrowsPolynomially.mul {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) : GrowsPolynomially fun x => f x * g x := by suffices : GrowsPolynomially fun x => |f x| * |g x| - · rcases eventually_atTop_nonneg_or_nonpos hf with hf'|hf' - case inl => - rcases eventually_atTop_nonneg_or_nonpos hg with hg'|hg' - case inl => + · cases eventually_atTop_nonneg_or_nonpos hf with + | inl hf' => + cases eventually_atTop_nonneg_or_nonpos hg with + | inl hg' => have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by filter_upwards [hf', hg'] with x hx₁ hx₂ rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂] rwa [iff_eventuallyEq hmain] - case inr => + | inr hg' => have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by filter_upwards [hf', hg'] with x hx₁ hx₂ simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂] simp only [iff_eventuallyEq hmain, neg_mul] exact this.neg - case inr => - rcases eventually_atTop_nonneg_or_nonpos hg with hg'|hg' - case inl => + | inr hf' => + cases eventually_atTop_nonneg_or_nonpos hg with + | inl hg' => have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by filter_upwards [hf', hg'] with x hx₁ hx₂ rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg] simp only [iff_eventuallyEq hmain, neg_mul] exact this.neg - case inr => + | inr hg' => have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by filter_upwards [hf', hg'] with x hx₁ hx₂ simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂] @@ -404,8 +404,8 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall intro b hb have hb_ub := hb.2 rw [isLittleO_iff] at hfg - rcases hf.eventually_atTop_nonneg_or_nonpos with hf'|hf' - case inl => -- f is eventually nonneg + cases hf.eventually_atTop_nonneg_or_nonpos with + | inl hf' => -- f is eventually nonneg have hf := hf b hb obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf specialize hfg (c := 1/2) (by norm_num) @@ -448,7 +448,7 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall _ ≤ 3/2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2 _ = 3*c₂ * (1/2 * f x) := by ring _ ≤ 3*c₂ * (f x + g x) := by gcongr - case inr => -- f is eventually nonpos + | inr hf' => -- f is eventually nonpos have hf := hf b hb obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf specialize hfg (c := 1/2) (by norm_num) @@ -507,23 +507,23 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall protected lemma GrowsPolynomially.inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun x => (f x)⁻¹ := by - rcases hf.eventually_atTop_zero_or_pos_or_neg with hf'|hf_pos_or_neg - case inl => + cases hf.eventually_atTop_zero_or_pos_or_neg with + | inl hf' => refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩ have hb_pos := hb.1 filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf'] with x hx hx' intro u hu simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1] - case inr => + | inr hf_pos_or_neg => suffices : GrowsPolynomially fun x => |(f x)⁻¹| - · rcases hf_pos_or_neg with hf'|hf' - case inl => + · cases hf_pos_or_neg with + | inl hf' => have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| := by filter_upwards [hf'] with x hx₁ rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))] rwa [iff_eventuallyEq hmain] - case inr => + | inr hf' => have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| := by filter_upwards [hf'] with x hx₁ simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))] @@ -566,8 +566,8 @@ protected lemma GrowsPolynomially.rpow (p : ℝ) (hf : GrowsPolynomially f) obtain ⟨c₁, (hc₁_mem : 0 < c₁), c₂, hc₂_mem, hfnew⟩ := hf b hb have hc₁p : 0 < c₁ ^ p := Real.rpow_pos_of_pos hc₁_mem _ have hc₂p : 0 < c₂ ^ p := Real.rpow_pos_of_pos hc₂_mem _ - obtain _ | hp := le_or_lt 0 p - case inl => -- 0 ≤ p + cases le_or_lt 0 p with + | inl => -- 0 ≤ p refine ⟨c₁^p, hc₁p, ?_⟩ refine ⟨c₂^p, hc₂p, ?_⟩ filter_upwards [eventually_gt_atTop 0, hfnew, hf_nonneg, @@ -582,9 +582,9 @@ protected lemma GrowsPolynomially.rpow (p : ℝ) (hf : GrowsPolynomially f) case ub => calc (f u)^p ≤ (c₂ * f x)^p := by gcongr; exact (hf₁ u hu).2 _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg] - case inr => -- p < 0 - rcases hf.eventually_atTop_zero_or_pos_or_neg with hzero|hpos|hneg - case inl => -- eventually zero + | inr hp => -- p < 0 + match hf.eventually_atTop_zero_or_pos_or_neg with + | .inl hzero => -- eventually zero refine ⟨1, by norm_num, 1, by norm_num, ?_⟩ filter_upwards [hzero, hfnew] with x hx hx' intro u hu @@ -592,7 +592,7 @@ protected lemma GrowsPolynomially.rpow (p : ℝ) (hf : GrowsPolynomially f) Set.Icc_self, Set.mem_singleton_iff] simp only [hx, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx' rw [hx' u hu, zero_rpow (ne_of_lt hp)] - case inr.inl => -- eventually positive + | .inr (.inl hpos) => -- eventually positive refine ⟨c₂^p, hc₂p, ?_⟩ refine ⟨c₁^p, hc₁p, ?_⟩ filter_upwards [eventually_gt_atTop 0, hfnew, hpos, @@ -607,7 +607,7 @@ protected lemma GrowsPolynomially.rpow (p : ℝ) (hf : GrowsPolynomially f) (f u)^p ≤ (c₁ * f x)^p := by exact rpow_le_rpow_of_exponent_nonpos (by positivity) (hf₁ u hu).1 (le_of_lt hp) _ = _ := by rw [← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)] - case inr.inr => -- eventually negative (which is impossible) + | .inr (.inr hneg) => -- eventually negative (which is impossible) have : ∀ᶠ (_:ℝ) in atTop, False := by filter_upwards [hf_nonneg, hneg] with x hx hx'; linarith rw [Filter.eventually_false_iff_eq_bot] at this exact False.elim <| (atTop_neBot).ne this diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean index 755dccdae6d70..d7a10223b7fa1 100644 --- a/Mathlib/Computability/Halting.lean +++ b/Mathlib/Computability/Halting.lean @@ -297,10 +297,10 @@ open Nat (Partrec') open Nat.Partrec' theorem to_part {n f} (pf : @Partrec' n f) : _root_.Partrec f := by - induction pf - case prim n f hf => exact hf.to_prim.to_comp - case comp m n f g _ _ hf hg => exact (Partrec.vector_mOfFn fun i => hg i).bind (hf.comp snd) - case rfind n f _ hf => + induction pf with + | prim hf => exact hf.to_prim.to_comp + | comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd) + | rfind _ hf => have := hf.comp (vector_cons.comp snd fst) have := ((Primrec.eq.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean index f7c6351f3a951..9207729655b42 100644 --- a/Mathlib/Computability/PartrecCode.lean +++ b/Mathlib/Computability/PartrecCode.lean @@ -696,36 +696,36 @@ theorem smn : #align nat.partrec.code.smn Nat.Partrec.Code.smn /-- A function is partial recursive if and only if there is a code implementing it. -/ -theorem exists_code {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∃ c : Code, eval c = f := - ⟨fun h => by - induction h - case zero => exact ⟨zero, rfl⟩ - case succ => exact ⟨succ, rfl⟩ - case left => exact ⟨left, rfl⟩ - case right => exact ⟨right, rfl⟩ - case pair f g pf pg hf hg => +theorem exists_code {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∃ c : Code, eval c = f := by + refine ⟨fun h => ?_, ?_⟩ + · induction h with + | zero => exact ⟨zero, rfl⟩ + | succ => exact ⟨succ, rfl⟩ + | left => exact ⟨left, rfl⟩ + | right => exact ⟨right, rfl⟩ + | pair pf pg hf hg => rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩ exact ⟨pair cf cg, rfl⟩ - case comp f g pf pg hf hg => + | comp pf pg hf hg => rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩ exact ⟨comp cf cg, rfl⟩ - case prec f g pf pg hf hg => + | prec pf pg hf hg => rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩ exact ⟨prec cf cg, rfl⟩ - case rfind f pf hf => + | rfind pf hf => rcases hf with ⟨cf, rfl⟩ refine' ⟨comp (rfind' cf) (pair Code.id zero), _⟩ - simp [eval, Seq.seq, pure, PFun.pure, Part.map_id'], - fun h => by - rcases h with ⟨c, rfl⟩; induction c - case zero => exact Nat.Partrec.zero - case succ => exact Nat.Partrec.succ - case left => exact Nat.Partrec.left - case right => exact Nat.Partrec.right - case pair cf cg pf pg => exact pf.pair pg - case comp cf cg pf pg => exact pf.comp pg - case prec cf cg pf pg => exact pf.prec pg - case rfind' cf pf => exact pf.rfind'⟩ + simp [eval, Seq.seq, pure, PFun.pure, Part.map_id'] + · rintro ⟨c, rfl⟩ + induction c with + | zero => exact Nat.Partrec.zero + | succ => exact Nat.Partrec.succ + | left => exact Nat.Partrec.left + | right => exact Nat.Partrec.right + | pair cf cg pf pg => exact pf.pair pg + | comp cf cg pf pg => exact pf.comp pg + | prec cf cg pf pg => exact pf.prec pg + | rfind' cf pf => exact pf.rfind' #align nat.partrec.code.exists_code Nat.Partrec.Code.exists_code -- Porting note: `>>`s in `evaln` are now `>>=` because `>>`s are not elaborated well in Lean4. @@ -858,73 +858,72 @@ theorem evaln_sound : ∀ {k c n x}, x ∈ evaln k c n → x ∈ eval c n exact ⟨z, by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hz, z0⟩ #align nat.partrec.code.evaln_sound Nat.Partrec.Code.evaln_sound -theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n := - ⟨fun h => by - rsuffices ⟨k, h⟩ : ∃ k, x ∈ evaln (k + 1) c n - · exact ⟨k + 1, h⟩ - induction c generalizing n x <;> simp [eval, evaln, pure, PFun.pure, Seq.seq, Bind.bind] at h ⊢ - iterate 4 exact ⟨⟨_, le_rfl⟩, h.symm⟩ - case pair cf cg hf hg => - rcases h with ⟨x, hx, y, hy, rfl⟩ - rcases hf hx with ⟨k₁, hk₁⟩; rcases hg hy with ⟨k₂, hk₂⟩ - refine' ⟨max k₁ k₂, _⟩ +theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n := by + refine ⟨fun h => ?_, fun ⟨k, h⟩ => evaln_sound h⟩ + rsuffices ⟨k, h⟩ : ∃ k, x ∈ evaln (k + 1) c n + · exact ⟨k + 1, h⟩ + induction c generalizing n x with simp [eval, evaln, pure, PFun.pure, Seq.seq, Bind.bind] at h ⊢ + | pair cf cg hf hg => + rcases h with ⟨x, hx, y, hy, rfl⟩ + rcases hf hx with ⟨k₁, hk₁⟩; rcases hg hy with ⟨k₂, hk₂⟩ + refine' ⟨max k₁ k₂, _⟩ + refine' + ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _, + evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, _, + evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂, rfl⟩ + | comp cf cg hf hg => + rcases h with ⟨y, hy, hx⟩ + rcases hg hy with ⟨k₁, hk₁⟩; rcases hf hx with ⟨k₂, hk₂⟩ + refine' ⟨max k₁ k₂, _⟩ + exact + ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _, + evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, + evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩ + | prec cf cg hf hg => + revert h + generalize n.unpair.1 = n₁; generalize n.unpair.2 = n₂ + induction' n₂ with m IH generalizing x n <;> simp + · intro h + rcases hf h with ⟨k, hk⟩ + exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩ + · intro y hy hx + rcases IH hy with ⟨k₁, nk₁, hk₁⟩ + rcases hg hx with ⟨k₂, hk₂⟩ refine' - ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _, - evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, _, - evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂, rfl⟩ - case comp cf cg hf hg => - rcases h with ⟨y, hy, hx⟩ - rcases hg hy with ⟨k₁, hk₁⟩; rcases hf hx with ⟨k₂, hk₂⟩ - refine' ⟨max k₁ k₂, _⟩ - exact - ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _, - evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, - evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩ - case prec cf cg hf hg => - revert h - generalize n.unpair.1 = n₁; generalize n.unpair.2 = n₂ - induction' n₂ with m IH generalizing x n <;> simp - · intro h - rcases hf h with ⟨k, hk⟩ - exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩ - · intro y hy hx - rcases IH hy with ⟨k₁, nk₁, hk₁⟩ - rcases hg hx with ⟨k₂, hk₂⟩ - refine' - ⟨(max k₁ k₂).succ, - Nat.le_succ_of_le <| le_max_of_le_left <| - le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y, - evaln_mono (Nat.succ_le_succ <| le_max_left _ _) _, - evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_right _ _) hk₂⟩ - simp only [evaln._eq_8, bind, unpaired, unpair_pair, Option.mem_def, Option.bind_eq_some, - Option.guard_eq_some', exists_and_left, exists_const] - exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩ - case rfind' cf hf => - rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩ - suffices ∃ k, y + n.unpair.2 ∈ evaln (k + 1) (rfind' cf) (Nat.pair n.unpair.1 n.unpair.2) by - simpa [evaln, Bind.bind] - revert hy₁ hy₂ - generalize n.unpair.2 = m - intro hy₁ hy₂ - induction' y with y IH generalizing m <;> simp [evaln, Bind.bind] - · simp at hy₁ - rcases hf hy₁ with ⟨k, hk⟩ - exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp; rfl⟩ - · rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩ - rcases hf ha with ⟨k₁, hk₁⟩ - rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁) - fun {i} hi => by - simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using - hy₂ (Nat.succ_lt_succ hi) with - ⟨k₂, hk₂⟩ - use (max k₁ k₂).succ - rw [zero_add] at hk₁ - use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁ - use a - use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁ - simpa [Nat.succ_eq_add_one, a0, -max_eq_left, -max_eq_right, add_comm, add_left_comm] using - evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂, - fun ⟨k, h⟩ => evaln_sound h⟩ + ⟨(max k₁ k₂).succ, + Nat.le_succ_of_le <| le_max_of_le_left <| + le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y, + evaln_mono (Nat.succ_le_succ <| le_max_left _ _) _, + evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_right _ _) hk₂⟩ + simp only [evaln._eq_8, bind, unpaired, unpair_pair, Option.mem_def, Option.bind_eq_some, + Option.guard_eq_some', exists_and_left, exists_const] + exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩ + | rfind' cf hf => + rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩ + suffices ∃ k, y + n.unpair.2 ∈ evaln (k + 1) (rfind' cf) (Nat.pair n.unpair.1 n.unpair.2) by + simpa [evaln, Bind.bind] + revert hy₁ hy₂ + generalize n.unpair.2 = m + intro hy₁ hy₂ + induction' y with y IH generalizing m <;> simp [evaln, Bind.bind] + · simp at hy₁ + rcases hf hy₁ with ⟨k, hk⟩ + exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp; rfl⟩ + · rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩ + rcases hf ha with ⟨k₁, hk₁⟩ + rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁) + fun {i} hi => by + simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using + hy₂ (Nat.succ_lt_succ hi) with + ⟨k₂, hk₂⟩ + use (max k₁ k₂).succ + rw [zero_add] at hk₁ + use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁ + use a + use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁ + simpa [Nat.succ_eq_add_one, a0, -max_eq_left, -max_eq_right, add_comm, add_left_comm] using + evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂ + | _ => exact ⟨⟨_, le_rfl⟩, h.symm⟩ #align nat.partrec.code.evaln_complete Nat.Partrec.Code.evaln_complete section diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean index eec9bbc1a0dcd..2cffe2ec1024d 100644 --- a/Mathlib/Computability/Primrec.lean +++ b/Mathlib/Computability/Primrec.lean @@ -1377,12 +1377,12 @@ namespace Nat.Primrec' open Vector Primrec theorem to_prim {n f} (pf : @Nat.Primrec' n f) : Primrec f := by - induction pf - case zero => exact .const 0 - case succ => exact _root_.Primrec.succ.comp .vector_head - case get n i => exact Primrec.vector_get.comp .id (.const i) - case comp m n f g _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i) - case prec n f g _ _ hf hg => + induction pf with + | zero => exact .const 0 + | succ => exact _root_.Primrec.succ.comp .vector_head + | get i => exact Primrec.vector_get.comp .id (.const i) + | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i) + | @prec n f g _ _ hf hg => exact .nat_rec' .vector_head (hf.comp Primrec.vector_tail) (hg.comp <| @@ -1525,14 +1525,14 @@ theorem of_prim {n f} : Primrec f → @Primrec' n f := Primrec'.encode).of_eq fun i => by simp [encodek] fun f hf => by - induction hf - case zero => exact const 0 - case succ => exact succ - case left => exact unpair₁ head - case right => exact unpair₂ head - case pair f g _ _ hf hg => exact natPair.comp₂ _ hf hg - case comp f g _ _ hf hg => exact hf.comp₁ _ hg - case prec f g _ _ hf hg => + induction hf with + | zero => exact const 0 + | succ => exact succ + | left => exact unpair₁ head + | right => exact unpair₂ head + | pair _ _ hf hg => exact natPair.comp₂ _ hf hg + | comp _ _ hf hg => exact hf.comp₁ _ hg + | prec _ _ hf hg => simpa using prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head)) (hg.comp₁ _ <| diff --git a/Mathlib/Computability/RegularExpressions.lean b/Mathlib/Computability/RegularExpressions.lean index 0571a9bac91ed..7185404a5d691 100644 --- a/Mathlib/Computability/RegularExpressions.lean +++ b/Mathlib/Computability/RegularExpressions.lean @@ -315,11 +315,11 @@ theorem star_rmatch_iff (P : RegularExpression α) : constructor · simp [hs, hsum] · intro t' ht' - cases ht' - case head ht' => + cases ht' with + | head ht' => simp only [ne_eq, not_false_iff, true_and, rmatch] exact ht - case tail ht' => exact helem t' ht' + | tail _ ht' => exact helem t' ht' · rintro ⟨S, hsum, helem⟩ cases' x with a x · rfl @@ -349,23 +349,23 @@ theorem star_rmatch_iff (P : RegularExpression α) : @[simp] theorem rmatch_iff_matches' (P : RegularExpression α) (x : List α) : P.rmatch x ↔ x ∈ P.matches' := by - induction P generalizing x - case zero => + induction P generalizing x with + | zero => rw [zero_def, zero_rmatch] tauto - case epsilon => + | epsilon => rw [one_def, one_rmatch_iff] rfl - case char => + | char => rw [char_rmatch_iff] rfl - case plus _ _ ih₁ ih₂ => + | plus _ _ ih₁ ih₂ => rw [plus_def, add_rmatch_iff, ih₁, ih₂] rfl - case comp P Q ih₁ ih₂ => + | comp P Q ih₁ ih₂ => simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *] tauto - case star _ ih => + | star _ ih => simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm] #align regular_expression.rmatch_iff_matches RegularExpression.rmatch_iff_matches' diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 4818e9c1406e8..342de6f9053b7 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -284,56 +284,57 @@ theorem exists_code.comp {m n} {f : Vector ℕ n →. ℕ} {g : Fin n → Vector theorem exists_code {n} {f : Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : ∃ c : Code, ∀ v : Vector ℕ n, c.eval v.1 = pure <$> f v := by - induction' hf with n f hf - induction hf - case prim.zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩ - case prim.succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩ - case prim.get n i => - refine' Fin.succRec (fun n => _) (fun n i IH => _) i - · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp [Bind.bind]; rfl⟩ - · obtain ⟨c, h⟩ := IH - exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩ - case prim.comp m n f g hf hg IHf IHg => - simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg - case prim.prec n f g _ _ IHf IHg => - obtain ⟨cf, hf⟩ := IHf - obtain ⟨cg, hg⟩ := IHg - simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg - refine' ⟨prec cf cg, fun v => _⟩ - rw [← v.cons_head_tail] - specialize hf v.tail - replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail) - simp only [Vector.cons_val, Vector.tail_val] at hf hg - simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons, Vector.head_cons, - PFun.coe_val, Vector.tail_val] - simp only [← Part.pure_eq_some] at hf hg ⊢ - induction' v.head with n _ <;> - simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, - show ∀ x, pure x = [x] from fun _ => rfl, Bind.bind, Functor.map] - suffices ∀ a b, a + b = n → - (n.succ :: 0 :: - g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: - v.val.tail : List ℕ) ∈ - PFun.fix - (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail)) - (fun x => Part.some (if v.tail.headI = 0 - then Sum.inl - (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ) - else Sum.inr - (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))) - (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by - erw [Part.eq_some_iff.2 (this 0 n (zero_add n))] - simp only [List.headI, Part.bind_some, List.tail_cons] - intro a b e - induction' b with b IH generalizing a - · refine' PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 _) - simp only [hg, ← e, Part.bind_some, List.tail_cons, pure] - rfl - · refine' PFun.mem_fix_iff.2 (Or.inr ⟨_, _, IH (a + 1) (by rwa [add_right_comm])⟩) - simp only [hg, eval, Part.bind_some, Nat.rec_add_one, List.tail_nil, List.tail_cons, pure] - exact Part.mem_some_iff.2 rfl - case comp m n f g _ _ IHf IHg => exact exists_code.comp IHf IHg - case rfind n f _ IHf => + induction hf with + | prim hf => + induction hf with + | zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩ + | succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩ + | get i => + refine' Fin.succRec (fun n => _) (fun n i IH => _) i + · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp [Bind.bind]; rfl⟩ + · obtain ⟨c, h⟩ := IH + exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩ + | comp g hf hg IHf IHg => + simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg + | @prec n f g _ _ IHf IHg => + obtain ⟨cf, hf⟩ := IHf + obtain ⟨cg, hg⟩ := IHg + simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg + refine' ⟨prec cf cg, fun v => _⟩ + rw [← v.cons_head_tail] + specialize hf v.tail + replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail) + simp only [Vector.cons_val, Vector.tail_val] at hf hg + simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons, + Vector.head_cons, PFun.coe_val, Vector.tail_val] + simp only [← Part.pure_eq_some] at hf hg ⊢ + induction' v.head with n _ <;> + simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, + show ∀ x, pure x = [x] from fun _ => rfl, Bind.bind, Functor.map] + suffices ∀ a b, a + b = n → + (n.succ :: 0 :: + g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: + v.val.tail : List ℕ) ∈ + PFun.fix + (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail)) + (fun x => Part.some (if v.tail.headI = 0 + then Sum.inl + (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ) + else Sum.inr + (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))) + (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by + erw [Part.eq_some_iff.2 (this 0 n (zero_add n))] + simp only [List.headI, Part.bind_some, List.tail_cons] + intro a b e + induction' b with b IH generalizing a + · refine' PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 _) + simp only [hg, ← e, Part.bind_some, List.tail_cons, pure] + rfl + · refine' PFun.mem_fix_iff.2 (Or.inr ⟨_, _, IH (a + 1) (by rwa [add_right_comm])⟩) + simp only [hg, eval, Part.bind_some, Nat.rec_add_one, List.tail_nil, List.tail_cons, pure] + exact Part.mem_some_iff.2 rfl + | comp g _ _ IHf IHg => exact exists_code.comp IHf IHg + | @rfind n f _ IHf => obtain ⟨cf, hf⟩ := IHf; refine' ⟨rfind cf, fun v => _⟩ replace hf := fun a => hf (a ::ᵥ v) simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val, @@ -566,30 +567,30 @@ equality, not a simulation; the original and embedded machines move in lock-step embedded machine reaches the halt state. -/ theorem stepNormal_then (c) (k k' : Cont) (v) : stepNormal c (k.then k') v = (stepNormal c k v).then k' := by - induction c generalizing k v <;> simp only [Cont.then, stepNormal, *] <;> - try { simp only [Cfg.then]; done } - case cons c c' ih _ => rw [← ih, Cont.then] - case comp c c' _ ih' => rw [← ih', Cont.then] - · cases v.headI <;> simp only [Nat.rec] - case fix c ih => rw [← ih, Cont.then] + induction c generalizing k v with simp only [Cont.then, stepNormal, *] + | cons c c' ih _ => rw [← ih, Cont.then] + | comp c c' _ ih' => rw [← ih', Cont.then] + | case => cases v.headI <;> simp only [Nat.rec] + | fix c ih => rw [← ih, Cont.then] + | _ => simp only [Cfg.then] #align turing.to_partrec.step_normal_then Turing.ToPartrec.stepNormal_then /-- The `stepRet` function respects the `then k'` homomorphism. Note that this is an exact equality, not a simulation; the original and embedded machines move in lock-step until the embedded machine reaches the halt state. -/ theorem stepRet_then {k k' : Cont} {v} : stepRet (k.then k') v = (stepRet k v).then k' := by - induction k generalizing v <;> simp only [Cont.then, stepRet, *] <;> - try { simp only [Cfg.then]; done } - case cons₁ => + induction k generalizing v with simp only [Cont.then, stepRet, *] + | cons₁ => rw [← stepNormal_then] rfl - case comp => + | comp => rw [← stepNormal_then] - case fix _ k_ih => + | fix _ _ k_ih => split_ifs · rw [← k_ih] · rw [← stepNormal_then] rfl + | _ => simp only [Cfg.then] #align turing.to_partrec.step_ret_then Turing.ToPartrec.stepRet_then /-- This is a temporary definition, because we will prove in `code_is_ok` that it always holds. @@ -611,15 +612,15 @@ theorem Code.Ok.zero {c} (h : Code.Ok c) {v} : #align turing.to_partrec.code.ok.zero Turing.ToPartrec.Code.Ok.zero theorem stepNormal.is_ret (c k v) : ∃ k' v', stepNormal c k v = Cfg.ret k' v' := by - induction c generalizing k v - iterate 3 exact ⟨_, _, rfl⟩ - case cons _f fs IHf _IHfs => apply IHf - case comp f _g _IHf IHg => apply IHg - case case f g IHf IHg => + induction c generalizing k v with + | cons _f fs IHf _IHfs => apply IHf + | comp f _g _IHf IHg => apply IHg + | case f g IHf IHg => rw [stepNormal] simp only [] cases v.headI <;> simp only [] <;> [apply IHf; apply IHg] - case fix f IHf => apply IHf + | fix f IHf => apply IHf + | _ => exact ⟨_, _, rfl⟩ #align turing.to_partrec.step_normal.is_ret Turing.ToPartrec.stepNormal.is_ret theorem cont_eval_fix {f k v} (fok : Code.Ok f) : @@ -696,23 +697,23 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) : #align turing.to_partrec.cont_eval_fix Turing.ToPartrec.cont_eval_fix theorem code_is_ok (c) : Code.Ok c := by - induction c <;> intro k v <;> rw [stepNormal] - iterate 3 simp only [Code.eval, pure_bind] - case cons f fs IHf IHfs => + induction c with (intro k v; rw [stepNormal]) + | cons f fs IHf IHfs => rw [Code.eval, IHf] simp only [bind_assoc, Cont.eval, pure_bind]; congr; funext v rw [reaches_eval]; swap; exact ReflTransGen.single rfl rw [stepRet, IHfs]; congr; funext v' refine' Eq.trans _ (Eq.symm _) <;> try exact reaches_eval (ReflTransGen.single rfl) - case comp f g IHf IHg => + | comp f g IHf IHg => rw [Code.eval, IHg] simp only [bind_assoc, Cont.eval, pure_bind]; congr; funext v rw [reaches_eval]; swap; exact ReflTransGen.single rfl rw [stepRet, IHf] - case case f g IHf IHg => + | case f g IHf IHg => simp only [Code.eval] cases v.headI <;> simp only [Code.eval] <;> [apply IHf; apply IHg] - case fix f IHf => rw [cont_eval_fix IHf] + | fix f IHf => rw [cont_eval_fix IHf] + | _ => simp only [Code.eval, pure_bind] #align turing.to_partrec.code_is_ok Turing.ToPartrec.code_is_ok theorem stepNormal_eval (c v) : eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v := @@ -720,22 +721,22 @@ theorem stepNormal_eval (c v) : eval step (stepNormal c Cont.halt v) = Cfg.halt #align turing.to_partrec.step_normal_eval Turing.ToPartrec.stepNormal_eval theorem stepRet_eval {k v} : eval step (stepRet k v) = Cfg.halt <$> k.eval v := by - induction k generalizing v - case halt => + induction k generalizing v with + | halt => simp only [mem_eval, Cont.eval, map_pure] exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩) - case cons₁ fs as k IH => + | cons₁ fs as k IH => rw [Cont.eval, stepRet, code_is_ok] simp only [← bind_pure_comp, bind_assoc]; congr; funext v' rw [reaches_eval]; swap; exact ReflTransGen.single rfl rw [stepRet, IH, bind_pure_comp] - case cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH - case comp f k IH => + | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH + | comp f k IH => rw [Cont.eval, stepRet, code_is_ok] simp only [← bind_pure_comp, bind_assoc]; congr; funext v' rw [reaches_eval]; swap; exact ReflTransGen.single rfl rw [IH, bind_pure_comp] - case fix f k IH => + | fix f k IH => rw [Cont.eval, stepRet]; simp only [bind_pure_comp] split_ifs; · exact IH simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)] @@ -947,31 +948,9 @@ instance Λ'.instInhabited : Inhabited Λ' := #align turing.partrec_to_TM2.Λ'.inhabited Turing.PartrecToTM2.Λ'.instInhabited instance Λ'.instDecidableEq : DecidableEq Λ' := fun a b => by - induction a generalizing b <;> cases b <;> try apply Decidable.isFalse; rintro ⟨⟨⟩⟩; done - case move.move _ _ _ _ I _ _ _ _ => - letI := I - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case clear.clear _ _ _ I _ _ _ => - letI := I - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case copy.copy _ I _ => - letI := I - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case push.push _ _ _ I _ _ _ => - letI := I - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case read.read _ I _ => - letI := I - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case succ.succ _ I _ => - letI := I - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case pred.pred _ _ I₁ I₂ _ _ => - letI := I₁ - letI := I₂ - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) - case ret.ret _ _ => - exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) + induction a generalizing b <;> cases b <;> first + | apply Decidable.isFalse; rintro ⟨⟨⟩⟩; done + | exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) #align turing.partrec_to_TM2.Λ'.decidable_eq Turing.PartrecToTM2.Λ'.instDecidableEq /-- The type of TM2 statements used by this machine. -/ @@ -1614,16 +1593,15 @@ theorem trNormal_respects (c k v s) : TrCfg (stepNormal c k v) b₂ ∧ Reaches₁ (TM2.step tr) ⟨some (trNormal c (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩ b₂ := by - induction c generalizing k v s - case zero' => refine' ⟨_, ⟨s, rfl⟩, TransGen.single _⟩; simp - case succ => refine' ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩ - case tail => + induction c generalizing k v s with + | zero' => refine' ⟨_, ⟨s, rfl⟩, TransGen.single _⟩; simp + | succ => refine' ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩ + | tail => let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons refine' ⟨_, ⟨o, rfl⟩, _⟩; convert clear_ok _ using 2; simp; rfl; swap refine' splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) _ cases v <;> simp - case - cons f fs IHf _ => + | cons f fs IHf _ => obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none refine' ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans _⟩ simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main, ne_eq, @@ -1631,8 +1609,8 @@ theorem trNormal_respects (c k v s) : refine' (copy_ok _ none [] (trList v).reverse _ _).trans _ convert h₂ using 2 simp [List.reverseAux_eq, trContStack] - case comp f _ _ IHg => exact IHg (Cont.comp f k) v s - case case f g IHf IHg => + | comp f _ _ IHg => exact IHg (Cont.comp f k) v s + | case f g IHf IHg => rw [stepNormal] simp only obtain ⟨s', h⟩ := pred_ok _ _ s v _ _ @@ -1641,17 +1619,16 @@ theorem trNormal_respects (c k v s) : exact ⟨_, h₁, h.trans h₂⟩ · obtain ⟨c, h₁, h₂⟩ := IHg k _ s' exact ⟨_, h₁, h.trans h₂⟩ - case fix f IH => apply IH + | fix f IH => apply IH #align turing.partrec_to_TM2.tr_normal_respects Turing.PartrecToTM2.trNormal_respects theorem tr_ret_respects (k v s) : ∃ b₂, TrCfg (stepRet k v) b₂ ∧ Reaches₁ (TM2.step tr) ⟨some (Λ'.ret (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩ b₂ := by - induction k generalizing v s - case halt => exact ⟨_, rfl, TransGen.single rfl⟩ - case - cons₁ fs as k _ => + induction k generalizing v s with + | halt => exact ⟨_, rfl, TransGen.single rfl⟩ + | cons₁ fs as k _ => obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none refine' ⟨s', h₁, TransGen.head rfl _⟩; simp refine' (move₂_ok (by decide) _ (splitAtPred_false _)).trans _; · rfl @@ -1667,13 +1644,13 @@ theorem tr_ret_respects (k v s) : ∃ b₂, List.append_nil, elim_update_main, id_eq, elim_update_aux, ne_eq, Function.update_noteq, elim_aux, elim_stack] exact h₂ - case cons₂ ns k IH => + | cons₂ ns k IH => obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩ - case comp f k _ => + | comp f k _ => obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s exact ⟨_, h₁, TransGen.head rfl h₂⟩ - case fix f k IH => + | fix f k IH => rw [stepRet] have : if v.headI = 0 then natEnd (trList v).head?.iget = true ∧ (trList v).tail = trList v.tail @@ -1953,12 +1930,12 @@ theorem head_supports {S k q} (H : (q : Λ').Supports S) : (head k q).Supports S theorem ret_supports {S k} (H₁ : contSupp k ⊆ S) : TM2.SupportsStmt S (tr (Λ'.ret k)) := by have W := fun {q} => trStmts₁_self q - cases k - case halt => trivial - case cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W - case cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W - case comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W) - case fix => + cases k with + | halt => trivial + | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W + | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W + | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W) + | fix => rw [contSupp_fix] at H₁ have L := @Finset.mem_union_left; have R := @Finset.mem_union_right intro s; dsimp only; cases natEnd s.iget @@ -1998,27 +1975,24 @@ theorem trStmts₁_supports' {S q K} (H₁ : (q : Λ').Supports S) (H₂ : trStm #align turing.partrec_to_TM2.tr_stmts₁_supports' Turing.PartrecToTM2.trStmts₁_supports' theorem trNormal_supports {S c k} (Hk : codeSupp c k ⊆ S) : (trNormal c k).Supports S := by - induction c generalizing k <;> simp [Λ'.Supports, head] - case zero' => exact Finset.union_subset_right Hk - case succ => intro; split_ifs <;> exact Finset.union_subset_right Hk - case tail => exact Finset.union_subset_right Hk - case cons f fs IHf _ => + induction c generalizing k with simp [Λ'.Supports, head] + | zero' => exact Finset.union_subset_right Hk + | succ => intro; split_ifs <;> exact Finset.union_subset_right Hk + | tail => exact Finset.union_subset_right Hk + | cons f fs IHf _ => apply IHf rw [codeSupp_cons] at Hk exact Finset.union_subset_right Hk - case comp f g _ IHg => apply IHg; rw [codeSupp_comp] at Hk; exact Finset.union_subset_right Hk - case - case f g IHf IHg => + | comp f g _ IHg => apply IHg; rw [codeSupp_comp] at Hk; exact Finset.union_subset_right Hk + | case f g IHf IHg => simp only [codeSupp_case, Finset.union_subset_iff] at Hk exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩ - case fix f IHf => apply IHf; rw [codeSupp_fix] at Hk; exact Finset.union_subset_right Hk + | fix f IHf => apply IHf; rw [codeSupp_fix] at Hk; exact Finset.union_subset_right Hk #align turing.partrec_to_TM2.tr_normal_supports Turing.PartrecToTM2.trNormal_supports theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp' c k) S := by - induction c generalizing k - iterate 3 - exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H) - case cons f fs IHf IHfs => + induction c generalizing k with + | cons f fs IHf IHfs => have H' := H; simp only [codeSupp_cons, Finset.union_subset_iff] at H' refine' trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => _ refine' supports_union.2 ⟨IHf H'.2, _⟩ @@ -2031,7 +2005,7 @@ theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp exact trStmts₁_supports (head_supports <| Finset.union_subset_right H) (Finset.union_subset_right h) - case comp f g IHf IHg => + | comp f g IHf IHg => have H' := H; rw [codeSupp_comp] at H'; have H' := Finset.union_subset_right H' refine' trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => _ refine' supports_union.2 ⟨IHg H', _⟩ @@ -2039,11 +2013,11 @@ theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp · simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢ exact ⟨h.2.2, H.2⟩ exact IHf (Finset.union_subset_right H') - case case f g IHf IHg => + | case f g IHf IHg => have H' := H; simp only [codeSupp_case, Finset.union_subset_iff] at H' refine' trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => _ exact supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩ - case fix f IHf => + | fix f IHf => have H' := H; simp only [codeSupp_fix, Finset.union_subset_iff] at H' refine' trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => _ refine' supports_union.2 ⟨IHf H'.2, _⟩ @@ -2052,24 +2026,25 @@ theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp Finset.insert_subset_iff] at h H ⊢ exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩ exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H) + | _ => exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H) #align turing.partrec_to_TM2.code_supp'_supports Turing.PartrecToTM2.codeSupp'_supports theorem contSupp_supports {S k} (H : contSupp k ⊆ S) : Supports (contSupp k) S := by - induction k - · simp [contSupp_halt, Supports] - case cons₁ f k IH => + induction k with + | halt => simp [contSupp_halt, Supports] + | cons₁ f k IH => have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁ refine' trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => _ refine' supports_union.2 ⟨codeSupp'_supports H₂, _⟩ simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂ exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH - case cons₂ k IH => + | cons₂ k IH => have H' := H; rw [contSupp_cons₂] at H' exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH - case comp f k IH => + | comp f k IH => have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H' exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩ - case fix f k IH => + | fix f k IH => rw [contSupp] at H exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩ #align turing.partrec_to_TM2.cont_supp_supports Turing.PartrecToTM2.contSupp_supports diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean index bb407555229ca..fd523cfeab727 100644 --- a/Mathlib/Computability/TuringMachine.lean +++ b/Mathlib/Computability/TuringMachine.lean @@ -1321,32 +1321,32 @@ theorem stmts₁_self {q : Stmt₁} : q ∈ stmts₁ q := by theorem stmts₁_trans {q₁ q₂ : Stmt₁} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ := by intro h₁₂ q₀ h₀₁ - induction' q₂ with _ q IH _ q IH _ q IH <;> simp only [stmts₁] at h₁₂ ⊢ <;> - simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂ - iterate 3 - rcases h₁₂ with (rfl | h₁₂) - · unfold stmts₁ at h₀₁ - exact h₀₁ - · exact Finset.mem_insert_of_mem (IH h₁₂) - case branch p q₁ q₂ IH₁ IH₂ => + induction q₂ with ( + simp only [stmts₁] at h₁₂ ⊢ + simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂) + | branch p q₁ q₂ IH₁ IH₂ => rcases h₁₂ with (rfl | h₁₂ | h₁₂) · unfold stmts₁ at h₀₁ exact h₀₁ · exact Finset.mem_insert_of_mem (Finset.mem_union_left _ <| IH₁ h₁₂) · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ <| IH₂ h₁₂) - case goto l => subst h₁₂; exact h₀₁ - case halt => subst h₁₂; exact h₀₁ + | goto l => subst h₁₂; exact h₀₁ + | halt => subst h₁₂; exact h₀₁ + | _ _ q IH => + rcases h₁₂ with rfl | h₁₂ + · exact h₀₁ + · exact Finset.mem_insert_of_mem (IH h₁₂) #align turing.TM1.stmts₁_trans Turing.TM1.stmts₁_trans theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₁} (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂) : SupportsStmt S q₁ := by - induction' q₂ with _ q IH _ q IH _ q IH <;> + induction q₂ with 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 goto l => subst h; exact hs - case halt => subst h; trivial + | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2] + | goto l => subst h; exact hs + | halt => subst h; trivial + | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs] #align turing.TM1.stmts₁_supports_stmt_mono Turing.TM1.stmts₁_supportsStmt_mono /-- The set of all statements in a Turing machine, plus one extra value `none` representing the @@ -1383,14 +1383,14 @@ theorem step_supports (M : Λ → Stmt₁) {S : Finset Λ} (ss : Supports M S) : | ⟨some l₁, v, T⟩, c', h₁, h₂ => by replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂) simp only [step, Option.mem_def, Option.some.injEq] at h₁; subst c' - revert h₂; induction' M l₁ with _ q IH _ q IH _ q IH generalizing v T <;> intro hs - iterate 3 exact IH _ _ hs - case branch p q₁' q₂' IH₁ IH₂ => + revert h₂; induction M l₁ generalizing v T with intro hs + | branch p q₁' q₂' IH₁ IH₂ => unfold stepAux; cases p T.1 v · exact IH₂ _ _ hs.2 · exact IH₁ _ _ hs.1 - case goto => exact Finset.some_mem_insertNone.2 (hs _ _) - case halt => apply Multiset.mem_cons_self + | goto => exact Finset.some_mem_insertNone.2 (hs _ _) + | halt => apply Multiset.mem_cons_self + | _ _ q IH => exact IH _ _ hs #align turing.TM1.step_supports Turing.TM1.step_supports variable [Inhabited σ] @@ -1501,15 +1501,15 @@ theorem tr_respects : fun_respects.2 fun ⟨l₁, v, T⟩ ↦ by cases' l₁ with l₁; · exact rfl simp only [trCfg, TM1.step, FRespects, Option.map] - induction' M l₁ with _ _ IH _ _ IH _ _ IH generalizing v T - case move _ _ IH => exact TransGen.head rfl (IH _ _) - case write _ _ IH => exact TransGen.head rfl (IH _ _) - case load _ _ IH => exact (reaches₁_eq (by rfl)).2 (IH _ _) - case branch p _ _ IH₁ IH₂ => + induction M l₁ generalizing v T with + | move _ _ IH => exact TransGen.head rfl (IH _ _) + | write _ _ IH => exact TransGen.head rfl (IH _ _) + | load _ _ IH => exact (reaches₁_eq (by rfl)).2 (IH _ _) + | branch p _ _ IH₁ IH₂ => unfold TM1.stepAux; cases e : p T.1 v · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₂ _ _) · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₁ _ _) - iterate 2 + | _ => exact TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T))) #align turing.TM1to0.tr_respects Turing.TM1to0.tr_respects @@ -1550,20 +1550,20 @@ theorem tr_supports {S : Finset Λ} (ss : TM1.Supports M S) : cases q'; · exact Multiset.mem_cons_self _ _ simp only [tr, Option.mem_def] at h₁ have := TM1.stmts_supportsStmt ss h₂ - revert this; induction q generalizing v <;> intro hs - case move d q => + revert this; induction q generalizing v with intro hs + | move d q => cases h₁; refine' TM1.stmts_trans _ h₂ unfold TM1.stmts₁ exact Finset.mem_insert_of_mem TM1.stmts₁_self - case write b q => + | write b q => cases h₁; refine' TM1.stmts_trans _ h₂ unfold TM1.stmts₁ exact Finset.mem_insert_of_mem TM1.stmts₁_self - case load b q IH => + | load b q IH => refine' IH _ (TM1.stmts_trans _ h₂) h₁ hs unfold TM1.stmts₁ exact Finset.mem_insert_of_mem TM1.stmts₁_self - case branch p q₁ q₂ IH₁ IH₂ => + | branch p q₁ q₂ IH₁ IH₂ => cases h : p a v <;> rw [trAux, h] at h₁ · refine' IH₂ _ (TM1.stmts_trans _ h₂) h₁ hs.2 unfold TM1.stmts₁ @@ -1571,10 +1571,10 @@ theorem tr_supports {S : Finset Λ} (ss : TM1.Supports M S) : · refine' IH₁ _ (TM1.stmts_trans _ h₂) h₁ hs.1 unfold TM1.stmts₁ exact Finset.mem_insert_of_mem (Finset.mem_union_left _ TM1.stmts₁_self) - case goto l => + | goto l => cases h₁ exact Finset.some_mem_insertNone.2 (Finset.mem_biUnion.2 ⟨_, hs _ _, TM1.stmts₁_self⟩) - case halt => cases h₁ + | halt => cases h₁ #align turing.TM1to0.tr_supports Turing.TM1to0.tr_supports end @@ -1859,30 +1859,30 @@ theorem tr_respects {enc₀} : exact this _ R clear R l₁ intro q R - induction' q generalizing v L R - case move d q IH => + induction q generalizing v L R with + | move d q IH => cases d <;> simp only [trNormal, iterate, stepAux_move, stepAux, ListBlank.head_cons, Tape.move_left_mk', ListBlank.cons_head_tail, ListBlank.tail_cons, trTape'_move_left enc0, trTape'_move_right enc0] <;> apply IH - case write f q IH => + | write f q IH => simp only [trNormal, stepAux_read dec enc0 encdec, stepAux] refine' ReflTransGen.head rfl _ obtain ⟨a, R, rfl⟩ := R.exists_cons rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move, trTape'_move_left enc0, ListBlank.head_cons, ListBlank.tail_cons, Tape.write_mk'] apply IH - case load a q IH => + | load a q IH => simp only [trNormal, stepAux_read dec enc0 encdec] apply IH - case branch p q₁ q₂ IH₁ IH₂ => + | branch p q₁ q₂ IH₁ IH₂ => simp only [trNormal, stepAux_read dec enc0 encdec, stepAux] cases p R.head v <;> [apply IH₂; apply IH₁] - case goto l => + | goto l => simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk'] apply ReflTransGen.refl - case halt => + | halt => simp only [trNormal, stepAux, trCfg, stepAux_move, trTape'_move_left enc0, trTape'_move_right enc0, trTape_mk'] apply ReflTransGen.refl @@ -1919,12 +1919,12 @@ theorem tr_supports {S : Finset Λ} (ss : Supports M S) : Supports (tr enc dec M rcases Finset.mem_insert.1 h with (rfl | h) exacts [this.1, this.2 _ h] intro q hs hw - induction q - case move d q IH => + induction q with + | move d q IH => unfold writes at hw ⊢ replace IH := IH hs hw; refine' ⟨_, IH.2⟩ cases d <;> simp only [trNormal, iterate, supportsStmt_move, IH] - case write f q IH => + | write f q IH => unfold writes at hw ⊢ simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, exists_prop, true_and_iff] at hw ⊢ @@ -1933,21 +1933,21 @@ theorem tr_supports {S : Finset Λ} (ss : Supports M S) : Supports (tr enc dec M rcases hq with (⟨a, q₂, rfl⟩ | hq) · simp only [tr, supportsStmt_write, supportsStmt_move, IH.1] · exact IH.2 _ hq - case load a q IH => + | load a q IH => unfold writes at hw ⊢ replace IH := IH hs hw refine' ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩ - case branch p q₁ q₂ IH₁ IH₂ => + | branch p q₁ q₂ IH₁ IH₂ => unfold writes at hw ⊢ simp only [Finset.mem_union] at hw ⊢ replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq) replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq) exact ⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩ - case goto l => + | goto l => simp only [writes, Finset.not_mem_empty]; refine' ⟨_, fun _ ↦ False.elim⟩ refine' supportsStmt_read _ fun a _ s ↦ _ exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩ - case halt => + | halt => simp only [writes, Finset.not_mem_empty]; refine' ⟨_, fun _ ↦ False.elim⟩ simp only [SupportsStmt, supportsStmt_move, trNormal]⟩ #align turing.TM1to1.tr_supports Turing.TM1to1.tr_supports @@ -2191,32 +2191,33 @@ theorem stmts₁_self {q : Stmt₂} : q ∈ stmts₁ q := by theorem stmts₁_trans {q₁ q₂ : Stmt₂} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ := by intro h₁₂ q₀ h₀₁ - induction' q₂ with _ _ q IH _ _ q IH _ _ q IH _ q IH <;> simp only [stmts₁] at h₁₂ ⊢ <;> - simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂ - iterate 4 - rcases h₁₂ with (rfl | h₁₂) - · unfold stmts₁ at h₀₁ - exact h₀₁ - · exact Finset.mem_insert_of_mem (IH h₁₂) - case branch f q₁ q₂ IH₁ IH₂ => + induction q₂ with ( + simp only [stmts₁] at h₁₂ ⊢ + simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂) + | branch f q₁ q₂ IH₁ IH₂ => rcases h₁₂ with (rfl | h₁₂ | h₁₂) · unfold stmts₁ at h₀₁ exact h₀₁ · exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂)) · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂)) - case goto l => subst h₁₂; exact h₀₁ - case halt => subst h₁₂; exact h₀₁ + | goto l => subst h₁₂; exact h₀₁ + | halt => subst h₁₂; exact h₀₁ + | load _ q IH | _ _ _ q IH => + rcases h₁₂ with (rfl | h₁₂) + · unfold stmts₁ at h₀₁ + exact h₀₁ + · exact Finset.mem_insert_of_mem (IH h₁₂) #align turing.TM2.stmts₁_trans Turing.TM2.stmts₁_trans theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₂} (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂) : SupportsStmt S q₁ := by - induction' q₂ with _ _ q IH _ _ q IH _ _ q IH _ q IH <;> + induction q₂ with 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 goto l => subst h; exact hs - case halt => subst h; trivial + | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2] + | goto l => subst h; exact hs + | halt => subst h; trivial + | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs] #align turing.TM2.stmts₁_supports_stmt_mono Turing.TM2.stmts₁_supportsStmt_mono /-- The set of statements accessible from initial set `S` of labels. -/ @@ -2251,14 +2252,14 @@ theorem step_supports (M : Λ → Stmt₂) {S : Finset Λ} (ss : Supports M S) : | ⟨some l₁, v, T⟩, c', h₁, h₂ => by replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂) simp only [step, Option.mem_def, Option.some.injEq] at h₁; subst c' - revert h₂; induction' M l₁ with _ _ q IH _ _ q IH _ _ q IH _ q IH generalizing v T <;> intro hs - iterate 4 exact IH _ _ hs - case branch p q₁' q₂' IH₁ IH₂ => + revert h₂; induction M l₁ generalizing v T with intro hs + | branch p q₁' q₂' IH₁ IH₂ => unfold stepAux; cases p v · exact IH₂ _ _ hs.2 · exact IH₁ _ _ hs.1 - case goto => exact Finset.some_mem_insertNone.2 (hs _) - case halt => apply Multiset.mem_cons_self + | goto => exact Finset.some_mem_insertNone.2 (hs _) + | halt => apply Multiset.mem_cons_self + | load _ _ IH | _ _ _ _ IH => exact IH _ _ hs #align turing.TM2.step_supports Turing.TM2.step_supports variable [Inhabited σ] @@ -2556,8 +2557,8 @@ theorem tr_respects_aux₂ {k : K} {q : Stmt₂₁} {v : σ} {S : ∀ k, List ( TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) = TM1.stepAux q v' ((Tape.move Dir.right)^[(S' k).length] (Tape.mk' ∅ (addBottom L'))) := by - dsimp only; simp; cases o <;> simp only [stWrite, stVar, trStAct, TM1.stepAux] - case push f => + dsimp only; simp; cases o with simp only [stWrite, stVar, trStAct, TM1.stepAux] + | push f => have := Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k (some (f v))) refine' ⟨_, fun k' ↦ _, by @@ -2586,7 +2587,7 @@ theorem tr_respects_aux₂ {k : K} {q : Stmt₂₁} {v : σ} {S : ∀ k, List ( List.length_append, List.length_map] · split_ifs <;> rw [Function.update_noteq h', ← proj_map_nth, hL] rw [Function.update_noteq h'] - case peek f => + | peek f => rw [Function.update_eq_self] use L, hL; rw [Tape.move_left_right]; congr cases e : S k; · rfl @@ -2594,7 +2595,7 @@ theorem tr_respects_aux₂ {k : K} {q : Stmt₂₁} {v : σ} {S : ∀ k, List ( Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hL k), e, List.reverse_cons, ← List.length_reverse, List.get?_concat_length] rfl - case pop f => + | pop f => cases' e : S k with hd tl · simp only [Tape.mk'_head, ListBlank.head_cons, Tape.move_left_mk', List.length, Tape.write_mk', List.head?, iterate_zero_apply, List.tail_nil] diff --git a/Mathlib/Control/Fold.lean b/Mathlib/Control/Fold.lean index e30d6b1ab5f57..6ea46443cbd3a 100644 --- a/Mathlib/Control/Fold.lean +++ b/Mathlib/Control/Fold.lean @@ -382,9 +382,9 @@ theorem foldr_map (g : β → γ) (f : γ → α → α) (a : α) (l : t β) : @[simp] theorem toList_eq_self {xs : List α} : toList xs = xs := by simp only [toList_spec, foldMap, traverse] - induction xs - case nil => rfl - case cons _ _ ih => conv_rhs => rw [← ih]; rfl + induction xs with + | nil => rfl + | cons _ _ ih => conv_rhs => rw [← ih]; rfl #align traversable.to_list_eq_self Traversable.toList_eq_self theorem length_toList {xs : t α} : length xs = List.length (toList xs) := by diff --git a/Mathlib/Data/List/BigOperators/Basic.lean b/Mathlib/Data/List/BigOperators/Basic.lean index 92b1aa09509f2..454854f55a781 100644 --- a/Mathlib/Data/List/BigOperators/Basic.lean +++ b/Mathlib/Data/List/BigOperators/Basic.lean @@ -291,12 +291,12 @@ of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`. -/ theorem Sublist.prod_le_prod' [Preorder M] [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)] [CovariantClass M M (· * ·) (· ≤ ·)] {l₁ l₂ : List M} (h : l₁ <+ l₂) (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod := by - induction h - case slnil => rfl - case cons l₁ l₂ a _ ih' => + induction h with + | slnil => rfl + | cons a _ ih' => simp only [prod_cons, forall_mem_cons] at h₁ ⊢ exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1) - case cons₂ l₁ l₂ a _ ih' => + | cons₂ a _ ih' => simp only [prod_cons, forall_mem_cons] at h₁ ⊢ exact mul_le_mul_left' (ih' h₁.2) _ #align list.sublist.prod_le_prod' List.Sublist.prod_le_prod' diff --git a/Mathlib/Data/List/EditDistance/Defs.lean b/Mathlib/Data/List/EditDistance/Defs.lean index bf4bd6a00415f..358eb311864ef 100644 --- a/Mathlib/Data/List/EditDistance/Defs.lean +++ b/Mathlib/Data/List/EditDistance/Defs.lean @@ -124,10 +124,9 @@ theorem impl_cons_fst_zero (h) (w' : 0 < List.length ds) : theorem impl_length (d : {r : List δ // 0 < r.length}) (w : d.1.length = xs.length + 1) : (impl C xs y d).1.length = xs.length + 1 := by - induction xs generalizing d - · case nil => - rfl - · case cons x xs ih => + induction xs generalizing d with + | nil => rfl + | cons x xs ih => dsimp [impl] match d, w with | ⟨d₁ :: d₂ :: ds, _⟩, w => @@ -164,14 +163,14 @@ variable {C} theorem suffixLevenshtein_length (xs : List α) (ys : List β) : (suffixLevenshtein C xs ys).1.length = xs.length + 1 := by - induction ys - · case nil => + induction ys with + | nil => dsimp [suffixLevenshtein] - induction xs - · case nil => rfl - · case cons _ xs ih => + induction xs with + | nil => rfl + | cons _ xs ih => simp_all - · case cons y ys ih => + | cons y ys ih => dsimp [suffixLevenshtein] rw [impl_length] exact ih @@ -229,10 +228,10 @@ theorem suffixLevenshtein_cons₁ suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).1, by simp⟩ := by - induction ys - · case nil => + induction ys with + | nil => dsimp [levenshtein, suffixLevenshtein] - · case cons y ys ih => + | cons y ys ih => apply suffixLevenshtein_cons₁_aux · rfl · rw [suffixLevenshtein_cons₂ (x :: xs), ih, impl_cons] @@ -265,10 +264,10 @@ theorem suffixLevenshtein_cons_cons_fst_get_zero theorem suffixLevenshtein_eq_tails_map (xs ys) : (suffixLevenshtein C xs ys).1 = xs.tails.map fun xs' => levenshtein C xs' ys := by - induction xs - · case nil => + induction xs with + | nil => simp only [List.map, suffixLevenshtein_nil'] - · case cons x xs ih => + | cons x xs ih => simp only [List.map, suffixLevenshtein_cons₁, ih] @[simp] diff --git a/Mathlib/Data/List/Func.lean b/Mathlib/Data/List/Func.lean index 5b078a11ff3e1..362cd548a1daa 100644 --- a/Mathlib/Data/List/Func.lean +++ b/Mathlib/Data/List/Func.lean @@ -170,20 +170,16 @@ theorem get_set_eq_of_ne {a : α} : contradiction cases as <;> simp only [set, get, get_nil] | as, k + 1, m, h1 => by - -- porting note : I somewhat rearranged the case split - cases as <;> cases m - case nil => - simp only [set, get] - case nil m => - have h3 : get m (nil {k ↦ a}) = default := by - rw [get_set_eq_of_ne k m, get_nil] - intro hc - apply h1 - simp [hc] - apply h3 - case zero => - simp only [set, get] - case _ _ m => + -- porting note: I somewhat rearranged the case split + match as, m with + | as, 0 => cases as <;> simp only [set, get] + | [], m+1 => + show get m (nil {k ↦ a}) = default + rw [get_set_eq_of_ne k m, get_nil] + intro hc + apply h1 + simp [hc] + | _::_, m+1 => apply get_set_eq_of_ne k m intro hc apply h1 diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index 7342462419e54..cb7aa7c2c7126 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -145,18 +145,17 @@ theorem perm_comp_perm : (Perm ∘r Perm : List α → List α → Prop) = Perm theorem perm_comp_forall₂ {l u v} (hlu : Perm l u) (huv : Forall₂ r u v) : (Forall₂ r ∘r Perm) l v := by - induction hlu generalizing v - case nil => cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩ - case cons a l u _hlu ih => + induction hlu generalizing v with + | nil => cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩ + | cons u _hlu ih => cases' huv with _ b _ v hab huv' rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩ exact ⟨b :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩ - case swap a₁ a₂ h₂₃ => + | swap a₁ a₂ h₂₃ => cases' huv with _ b₁ _ l₂ h₁ hr₂₃ cases' hr₂₃ with _ b₂ _ l₂ h₂ h₁₂ exact ⟨b₂ :: b₁ :: l₂, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩ - case - trans la₁ la₂ la₃ _ _ ih₁ ih₂ => + | trans _ _ ih₁ ih₂ => rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩ rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩ exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩ @@ -267,11 +266,11 @@ theorem Perm.foldl_eq {f : β → α → β} {l₁ l₂ : List α} (rcomm : Righ theorem Perm.foldr_eq {f : α → β → β} {l₁ l₂ : List α} (lcomm : LeftCommutative f) (p : l₁ ~ l₂) : ∀ b, foldr f b l₁ = foldr f b l₂ := by intro b - induction p using Perm.recOnSwap' generalizing b - case nil => rfl - case cons r => simp; rw [r b] - case swap' r => simp; rw [lcomm, r b] - case trans r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b) + induction p using Perm.recOnSwap' generalizing b with + | nil => rfl + | cons _ _ r => simp; rw [r b] + | swap' _ _ _ r => simp; rw [lcomm, r b] + | trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b) #align list.perm.foldr_eq List.Perm.foldr_eq #align list.perm.rec_heq List.Perm.rec_heq @@ -358,16 +357,16 @@ alias ⟨subperm.of_cons, subperm.cons⟩ := subperm_cons theorem cons_subperm_of_mem {a : α} {l₁ l₂ : List α} (d₁ : Nodup l₁) (h₁ : a ∉ l₁) (h₂ : a ∈ l₂) (s : l₁ <+~ l₂) : a :: l₁ <+~ l₂ := by rcases s with ⟨l, p, s⟩ - induction s generalizing l₁ - case slnil => cases h₂ - case cons r₁ r₂ b s' ih => + induction s generalizing l₁ with + | slnil => cases h₂ + | @cons r₁ r₂ b s' ih => simp? at h₂ says simp only [mem_cons] at h₂ cases' h₂ with e m · subst b exact ⟨a :: r₁, p.cons a, s'.cons₂ _⟩ · rcases ih d₁ h₁ m p with ⟨t, p', s'⟩ exact ⟨t, p', s'.cons _⟩ - case cons₂ r₁ r₂ b _ ih => + | @cons₂ r₁ r₂ b _ ih => have bm : b ∈ l₁ := p.subset <| mem_cons_self _ _ have am : a ∈ r₂ := by simp only [find?, mem_cons] at h₂ @@ -503,9 +502,9 @@ theorem Perm.dedup {l₁ l₂ : List α} (p : l₁ ~ l₂) : dedup l₁ ~ dedup theorem Perm.inter_append {l t₁ t₂ : List α} (h : Disjoint t₁ t₂) : l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ := by - induction l - case nil => simp - case cons x xs l_ih => + induction l with + | nil => simp + | cons x xs l_ih => by_cases h₁ : x ∈ t₁ · have h₂ : x ∉ t₂ := h h₁ simp [*] diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean index 4d9ab07fff437..5021bd92f5060 100644 --- a/Mathlib/Data/List/Sublists.lean +++ b/Mathlib/Data/List/Sublists.lean @@ -157,11 +157,11 @@ theorem sublistsAux_eq_bind : theorem sublists_append (l₁ l₂ : List α) : sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x)) := by simp only [sublists, foldr_append] - induction l₁ - · case nil => simp - · case cons a l₁ ih => - rw [foldr_cons, ih] - simp [List.bind, join_join, Function.comp] + induction l₁ with + | nil => simp + | cons a l₁ ih => + rw [foldr_cons, ih] + simp [List.bind, join_join, Function.comp] #align list.sublists_append List.sublists_append --Portin note: New theorem diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 08a0cb1fb359f..fdb2cb1b51825 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -2778,18 +2778,17 @@ theorem rel_eq {s t : Multiset α} : Rel (· = ·) s t ↔ s = t := by theorem Rel.mono {r p : α → β → Prop} {s t} (hst : Rel r s t) (h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b) : Rel p s t := by - induction hst - case zero => exact Rel.zero - case - cons a b s t hab _hst ih => + induction hst with + | zero => exact Rel.zero + | @cons a b s t hab _hst ih => apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab) exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h' #align multiset.rel.mono Multiset.Rel.mono theorem Rel.add {s t u v} (hst : Rel r s t) (huv : Rel r u v) : Rel r (s + u) (t + v) := by - induction hst - case zero => simpa using huv - case cons a b s t hab hst ih => simpa using ih.cons hab + induction hst with + | zero => simpa using huv + | cons hab hst ih => simpa using ih.cons hab #align multiset.rel.add Multiset.Rel.add theorem rel_flip_eq {s t : Multiset α} : Rel (fun a b => b = a) s t ↔ s = t := @@ -2809,10 +2808,9 @@ theorem rel_cons_left {a as bs} : constructor · generalize hm : a ::ₘ as = m intro h - induction h generalizing as - case zero => simp at hm - case - cons a' b as' bs ha'b h ih => + induction h generalizing as with + | zero => simp at hm + | @cons a' b as' bs ha'b h ih => rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩) · subst eq₁ subst eq₂ diff --git a/Mathlib/Data/Multiset/Bind.lean b/Mathlib/Data/Multiset/Bind.lean index c4fc8b85216ba..275725fde8fad 100644 --- a/Mathlib/Data/Multiset/Bind.lean +++ b/Mathlib/Data/Multiset/Bind.lean @@ -76,9 +76,9 @@ theorem card_join (S) : card (@join α S) = sum (map card S) := #align multiset.card_join Multiset.card_join theorem rel_join {r : α → β → Prop} {s t} (h : Rel (Rel r) s t) : Rel r s.join t.join := by - induction h - case zero => simp - case cons a b s t hab hst ih => simpa using hab.add ih + induction h with + | zero => simp + | cons hab hst ih => simpa using hab.add ih #align multiset.rel_join Multiset.rel_join /-! ### Bind -/ diff --git a/Mathlib/Data/Multiset/Functor.lean b/Mathlib/Data/Multiset/Functor.lean index 7b98d000e794c..9866ed29c04a4 100644 --- a/Mathlib/Data/Multiset/Functor.lean +++ b/Mathlib/Data/Multiset/Functor.lean @@ -41,14 +41,14 @@ variable {α' β' : Type u} (f : α' → F β') def traverse : Multiset α' → F (Multiset β') := by refine' Quotient.lift (Functor.map Coe.coe ∘ Traversable.traverse f) _ introv p; unfold Function.comp - induction p - case nil => rfl - case cons x l₁ l₂ _ h => + induction p with + | nil => rfl + | @cons x l₁ l₂ _ h => have : Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ = Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ := by rw [h] simpa [functor_norm] using this - case swap x y l => + | swap x y l => have : (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by @@ -57,7 +57,7 @@ def traverse : Multiset α' → F (Multiset β') := by funext a b l simpa [flip] using Perm.swap a b l simp [(· ∘ ·), this, functor_norm, Coe.coe] - case trans => simp [*] + | trans => simp [*] #align multiset.traverse Multiset.traverse instance : Monad Multiset := diff --git a/Mathlib/Data/Multiset/Sections.lean b/Mathlib/Data/Multiset/Sections.lean index 66eb763db0f4b..ac7819f0a695e 100644 --- a/Mathlib/Data/Multiset/Sections.lean +++ b/Mathlib/Data/Multiset/Sections.lean @@ -58,9 +58,9 @@ theorem sections_add (s t : Multiset (Multiset α)) : theorem mem_sections {s : Multiset (Multiset α)} : ∀ {a}, a ∈ Sections s ↔ s.Rel (fun s a => a ∈ s) a := by - induction s using Multiset.induction_on - case empty => simp - case cons a a' ih => simp [ih, rel_cons_left, eq_comm] + induction s using Multiset.induction_on with + | empty => simp + | cons ih => simp [ih, rel_cons_left, eq_comm] #align multiset.mem_sections Multiset.mem_sections theorem card_sections {s : Multiset (Multiset α)} : card (Sections s) = prod (s.map card) := diff --git a/Mathlib/Data/MvPolynomial/Basic.lean b/Mathlib/Data/MvPolynomial/Basic.lean index 6120acc00166c..5bafaae1547a1 100644 --- a/Mathlib/Data/MvPolynomial/Basic.lean +++ b/Mathlib/Data/MvPolynomial/Basic.lean @@ -508,10 +508,10 @@ theorem algHom_C (f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (r : R) : f theorem adjoin_range_X : Algebra.adjoin R (range (X : σ → MvPolynomial σ R)) = ⊤ := by set S := Algebra.adjoin R (range (X : σ → MvPolynomial σ R)) refine' top_unique fun p hp => _; clear hp - induction p using MvPolynomial.induction_on - case h_C => exact S.algebraMap_mem _ - case h_add p q hp hq => exact S.add_mem hp hq - case h_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _) + induction p using MvPolynomial.induction_on with + | h_C => exact S.algebraMap_mem _ + | h_add p q hp hq => exact S.add_mem hp hq + | h_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _) #align mv_polynomial.adjoin_range_X MvPolynomial.adjoin_range_X @[ext] diff --git a/Mathlib/Data/Nat/Choose/Sum.lean b/Mathlib/Data/Nat/Choose/Sum.lean index 7b884dc00bfe1..4fc5443a4c328 100644 --- a/Mathlib/Data/Nat/Choose/Sum.lean +++ b/Mathlib/Data/Nat/Choose/Sum.lean @@ -136,8 +136,9 @@ end Nat theorem Int.alternating_sum_range_choose {n : ℕ} : (∑ m in range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ)) = if n = 0 then 1 else 0 := by - cases n; · simp - case succ n => + cases n with + | zero => simp + | succ n => have h := add_pow (-1 : ℤ) 1 n.succ simp only [one_pow, mul_one, add_left_neg] at h rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)] diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 04a3e396ce47a..bee9a51e38009 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -70,8 +70,7 @@ of `p` in the factorization of `n`: we declare the former to be the simp-normal theorem factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p := by rcases n.eq_zero_or_pos with (rfl | hn0) · simp [factorization, count] - by_cases pp : p.Prime - case neg => + if pp : p.Prime then ?_ else rw [count_eq_zero_of_not_mem (mt prime_of_mem_factors pp)] simp [factorization, pp] simp only [factorization, coe_mk, pp, if_true] @@ -337,8 +336,7 @@ theorem ord_compl_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ord_compl[p] n = n #align nat.ord_compl_of_not_prime Nat.ord_compl_of_not_prime theorem ord_proj_dvd (n p : ℕ) : ord_proj[p] n ∣ n := by - by_cases hp : p.Prime - case neg => simp [hp] + if hp : p.Prime then ?_ else simp [hp] rw [← factors_count_eq] apply dvd_of_factors_subperm (pow_ne_zero _ hp.ne_zero) rw [hp.factors_pow, List.subperm_ext_iff] @@ -351,9 +349,7 @@ theorem ord_compl_dvd (n p : ℕ) : ord_compl[p] n ∣ n := #align nat.ord_compl_dvd Nat.ord_compl_dvd theorem ord_proj_pos (n p : ℕ) : 0 < ord_proj[p] n := by - by_cases pp : p.Prime - · simp [pow_pos pp.pos] - · simp [pp] + if pp : p.Prime then simp [pow_pos pp.pos] else simp [pp] #align nat.ord_proj_pos Nat.ord_proj_pos theorem ord_proj_le {n : ℕ} (p : ℕ) (hn : n ≠ 0) : ord_proj[p] n ≤ n := @@ -361,9 +357,10 @@ theorem ord_proj_le {n : ℕ} (p : ℕ) (hn : n ≠ 0) : ord_proj[p] n ≤ n := #align nat.ord_proj_le Nat.ord_proj_le theorem ord_compl_pos {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < ord_compl[p] n := by - cases' em' p.Prime with pp pp - · simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt - exact Nat.div_pos (ord_proj_le p hn) (ord_proj_pos n p) + if pp : p.Prime then + exact Nat.div_pos (ord_proj_le p hn) (ord_proj_pos n p) + else + simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt #align nat.ord_compl_pos Nat.ord_compl_pos theorem ord_compl_le (n p : ℕ) : ord_compl[p] n ≤ n := @@ -380,10 +377,8 @@ theorem ord_proj_mul {a b : ℕ} (p : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : #align nat.ord_proj_mul Nat.ord_proj_mul theorem ord_compl_mul (a b p : ℕ) : ord_compl[p] (a * b) = ord_compl[p] a * ord_compl[p] b := by - rcases eq_or_ne a 0 with (rfl | ha) - · simp - rcases eq_or_ne b 0 with (rfl | hb) - · simp + if ha : a = 0 then simp [ha] else + if hb : b = 0 then simp [hb] else simp only [ord_proj_mul p ha hb] rw [mul_div_mul_comm_of_dvd_dvd (ord_proj_dvd a p) (ord_proj_dvd b p)] #align nat.ord_compl_mul Nat.ord_compl_mul @@ -401,11 +396,11 @@ theorem factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p /-- An upper bound on `n.factorization p` -/ theorem factorization_le_of_le_pow {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b := by - rcases eq_or_ne n 0 with (rfl | hn) - · simp - by_cases pp : p.Prime - · exact (pow_le_pow_iff_right pp.one_lt).1 ((ord_proj_le p hn).trans hb) - · simp [factorization_eq_zero_of_non_prime n pp] + if hn : n = 0 then simp [hn] else + if pp : p.Prime then + exact (pow_le_pow_iff_right pp.one_lt).1 ((ord_proj_le p hn).trans hb) + else + simp [factorization_eq_zero_of_non_prime n pp] #align nat.factorization_le_of_le_pow Nat.factorization_le_of_le_pow theorem factorization_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : @@ -501,9 +496,8 @@ theorem coprime_ord_compl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : Coprime p theorem factorization_ord_compl (n p : ℕ) : (ord_compl[p] n).factorization = n.factorization.erase p := by - rcases eq_or_ne n 0 with (rfl | hn); · simp - by_cases pp : p.Prime - case neg => + if hn : n = 0 then simp [hn] else + if pp : p.Prime then ?_ else -- porting note: needed to solve side goal explicitly rw [Finsupp.erase_of_not_mem_support] <;> simp [pp] ext q @@ -517,14 +511,14 @@ theorem factorization_ord_compl (n p : ℕ) : -- `ord_compl[p] n` is the largest divisor of `n` not divisible by `p`. theorem dvd_ord_compl_of_dvd_not_dvd {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) : d ∣ ord_compl[p] n := by - rcases eq_or_ne n 0 with (rfl | hn0); · simp - rcases eq_or_ne d 0 with (rfl | hd0); - · simp at hpd + if hn0 : n = 0 then simp [hn0] else + if hd0 : d = 0 then simp [hd0] at hpd else rw [← factorization_le_iff_dvd hd0 (ord_compl_pos p hn0).ne', factorization_ord_compl] intro q - rcases eq_or_ne q p with (rfl | hqp) - · simp [factorization_eq_zero_iff, hpd] - · simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q] + if hqp : q = p then + simp [factorization_eq_zero_iff, hqp, hpd] + else + simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q] #align nat.dvd_ord_compl_of_dvd_not_dvd Nat.dvd_ord_compl_of_dvd_not_dvd /-- If `n` is a nonzero natural number and `p ≠ 1`, then there are natural numbers `e` @@ -591,10 +585,8 @@ theorem ord_compl_dvd_ord_compl_iff_dvd (a b : ℕ) : refine' ⟨fun h => _, fun hab p => ord_compl_dvd_ord_compl_of_dvd hab p⟩ rcases eq_or_ne b 0 with (rfl | hb0) · simp - by_cases pa : a.Prime - case neg => simpa [pa] using h a - by_cases pb : b.Prime - case neg => simpa [pb] using h b + if pa : a.Prime then ?_ else simpa [pa] using h a + if pb : b.Prime then ?_ else simpa [pb] using h b rw [prime_dvd_prime_iff_eq pa pb] by_contra hab apply pa.ne_one diff --git a/Mathlib/Data/Nat/ForSqrt.lean b/Mathlib/Data/Nat/ForSqrt.lean index 3b65c86705b99..cc60bdfbc1620 100644 --- a/Mathlib/Data/Nat/ForSqrt.lean +++ b/Mathlib/Data/Nat/ForSqrt.lean @@ -20,16 +20,15 @@ section Misc -- porting note: Miscellaneous lemmas that should be integrated with `Mathlib` in the future protected lemma mul_le_of_le_div (k x y : ℕ) (h : x ≤ y / k) : x * k ≤ y := by - by_cases hk : k = 0 - case pos => rw [hk, mul_zero]; exact zero_le _ - case neg => rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)] + if hk : k = 0 then + rw [hk, mul_zero]; exact zero_le _ + else + rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)] protected lemma div_mul_div_le (a b c d : ℕ) : (a / b) * (c / d) ≤ (a * c) / (b * d) := by - by_cases hb : b = 0 - case pos => simp [hb] - by_cases hd : d = 0 - case pos => simp [hd] + if hb : b = 0 then simp [hb] else + if hd : d = 0 then simp [hd] else have hbd : b * d ≠ 0 := mul_ne_zero hb hd rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)] transitivity ((a / b) * b) * ((c / d) * d) @@ -41,9 +40,10 @@ private lemma iter_fp_bound (n k : ℕ) : sqrt.iter n k ≤ iter_next n (sqrt.iter n k) := by intro iter_next unfold sqrt.iter - by_cases h : (k + n / k) / 2 < k - case pos => simp [if_pos h]; exact iter_fp_bound _ _ - case neg => simp [if_neg h]; exact Nat.le_of_not_lt h + if h : (k + n / k) / 2 < k then + simp [if_pos h]; exact iter_fp_bound _ _ + else + simp [if_neg h]; exact Nat.le_of_not_lt h private lemma AM_GM : {a b : ℕ} → (4 * a * b ≤ (a + b) * (a + b)) | 0, _ => by rw [mul_zero, zero_mul]; exact zero_le _ @@ -63,9 +63,9 @@ section Std lemma sqrt.iter_sq_le (n guess : ℕ) : sqrt.iter n guess * sqrt.iter n guess ≤ n := by unfold sqrt.iter let next := (guess + n / guess) / 2 - by_cases h : next < guess - case pos => simpa only [dif_pos h] using sqrt.iter_sq_le n next - case neg => + if h : next < guess then + simpa only [dif_pos h] using sqrt.iter_sq_le n next + else simp only [dif_neg h] apply Nat.mul_le_of_le_div apply le_of_add_le_add_left (a := guess) @@ -78,8 +78,7 @@ lemma sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) unfold sqrt.iter -- m was `next` let m := (guess + n / guess) / 2 - by_cases h : m < guess - case pos => + if h : m < guess then suffices n < (m + 1) * (m + 1) by simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le @@ -95,7 +94,7 @@ lemma sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma) rw [add_assoc, mul_add] exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _ - case neg => + else simpa only [dif_neg h] using hn end Std diff --git a/Mathlib/Data/Nat/GCD/Basic.lean b/Mathlib/Data/Nat/GCD/Basic.lean index f479a85070d46..bc2dd4c6a0581 100644 --- a/Mathlib/Data/Nat/GCD/Basic.lean +++ b/Mathlib/Data/Nat/GCD/Basic.lean @@ -283,12 +283,12 @@ See `exists_dvd_and_dvd_of_dvd_mul` for the more general but less constructive v `GCDMonoid`s. -/ def prodDvdAndDvdOfDvdProd {m n k : ℕ} (H : k ∣ m * n) : { d : { m' // m' ∣ m } × { n' // n' ∣ n } // k = d.1 * d.2 } := by - cases h0 : gcd k m - case zero => + cases h0 : gcd k m with + | zero => obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0 obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0 exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩ - case succ tmp => + | succ tmp => have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _; clear h0 tmp have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m) refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩ diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean index b4a612239c28f..9aa0fff361729 100644 --- a/Mathlib/Data/Num/Lemmas.lean +++ b/Mathlib/Data/Num/Lemmas.lean @@ -970,10 +970,10 @@ theorem castNum_shiftRight (m : Num) (n : Nat) : ↑(m >>> n) = (m : ℕ) >>> (n @[simp] theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by -- Porting note: `unfold` → `dsimp only` - cases m <;> dsimp only [testBit] - case zero => + cases m with dsimp only [testBit] + | zero => rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit] - case pos m => + | pos m => rw [cast_pos] induction' n with n IH generalizing m <;> cases' m with m m <;> dsimp only [PosNum.testBit, Nat.zero_eq] diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean index 695ef5d7fedcd..56dc69b12e1a1 100644 --- a/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean +++ b/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean @@ -266,10 +266,10 @@ theorem Cofix.bisim_rel {α : TypeVec n} (r : Cofix F α → Cofix F α → Prop left rfl · intro x y r'xy - cases r'xy - case inl h => + cases r'xy with + | inl h => rw [h] - case inr r'xy => + | inr r'xy => have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h rw [← Quot.factor_mk_eq _ _ this] dsimp diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean index 9f0f96058ea8e..c01cd76908b93 100644 --- a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean +++ b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean @@ -123,10 +123,10 @@ set_option linter.uppercaseLean3 false in #align mvqpf.Wequiv.refl MvQPF.wEquiv.refl theorem wEquiv.symm {α : TypeVec n} (x y : q.P.W α) : WEquiv x y → WEquiv y x := by - intro h; induction h - case ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih - case abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm - case trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁ + intro h; induction h with + | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih + | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm + | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁ set_option linter.uppercaseLean3 false in #align mvqpf.Wequiv.symm MvQPF.wEquiv.symm @@ -156,16 +156,15 @@ set_option linter.uppercaseLean3 false in theorem wEquiv_map {α β : TypeVec n} (g : α ⟹ β) (x y : q.P.W α) : WEquiv x y → WEquiv (g <$$> x) (g <$$> y) := by - intro h; induction h - case ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih - case - abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => + intro h; induction h with + | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih + | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs show abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) = abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x)) rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h] - case trans x y z _ _ ih₁ ih₂ => apply MvQPF.WEquiv.trans; apply ih₁; apply ih₂ + | trans x y z _ _ ih₁ ih₂ => apply MvQPF.WEquiv.trans; apply ih₁; apply ih₂ set_option linter.uppercaseLean3 false in #align mvqpf.Wequiv_map MvQPF.wEquiv_map diff --git a/Mathlib/Data/QPF/Univariate/Basic.lean b/Mathlib/Data/QPF/Univariate/Basic.lean index ee47afa0ec54e..9f3873f283372 100644 --- a/Mathlib/Data/QPF/Univariate/Basic.lean +++ b/Mathlib/Data/QPF/Univariate/Basic.lean @@ -192,10 +192,10 @@ set_option linter.uppercaseLean3 false in theorem recF_eq_of_Wequiv {α : Type u} (u : F α → α) (x y : q.P.W) : Wequiv x y → recF u x = recF u y := by intro h - induction h - case ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp, ih] - case abs a f a' f' h => simp only [recF_eq', abs_map, h] - case trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂ + induction h with + | ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp, ih] + | abs a f a' f' h => simp only [recF_eq', abs_map, h] + | trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂ set_option linter.uppercaseLean3 false in #align qpf.recF_eq_of_Wequiv QPF.recF_eq_of_Wequiv @@ -215,10 +215,10 @@ set_option linter.uppercaseLean3 false in theorem Wequiv.symm (x y : q.P.W) : Wequiv x y → Wequiv y x := by intro h - induction h - case ind a f f' _ ih => exact Wequiv.ind _ _ _ ih - case abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm - case trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁ + induction h with + | ind a f f' _ ih => exact Wequiv.ind _ _ _ ih + | abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm + | trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁ set_option linter.uppercaseLean3 false in #align qpf.Wequiv.symm QPF.Wequiv.symm diff --git a/Mathlib/Data/Set/Enumerate.lean b/Mathlib/Data/Set/Enumerate.lean index 0d80176c23ea9..c41c89c9a0da6 100644 --- a/Mathlib/Data/Set/Enumerate.lean +++ b/Mathlib/Data/Set/Enumerate.lean @@ -49,10 +49,9 @@ theorem enumerate_eq_none : | s, n + 1, m => fun h hm ↦ by cases hs : sel s · exact enumerate_eq_none_of_sel sel hs - · cases m - case zero => - contradiction - case succ m' => + · cases m with + | zero => contradiction + | succ m' => simp? [hs, enumerate] at h ⊢ says simp only [enumerate, hs, Nat.add_eq, add_zero] at h ⊢ have hm : n ≤ m' := Nat.le_of_succ_le_succ hm exact enumerate_eq_none h hm @@ -62,9 +61,9 @@ theorem enumerate_mem (h_sel : ∀ s a, sel s = some a → a ∈ s) : ∀ {s n a}, enumerate sel s n = some a → a ∈ s | s, 0, a => h_sel s a | s, n + 1, a => by - cases h : sel s - case none => simp [enumerate_eq_none_of_sel, h] - case some a' => + cases h : sel s with + | none => simp [enumerate_eq_none_of_sel, h] + | some a' => simp only [enumerate, h, Nat.add_eq, add_zero] exact fun h' : enumerate sel (s \ {a'}) n = some a ↦ have : a ∈ s \ {a'} := enumerate_mem h_sel h' @@ -80,21 +79,21 @@ theorem enumerate_inj {n₁ n₂ : ℕ} {a : α} {s : Set α} (h_sel : ∀ s a, all_goals rcases Nat.le.dest hn with ⟨m, rfl⟩ clear hn - induction n₁ generalizing s - case zero => - cases m - case zero => rfl - case succ m => + induction n₁ generalizing s with + | zero => + cases m with + | zero => rfl + | succ m => have h' : enumerate sel (s \ {a}) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add]; exact h₂ have : a ∈ s \ {a} := enumerate_mem sel h_sel h' simp_all [Set.mem_diff_singleton] - case succ k ih => - cases h : sel s + | succ k ih => + cases h : sel s with /- porting note : The original covered both goals with just `simp_all <;> tauto` -/ - case none => + | none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h] - case some _ => + | some => simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2, Nat.succ.injEq] exact ih h₁ h₂ diff --git a/Mathlib/Data/Stream/Init.lean b/Mathlib/Data/Stream/Init.lean index f49b1f28083b4..91d7f74a4b541 100644 --- a/Mathlib/Data/Stream/Init.lean +++ b/Mathlib/Data/Stream/Init.lean @@ -606,8 +606,9 @@ theorem get?_take_succ (n : Nat) (s : Stream' α) : @[simp] theorem dropLast_take {xs : Stream' α} : (Stream'.take n xs).dropLast = Stream'.take (n-1) xs := by - cases n; case zero => simp - case succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one] + cases n with + | zero => simp + | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one] @[simp] theorem append_take_drop : ∀ (n : Nat) (s : Stream' α), diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean index fbba2143b40e0..e5a84d7624755 100644 --- a/Mathlib/Data/TypeVec.lean +++ b/Mathlib/Data/TypeVec.lean @@ -489,9 +489,9 @@ def ofRepeat {α : Sort _} : ∀ {n i}, «repeat» n α i → α #align typevec.of_repeat TypeVec.ofRepeat theorem const_iff_true {α : TypeVec n} {i x p} : ofRepeat (TypeVec.const p α i x) ↔ p := by - induction i - case fz => rfl - case fs _ ih => erw [TypeVec.const, @ih (drop α) x] + induction i with + | fz => rfl + | fs _ ih => erw [TypeVec.const, @ih (drop α) x] #align typevec.const_iff_true TypeVec.const_iff_true @@ -556,28 +556,28 @@ protected def prod.map : ∀ {n} {α α' β β' : TypeVec.{u} n}, α ⟹ β → theorem fst_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') : TypeVec.prod.fst ⊚ (f ⊗' g) = f ⊚ TypeVec.prod.fst := by - funext i; induction i - case fz => rfl - case fs _ _ i_ih => apply i_ih + funext i; induction i with + | fz => rfl + | fs _ i_ih => apply i_ih #align typevec.fst_prod_mk TypeVec.fst_prod_mk theorem snd_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') : TypeVec.prod.snd ⊚ (f ⊗' g) = g ⊚ TypeVec.prod.snd := by - funext i; induction i - case fz => rfl - case fs _ _ i_ih => apply i_ih + funext i; induction i with + | fz => rfl + | fs _ i_ih => apply i_ih #align typevec.snd_prod_mk TypeVec.snd_prod_mk theorem fst_diag {α : TypeVec n} : TypeVec.prod.fst ⊚ (prod.diag : α ⟹ _) = id := by - funext i; induction i - case fz => rfl - case fs _ _ i_ih => apply i_ih + funext i; induction i with + | fz => rfl + | fs _ i_ih => apply i_ih #align typevec.fst_diag TypeVec.fst_diag theorem snd_diag {α : TypeVec n} : TypeVec.prod.snd ⊚ (prod.diag : α ⟹ _) = id := by - funext i; induction i - case fz => rfl - case fs _ _ i_ih => apply i_ih + funext i; induction i with + | fz => rfl + | fs _ i_ih => apply i_ih #align typevec.snd_diag TypeVec.snd_diag theorem repeatEq_iff_eq {α : TypeVec n} {i x y} : diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean index e3001bb438f2f..37fbf3562f6f6 100644 --- a/Mathlib/Data/Vector/Basic.lean +++ b/Mathlib/Data/Vector/Basic.lean @@ -799,10 +799,10 @@ variable (ys : Vector β n) theorem get_map₂ (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β → γ) (i : Fin n) : get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i) := by clear * - v₁ v₂ - induction v₁, v₂ using inductionOn₂ - case nil => + induction v₁, v₂ using inductionOn₂ with + | nil => exact Fin.elim0 i - case cons x xs y ys ih => + | cons ih => rw [map₂_cons] cases i using Fin.cases · simp only [get_zero, head_cons] diff --git a/Mathlib/Data/Vector/MapLemmas.lean b/Mathlib/Data/Vector/MapLemmas.lean index 7790a8ff975bd..056653ebd02d6 100644 --- a/Mathlib/Data/Vector/MapLemmas.lean +++ b/Mathlib/Data/Vector/MapLemmas.lean @@ -342,10 +342,9 @@ variable {xs : Vector α n} {ys : Vector β n} theorem mapAccumr₂_unused_input_left [Inhabited α] (f : α → β → σ → σ × γ) (h : ∀ a b s, f default b s = f a b s) : mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s := by - induction xs, ys using Vector.revInductionOn₂ generalizing s - case nil => rfl - case snoc xs ys x y ih => - simp[h x y s, ih] + induction xs, ys using Vector.revInductionOn₂ generalizing s with + | nil => rfl + | snoc xs ys x y ih => simp [h x y s, ih] /-- If `f` returns the same output and next state for every value of it's second argument, then @@ -355,10 +354,9 @@ theorem mapAccumr₂_unused_input_left [Inhabited α] (f : α → β → σ → theorem mapAccumr₂_unused_input_right [Inhabited β] (f : α → β → σ → σ × γ) (h : ∀ a b s, f a default s = f a b s) : mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s := by - induction xs, ys using Vector.revInductionOn₂ generalizing s - case nil => rfl - case snoc xs ys x y ih => - simp[h x y s, ih] + induction xs, ys using Vector.revInductionOn₂ generalizing s with + | nil => rfl + | snoc xs ys x y ih => simp [h x y s, ih] end UnusedInput diff --git a/Mathlib/Data/Vector/Snoc.lean b/Mathlib/Data/Vector/Snoc.lean index f9afb271985ed..e619a76d802ba 100644 --- a/Mathlib/Data/Vector/Snoc.lean +++ b/Mathlib/Data/Vector/Snoc.lean @@ -55,14 +55,12 @@ theorem reverse_snoc : reverse (xs.snoc x) = x ::ᵥ (reverse xs) := by theorem replicate_succ_to_snoc (val : α) : replicate (n+1) val = (replicate n val).snoc val := by clear xs - induction n - case zero => rfl - case succ n ih => + induction n with + | zero => rfl + | succ n ih => rw [replicate_succ] - conv => { - rhs; rw [replicate_succ] - } - rw[snoc_cons, ih] + conv => rhs; rw [replicate_succ] + rw [snoc_cons, ih] end Simp diff --git a/Mathlib/Deprecated/Submonoid.lean b/Mathlib/Deprecated/Submonoid.lean index 74979843dd31b..e1fa90237a3b4 100644 --- a/Mathlib/Deprecated/Submonoid.lean +++ b/Mathlib/Deprecated/Submonoid.lean @@ -370,10 +370,10 @@ a list of elements of `s` whose product is `a`. -/ a set `s`, there exists a list of elements of `s` whose sum is `a`."] theorem exists_list_of_mem_closure {s : Set M} {a : M} (h : a ∈ Closure s) : ∃ l : List M, (∀ x ∈ l, x ∈ s) ∧ l.prod = a := by - induction h - case basic a ha => exists [a]; simp [ha] - case one => exists []; simp - case mul a b _ _ ha hb => + induction h with + | @basic a ha => exists [a]; simp [ha] + | one => exists []; simp + | mul _ _ ha hb => rcases ha with ⟨la, ha, eqa⟩ rcases hb with ⟨lb, hb, eqb⟩ exists la ++ lb diff --git a/Mathlib/FieldTheory/PerfectClosure.lean b/Mathlib/FieldTheory/PerfectClosure.lean index a74acb381759f..0489e266fb725 100644 --- a/Mathlib/FieldTheory/PerfectClosure.lean +++ b/Mathlib/FieldTheory/PerfectClosure.lean @@ -286,11 +286,11 @@ theorem eq_iff' (x y : ℕ × K) : constructor · intro H replace H := Quot.exact _ H - induction H - case rel x y H => cases' H with n x; exact ⟨0, rfl⟩ - case refl H => exact ⟨0, rfl⟩ - case symm x y H ih => cases' ih with w ih; exact ⟨w, ih.symm⟩ - case trans x y z H1 H2 ih1 ih2 => + induction H with + | rel x y H => cases' H with n x; exact ⟨0, rfl⟩ + | refl H => exact ⟨0, rfl⟩ + | symm x y H ih => cases' ih with w ih; exact ⟨w, ih.symm⟩ + | trans x y z H1 H2 ih1 ih2 => cases' ih1 with z1 ih1 cases' ih2 with z2 ih2 exists z2 + (y.1 + z1) @@ -344,9 +344,9 @@ theorem frobenius_mk (x : ℕ × K) : dsimp only suffices ∀ p' : ℕ, mk K p (n, x) ^ p' = mk K p (n, x ^ p') by apply this intro p - induction' p with p ih - case zero => apply R.sound; rw [(frobenius _ _).iterate_map_one, pow_zero] - case succ => + induction p with + | zero => apply R.sound; rw [(frobenius _ _).iterate_map_one, pow_zero] + | succ p ih => rw [pow_succ, ih] symm apply R.sound diff --git a/Mathlib/GroupTheory/Coprod/Basic.lean b/Mathlib/GroupTheory/Coprod/Basic.lean index 223653e25dcc6..27f597591adbf 100644 --- a/Mathlib/GroupTheory/Coprod/Basic.lean +++ b/Mathlib/GroupTheory/Coprod/Basic.lean @@ -573,9 +573,9 @@ theorem mk_of_inv_mul : ∀ x : G ⊕ H, mk (of (x.map Inv.inv Inv.inv)) * mk (o theorem con_mul_left_inv (x : FreeMonoid (G ⊕ H)) : coprodCon G H (ofList (x.toList.map (Sum.map Inv.inv Inv.inv)).reverse * x) 1 := by rw [← mk_eq_mk, map_mul, map_one] - induction x using FreeMonoid.recOn - case h0 => simp [map_one mk] -- TODO: fails without `[map_one mk]` - case ih x xs ihx => + induction x using FreeMonoid.recOn with + | h0 => simp [map_one mk] -- TODO: fails without `[map_one mk]` + | ih x xs ihx => simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ihx, ofList_singleton] rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul] diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean index 2dad3da8a9ef3..4a10af8348449 100644 --- a/Mathlib/GroupTheory/FreeGroup/Basic.lean +++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean @@ -402,8 +402,8 @@ theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length := theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)}, Step L₁ L₂ → sizeOf L₂ < sizeOf L₁ | _, _, @Step.not _ L1 L2 x b => by - induction' L1 with hd tl ih - case nil => + induction L1 with + | nil => -- dsimp [sizeOf] dsimp simp only [Bool.sizeOf_eq_one] @@ -416,7 +416,7 @@ theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)}, apply Nat.lt_add_of_pos_right apply Nat.lt_add_right apply Nat.zero_lt_one - case cons => + | cons hd tl ih => dsimp exact Nat.add_lt_add_left ih _ #align free_group.red.sizeof_of_step FreeGroup.Red.sizeof_of_step @@ -1123,16 +1123,16 @@ theorem reduce.cons (x) : @[to_additive "The first theorem that characterises the function `reduce`: a word reduces to its maximal reduction."] theorem reduce.red : Red L (reduce L) := by - induction' L with hd1 tl1 ih - case nil => constructor - case cons => + induction L with + | nil => constructor + | cons hd1 tl1 ih => dsimp revert ih generalize htl : reduce tl1 = TL intro ih - cases' TL with hd2 tl2 - case nil => exact Red.cons_cons ih - case cons => + cases TL with + | nil => exact Red.cons_cons ih + | cons hd2 tl2 => dsimp only split_ifs with h · trans @@ -1147,41 +1147,37 @@ theorem reduce.red : Red L (reduce L) := by #align free_group.reduce.red FreeGroup.reduce.red #align free_add_group.reduce.red FreeAddGroup.reduce.red --- porting notes: deleted mathport junk and manually formatted below. @[to_additive] -theorem reduce.not {p : Prop} : ∀ {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b}, - ((reduce L₁) = L₂ ++ ((x,b)::(x ,!b)::L₃)) → p - | [], L2 ,L3, _, _ => fun h => by cases L2 <;> injections - | (x, b)::L1, L2, L3, x', b' => by - dsimp - cases r : reduce L1 with - | nil => - dsimp - intro h - exfalso - have := congr_arg List.length h - simp? [List.length] at this says - simp only [List.length, zero_add, List.length_append] at this - rw [add_comm, add_assoc, add_assoc, add_comm, <-add_assoc] at this - simp [Nat.one_eq_succ_zero, Nat.succ_add] at this - -- Porting note: needed to add this step in #3414. - -- This is caused by https://github.com/leanprover/lean4/pull/2146. - -- Nevertheless the proof could be cleaned up. - cases this - | cons hd tail => - cases' hd with y c - dsimp only - split_ifs with h <;> intro H - · rw [ H ] at r - exact @reduce.not _ L1 ((y, c)::L2) L3 x' b' r - · rcases L2 with ( _ | ⟨ a , L2 ⟩ ) - · injections - subst_vars - simp at h - · refine' @reduce.not _ L1 L2 L3 x' b' _ - injection H with _ H - rw [ r , H ] - rfl +theorem reduce.not {p : Prop} : + ∀ {L₁ L₂ L₃ : List (α × Bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p + | [], L2, L3, _, _ => fun h => by cases L2 <;> injections + | (x, b) :: L1, L2, L3, x', b' => by + dsimp + cases r : reduce L1 with + | nil => + dsimp; intro h + exfalso + have := congr_arg List.length h + simp? [List.length] at this says + simp only [List.length, zero_add, List.length_append] at this + rw [add_comm, add_assoc, add_assoc, add_comm, <-add_assoc] at this + simp [Nat.one_eq_succ_zero, Nat.succ_add] at this + -- Porting note: needed to add this step in #3414. + -- This is caused by https://github.com/leanprover/lean4/pull/2146. + -- Nevertheless the proof could be cleaned up. + cases this + | cons hd tail => + cases' hd with y c + dsimp only + split_ifs with h <;> intro H + · rw [H] at r + exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r + rcases L2 with (_ | ⟨a, L2⟩) + · injections; subst_vars + simp at h + · refine' @reduce.not _ L1 L2 L3 x' b' _ + injection H with _ H + rw [r, H]; rfl #align free_group.reduce.not FreeGroup.reduce.not #align free_add_group.reduce.not FreeAddGroup.reduce.not diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean index e275366c33b1e..4c90b75b8f2df 100644 --- a/Mathlib/Init/Data/Nat/Bitwise.lean +++ b/Mathlib/Init/Data/Nat/Bitwise.lean @@ -116,12 +116,7 @@ theorem div2_two : div2 2 = 1 := @[simp] theorem div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by simp only [bodd, boddDiv2, div2] - cases' boddDiv2 n with fst snd - cases fst - case mk.false => - simp - case mk.true => - simp + rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp #align nat.div2_succ Nat.div2_succ attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc @@ -325,24 +320,19 @@ theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (h : f false 0 z = z) (b n) : binaryRec z f (bit b n) = f b n (binaryRec z f n) := by rw [binaryRec] - by_cases h : bit b n = 0 - -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0` - case pos h' => - simp only [dif_pos h] - generalize binaryRec z f (bit b n) = e + split <;> rename_i h' + · generalize binaryRec z f (bit b n) = e revert e have bf := bodd_bit b n have n0 := div2_bit b n - rw [h] at bf n0 + rw [h'] at bf n0 simp only [bodd_zero, div2_zero] at bf n0 subst bf n0 rw [binaryRec_zero] intros - rw [h'] + rw [h] rfl - case neg h' => - simp only [dif_neg h] - generalize_proofs h + · simp only; generalize_proofs h revert h rw [bodd_bit, div2_bit] intros; rfl diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean index 87b1725ce4bdf..25a14c70fd10b 100644 --- a/Mathlib/Init/Data/Nat/Lemmas.lean +++ b/Mathlib/Init/Data/Nat/Lemmas.lean @@ -734,9 +734,9 @@ lemma to_digits_core_lens_eq_aux (b f : Nat) : induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen) | zero => assumption | succ f ih => - by_cases hx : n / b = 0 - case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen] - case neg => + if hx : n / b = 0 then + simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen] + else simp only [hx, if_false] specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2) simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih @@ -746,9 +746,9 @@ lemma to_digits_core_lens_eq (b f : Nat) : ∀ (n : Nat) (c : Char) (tl : List C (Nat.toDigitsCore b f n (c :: tl)).length = (Nat.toDigitsCore b f n tl).length + 1 := by induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length]) | succ f ih => - by_cases hnb : (n / b) = 0 - case pos => simp only [hnb, if_true, List.length] - case neg => + if hnb : (n / b) = 0 then + simp only [hnb, if_true, List.length] + else generalize hx: Nat.digitChar (n % b) = x simp only [hx, hnb, if_false] at ih simp only [hnb, if_false] @@ -773,17 +773,16 @@ lemma to_digits_core_length (b : Nat) (h : 2 <= b) (f n e : Nat) cases e with | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos) | succ e => - by_cases h_pred_pos : 0 < e - case pos => + if h_pred_pos : 0 < e then have _ : 0 < b := Nat.lt_trans (by decide) h specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos - by_cases hdiv_ten : n / b = 0 - case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos - case neg => + if hdiv_ten : n / b = 0 then + simp only [hdiv_ten]; exact Nat.le.step h_pred_pos + else simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false] exact Nat.succ_le_succ ih - case neg => + else obtain rfl : e = 0 := Nat.eq_zero_of_not_pos h_pred_pos have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul] have _ : n < b := ‹b ^ 1 = b› ▸ hlt @@ -797,8 +796,9 @@ lemma repr_length (n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length <= (intro e0 he; simp only [Nat.repr, Nat.toDigits, String.length, List.asString]) | zero => assumption | succ n => - by_cases hterm : n.succ / 10 = 0 - case pos => simp only [hterm, Nat.toDigitsCore]; assumption - case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0 + if hterm : n.succ / 10 = 0 then + simp only [hterm, Nat.toDigitsCore]; assumption + else + exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0 end Nat diff --git a/Mathlib/Init/Order/Defs.lean b/Mathlib/Init/Order/Defs.lean index b823526c32e79..c0f97b9393654 100644 --- a/Mathlib/Init/Order/Defs.lean +++ b/Mathlib/Init/Order/Defs.lean @@ -430,7 +430,7 @@ theorem compare_gt_iff_gt {a b : α} : (compare a b = .gt) ↔ a > b := by theorem compare_eq_iff_eq {a b : α} : (compare a b = .eq) ↔ a = b := by rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq] - split_ifs <;> try simp only [] + split_ifs <;> try simp only case _ h => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h case _ _ h => exact true_iff_iff.2 h case _ _ h => exact false_iff_iff.2 h diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean index 2aacfde94d665..5f83f8a7c9375 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean @@ -156,11 +156,11 @@ theorem reverse_comp_involute : (involute.toLinearMap.comp reverse : _ →ₗ[R] CliffordAlgebra Q) := by ext x simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply] - induction x using CliffordAlgebra.induction - case h_grade0 => simp - case h_grade1 => simp - case h_mul a b ha hb => simp only [ha, hb, reverse.map_mul, AlgHom.map_mul] - case h_add a b ha hb => simp only [ha, hb, reverse.map_add, AlgHom.map_add] + induction x using CliffordAlgebra.induction with + | h_grade0 => simp + | h_grade1 => simp + | h_mul a b ha hb => simp only [ha, hb, reverse.map_mul, AlgHom.map_mul] + | h_add a b ha hb => simp only [ha, hb, reverse.map_add, AlgHom.map_add] #align clifford_algebra.reverse_comp_involute CliffordAlgebra.reverse_comp_involute /-- `CliffordAlgebra.reverse` and `CliffordAlgebra.involute` commute. Note that the composition diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index 694a974931491..278eb81150964 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -80,20 +80,20 @@ theorem ι_eq_zero : ι (0 : QuadraticForm R Unit) = 0 := instance : CommRing (CliffordAlgebra (0 : QuadraticForm R Unit)) := { CliffordAlgebra.instRing _ with mul_comm := fun x y => by - induction x using CliffordAlgebra.induction - case h_grade0 r => apply Algebra.commutes - case h_grade1 x => simp - case h_add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂] - case h_mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc] } + induction x using CliffordAlgebra.induction with + | h_grade0 r => apply Algebra.commutes + | h_grade1 x => simp + | h_add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂] + | h_mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc] } -- Porting note: Changed `x.reverse` to `reverse (R := R) x` theorem reverse_apply (x : CliffordAlgebra (0 : QuadraticForm R Unit)) : reverse (R := R) x = x := by - induction x using CliffordAlgebra.induction - case h_grade0 r => exact reverse.commutes _ - case h_grade1 x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero] - case h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂] - case h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂] + induction x using CliffordAlgebra.induction with + | h_grade0 r => exact reverse.commutes _ + | h_grade1 x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero] + | h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂] + | h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂] #align clifford_algebra_ring.reverse_apply CliffordAlgebraRing.reverse_apply @[simp] @@ -221,11 +221,11 @@ instance : CommRing (CliffordAlgebra Q) := -- Porting note: Changed `x.reverse` to `reverse (R := ℝ) x` /-- `reverse` is a no-op over `CliffordAlgebraComplex.Q`. -/ theorem reverse_apply (x : CliffordAlgebra Q) : reverse (R := ℝ) x = x := by - induction x using CliffordAlgebra.induction - case h_grade0 r => exact reverse.commutes _ - case h_grade1 x => rw [reverse_ι] - case h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂] - case h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂] + induction x using CliffordAlgebra.induction with + | h_grade0 r => exact reverse.commutes _ + | h_grade1 x => rw [reverse_ι] + | h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂] + | h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂] #align clifford_algebra_complex.reverse_apply CliffordAlgebraComplex.reverse_apply @[simp] @@ -311,15 +311,15 @@ theorem toQuaternion_ι (v : R × R) : theorem toQuaternion_star (c : CliffordAlgebra (Q c₁ c₂)) : toQuaternion (star c) = star (toQuaternion c) := by simp only [CliffordAlgebra.star_def'] - induction c using CliffordAlgebra.induction - case h_grade0 r => + induction c using CliffordAlgebra.induction with + | h_grade0 r => simp only [reverse.commutes, AlgHom.commutes, QuaternionAlgebra.coe_algebraMap, QuaternionAlgebra.star_coe] - case h_grade1 x => + | h_grade1 x => rw [reverse_ι, involute_ι, toQuaternion_ι, AlgHom.map_neg, toQuaternion_ι, QuaternionAlgebra.neg_mk, star_mk, neg_zero] - case h_mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul] - case h_add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add] + | h_mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul] + | h_add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add] #align clifford_algebra_quaternion.to_quaternion_star CliffordAlgebraQuaternion.toQuaternion_star /-- Map a quaternion into the clifford algebra. -/ diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean index e04848f971f0c..d72a3af554a56 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean @@ -247,15 +247,15 @@ subalgebra is just the reverse of the representation. -/ theorem coe_toEven_reverse_involute (x : CliffordAlgebra Q) : ↑(toEven Q (reverse (involute x))) = reverse (Q := Q' Q) (toEven Q x : CliffordAlgebra (Q' Q)) := by - induction x using CliffordAlgebra.induction - case h_grade0 r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes] - case h_grade1 m => + induction x using CliffordAlgebra.induction with + | h_grade0 r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes] + | h_grade1 m => -- porting note: added `letI` letI : SubtractionMonoid (even (Q' Q)) := AddGroup.toSubtractionMonoid simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0, reverse_ι, neg_e0_mul_v, map_neg] - case h_mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy] - case h_add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy] + | h_mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy] + | h_add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy] #align clifford_algebra.coe_to_even_reverse_involute CliffordAlgebra.coe_toEven_reverse_involute /-! ### Constructions needed for `CliffordAlgebra.evenEquivEvenNeg` -/ diff --git a/Mathlib/Logic/Denumerable.lean b/Mathlib/Logic/Denumerable.lean index 1ce3fe95aea04..c28dd184e9cd1 100644 --- a/Mathlib/Logic/Denumerable.lean +++ b/Mathlib/Logic/Denumerable.lean @@ -127,11 +127,11 @@ theorem ofNat_nat (n) : ofNat ℕ n = n := /-- If `α` is denumerable, then so is `Option α`. -/ instance option : Denumerable (Option α) := ⟨fun n => by - cases n - case zero => + cases n with + | zero => refine' ⟨none, _, encode_none⟩ rw [decode_option_zero, Option.mem_def] - case succ n => + | succ n => refine' ⟨some (ofNat α n), _, _⟩ · rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def] rw [encode_some, encode_ofNat]⟩ diff --git a/Mathlib/Logic/Hydra.lean b/Mathlib/Logic/Hydra.lean index 9130d740a1e83..915fa10f264b2 100644 --- a/Mathlib/Logic/Hydra.lean +++ b/Mathlib/Logic/Hydra.lean @@ -125,9 +125,9 @@ theorem cutExpand_fibration (r : α → α → Prop) : assuming `r` is irreflexive. -/ theorem acc_of_singleton [IsIrrefl α r] {s : Multiset α} (hs : ∀ a ∈ s, Acc (CutExpand r) {a}) : Acc (CutExpand r) s := by - induction s using Multiset.induction - case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim - case cons a s ihs => + induction s using Multiset.induction with + | empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim + | @cons a s ihs => rw [← s.singleton_add a] rw [forall_mem_cons] at hs exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r) diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean index 3f4fbdaf26df9..544154eba73fb 100644 --- a/Mathlib/Logic/Relation.lean +++ b/Mathlib/Logic/Relation.lean @@ -296,9 +296,9 @@ namespace ReflTransGen @[trans] theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by - induction hbc - case refl => assumption - case tail c d _ hcd hac => exact hac.tail hcd + induction hbc with + | refl => assumption + | tail _ hcd hac => exact hac.tail hcd #align relation.refl_trans_gen.trans Relation.ReflTransGen.trans theorem single (hab : r a b) : ReflTransGen r a b := @@ -306,9 +306,9 @@ theorem single (hab : r a b) : ReflTransGen r a b := #align relation.refl_trans_gen.single Relation.ReflTransGen.single theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by - induction hbc - case refl => exact refl.tail hab - case tail c d _ hcd hac => exact hac.tail hcd + induction hbc with + | refl => exact refl.tail hab + | tail _ hcd hac => exact hac.tail hcd #align relation.refl_trans_gen.head Relation.ReflTransGen.head theorem symmetric (h : Symmetric r) : Symmetric (ReflTransGen r) := by @@ -326,13 +326,13 @@ theorem cases_tail : ReflTransGen r a b → b = a ∨ ∃ c, ReflTransGen r a c theorem head_induction_on {P : ∀ a : α, ReflTransGen r a b → Prop} {a : α} (h : ReflTransGen r a b) (refl : P b refl) (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (h.head h')) : P a h := by - induction h - case refl => exact refl - case tail b c _ hbc ih => + induction h with + | refl => exact refl + | @tail b c _ hbc ih => -- Porting note: Lean 3 figured out the motive and `apply ih` worked refine @ih (λ {a : α} (hab : ReflTransGen r a b) => P a (ReflTransGen.tail hab hbc)) ?_ ?_ - { exact head hbc _ refl } - { exact fun h1 h2 ↦ head h1 (h2.tail hbc) } + · exact head hbc _ refl + · exact fun h1 h2 ↦ head h1 (h2.tail hbc) #align relation.refl_trans_gen.head_induction_on Relation.ReflTransGen.head_induction_on @[elab_as_elim] @@ -340,9 +340,9 @@ theorem trans_induction_on {P : ∀ {a b : α}, ReflTransGen r a b → Prop} {a (h : ReflTransGen r a b) (ih₁ : ∀ a, @P a a refl) (ih₂ : ∀ {a b} (h : r a b), P (single h)) (ih₃ : ∀ {a b c} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) : P h := by - induction h - case refl => exact ih₁ a - case tail b c hab hbc ih => exact ih₃ hab (single hbc) ih (ih₂ hbc) + induction h with + | refl => exact ih₁ a + | tail hab hbc ih => exact ih₃ hab (single hbc) ih (ih₂ hbc) #align relation.refl_trans_gen.trans_induction_on Relation.ReflTransGen.trans_induction_on theorem cases_head (h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by @@ -384,9 +384,9 @@ theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by #align relation.trans_gen.to_refl Relation.TransGen.to_reflTransGen theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by - induction hbc - case refl => assumption - case tail c d _ hcd hac => exact hac.tail hcd + induction hbc with + | refl => assumption + | tail _ hcd hac => exact hac.tail hcd #align relation.trans_gen.trans_left Relation.TransGen.trans_left instance : Trans (TransGen r) (ReflTransGen r) (TransGen r) := @@ -405,9 +405,9 @@ theorem head' (hab : r a b) (hbc : ReflTransGen r b c) : TransGen r a c := #align relation.trans_gen.head' Relation.TransGen.head' theorem tail' (hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c := by - induction hab generalizing c - case refl => exact single hbc - case tail _ _ _ hdb IH => exact tail (IH hdb) hbc + induction hab generalizing c with + | refl => exact single hbc + | tail _ hdb IH => exact tail (IH hdb) hbc #align relation.trans_gen.tail' Relation.TransGen.tail' theorem head (hab : r a b) (hbc : TransGen r b c) : TransGen r a c := @@ -418,9 +418,9 @@ theorem head (hab : r a b) (hbc : TransGen r b c) : TransGen r a c := theorem head_induction_on {P : ∀ a : α, TransGen r a b → Prop} {a : α} (h : TransGen r a b) (base : ∀ {a} (h : r a b), P a (single h)) (ih : ∀ {a c} (h' : r a c) (h : TransGen r c b), P c h → P a (h.head h')) : P a h := by - induction h - case single a h => exact base h - case tail b c _ hbc h_ih => + induction h with + | single h => exact base h + | @tail b c _ hbc h_ih => -- Lean 3 could figure out the motive and `apply h_ih` worked refine @h_ih (λ {a : α} (hab : @TransGen α r a b) => P a (TransGen.tail hab hbc)) ?_ ?_; exact fun h ↦ ih h (single hbc) (base hbc) @@ -438,9 +438,9 @@ theorem trans_induction_on {P : ∀ {a b : α}, TransGen r a b → Prop} {a b : #align relation.trans_gen.trans_induction_on Relation.TransGen.trans_induction_on theorem trans_right (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c := by - induction hbc - case single c hbc => exact tail' hab hbc - case tail c d _ hcd hac => exact hac.tail hcd + induction hbc with + | single hbc => exact tail' hab hbc + | tail _ hcd hac => exact hac.tail hcd #align relation.trans_gen.trans_right Relation.TransGen.trans_right instance : Trans (ReflTransGen r) (TransGen r) (TransGen r) := @@ -455,9 +455,9 @@ theorem tail'_iff : TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c := by theorem head'_iff : TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c := by refine' ⟨fun h ↦ _, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩ - induction h - case single c hac => exact ⟨_, hac, by rfl⟩ - case tail b c _ hbc IH => + induction h with + | single hac => exact ⟨_, hac, by rfl⟩ + | tail _ hbc IH => rcases IH with ⟨d, had, hdb⟩ exact ⟨_, had, hdb.tail hbc⟩ #align relation.trans_gen.head'_iff Relation.TransGen.head'_iff @@ -498,9 +498,9 @@ section TransGen theorem transGen_eq_self (trans : Transitive r) : TransGen r = r := funext fun a ↦ funext fun b ↦ propext <| ⟨fun h ↦ by - induction h - case single _ hc => exact hc - case tail c d _ hcd hac => exact trans hac hcd, TransGen.single⟩ + induction h with + | single hc => exact hc + | tail _ hcd hac => exact trans hac hcd, TransGen.single⟩ #align relation.trans_gen_eq_self Relation.transGen_eq_self theorem transitive_transGen : Transitive (TransGen r) := fun _ _ _ ↦ TransGen.trans @@ -515,9 +515,9 @@ theorem transGen_idem : TransGen (TransGen r) = TransGen r := theorem TransGen.lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b)) (hab : TransGen r a b) : TransGen p (f a) (f b) := by - induction hab - case single c hac => exact TransGen.single (h a c hac) - case tail c d _ hcd hac => exact TransGen.tail hac (h c d hcd) + induction hab with + | single hac => exact TransGen.single (h a _ hac) + | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd) #align relation.trans_gen.lift Relation.TransGen.lift theorem TransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β) @@ -675,24 +675,24 @@ open ReflTransGen ReflGen /-- A sufficient condition for the Church-Rosser property. -/ theorem church_rosser (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c := by - induction hab - case refl => exact ⟨c, hac, refl⟩ - case tail d e _ hde ih => - rcases ih with ⟨b, hdb, hcb⟩ - have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by - clear hcb - induction hdb - case refl => exact ⟨e, refl, ReflGen.single hde⟩ - case tail f b _ hfb ih => - rcases ih with ⟨a, hea, hfa⟩ - cases' hfa with _ hfa - · exact ⟨b, hea.tail hfb, ReflGen.refl⟩ - · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩ - exact ⟨c, hea.trans hac, hbc⟩ - rcases this with ⟨a, hea, hba⟩ - cases' hba with _ hba - · exact ⟨b, hea, hcb⟩ - · exact ⟨a, hea, hcb.tail hba⟩ + induction hab with + | refl => exact ⟨c, hac, refl⟩ + | @tail d e _ hde ih => + rcases ih with ⟨b, hdb, hcb⟩ + have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by + clear hcb + induction hdb with + | refl => exact ⟨e, refl, ReflGen.single hde⟩ + | @tail f b _ hfb ih => + rcases ih with ⟨a, hea, hfa⟩ + cases' hfa with _ hfa + · exact ⟨b, hea.tail hfb, ReflGen.refl⟩ + · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩ + exact ⟨c, hea.trans hac, hbc⟩ + rcases this with ⟨a, hea, hba⟩ + cases' hba with _ hba + · exact ⟨b, hea, hcb⟩ + · exact ⟨a, hea, hcb.tail hba⟩ #align relation.church_rosser Relation.church_rosser diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index 1d0e05cec9e24..8f0d99b868349 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -82,12 +82,11 @@ theorem borel_eq_generateFrom_of_subbasis {s : Set (Set α)} [t : TopologicalSpa le_antisymm (generateFrom_le fun u (hu : t.IsOpen u) => by rw [hs] at hu - induction hu - case basic u hu => exact GenerateMeasurable.basic u hu - case univ => exact @MeasurableSet.univ α (generateFrom s) - case inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂ - case - sUnion f hf ih => + induction hu with + | basic u hu => exact GenerateMeasurable.basic u hu + | univ => exact @MeasurableSet.univ α (generateFrom s) + | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂ + | sUnion f hf ih => rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩ rw [← vu] exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)) diff --git a/Mathlib/MeasureTheory/Integral/Marginal.lean b/Mathlib/MeasureTheory/Integral/Marginal.lean index 6568cf9f2ea25..d0a3fe41a9b4d 100644 --- a/Mathlib/MeasureTheory/Integral/Marginal.lean +++ b/Mathlib/MeasureTheory/Integral/Marginal.lean @@ -203,9 +203,9 @@ theorem lmarginal_image [DecidableEq δ'] {e : δ' → δ} (he : Injective e) (s (∫⋯∫⁻_s.image e, f ∘ (· ∘' e) ∂μ) x = (∫⋯∫⁻_s, f ∂μ ∘' e) (x ∘' e) := by have h : Measurable ((· ∘' e) : (∀ i, π i) → _) := measurable_pi_iff.mpr <| λ i ↦ measurable_pi_apply (e i) - induction s using Finset.induction generalizing x - case empty => simp - case insert i s hi ih => + induction s using Finset.induction generalizing x with + | empty => simp + | insert hi ih => rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi), lmarginal_insert _ hf hi] simp_rw [ih, ← update_comp_eq_of_injective' x he] @@ -213,9 +213,9 @@ theorem lmarginal_image [DecidableEq δ'] {e : δ' → δ} (he : Injective e) (s theorem lmarginal_update_of_not_mem {i : δ} {f : (∀ i, π i) → ℝ≥0∞} (hf : Measurable f) (hi : i ∉ s) (x : ∀ i, π i) (y : π i) : (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∘ (Function.update · i y) ∂μ) x := by - induction s using Finset.induction generalizing x - case empty => simp - case insert i' s hi' ih => + induction s using Finset.induction generalizing x with + | empty => simp + | @insert i' s hi' ih => rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi'] have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)] diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean index 53f6968182cf1..ed66ca6f091de 100644 --- a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean +++ b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean @@ -205,10 +205,10 @@ theorem lintegral_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Me (s : Finset ι) {f : ι → α → ℝ≥0∞} (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : ∑ i in s, p i = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) : ∫⁻ a, ∏ i in s, f i a ^ p i ∂μ ≤ ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by - induction s using Finset.induction generalizing p - case empty => + induction s using Finset.induction generalizing p with + | empty => simp at hp - case insert i₀ s hi₀ ih => + | @insert i₀ s hi₀ ih => rcases eq_or_ne (p i₀) 1 with h2i₀|h2i₀ · simp [hi₀] have h2p : ∀ i ∈ s, p i = 0 := by diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean index ea357f76a7d62..106e1c287e6a3 100644 --- a/Mathlib/ModelTheory/Satisfiability.lean +++ b/Mathlib/ModelTheory/Satisfiability.lean @@ -260,11 +260,11 @@ direction between then `M` and a structure of cardinality `κ`. -/ theorem exists_elementaryEmbedding_card_eq (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) : ∃ N : Bundled L.Structure, (Nonempty (N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] N)) ∧ #N = κ := by - cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) - case inl h => + cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) with + | inl h => obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h exact ⟨N, Or.inl hN1, hN2⟩ - case inr h => + | inr h => obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h) exact ⟨N, Or.inr hN1, hN2⟩ #align first_order.language.exists_elementary_embedding_card_eq FirstOrder.Language.exists_elementaryEmbedding_card_eq diff --git a/Mathlib/ModelTheory/Ultraproducts.lean b/Mathlib/ModelTheory/Ultraproducts.lean index e7e2cc3eeaebf..1f192cae9a913 100644 --- a/Mathlib/ModelTheory/Ultraproducts.lean +++ b/Mathlib/ModelTheory/Ultraproducts.lean @@ -86,12 +86,9 @@ theorem term_realize_cast {β : Type*} (x : β → ∀ a, M a) (t : L.Term β) : convert @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M) (Ultraproduct.setoidPrestructure M u) _ t x using 2 ext a - induction t - case var => - rfl - case func _ _ _ t_ih => - simp only [Term.realize, t_ih] - rfl + induction t with + | var => rfl + | func _ _ t_ih => simp only [Term.realize, t_ih]; rfl #align first_order.language.ultraproduct.term_realize_cast FirstOrder.Language.Ultraproduct.term_realize_cast variable [∀ a : α, Nonempty (M a)] diff --git a/Mathlib/Order/Atoms.lean b/Mathlib/Order/Atoms.lean index 2110a42e4bbaf..f967ed6d32a64 100644 --- a/Mathlib/Order/Atoms.lean +++ b/Mathlib/Order/Atoms.lean @@ -499,7 +499,7 @@ instance {α} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α where have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq, iInf_const] rw [← this]; clear this simp_rw [iInf_iSup_eq, iSup_le_iff]; intro g - by_cases h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥; case pos => simp [h] + if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h] else refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right) revert this @@ -1002,7 +1002,7 @@ theorem isAtom_iff {f : ∀ i, π i} [∀ i, PartialOrder (π i)] [∀ i, OrderB refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩ have ⟨hgf, k, hgfk⟩ := Pi.lt_def.1 hgf obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk; simp at hgfk - by_cases hij : j = i; case pos => subst hij; refine hlt _ hgfk + if hij : j = i then subst hij; refine hlt _ hgfk else refine eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij)) case mp => rintro ⟨hbot, h⟩ @@ -1063,14 +1063,12 @@ instance isAtomistic [∀ i, CompleteLattice (π i)] [∀ i, IsAtomistic (π i)] refine le_antisymm ?le ?ge case le => refine sSup_le fun a ⟨ha, hle⟩ => ?_ - refine le_sSup ⟨⟨_, ⟨_, _, ha, rfl⟩, ?_⟩, by simp⟩ - intro j; by_cases hij : j = i - case pos => subst hij; simpa - case neg => simp [hij] + refine le_sSup ⟨⟨_, ⟨_, _, ha, rfl⟩, fun j => ?_⟩, by simp⟩ + if hij : j = i then subst hij; simpa else simp [hij] case ge => refine sSup_le ?_ rintro _ ⟨⟨_, ⟨j, a, ha, rfl⟩, hle⟩, rfl⟩ - by_cases hij : i = j; case neg => simp [Function.update_noteq hij] + if hij : i = j then ?_ else simp [Function.update_noteq hij] subst hij; simp only [Function.update_same] exact le_sSup ⟨ha, by simpa using hle i⟩ diff --git a/Mathlib/Order/Chain.lean b/Mathlib/Order/Chain.lean index e6a3dd37055cf..74968f2a45755 100644 --- a/Mathlib/Order/Chain.lean +++ b/Mathlib/Order/Chain.lean @@ -219,24 +219,24 @@ theorem chainClosure_maxChain : ChainClosure r (maxChain r) := private theorem chainClosure_succ_total_aux (hc₁ : ChainClosure r c₁) (h : ∀ ⦃c₃⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂) : SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂ := by - induction hc₁ - case succ c₃ hc₃ ih => + induction hc₁ with + | @succ c₃ hc₃ ih => cases' ih with ih ih · exact Or.inl (ih.trans subset_succChain) · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl - case union s _ ih => + | union _ ih => refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _ exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha private theorem chainClosure_succ_total (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) (h : c₁ ⊆ c₂) : c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂ := by - induction hc₂ generalizing c₁ hc₁ - case succ c₂ _ ih => + induction hc₂ generalizing c₁ hc₁ with + | succ _ ih => refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _ obtain rfl | h₂ := ih hc₁ h₁ · exact Subset.rfl · exact h₂.trans subset_succChain - case union s _ ih => + | union _ ih => apply Or.imp_left h.antisymm' apply by_contradiction simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index] @@ -255,9 +255,9 @@ theorem ChainClosure.total (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r theorem ChainClosure.succ_fixpoint (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) (hc : SuccChain r c₂ = c₂) : c₁ ⊆ c₂ := by - induction hc₁ - case succ s₁ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id - case union s _ ih => exact sUnion_subset ih + induction hc₁ with + | succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id + | union _ ih => exact sUnion_subset ih #align chain_closure.succ_fixpoint ChainClosure.succ_fixpoint theorem ChainClosure.succ_fixpoint_iff (hc : ChainClosure r c) : @@ -267,9 +267,9 @@ theorem ChainClosure.succ_fixpoint_iff (hc : ChainClosure r c) : #align chain_closure.succ_fixpoint_iff ChainClosure.succ_fixpoint_iff theorem ChainClosure.isChain (hc : ChainClosure r c) : IsChain r c := by - induction hc - case succ c _ h => exact h.succ - case union s hs h => + induction hc with + | succ _ h => exact h.succ + | union hs h => exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq => ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht => h t₁ ht₁ hc₁ (ht hc₂) hneq diff --git a/Mathlib/Order/CompleteBooleanAlgebra.lean b/Mathlib/Order/CompleteBooleanAlgebra.lean index cebbaedd062a1..685d2f21ba9c7 100644 --- a/Mathlib/Order/CompleteBooleanAlgebra.lean +++ b/Mathlib/Order/CompleteBooleanAlgebra.lean @@ -139,9 +139,9 @@ instance (priority := 100) CompletelyDistribLattice.toCompleteDistribLattice _ = ⨅ b : s, ⨆ x : Bool, cond x a b := by simp_rw [iInf_subtype, iSup_bool_eq, cond] _ = _ := iInf_iSup_eq _ ≤ _ := iSup_le fun f => by - by_cases h : ∀ i, f i = false - case pos => simp [h, iInf_subtype, ← sInf_eq_iInf] - case neg => + if h : ∀ i, f i = false then + simp [h, iInf_subtype, ← sInf_eq_iInf] + else have ⟨i, h⟩ : ∃ i, f i = true := by simpa using h refine le_trans (iInf_le _ i) ?_ simp [h] @@ -162,8 +162,7 @@ instance (priority := 100) CompleteLinearOrder.toCompletelyDistribLattice [Compl let lhs := ⨅ a, ⨆ b, g a b let rhs := ⨆ h : ∀ a, β a, ⨅ a, g a (h a) suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup - by_cases h : ∃ x, rhs < x ∧ x < lhs - case pos => + if h : ∃ x, rhs < x ∧ x < lhs then rcases h with ⟨x, hr, hl⟩ suffices rhs ≥ x from nomatch not_lt.2 this hr have : ∀ a, ∃ b, x < g a b := fun a => @@ -172,7 +171,7 @@ instance (priority := 100) CompleteLinearOrder.toCompletelyDistribLattice [Compl choose f hf using this refine le_trans ?_ (le_iSup _ f) refine le_iInf fun a => le_of_lt (hf a) - case neg => + else refine le_of_not_lt fun hrl : rhs < lhs => not_le_of_lt hrl ?_ replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by simpa only [not_exists, not_and_or, not_or, not_lt] using h diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index 69553696881f4..dcd3fe24bb720 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -375,14 +375,14 @@ theorem le_generate_iff {s : Set (Set α)} {f : Filter α} : f ≤ generate s theorem mem_generate_iff {s : Set <| Set α} {U : Set α} : U ∈ generate s ↔ ∃ t ⊆ s, Set.Finite t ∧ ⋂₀ t ⊆ U := by constructor <;> intro h - · induction h - case basic V V_in => + · induction h with + | @basic V V_in => exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩ - case univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩ - case superset V W _ hVW hV => + | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩ + | superset _ hVW hV => rcases hV with ⟨t, hts, ht, htV⟩ exact ⟨t, hts, ht, htV.trans hVW⟩ - case inter V W _ _ hV hW => + | inter _ _ hV hW => rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩ exact ⟨t ∪ u, union_subset hts hus, ht.union hu, @@ -972,9 +972,9 @@ theorem iInf_sets_induct {f : ι → Filter α} {s : Set α} (hs : s ∈ iInf f) rw [mem_iInf_finite'] at hs simp only [← Finset.inf_eq_iInf] at hs rcases hs with ⟨is, his⟩ - induction is using Finset.induction_on generalizing s - case empty => rwa [mem_top.1 his] - case insert ih => + induction is using Finset.induction_on generalizing s with + | empty => rwa [mem_top.1 his] + | insert _ ih => rw [Finset.inf_insert, mem_inf_iff] at his rcases his with ⟨s₁, hs₁, s₂, hs₂, rfl⟩ exact ins hs₁ (ih hs₂) @@ -2957,11 +2957,11 @@ theorem mem_traverse_iff (fs : List β') (t : Set (List α')) : t ∈ traverse f fs ↔ ∃ us : List (Set α'), Forall₂ (fun b (s : Set α') => s ∈ f b) fs us ∧ sequence us ⊆ t := by constructor - · induction fs generalizing t - case nil => + · induction fs generalizing t with + | nil => simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def, singleton_subset_iff, traverse_nil] - case cons b fs ih => + | cons b fs ih => intro ht rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩ rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩ diff --git a/Mathlib/RingTheory/Int/Basic.lean b/Mathlib/RingTheory/Int/Basic.lean index c616f9e1b1eb4..7bcb9fc5d5e92 100644 --- a/Mathlib/RingTheory/Int/Basic.lean +++ b/Mathlib/RingTheory/Int/Basic.lean @@ -304,9 +304,9 @@ theorem Int.exists_prime_and_dvd {n : ℤ} (hn : n.natAbs ≠ 1) : ∃ p, Prime open UniqueFactorizationMonoid theorem Nat.factors_eq {n : ℕ} : normalizedFactors n = n.factors := by - cases n - case zero => simp - case succ n => + cases n with + | zero => simp + | succ n => rw [← Multiset.rel_eq, ← associated_eq_eq] apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _ · rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero] diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean index 6bf87d61e679d..d5b05d9da86d0 100644 --- a/Mathlib/RingTheory/PrincipalIdealDomain.lean +++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean @@ -173,12 +173,12 @@ theorem to_maximal_ideal [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : ⟨(ne_top_iff_one S).1 hpi.1, by intro T x hST hxS hxT cases' (mem_iff_generator_dvd _).1 (hST <| generator_mem S) with z hz - cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) - case inl h => + cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with + | inl h => have hTS : T ≤ S rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff] exact (hxS <| hTS hxT).elim - case inr h => + | inr h => cases' (mem_iff_generator_dvd _).1 h with y hy have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 6369a5f29a852..3baa51a8817de 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -99,12 +99,12 @@ theorem isPreconnected_of_forall {s : Set α} (x : α) rcases H y ys with ⟨t, ts, xt, -, -⟩ exact ts xt -- porting note: todo: use `wlog xu : x ∈ u := hs xs using u v y z, v u z y` - cases hs xs - case inl xu => + cases hs xs with + | inl xu => rcases H y ys with ⟨t, ts, xt, yt, ht⟩ have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩ exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩ - case inr xv => + | inr xv => rcases H z zs with ⟨t, ts, xt, zt, ht⟩ have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩ exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩ @@ -172,12 +172,12 @@ theorem IsPreconnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by - induction h - case refl => + induction h with + | refl => refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩ rw [biUnion_singleton] exact H i hi - case tail j k _ hjk ih => + | @tail j k _ hjk ih => obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2 refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, mem_insert k p, ?_⟩ @@ -1043,9 +1043,9 @@ theorem isConnected_iff_sUnion_disjoint_open {s : Set α} : (∀ u ∈ U, IsOpen u) → (s ⊆ ⋃₀ ↑U) → ∃ u ∈ U, s ⊆ u := by rw [IsConnected, isPreconnected_iff_subset_of_disjoint] refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩ - · induction U using Finset.induction_on - case empty => exact absurd (by simpa using hsU) hne.not_subset_empty - case insert u U uU IH => + · induction U using Finset.induction_on with + | empty => exact absurd (by simpa using hsU) hne.not_subset_empty + | @insert u U uU IH => simp only [← ball_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert, Finset.coe_insert, sUnion_insert, implies_true, true_and] at * refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_ diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean index cfd536a0463f5..fb0f39723ead5 100644 --- a/Mathlib/Topology/EMetricSpace/Basic.lean +++ b/Mathlib/Topology/EMetricSpace/Basic.lean @@ -132,9 +132,9 @@ theorem edist_triangle4 (x y z t : α) : edist x t ≤ edist x y + edist y z + e /-- The triangle (polygon) inequality for sequences of points; `Finset.Ico` version. -/ theorem edist_le_Ico_sum_edist (f : ℕ → α) {m n} (h : m ≤ n) : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1)) := by - induction n, h using Nat.le_induction - case base => rw [Finset.Ico_self, Finset.sum_empty, edist_self] - case succ n hle ihn => + induction n, h using Nat.le_induction with + | base => rw [Finset.Ico_self, Finset.sum_empty, edist_self] + | succ n hle ihn => calc edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _ _ ≤ (∑ i in Finset.Ico m n, _) + _ := add_le_add ihn le_rfl diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean index 8f7f08d59a901..e829987f55b54 100644 --- a/Mathlib/Topology/Irreducible.lean +++ b/Mathlib/Topology/Irreducible.lean @@ -254,9 +254,9 @@ theorem isIrreducible_iff_sInter : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty := by refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩ - · induction U using Finset.induction_on - case empty => simpa using h.nonempty - case insert u U _ IH => + · induction U using Finset.induction_on with + | empty => simpa using h.nonempty + | @insert u U _ IH => rw [Finset.coe_insert, sInter_insert] rw [Finset.forall_mem_insert] at hu hU exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2) diff --git a/Mathlib/Topology/List.lean b/Mathlib/Topology/List.lean index 2720ef7c2e1b0..7d3e3e3eba950 100644 --- a/Mathlib/Topology/List.lean +++ b/Mathlib/Topology/List.lean @@ -26,9 +26,9 @@ instance : TopologicalSpace (List α) := theorem nhds_list (as : List α) : 𝓝 as = traverse 𝓝 as := by refine' nhds_mkOfNhds _ _ _ _ · intro l - induction l - case nil => exact le_rfl - case cons a l ih => + induction l with + | nil => exact le_rfl + | cons a l ih => suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by simpa only [functor_norm] using this exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih @@ -36,13 +36,13 @@ theorem nhds_list (as : List α) : 𝓝 as = traverse 𝓝 as := by rcases (mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩ clear as hs have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s - induction hu generalizing s - case nil _hs => + induction hu generalizing s with + | nil => exists [] simp only [List.forall₂_nil_left_iff, exists_eq_left] exact ⟨trivial, hus⟩ -- porting note -- renamed reordered variables based on previous types - case cons a s as ss hts h ht _ ih => + | cons ht _ ih => rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩ rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩ exact diff --git a/Mathlib/Topology/Order/LowerUpperTopology.lean b/Mathlib/Topology/Order/LowerUpperTopology.lean index 7bfb62fc347cb..273580aee242c 100644 --- a/Mathlib/Topology/Order/LowerUpperTopology.lean +++ b/Mathlib/Topology/Order/LowerUpperTopology.lean @@ -241,11 +241,11 @@ theorem isClosed_upperClosure (h : s.Finite) : IsClosed (upperClosure s : Set α theorem isLowerSet_of_isOpen (h : IsOpen s) : IsLowerSet s := by -- porting note: `rw` leaves a shadowed assumption replace h := isOpen_iff_generate_Ici_compl.1 h - induction h - case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl - case univ => exact isLowerSet_univ - case inter u v _ _ hu2 hv2 => exact hu2.inter hv2 - case sUnion _ _ ih => exact isLowerSet_sUnion ih + induction h with + | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl + | univ => exact isLowerSet_univ + | inter u v _ _ hu2 hv2 => exact hu2.inter hv2 + | sUnion _ _ ih => exact isLowerSet_sUnion ih #align lower_topology.is_lower_set_of_is_open Topology.IsLower.isLowerSet_of_isOpen theorem isUpperSet_of_isClosed (h : IsClosed s) : IsUpperSet s :=