chore: add missing hypothesis names to by_cases (#2679)

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -704,7 +704,7 @@ end GCD
 section LCM
 
 theorem lcm_dvd_iff [GCDMonoid α] {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c := by
-  by_cases a = 0 ∨ b = 0
+  by_cases h : a = 0 ∨ b = 0
   · rcases h with (rfl | rfl) <;>
       simp (config := { contextual := true }) only [iff_def, lcm_zero_left, lcm_zero_right,
         zero_dvd_iff, dvd_zero, eq_self_iff_true, and_true_iff, imp_true_iff]

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -97,7 +97,7 @@ variable [DecidableEq α]
 @[simp]
 theorem lcm_dedup (s : Multiset α) : (dedup s).lcm = s.lcm :=
   Multiset.induction_on s (by simp) <| fun a s IH ↦ by
-    by_cases a ∈ s <;> simp [IH, h]
+    by_cases h : a ∈ s <;> simp [IH, h]
     unfold lcm
     rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
     apply lcm_eq_of_associated_left (associated_normalize _)
@@ -200,7 +200,7 @@ variable [DecidableEq α]
 @[simp]
 theorem gcd_dedup (s : Multiset α) : (dedup s).gcd = s.gcd :=
   Multiset.induction_on s (by simp) <| fun a s IH ↦ by
-    by_cases a ∈ s <;> simp [IH, h]
+    by_cases h : a ∈ s <;> simp [IH, h]
     unfold gcd
     rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
     apply (associated_normalize _).gcd_eq_left

Mathlib/Combinatorics/SetFamily/Compression/UV.lean

@@ -162,7 +162,7 @@ theorem compress_idem (u v a : α) : compress u v (compress u v a) = compress u
 
 theorem compress_mem_compression (ha : a ∈ s) : compress u v a ∈ 𝓒 u v s := by
   rw [mem_compression]
-  by_cases compress u v a ∈ s
+  by_cases h : compress u v a ∈ s
   · rw [compress_idem]
     exact Or.inl ⟨h, h⟩
   · exact Or.inr ⟨h, a, ha, rfl⟩

Mathlib/Combinatorics/SetFamily/Intersecting.lean

@@ -204,7 +204,7 @@ theorem Intersecting.exists_card_eq (hs : (s : Set α).Intersecting) :
   revert hs
   refine' s.strongDownwardInductionOn _ this
   rintro s ih _hcard hs
-  by_cases ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
+  by_cases h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
   · exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩
   push_neg  at h
   obtain ⟨t, ht, hst⟩ := h

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -160,7 +160,7 @@ theorem slice_union_shadow_falling_succ : 𝒜 # k ∪ (∂ ) (falling (k + 1) 
     rw [card_erase_of_mem ha, hs]
     rfl
   · rintro ⟨⟨t, ht, hst⟩, hs⟩
-    by_cases s ∈ 𝒜
+    by_cases h : s ∈ 𝒜
     · exact Or.inl ⟨h, hs⟩
     obtain ⟨a, ha, hst⟩ := ssubset_iff.1
         (ssubset_of_subset_of_ne hst (Membership.Mem.ne_of_not_mem ht h).symm)

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -287,9 +287,9 @@ instance : BooleanAlgebra (SimpleGraph V) :=
     le_sup_inf := by aesop_graph
     inf_compl_le_bot := fun a v w h => False.elim <| h.2.2 h.1
     top_le_sup_compl := fun a v w ne => by
-      by_cases a.Adj v w
-      exact Or.inl h
-      exact Or.inr ⟨ne, h⟩
+      by_cases h : a.Adj v w
+      · exact Or.inl h
+      · exact Or.inr ⟨ne, h⟩
     inf_le_left := fun x y v w h => h.1
     inf_le_right := fun x y v w h => h.2 }
 

Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

@@ -79,7 +79,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
     least one part `u` of `P` has size `m + 1` (in which case we take `t` to be an arbitrary subset
     of `u` of size `n`). The rest of each branch is just tedious calculations to satisfy the
     induction hypothesis. -/
-  by_cases ∀ u ∈ P.parts, card u < m + 1
+  by_cases h : ∀ u ∈ P.parts, card u < m + 1
   · obtain ⟨t, hts, htn⟩ := exists_smaller_set s n (hn₂.trans_eq hs)
     have ht : t.Nonempty := by rwa [← card_pos, htn]
     have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card := by

Mathlib/Computability/TuringMachine.lean

@@ -2741,7 +2741,7 @@ theorem trCfg_init (k) (L : List (Γ k)) : TrCfg (TM2.init k L) (TM1.init (trIni
       = fun a => (proj k').f (update (β := fun k => Option (Γ k)) default k (some a)) := rfl
     rw [this, List.get?_map, proj, PointedMap.mk_val]
     simp only []
-    by_cases k' = k
+    by_cases h : k' = k
     · subst k'
       simp only [Function.update_same]
       rw [ListBlank.nth_mk, List.getI_eq_iget_get?, ← List.map_reverse, List.get?_map]

Mathlib/Data/Bitvec/Core.lean

@@ -78,7 +78,7 @@ bitvector. -/
 def fillShr (x : Bitvec n) (i : ℕ) (fill : Bool) : Bitvec n :=
   Bitvec.cong
       (by
-        by_cases i ≤ n
+        by_cases h : i ≤ n
         · have h₁ := Nat.sub_le n i
           rw [min_eq_right h]
           rw [min_eq_left h₁, ← add_tsub_assoc_of_le h, Nat.add_comm, add_tsub_cancel_right]

Mathlib/Data/Dfinsupp/Basic.lean

@@ -1184,10 +1184,10 @@ theorem mapRange_def [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] {f : ∀ i, β
 theorem mapRange_single {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {i : ι} {b : β₁ i} :
     mapRange f hf (single i b) = single i (f i b) :=
   Dfinsupp.ext fun i' => by
-    by_cases i = i' <;>
-      [·
-        subst i'
-        simp, simp [h, hf]]
+    by_cases h : i = i'
+    · subst i'
+      simp
+    · simp [h, hf]
 #align dfinsupp.map_range_single Dfinsupp.mapRange_single
 
 variable [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ (i) (x : β₂ i), Decidable (x ≠ 0)]

Mathlib/Data/FinEnum.lean

@@ -157,7 +157,7 @@ theorem Finset.mem_enum [DecidableEq α] (s : Finset α) (xs : List α) :
       simp only [and_imp, mem_sdiff, mem_singleton]
       simp only [or_iff_not_imp_left] at h
       exists h
-      by_cases xs_hd ∈ s
+      by_cases h : xs_hd ∈ s
       · have : {xs_hd} ⊆ s
         simp only [HasSubset.Subset, *, forall_eq, mem_singleton]
         simp only [union_sdiff_of_subset this, or_true_iff, Finset.union_sdiff_of_subset,

Mathlib/Data/Finset/Basic.lean

@@ -3063,7 +3063,7 @@ theorem toFinset_add (s t : Multiset α) : toFinset (s + t) = toFinset s ∪ toF
 theorem toFinset_nsmul (s : Multiset α) : ∀ (n : ℕ) (_ : n ≠ 0), (n • s).toFinset = s.toFinset
   | 0, h => by contradiction
   | n + 1, _ => by
-    by_cases n = 0
+    by_cases h : n = 0
     · rw [h, zero_add, one_nsmul]
     · rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
 #align multiset.to_finset_nsmul Multiset.toFinset_nsmul

Mathlib/Data/Finset/Fold.lean

@@ -122,7 +122,7 @@ theorem fold_union_inter [DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : 
 @[simp]
 theorem fold_insert_idem [DecidableEq α] [hi : IsIdempotent β op] :
     (insert a s).fold op b f = f a * s.fold op b f := by
-  by_cases a ∈ s
+  by_cases h : a ∈ s
   · rw [← insert_erase h]
     simp [← ha.assoc, hi.idempotent]
   · apply fold_insert h

Mathlib/Data/Finsupp/Basic.lean

@@ -599,7 +599,7 @@ theorem sum_mapDomain_index_addMonoidHom [AddCommMonoid N] {f : α → β} {s :
 
 theorem embDomain_eq_mapDomain (f : α ↪ β) (v : α →₀ M) : embDomain f v = mapDomain f v := by
   ext a
-  by_cases a ∈ Set.range f
+  by_cases h : a ∈ Set.range f
   · rcases h with ⟨a, rfl⟩
     rw [mapDomain_apply f.injective, embDomain_apply]
   · rw [mapDomain_notin_range, embDomain_notin_range] <;> assumption
@@ -1183,7 +1183,7 @@ theorem mem_support_multiset_sum [AddCommMonoid M] {s : Multiset (α →₀ M)}
   Multiset.induction_on s (fun h => False.elim (by simp at h))
     (by
       intro f s ih ha
-      by_cases a ∈ f.support
+      by_cases h : a ∈ f.support
       · exact ⟨f, Multiset.mem_cons_self _ _, h⟩
       · simp only [Multiset.sum_cons, mem_support_iff, add_apply, not_mem_support_iff.1 h,
           zero_add] at ha
@@ -1413,7 +1413,7 @@ variable [Zero M] [MonoidWithZero R] [MulActionWithZero R M]
 
 @[simp]
 theorem single_smul (a b : α) (f : α → M) (r : R) : single a r b • f a = single a (r • f b) b := by
-  by_cases a = b <;> simp [h]
+  by_cases h : a = b <;> simp [h]
 #align finsupp.single_smul Finsupp.single_smul
 
 end

Mathlib/Data/Finsupp/Defs.lean

@@ -405,7 +405,7 @@ theorem single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : M) :
     single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 := by
   constructor
   · intro eq
-    by_cases a₁ = a₂
+    by_cases h : a₁ = a₂
     · refine' Or.inl ⟨h, _⟩
       rwa [h, (single_injective a₂).eq_iff] at eq
     · rw [FunLike.ext_iff] at eq

Mathlib/Data/List/Basic.lean

@@ -1197,7 +1197,7 @@ theorem indexOf_cons_ne {a b : α} (l : List α) : a ≠ b → indexOf a (b :: l
     cases l with
     | nil => rw [indexOf, findIdx, findIdx.go, beq_false_of_ne n, cond, ←succ_eq_add_one]; rfl
     | cons head tail =>
-      by_cases a = head
+      by_cases h : a = head
       · rw [indexOf_cons_eq tail h, indexOf, findIdx, findIdx.go, beq_false_of_ne n, cond, h,
           findIdx.go, beq_self_eq_true head, cond]
       · rw [indexOf, findIdx, findIdx, findIdx.go, beq_false_of_ne, cond, findIdx.go,
@@ -1220,7 +1220,7 @@ where
 -- rfl
 theorem indexOf_cons (a b : α) (l : List α) :
     indexOf a (b :: l) = if a = b then 0 else succ (indexOf a l) := by
-  cases l <;> by_cases a = b
+  cases l <;> by_cases h : a = b
   case pos | pos => rw [if_pos h]; exact indexOf_cons_eq _ h
   case neg | neg => rw [if_neg h]; exact indexOf_cons_ne _ h
 #align list.index_of_cons List.indexOf_cons
@@ -2910,7 +2910,7 @@ variable (p : α → Bool) (xs ys : List α) (ls : List (List α)) (f : List α
 
 @[simp]
 theorem splitAt_eq_take_drop (n : ℕ) (l : List α) : splitAt n l = (take n l, drop n l) := by
-  by_cases n < l.length <;> rw [splitAt, go_eq_take_drop]
+  by_cases h : n < l.length <;> rw [splitAt, go_eq_take_drop]
   · rw [if_pos h]; rfl
   · rw [if_neg h, take_all_of_le <| le_of_not_lt h, drop_eq_nil_of_le <| le_of_not_lt h]
 where
@@ -2969,7 +2969,7 @@ theorem splitOnP.go_append (xs : List α) (acc : Array α) (r : Array (List α))
   | nil => rfl
   | cons a as =>
     simp only [go]
-    by_cases p a
+    by_cases h : p a
     · simp only [h, cond_true]
       rw [go_append as, go_append as _ (Array.push #[] (Array.toList acc))]
       simp only [Array.toListAppend_eq, Array.push_data]
@@ -2983,7 +2983,7 @@ theorem splitOnP.go_acc (xs : List α) (acc : Array α) :
   | nil => rfl
   | cons hd tl =>
     simp only [go]
-    by_cases p hd
+    by_cases h : p hd
     · simp only [h, cond_true]
       rw [go_append, go_append _ _ _ (Array.push #[] (Array.toList #[]))]
       rfl
@@ -2999,7 +2999,7 @@ theorem splitOnP_ne_nil (xs : List α) : xs.splitOnP p ≠ [] := by
   | nil => exact cons_ne_nil [] []
   | cons hd tl =>
     rw [splitOnP, splitOnP.go]
-    by_cases p hd
+    by_cases h : p hd
     · rw [h, cond_true, splitOnP.go_append]
       exact append_ne_nil_of_ne_nil_left [[]] _ (cons_ne_nil [] [])
     · rw [eq_false_of_ne_true h, cond_false, splitOnP.go_acc, ←splitOnP]
@@ -3014,7 +3014,7 @@ theorem splitOnP_cons (x : α) (xs : List α) :
     (x :: xs).splitOnP p =
       if p x then [] :: xs.splitOnP p else (xs.splitOnP p).modifyHead (cons x) := by
   rw [splitOnP, splitOnP.go]
-  by_cases p x
+  by_cases h : p x
   · rw [if_pos h, h, cond_true, splitOnP.go_append, splitOnP]; rfl
   · rw [if_neg h, eq_false_of_ne_true h, cond_false, splitOnP.go_acc, splitOnP]; congr 1
 #align list.split_on_p_cons List.splitOnP_consₓ
@@ -3027,7 +3027,7 @@ theorem splitOnP_spec (as : List α) :
   | nil => rfl
   | cons a as' ih =>
     rw [splitOnP_cons, filter]
-    by_cases p a
+    by_cases h : p a
     · rw [if_pos h, h, map, cons_append, zipWith, nil_append, join, cons_append, cons_inj]
       exact ih
     · rw [if_neg h, eq_false_of_ne_true h, join_zipWith (splitOnP_ne_nil _ _)
@@ -3806,7 +3806,8 @@ theorem monotone_filter_left (p : α → Bool) ⦃l l' : List α⦄ (h : l ⊆ l
 theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
   induction' l with a l ih
   · exact iff_of_true rfl (forall_mem_nil _)
-  rw [forall_mem_cons]; by_cases p a
+  rw [forall_mem_cons]
+  by_cases h : p a
   · rw [filter_cons_of_pos _ h, cons_inj, ih, and_iff_right h]
   · refine' iff_of_false (fun hl => h <| of_mem_filter (_ : a ∈ filter p (a :: l))) (mt And.left h)
     rw [hl]

Mathlib/Data/List/Count.lean

@@ -39,7 +39,7 @@ protected theorem countp_go_eq_add (l) : countp.go p l n = n + countp.go p l 0 :
   · rfl
   · unfold countp.go
     rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
-    by_cases p head
+    by_cases h : p head
     · simp [h, add_assoc]
     · simp [h]
 
@@ -68,7 +68,7 @@ theorem countp_cons (a : α) (l) : countp p (a :: l) = countp p l + if p a then
 theorem length_eq_countp_add_countp (l) : length l = countp p l + countp (fun a => ¬p a) l := by
   induction' l with x h ih
   · rfl
-  by_cases p x
+  by_cases h : p x
   · rw [countp_cons_of_pos _ _ h, countp_cons_of_neg _ _ _, length, ih]
     · ac_rfl
     · simp only [h]
@@ -80,7 +80,7 @@ theorem length_eq_countp_add_countp (l) : length l = countp p l + countp (fun a
 theorem countp_eq_length_filter (l) : countp p l = length (filter p l) := by
   induction' l with x l ih
   · rfl
-  by_cases p x
+  by_cases h : p x
   · rw [countp_cons_of_pos p l h, ih, filter_cons_of_pos l h, length]
   · rw [countp_cons_of_neg p l h, ih, filter_cons_of_neg l h]
 #align list.countp_eq_length_filter List.countp_eq_length_filter

Mathlib/Data/List/Dedup.lean

@@ -93,10 +93,10 @@ theorem dedup_idempotent {l : List α} : dedup (dedup l) = dedup l :=
 theorem dedup_append (l₁ l₂ : List α) : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂ := by
   induction' l₁ with a l₁ IH; · rfl
   simp only [instUnionList, cons_union] at *
-  rw [← IH]
-  show dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
-  by_cases a ∈ dedup (l₁ ++ l₂) <;> [rw [dedup_cons_of_mem' h, insert_of_mem h],
-    rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]]
+  rw [← IH, cons_append]
+  by_cases h : a ∈ dedup (l₁ ++ l₂)
+  · rw [dedup_cons_of_mem' h, insert_of_mem h]
+  · rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]
 #align list.dedup_append List.dedup_append
 
 theorem replicate_dedup {x : α} : ∀ {k}, k ≠ 0 → (replicate k x).dedup = [x]

Mathlib/Data/List/Forall2.lean

@@ -297,7 +297,7 @@ theorem rel_filter {p : α → Bool} {q : β → Bool}
   | _, _, Forall₂.nil => Forall₂.nil
   | a :: as, b :: bs, Forall₂.cons h₁ h₂ => by
     dsimp [LiftFun] at hpq
-    by_cases p a
+    by_cases h : p a
     · have : q b := by rwa [← hpq h₁]
       simp only [filter_cons_of_pos _ h, filter_cons_of_pos _ this, forall₂_cons, h₁, true_and_iff,
         rel_filter hpq h₂]

Mathlib/Data/List/Infix.lean

@@ -698,7 +698,7 @@ theorem insert.def (a : α) (l : List α) : insert a l = if a ∈ l then l else
 
 @[simp]
 theorem suffix_insert (a : α) (l : List α) : l <:+ l.insert a := by
-  by_cases a ∈ l
+  by_cases h : a ∈ l
   · simp only [insert_of_mem h, insert, suffix_refl]
   · simp only [insert_of_not_mem h, suffix_cons, insert]
 

Mathlib/Data/List/Lattice.lean

@@ -233,7 +233,7 @@ theorem cons_bagInter_of_neg (l₁ : List α) (h : a ∉ l₂) :
 theorem mem_bagInter {a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
   | [], l₂ => by simp only [nil_bagInter, not_mem_nil, false_and_iff]
   | b :: l₁, l₂ => by
-    by_cases b ∈ l₂
+    by_cases h : b ∈ l₂
     · rw [cons_bagInter_of_pos _ h, mem_cons, mem_cons, mem_bagInter]
       by_cases ba : a = b
       · simp only [ba, h, eq_self_iff_true, true_or_iff, true_and_iff]
@@ -269,7 +269,7 @@ theorem bagInter_sublist_left : ∀ l₁ l₂ : List α, l₁.bagInter l₂ <+ l
   | [], l₂ => by simp
   | b :: l₁, l₂ =>
     by
-    by_cases b ∈ l₂ <;> simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
+    by_cases h : b ∈ l₂ <;> simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
     · exact (bagInter_sublist_left _ _).cons_cons _
     · apply sublist_cons_of_sublist
       apply bagInter_sublist_left

Mathlib/Data/List/Nodup.lean

@@ -304,7 +304,7 @@ theorem nodup_reverse {l : List α} : Nodup (reverse l) ↔ Nodup l :=
 theorem Nodup.erase_eq_filter [DecidableEq α] {l} (d : Nodup l) (a : α) :
     l.erase a = l.filter (· ≠ a) := by
   induction' d with b l m _ IH; · rfl
-  by_cases b = a
+  by_cases h : b = a
   · subst h
     rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
     symm

Mathlib/Data/List/Pairwise.lean

@@ -393,7 +393,7 @@ theorem pwFilter_map (f : β → α) :
 theorem pwFilter_sublist : ∀ l : List α, pwFilter R l <+ l
   | [] => nil_sublist _
   | x :: l => by
-    by_cases ∀ y ∈ pwFilter R l, R x y
+    by_cases h : ∀ y ∈ pwFilter R l, R x y
     · rw [pwFilter_cons_of_pos h]
       exact (pwFilter_sublist l).cons_cons _
     · rw [pwFilter_cons_of_neg h]
@@ -407,7 +407,7 @@ theorem pwFilter_subset (l : List α) : pwFilter R l ⊆ l :=
 theorem pairwise_pwFilter : ∀ l : List α, Pairwise R (pwFilter R l)
   | [] => Pairwise.nil
   | x :: l => by
-    by_cases ∀ y ∈ pwFilter R l, R x y
+    by_cases h : ∀ y ∈ pwFilter R l, R x y
     · rw [pwFilter_cons_of_pos h]
       exact pairwise_cons.2 ⟨h, pairwise_pwFilter l⟩
     · rw [pwFilter_cons_of_neg h]
@@ -438,7 +438,7 @@ theorem forall_mem_pwFilter (neg_trans : ∀ {x y z}, R x z → R x y ∨ R y z)
   ⟨by
     induction' l with x l IH; · exact fun _ _ h => (not_mem_nil _ h).elim
     simp only [forall_mem_cons]
-    by_cases ∀ y ∈ pwFilter R l, R x y <;> dsimp at h
+    by_cases h : ∀ y ∈ pwFilter R l, R x y <;> dsimp at h
     · simp only [pwFilter_cons_of_pos h, forall_mem_cons, and_imp]
       exact fun r H => ⟨r, IH H⟩
     · rw [pwFilter_cons_of_neg h]

Mathlib/Data/List/Perm.lean

@@ -841,7 +841,7 @@ theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂
     l₁.bagInter t ~ l₂.bagInter t := by
   induction' h with x _ _ _ _ x y _ _ _ _ _ _ ih_1 ih_2 generalizing t; · simp
   · by_cases x ∈ t <;> simp [*, Perm.cons]
-  · by_cases x = y
+  · by_cases h : x = y
     · simp [h]
     by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
     · simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
@@ -854,7 +854,7 @@ theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂
 theorem Perm.bagInter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) :
     l.bagInter t₁ = l.bagInter t₂ := by
   induction' l with a l IH generalizing t₁ t₂ p; · simp
-  by_cases a ∈ t₁
+  by_cases h : a ∈ t₁
   · simp [h, p.subset h, IH (p.erase _)]
   · simp [h, mt p.mem_iff.2 h, IH p]
 #align list.perm.bag_inter_left List.Perm.bagInter_left
@@ -880,11 +880,11 @@ theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l
       specialize H b
       simp at H
       contradiction
-    · have : a ∈ l₂ := count_pos.1 (by rw [← H] ; simp)
+    · have : a ∈ l₂ := count_pos.1 (by rw [← H]; simp)
       refine' ((IH fun b => _).cons a).trans (perm_cons_erase this).symm
       specialize H b
       rw [(perm_cons_erase this).count_eq] at H
-      by_cases b = a <;> simp [h] at H⊢ <;> assumption⟩
+      by_cases h : b = a <;> simpa [h] using H⟩
 #align list.perm_iff_count List.perm_iff_count
 
 theorem perm_replicate_append_replicate {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) :