refactor: hypothesis naming in custom recursors (#1658)

agjftucker · agjftucker · commit ac1e75f550b4 · 2023-03-30T13:54:48.000Z
I have renamed hypotheses in `WithBot.recBotCoe`, `WithTop.recTopCoe` and `Finset.cons_induction` on the basis that rather than ```lean cases f₁ using WithBot.recBotCoe with | h₁ => … | h₂ f₁ => … ``` we would prefer to be able to write ```lean cases f₁ using WithBot.recBotCoe with | bot => … | coe f₁ => … ``` and rather than ```lean induction s using cons_induction with | h₁ => … | @h₂ c s hc ih => … ``` we would prefer ```lean induction s using cons_induction with | empty => … | @COns c t hc ih => … ```` I also tidied up some of inf' stuff in Finset.Lattice by using named arguments to specify the dual type instead of `@`s and `_ _ _`.
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
@@ -1184,17 +1184,19 @@ theorem ssubset_insert (h : a ∉ s) : s ⊂ insert a s :=
   ssubset_iff.mpr ⟨a, h, Subset.rfl⟩
 #align finset.ssubset_insert Finset.ssubset_insert
 
+#check Finset.mk
+
 @[elab_as_elim]
-theorem cons_induction {α : Type _} {p : Finset α → Prop} (h₁ : p ∅)
-    (h₂ : ∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (cons a s h)) : ∀ s, p s
-  | ⟨s, nd⟩ =>
-    Multiset.induction_on s (fun _ => h₁)
-      (fun a s IH nd => by
-        cases' nodup_cons.1 nd with m nd'
-        rw [← (eq_of_veq _ : cons a (Finset.mk s _) m = ⟨a ::ₘ s, nd⟩)]
-        · exact h₂ m (IH nd')
-        · rw [cons_val])
-      nd
+theorem cons_induction {α : Type _} {p : Finset α → Prop} (empty : p ∅)
+    (cons : ∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (cons a s h)) : ∀ s, p s
+  | ⟨s, nd⟩ => by
+    induction s using Multiset.induction with
+    | empty => exact empty
+    | @cons a s IH =>
+      cases' nodup_cons.1 nd with m nd'
+      rw [← (eq_of_veq _ : Finset.cons a ⟨s, _⟩ m = ⟨a ::ₘ s, nd⟩)]
+      · exact cons m (IH nd')
+      · rw [cons_val]
 #align finset.cons_induction Finset.cons_induction
 
 @[elab_as_elim]
@@ -1204,9 +1206,9 @@ theorem cons_induction_on {α : Type _} {p : Finset α → Prop} (s : Finset α)
 #align finset.cons_induction_on Finset.cons_induction_on
 
 @[elab_as_elim]
-protected theorem induction {α : Type _} {p : Finset α → Prop} [DecidableEq α] (h₁ : p ∅)
-    (h₂ : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) : ∀ s, p s :=
-  cons_induction h₁ fun a s ha => (s.cons_eq_insert a ha).symm ▸ h₂ ha
+protected theorem induction {α : Type _} {p : Finset α → Prop} [DecidableEq α] (empty : p ∅)
+    (insert : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) : ∀ s, p s :=
+  cons_induction empty fun a s ha => (s.cons_eq_insert a ha).symm ▸ insert ha
 #align finset.induction Finset.induction
 
 /-- To prove a proposition about an arbitrary `Finset α`,
diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
@@ -568,35 +568,27 @@ theorem comp_sup_eq_sup_comp_of_is_total [SemilatticeSup β] [OrderBot β] (g :
 @[simp]
 protected theorem le_sup_iff (ha : ⊥ < a) : a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b := by
   apply Iff.intro
-  · intro h'
-    induction s using Finset.cons_induction with
-    | h₁ => exact False.elim (not_le_of_lt ha h')
-    | @h₂ c s hc ih =>
-      rw [sup_cons, _root_.le_sup_iff] at h'
-      cases h' with
-      | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), h⟩
-      | inr h =>
-        rcases ih h with ⟨b, hb, hle⟩
-        exact ⟨b, mem_cons.2 (Or.inr hb), hle⟩
-  · rintro ⟨b, hb, hle⟩
-    exact le_trans hle (le_sup hb)
+  · induction s using cons_induction with
+    | empty => exact (absurd · (not_le_of_lt ha))
+    | @cons c t hc ih =>
+      rw [sup_cons, le_sup_iff]
+      exact fun
+      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
+      | Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩
+  · exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)
 #align finset.le_sup_iff Finset.le_sup_iff
 
 @[simp]
 protected theorem lt_sup_iff : a < s.sup f ↔ ∃ b ∈ s, a < f b := by
   apply Iff.intro
-  · intro h'
-    induction s using Finset.cons_induction with
-    | h₁ => exact False.elim (not_lt_bot h')
-    | @h₂ c s hc ih =>
-      rw [sup_cons, _root_.lt_sup_iff] at h'
-      cases h' with
-      | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), h⟩
-      | inr h =>
-        rcases ih h with ⟨b, hb, hlt⟩
-        exact ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
-  · rintro ⟨b, hb, hlt⟩
-    exact lt_of_lt_of_le hlt (le_sup hb)
+  · induction s using cons_induction with
+    | empty => exact (absurd · not_lt_bot)
+    | @cons c t hc ih =>
+      rw [sup_cons, lt_sup_iff]
+      exact fun
+      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
+      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
+  · exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)
 #align finset.lt_sup_iff Finset.lt_sup_iff
 
 @[simp]
@@ -738,27 +730,27 @@ theorem comp_sup'_eq_sup'_comp [SemilatticeSup γ] {s : Finset β} (H : s.Nonemp
   rw [coe_sup']
   refine' comp_sup_eq_sup_comp g' _ rfl
   intro f₁ f₂
-  induction f₁ using WithBot.recBotCoe with
-  | h₁ =>
+  cases f₁ using WithBot.recBotCoe with
+  | bot =>
     rw [bot_sup_eq]
     exact bot_sup_eq.symm
-  | h₂ f₁ =>
-    induction f₂ using WithBot.recBotCoe with
-    | h₁ => rfl
-    | h₂ f₂ => exact congr_arg _ (g_sup f₁ f₂)
+  | coe f₁ =>
+    cases f₂ using WithBot.recBotCoe with
+    | bot => rfl
+    | coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
 #align finset.comp_sup'_eq_sup'_comp Finset.comp_sup'_eq_sup'_comp
 
 theorem sup'_induction {p : α → Prop} (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂))
     (hs : ∀ b ∈ s, p (f b)) : p (s.sup' H f) := by
   show @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)
   rw [coe_sup']
   refine' sup_induction trivial _ hs
-  rintro (_ | a₁) h1 a₂ h2
+  rintro (_ | a₁) h₁ a₂ h₂
   · rw [WithBot.none_eq_bot, bot_sup_eq]
-    exact h2
-  induction a₂ using WithBot.recBotCoe with
-  | h₁ => exact h1
-  | h₂ a₂ => exact hp a₁ h1 a₂ h2
+    exact h₂
+  · cases a₂ using WithBot.recBotCoe with
+    | bot => exact h₁
+    | coe a₂ => exact hp a₁ h₁ a₂ h₂
 #align finset.sup'_induction Finset.sup'_induction
 
 theorem sup'_mem (s : Set α) (w : ∀ (x) (_ : x ∈ s) (y) (_ : y ∈ s), x ⊔ y ∈ s) {ι : Type _}
@@ -824,37 +816,37 @@ theorem inf'_singleton {b : β} {h : ({b} : Finset β).Nonempty} : ({b} : Finset
 #align finset.inf'_singleton Finset.inf'_singleton
 
 theorem le_inf' {a : α} (hs : ∀ b ∈ s, a ≤ f b) : a ≤ s.inf' H f :=
-  @sup'_le αᵒᵈ _ _ _ H f _ hs
+  sup'_le (α := αᵒᵈ) H f hs
 #align finset.le_inf' Finset.le_inf'
 
 theorem inf'_le {b : β} (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b :=
-  @le_sup' αᵒᵈ _ _ _ f _ h
+  le_sup' (α := αᵒᵈ) f h
 #align finset.inf'_le Finset.inf'_le
 
 @[simp]
 theorem inf'_const (a : α) : (s.inf' H fun _ => a) = a :=
-  @sup'_const αᵒᵈ _ _ _ H _
+  sup'_const (α := αᵒᵈ) H a
 #align finset.inf'_const Finset.inf'_const
 
 @[simp]
 theorem le_inf'_iff {a : α} : a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b :=
-  @sup'_le_iff αᵒᵈ _ _ _ H f _
+  sup'_le_iff (α := αᵒᵈ) H f
 #align finset.le_inf'_iff Finset.le_inf'_iff
 
 theorem inf'_bunionᵢ [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β}
     (Ht : ∀ b, (t b).Nonempty) :
     (s.bunionᵢ t).inf' (Hs.bunionᵢ fun b _ => Ht b) f = s.inf' Hs (fun b => (t b).inf' (Ht b) f) :=
-  @sup'_bunionᵢ αᵒᵈ _ _ _ _ _ _ Hs _ Ht
+  sup'_bunionᵢ (α := αᵒᵈ) _ Hs Ht
 #align finset.inf'_bUnion Finset.inf'_bunionᵢ
 
 theorem comp_inf'_eq_inf'_comp [SemilatticeInf γ] {s : Finset β} (H : s.Nonempty) {f : β → α}
     (g : α → γ) (g_inf : ∀ x y, g (x ⊓ y) = g x ⊓ g y) : g (s.inf' H f) = s.inf' H (g ∘ f) :=
-  @comp_sup'_eq_sup'_comp αᵒᵈ _ γᵒᵈ _ _ _ H f g g_inf
+  comp_sup'_eq_sup'_comp (α := αᵒᵈ) (γ := γᵒᵈ) H g g_inf
 #align finset.comp_inf'_eq_inf'_comp Finset.comp_inf'_eq_inf'_comp
 
 theorem inf'_induction {p : α → Prop} (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊓ a₂))
     (hs : ∀ b ∈ s, p (f b)) : p (s.inf' H f) :=
-  @sup'_induction αᵒᵈ _ _ _ H f _ hp hs
+  sup'_induction (α := αᵒᵈ) H f hp hs
 #align finset.inf'_induction Finset.inf'_induction
 
 theorem inf'_mem (s : Set α) (w : ∀ (x) (_ : x ∈ s) (y) (_ : y ∈ s), x ⊓ y ∈ s) {ι : Type _}
@@ -865,13 +857,13 @@ theorem inf'_mem (s : Set α) (w : ∀ (x) (_ : x ∈ s) (y) (_ : y ∈ s), x 
 @[congr]
 theorem inf'_congr {t : Finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) :
     s.inf' H f = t.inf' (h₁ ▸ H) g :=
-  @sup'_congr αᵒᵈ _ _ _ H _ _ _ h₁ h₂
+  sup'_congr (α := αᵒᵈ) H h₁ h₂
 #align finset.inf'_congr Finset.inf'_congr
 
 @[simp]
 theorem inf'_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f).Nonempty)
     (hs' : s.Nonempty := Finset.map_nonempty.mp hs) : (s.map f).inf' hs g = s.inf' hs' (g ∘ f) :=
-  @sup'_map αᵒᵈ _ _ _ _ _ _ hs hs'
+  sup'_map (α := αᵒᵈ) _ hs hs'
 #align finset.inf'_map Finset.inf'_map
 
 end Inf'
@@ -900,17 +892,17 @@ section Inf
 variable [SemilatticeInf α] [OrderTop α]
 
 theorem inf'_eq_inf {s : Finset β} (H : s.Nonempty) (f : β → α) : s.inf' H f = s.inf f :=
-  @sup'_eq_sup αᵒᵈ _ _ _ _ H f
+  sup'_eq_sup (α := αᵒᵈ) H f
 #align finset.inf'_eq_inf Finset.inf'_eq_inf
 
 theorem inf_closed_of_inf_closed {s : Set α} (t : Finset α) (htne : t.Nonempty) (h_subset : ↑t ⊆ s)
     (h : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), a ⊓ b ∈ s) : t.inf id ∈ s :=
-  @sup_closed_of_sup_closed αᵒᵈ _ _ _ t htne h_subset h
+  sup_closed_of_sup_closed (α := αᵒᵈ) t htne h_subset h
 #align finset.inf_closed_of_inf_closed Finset.inf_closed_of_inf_closed
 
 theorem coe_inf_of_nonempty {s : Finset β} (h : s.Nonempty) (f : β → α) :
     (↑(s.inf f) : WithTop α) = s.inf ((↑) ∘ f) :=
-  @coe_sup_of_nonempty αᵒᵈ _ _ _ _ h f
+  coe_sup_of_nonempty (α := αᵒᵈ) h f
 #align finset.coe_inf_of_nonempty Finset.coe_inf_of_nonempty
 
 end Inf
@@ -926,7 +918,7 @@ protected theorem sup_apply {C : β → Type _} [∀ b : β, SemilatticeSup (C b
 protected theorem inf_apply {C : β → Type _} [∀ b : β, SemilatticeInf (C b)]
     [∀ b : β, OrderTop (C b)] (s : Finset α) (f : α → ∀ b : β, C b) (b : β) :
     s.inf f b = s.inf fun a => f a b :=
-  @Finset.sup_apply _ _ (fun b => (C b)ᵒᵈ) _ _ s f b
+  Finset.sup_apply (C := fun b => (C b)ᵒᵈ) s f b
 #align finset.inf_apply Finset.inf_apply
 
 @[simp]
@@ -940,7 +932,7 @@ protected theorem sup'_apply {C : β → Type _} [∀ b : β, SemilatticeSup (C
 protected theorem inf'_apply {C : β → Type _} [∀ b : β, SemilatticeInf (C b)]
     {s : Finset α} (H : s.Nonempty) (f : α → ∀ b : β, C b) (b : β) :
     s.inf' H f b = s.inf' H fun a => f a b :=
-  @Finset.sup'_apply _ _ (fun b => (C b)ᵒᵈ) _ _ H f b
+  Finset.sup'_apply (C := fun b => (C b)ᵒᵈ) H f b
 #align finset.inf'_apply Finset.inf'_apply
 
 @[simp]
@@ -991,17 +983,17 @@ theorem sup'_lt_iff : s.sup' H f < a ↔ ∀ i ∈ s, f i < a := by
 
 @[simp]
 theorem inf'_le_iff : s.inf' H f ≤ a ↔ ∃ i ∈ s, f i ≤ a :=
-  @le_sup'_iff αᵒᵈ _ _ _ H f _
+  le_sup'_iff (α := αᵒᵈ) H
 #align finset.inf'_le_iff Finset.inf'_le_iff
 
 @[simp]
 theorem inf'_lt_iff : s.inf' H f < a ↔ ∃ i ∈ s, f i < a :=
-  @lt_sup'_iff αᵒᵈ _ _ _ H f _
+  lt_sup'_iff (α := αᵒᵈ) H
 #align finset.inf'_lt_iff Finset.inf'_lt_iff
 
 @[simp]
 theorem lt_inf'_iff : a < s.inf' H f ↔ ∀ i ∈ s, a < f i :=
-  @sup'_lt_iff αᵒᵈ _ _ _ H f _
+  sup'_lt_iff (α := αᵒᵈ) H
 #align finset.lt_inf'_iff Finset.lt_inf'_iff
 
 theorem exists_mem_eq_sup' (f : ι → α) : ∃ i, i ∈ s ∧ s.sup' H f = f i := by
@@ -1015,7 +1007,7 @@ theorem exists_mem_eq_sup' (f : ι → α) : ∃ i, i ∈ s ∧ s.sup' H f = f i
 #align finset.exists_mem_eq_sup' Finset.exists_mem_eq_sup'
 
 theorem exists_mem_eq_inf' (f : ι → α) : ∃ i, i ∈ s ∧ s.inf' H f = f i :=
-  @exists_mem_eq_sup' αᵒᵈ _ _ _ H f
+  exists_mem_eq_sup' (α := αᵒᵈ) H f
 #align finset.exists_mem_eq_inf' Finset.exists_mem_eq_inf'
 
 theorem exists_mem_eq_sup [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) :
@@ -1025,7 +1017,7 @@ theorem exists_mem_eq_sup [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ι
 
 theorem exists_mem_eq_inf [OrderTop α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) :
     ∃ i, i ∈ s ∧ s.inf f = f i :=
-  @exists_mem_eq_sup αᵒᵈ _ _ _ _ h f
+  exists_mem_eq_sup (α := αᵒᵈ) s h f
 #align finset.exists_mem_eq_inf Finset.exists_mem_eq_inf
 
 end LinearOrder
diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
@@ -152,9 +152,9 @@ theorem cons_inj_right (a : α) : ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t
 #align multiset.cons_inj_right Multiset.cons_inj_right
 
 @[recursor 5]
-protected theorem induction {p : Multiset α → Prop} (h₁ : p 0)
-    (h₂ : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) : ∀ s, p s := by
-  rintro ⟨l⟩; induction' l with _ _ ih <;> [exact h₁, exact h₂ ih]
+protected theorem induction {p : Multiset α → Prop} (empty : p 0)
+    (cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) : ∀ s, p s := by
+  rintro ⟨l⟩; induction' l with _ _ ih <;> [exact empty, exact cons ih]
 #align multiset.induction Multiset.induction
 
 @[elab_as_elim]
diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
@@ -95,11 +95,9 @@ theorem coe_ne_bot : (a : WithBot α) ≠ ⊥ :=
 
 /-- Recursor for `WithBot` using the preferred forms `⊥` and `↑a`. -/
 @[elab_as_elim]
-def recBotCoe {C : WithBot α → Sort _} (h₁ : C ⊥) (h₂ : ∀ a : α, C a) :
-  ∀ n : WithBot α, C n
-| none => h₁
-| Option.some a => h₂ a
-
+def recBotCoe {C : WithBot α → Sort _} (bot : C ⊥) (coe : ∀ a : α, C a) : ∀ n : WithBot α, C n
+| none => bot
+| Option.some a => coe a
 #align with_bot.rec_bot_coe WithBot.recBotCoe
 
 @[simp]
@@ -612,9 +610,9 @@ theorem coe_ne_top : (a : WithTop α) ≠ ⊤ :=
 
 /-- Recursor for `WithTop` using the preferred forms `⊤` and `↑a`. -/
 @[elab_as_elim]
-def recTopCoe {C : WithTop α → Sort _} (h₁ : C ⊤) (h₂ : ∀ a : α, C a) : ∀ n : WithTop α, C n
-| none => h₁
-| Option.some a => h₂ a
+def recTopCoe {C : WithTop α → Sort _} (top : C ⊤) (coe : ∀ a : α, C a) : ∀ n : WithTop α, C n
+| none => top
+| Option.some a => coe a
 #align with_top.rec_top_coe WithTop.recTopCoe
 
 @[simp]
