[Merged by Bors] - feat: port Logic.Hydra

Mathlib/Data/Multiset/Basic.lean

@@ -158,9 +158,9 @@ protected theorem induction {p : Multiset α → Prop} (empty : p 0)
 #align multiset.induction Multiset.induction
 
 @[elab_as_elim]
-protected theorem induction_on {p : Multiset α → Prop} (s : Multiset α) (h₁ : p 0)
-    (h₂ : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) : p s :=
-  Multiset.induction h₁ h₂ s
+protected theorem induction_on {p : Multiset α → Prop} (s : Multiset α) (empty : p 0)
+    (cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) : p s :=
+  Multiset.induction empty cons s
 #align multiset.induction_on Multiset.induction_on
 
 theorem cons_swap (a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s :=

Mathlib/Data/Multiset/Sections.lean

@@ -62,8 +62,8 @@ 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 h₁ => simp
-  case h₂ a a' ih => simp [ih, rel_cons_left, eq_comm]
+  case empty => simp
+  case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
 
 #align multiset.mem_sections Multiset.mem_sections
 

Mathlib/Logic/Hydra.lean

@@ -23,10 +23,10 @@ what order) you choose cut off the heads, the game always terminates, i.e. all h
 eventually be cut off (but of course it can last arbitrarily long, i.e. takes an
 arbitrary finite number of steps).
 
-This result is stated as the well-foundedness of the `cut_expand` relation defined in
+This result is stated as the well-foundedness of the `CutExpand` relation defined in
 this file: we model the heads of the hydra as a multiset of elements of `α`, and the
-valid "moves" of the game are modelled by the relation `cut_expand r` on `multiset α`:
-`cut_expand r s' s` is true iff `s'` is obtained by removing one head `a ∈ s` and
+valid "moves" of the game are modelled by the relation `CutExpand r` on `Multiset α`:
+`CutExpand r s' s` is true iff `s'` is obtained by removing one head `a ∈ s` and
 adding back an arbitrary multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.
 
 We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332.
@@ -42,122 +42,118 @@ open Multiset Prod
 
 variable {α : Type _}
 
-/-- The relation that specifies valid moves in our hydra game. `cut_expand r s' s`
+/-- The relation that specifies valid moves in our hydra game. `CutExpand r s' s`
   means that `s'` is obtained by removing one head `a ∈ s` and adding back an arbitrary
   multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.
 
-  This is most directly translated into `s' = s.erase a + t`, but `multiset.erase` requires
-  `decidable_eq α`, so we use the equivalent condition `s' + {a} = s + t` instead, which
+  This is most directly translated into `s' = s.erase a + t`, but `Multiset.erase` requires
+  `DecidableEq α`, so we use the equivalent condition `s' + {a} = s + t` instead, which
   is also easier to verify for explicit multisets `s'`, `s` and `t`.
 
   We also don't include the condition `a ∈ s` because `s' + {a} = s + t` already
   guarantees `a ∈ s + t`, and if `r` is irreflexive then `a ∉ t`, which is the
   case when `r` is well-founded, the case we are primarily interested in.
 
-  The lemma `relation.cut_expand_iff` below converts between this convenient definition
+  The lemma `Relation.cutExpand_iff` below converts between this convenient definition
   and the direct translation when `r` is irreflexive. -/
 def CutExpand (r : α → α → Prop) (s' s : Multiset α) : Prop :=
-  ∃ (t : Multiset α)(a : α), (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t
+  ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t
 #align relation.cut_expand Relation.CutExpand
 
 variable {r : α → α → Prop}
 
-theorem cutExpand_le_invImage_lex [hi : IsIrrefl α r] :
-    CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp :=
-  fun s t ⟨u, a, hr, he⟩ => by
+theorem cutExpand_le_invImage_lex [IsIrrefl α r] :
+    CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp := by
+  rintro s t ⟨u, a, hr, he⟩
+  replace hr := fun a' ↦ mt (hr a')
   classical
-    refine' ⟨a, fun b h => _, _⟩ <;> simp_rw [to_finsupp_apply]
-    · apply_fun count b  at he
-      simp_rw [count_add] at he
-      convert he <;> convert (add_zero _).symm <;> rw [count_eq_zero] <;> intro hb
-      exacts[h.2 (mem_singleton.1 hb), h.1 (hr b hb)]
-    · apply_fun count a  at he
-      simp_rw [count_add, count_singleton_self] at he
-      apply Nat.lt_of_succ_le
-      convert he.le
-      convert (add_zero _).symm
-      exact count_eq_zero.2 fun ha => hi.irrefl a <| hr a ha
+  refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
+  · replace he := congr_arg (count b) he -- porting note: was apply_fun count b  at he
+    simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
+      using he
+  · replace he := congr_arg (count a) he -- porting note: was apply_fun count a  at he
+    simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
+      add_zero] at he
+    exact he ▸ Nat.lt_succ_self _
 #align relation.cut_expand_le_inv_image_lex Relation.cutExpand_le_invImage_lex
 
 theorem cutExpand_singleton {s x} (h : ∀ x' ∈ s, r x' x) : CutExpand r s {x} :=
   ⟨s, x, h, add_comm s _⟩
 #align relation.cut_expand_singleton Relation.cutExpand_singleton
 
 theorem cutExpand_singleton_singleton {x' x} (h : r x' x) : CutExpand r {x'} {x} :=
-  cutExpand_singleton fun a h => by rwa [mem_singleton.1 h]
+  cutExpand_singleton fun a h ↦ by rwa [mem_singleton.1 h]
 #align relation.cut_expand_singleton_singleton Relation.cutExpand_singleton_singleton
 
 theorem cutExpand_add_left {t u} (s) : CutExpand r (s + t) (s + u) ↔ CutExpand r t u :=
-  exists₂_congr fun _ _ => and_congr Iff.rfl <| by rw [add_assoc, add_assoc, add_left_cancel_iff]
+  exists₂_congr fun _ _ ↦ and_congr Iff.rfl <| by rw [add_assoc, add_assoc, add_left_cancel_iff]
 #align relation.cut_expand_add_left Relation.cutExpand_add_left
 
 theorem cutExpand_iff [DecidableEq α] [IsIrrefl α r] {s' s : Multiset α} :
     CutExpand r s' s ↔
-      ∃ (t : Multiset α)(a : _), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.eraseₓ a + t := by
-  simp_rw [cut_expand, add_singleton_eq_iff]
-  refine' exists₂_congr fun t a => ⟨_, _⟩
+      ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t := by
+  simp_rw [CutExpand, add_singleton_eq_iff]
+  refine' exists₂_congr fun t a ↦ ⟨_, _⟩
   · rintro ⟨ht, ha, rfl⟩
     obtain h | h := mem_add.1 ha
-    exacts[⟨ht, h, t.erase_add_left_pos h⟩, (@irrefl α r _ a (ht a h)).elim]
+    exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
   · rintro ⟨ht, h, rfl⟩
-    exact ⟨ht, mem_add.2 (Or.inl h), (t.erase_add_left_pos h).symm⟩
+    exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩
 #align relation.cut_expand_iff Relation.cutExpand_iff
 
 theorem not_cutExpand_zero [IsIrrefl α r] (s) : ¬CutExpand r s 0 := by
   classical
-    rw [cut_expand_iff]
-    rintro ⟨_, _, _, ⟨⟩, _⟩
+  rw [cutExpand_iff]
+  rintro ⟨_, _, _, ⟨⟩, _⟩
 #align relation.not_cut_expand_zero Relation.not_cutExpand_zero
 
-/-- For any relation `r` on `α`, multiset addition `multiset α × multiset α → multiset α` is a
-  fibration between the game sum of `cut_expand r` with itself and `cut_expand r` itself. -/
+/-- For any relation `r` on `α`, multiset addition `Multiset α × Multiset α → Multiset α` is a
+  fibration between the game sum of `CutExpand r` with itself and `CutExpand r` itself. -/
 theorem cutExpand_fibration (r : α → α → Prop) :
-    Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s => s.1 + s.2 := by
-  rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he⊢
+    Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2 := by
+  rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢
   classical
-    obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
-    rw [add_assoc, mem_add] at ha
-    obtain h | h := ha
-    · refine' ⟨(s₁.erase a + t, s₂), game_add.fst ⟨t, a, hr, _⟩, _⟩
-      · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
-      · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
-    · refine' ⟨(s₁, (s₂ + t).eraseₓ a), game_add.snd ⟨t, a, hr, _⟩, _⟩
-      · rw [add_comm, singleton_add, cons_erase h]
-      · rw [add_assoc, erase_add_right_pos _ h]
+  -- Porting note: Originally `obtain ⟨ha, rfl⟩`
+  obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
+  rw [hb]
+  rw [add_assoc, mem_add] at ha
+  obtain h | h := ha
+  · refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
+    · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
+    · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
+  · refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
+    · rw [add_comm, singleton_add, cons_erase h]
+    · rw [add_assoc, erase_add_right_pos _ h]
 #align relation.cut_expand_fibration Relation.cutExpand_fibration
 
-/-- A multiset is accessible under `cut_expand` if all its singleton subsets are,
+/-- A multiset is accessible under `CutExpand` if all its singleton subsets are,
   assuming `r` is irreflexive. -/
-theorem acc_of_singleton [IsIrrefl α r] {s : Multiset α} :
-    (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s := by
-  refine' Multiset.induction _ _ s
-  · exact fun _ => Acc.intro 0 fun s h => (not_cut_expand_zero s h).elim
-  · intro a s ih hacc
+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 =>
     rw [← s.singleton_add a]
-    exact
-      ((hacc a <| s.mem_cons_self a).prod_gameAdd <|
-            ih fun a ha => hacc a <| mem_cons_of_mem ha).of_fibration
-        _ (cut_expand_fibration r)
+    rw [forall_mem_cons] at hs
+    exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
 #align relation.acc_of_singleton Relation.acc_of_singleton
 
-/-- A singleton `{a}` is accessible under `cut_expand r` if `a` is accessible under `r`,
+/-- A singleton `{a}` is accessible under `CutExpand r` if `a` is accessible under `r`,
   assuming `r` is irreflexive. -/
-theorem Acc.cutExpand [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (CutExpand r) {a} := by
+theorem _root_.Acc.cutExpand [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (CutExpand r) {a} := by
   induction' hacc with a h ih
-  refine' Acc.intro _ fun s => _
+  refine' Acc.intro _ fun s ↦ _
   classical
-    rw [cut_expand_iff]
-    rintro ⟨t, a, hr, rfl | ⟨⟨⟩⟩, rfl⟩
-    refine' acc_of_singleton fun a' => _
-    rw [erase_singleton, zero_add]
-    exact ih a' ∘ hr a'
+  simp only [cutExpand_iff, mem_singleton]
+  rintro ⟨t, a, hr, rfl, rfl⟩
+  refine' acc_of_singleton fun a' ↦ _
+  rw [erase_singleton, zero_add]
+  exact ih a' ∘ hr a'
 #align acc.cut_expand Acc.cutExpand
 
-/-- `cut_expand r` is well-founded when `r` is. -/
-theorem WellFounded.cutExpand (hr : WellFounded r) : WellFounded (CutExpand r) :=
-  ⟨letI h := hr.is_irrefl
-    fun s => acc_of_singleton fun a _ => (hr.apply a).CutExpand⟩
+/-- `CutExpand r` is well-founded when `r` is. -/
+theorem _root_.WellFounded.cutExpand (hr : WellFounded r) : WellFounded (CutExpand r) :=
+  ⟨have := hr.isIrrefl; fun _ ↦ acc_of_singleton fun a _ ↦ (hr.apply a).cutExpand⟩
 #align well_founded.cut_expand WellFounded.cutExpand
 
 end Relation
-