From ceb42c50ce60f62b241a00b4de90a1d4d5bb8b7c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 24 Jun 2023 01:01:09 +0000 Subject: [PATCH] chore: remove legacy `termination_by'` (#5426) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds a couple of `WellFoundedRelation` instances, like for example `WellFoundedRelation (WithBot Nat)`. Longer-term, we should probably add a `WellFoundedOrder` class for types with a well-founded less-than relation and a `[WellFoundOrder α] : WellFoundedRelation α` instance (or maybe just `[LT α] [IsWellFounded fun a b : α => a < b] : WellFoundedRelation α`). --- Mathlib/Algebra/EuclideanDomain/Defs.lean | 54 ++++++++-------- Mathlib/Data/Finsupp/Multiset.lean | 5 ++ Mathlib/Data/List/Basic.lean | 2 +- Mathlib/Data/Nat/Cast/WithTop.lean | 3 + Mathlib/Data/Nat/Squarefree.lean | 79 +++++++++++------------ Mathlib/Data/Nat/WithBot.lean | 4 ++ Mathlib/Data/Polynomial/Inductions.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Basic.lean | 50 +++++++------- Mathlib/RingTheory/PowerSeries/Basic.lean | 2 +- Mathlib/SetTheory/Lists.lean | 8 ++- Mathlib/SetTheory/Ordinal/NaturalOps.lean | 17 +++-- Mathlib/SetTheory/ZFC/Basic.lean | 6 +- 12 files changed, 122 insertions(+), 110 deletions(-) diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean index 476462aabaa96..91274b9299526 100644 --- a/Mathlib/Algebra/EuclideanDomain/Defs.lean +++ b/Mathlib/Algebra/EuclideanDomain/Defs.lean @@ -113,6 +113,9 @@ variable {R : Type u} [EuclideanDomain R] /-- Abbreviated notation for the well-founded relation `r` in a Euclidean domain. -/ local infixl:50 " ≺ " => EuclideanDomain.r +local instance wellFoundedRelation : WellFoundedRelation R where + wf := r_wellFounded + -- see Note [lower instance priority] instance (priority := 70) : Div R := ⟨EuclideanDomain.quotient⟩ @@ -177,18 +180,17 @@ section open Classical @[elab_as_elim] -theorem GCD.induction {P : R → R → Prop} : - ∀ a b : R, (H0 : ∀ x, P 0 x) → (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) → P a b - | a => fun b H0 H1 => - if a0 : a = 0 then by - -- Porting note: required for hygiene, the equation compiler introduces a dummy variable `x` - -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unnecessarily.20tombstoned.20argument/near/314573315 - change P a b - exact a0.symm ▸ H0 b - else - have _ := mod_lt b a0 - H1 _ _ a0 (GCD.induction (b % a) a H0 H1) - termination_by' ⟨_, r_wellFounded⟩ +theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x) + (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b := + if a0 : a = 0 then by + -- Porting note: required for hygiene, the equation compiler introduces a dummy variable `x` + -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unnecessarily.20tombstoned.20argument/near/314573315 + change P a b + exact a0.symm ▸ H0 b + else + have _ := mod_lt b a0 + H1 _ _ a0 (GCD.induction (b % a) a H0 H1) +termination_by _ => a #align euclidean_domain.gcd.induction EuclideanDomain.GCD.induction end @@ -199,13 +201,12 @@ variable [DecidableEq R] /-- `gcd a b` is a (non-unique) element such that `gcd a b ∣ a` `gcd a b ∣ b`, and for any element `c` such that `c ∣ a` and `c ∣ b`, then `c ∣ gcd a b` -/ -def gcd : R → R → R - | a => fun b => - if a0 : a = 0 then b - else - have _ := mod_lt b a0 - gcd (b % a) a - termination_by' ⟨_, r_wellFounded⟩ +def gcd (a b : R) : R := + if a0 : a = 0 then b + else + have _ := mod_lt b a0 + gcd (b % a) a +termination_by _ => a #align euclidean_domain.gcd EuclideanDomain.gcd @[simp] @@ -223,14 +224,13 @@ The function `xgcdAux` takes in two triples, and from these recursively computes xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t) ``` -/ -def xgcdAux : R → R → R → R → R → R → R × R × R - | r => fun s t r' s' t' => - if _hr : r = 0 then (r', s', t') - else - let q := r' / r - xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t - termination_by' ⟨_, r_wellFounded⟩ - decreasing_by (exact mod_lt _ _hr) +def xgcdAux (r s t r' s' t' : R) : R × R × R := + if _hr : r = 0 then (r', s', t') + else + let q := r' / r + have _ := mod_lt r' _hr + xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t +termination_by _ => r #align euclidean_domain.xgcd_aux EuclideanDomain.xgcdAux @[simp] diff --git a/Mathlib/Data/Finsupp/Multiset.lean b/Mathlib/Data/Finsupp/Multiset.lean index 874a4d53622f7..61addf25f81d6 100644 --- a/Mathlib/Data/Finsupp/Multiset.lean +++ b/Mathlib/Data/Finsupp/Multiset.lean @@ -233,6 +233,11 @@ theorem lt_wf : WellFounded (@LT.lt (ι →₀ ℕ) _) := Subrelation.wf (sum_id_lt_of_lt _ _) <| InvImage.wf _ Nat.lt_wfRel.2 #align finsupp.lt_wf Finsupp.lt_wf +-- TODO: generalize to `[WellFoundedRelation α] → WellFoundedRelation (ι →₀ α)` +instance : WellFoundedRelation (ι →₀ ℕ) where + rel := (· < ·) + wf := lt_wf _ + end Finsupp theorem Multiset.toFinsupp_strictMono : StrictMono (@Multiset.toFinsupp ι) := diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 5fc444fb9e18b..3679a3382698e 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -1018,7 +1018,7 @@ def bidirectionalRec {C : List α → Sort _} (H0 : C []) (H1 : ∀ a : α, C [a rw [← dropLast_append_getLast (cons_ne_nil b l)] have : C l' := bidirectionalRec H0 H1 Hn l' exact Hn a l' b' this -termination_by' measure List.length +termination_by _ l => l.length #align list.bidirectional_rec List.bidirectionalRecₓ -- universe order /-- Like `bidirectionalRec`, but with the list parameter placed first. -/ diff --git a/Mathlib/Data/Nat/Cast/WithTop.lean b/Mathlib/Data/Nat/Cast/WithTop.lean index 6500d4dbcf274..bf097ebd79e62 100644 --- a/Mathlib/Data/Nat/Cast/WithTop.lean +++ b/Mathlib/Data/Nat/Cast/WithTop.lean @@ -18,6 +18,9 @@ An orphaned lemma about casting from `ℕ` to `WithBot ℕ`, exiled here to minimize imports to `data.rat.order` for porting purposes. -/ +instance : WellFoundedRelation (WithTop ℕ) where + rel := (· < ·) + wf := IsWellFounded.wf theorem Nat.cast_withTop (n : ℕ) : Nat.cast n = WithTop.some n := rfl diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index bfef060c49054..e3c5d124a20af 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -154,46 +154,45 @@ theorem minSqFacProp_div (n) {k} (pk : Prime k) (dk : k ∣ n) (dkk : ¬k * k #align nat.min_sq_fac_prop_div Nat.minSqFacProp_div --Porting note: I had to replace two uses of `by decide` by `linarith`. -theorem minSqFacAux_has_prop : - ∀ {n : ℕ} (k), - 0 < n → ∀ i, k = 2 * i + 3 → (∀ m, Prime m → m ∣ n → k ≤ m) → MinSqFacProp n (minSqFacAux n k) - | n, k => fun n0 i e ih => by - rw [minSqFacAux] - by_cases h : n < k * k <;> simp [h] - · refine' squarefree_iff_prime_squarefree.2 fun p pp d => _ - have := ih p pp (dvd_trans ⟨_, rfl⟩ d) - have := Nat.mul_le_mul this this - exact not_le_of_lt h (le_trans this (le_of_dvd n0 d)) - have k2 : 2 ≤ k := by - subst e - linarith - have k0 : 0 < k := lt_of_lt_of_le (by decide) k2 - have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) := by - intro n' nd' nk - have hn' := le_of_dvd n0 nd' - refine' - have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k := - lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h) - @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1) - (by simp [e, left_distrib]) fun m m2 d => _ - cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml - · subst me - contradiction - apply (Nat.eq_or_lt_of_le ml).resolve_left - intro me - rw [← me, e] at d - change 2 * (i + 2) ∣ n' at d - have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd') - rw [e] at this - exact absurd this (by linarith) - have pk : k ∣ n → Prime k := by - refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩ - exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk) - split_ifs with dk dkk - · exact ⟨pk dk, (Nat.dvd_div_iff dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩ - · specialize IH (n / k) (div_dvd_of_dvd dk) dkk - exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff dk).2 dkk) IH - · exact IH n (dvd_refl _) dk termination_by' ⟨_, (measure fun ⟨n, k⟩ => Nat.sqrt n + 2 - k).wf⟩ +theorem minSqFacAux_has_prop {n : ℕ} (k) (n0 : 0 < n) (i) (e : k = 2 * i + 3) + (ih : ∀ m, Prime m → m ∣ n → k ≤ m) : MinSqFacProp n (minSqFacAux n k) := by + rw [minSqFacAux] + by_cases h : n < k * k <;> simp [h] + · refine' squarefree_iff_prime_squarefree.2 fun p pp d => _ + have := ih p pp (dvd_trans ⟨_, rfl⟩ d) + have := Nat.mul_le_mul this this + exact not_le_of_lt h (le_trans this (le_of_dvd n0 d)) + have k2 : 2 ≤ k := by + subst e + linarith + have k0 : 0 < k := lt_of_lt_of_le (by decide) k2 + have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) := by + intro n' nd' nk + have hn' := le_of_dvd n0 nd' + refine' + have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k := + lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h) + @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1) + (by simp [e, left_distrib]) fun m m2 d => _ + cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml + · subst me + contradiction + apply (Nat.eq_or_lt_of_le ml).resolve_left + intro me + rw [← me, e] at d + change 2 * (i + 2) ∣ n' at d + have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd') + rw [e] at this + exact absurd this (by linarith) + have pk : k ∣ n → Prime k := by + refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩ + exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk) + split_ifs with dk dkk + · exact ⟨pk dk, (Nat.dvd_div_iff dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩ + · specialize IH (n / k) (div_dvd_of_dvd dk) dkk + exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff dk).2 dkk) IH + · exact IH n (dvd_refl _) dk +termination_by _ => n.sqrt + 2 - k #align nat.min_sq_fac_aux_has_prop Nat.minSqFacAux_has_prop theorem minSqFac_has_prop (n : ℕ) : MinSqFacProp n (minSqFac n) := by diff --git a/Mathlib/Data/Nat/WithBot.lean b/Mathlib/Data/Nat/WithBot.lean index 9f176e7c6026c..4724aaa0763d0 100644 --- a/Mathlib/Data/Nat/WithBot.lean +++ b/Mathlib/Data/Nat/WithBot.lean @@ -23,6 +23,10 @@ namespace Nat namespace WithBot +instance : WellFoundedRelation (WithBot ℕ) where + rel := (· < ·) + wf := IsWellFounded.wf + theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := by rcases n, m with ⟨_ | _, _ | _⟩ any_goals (exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩) diff --git a/Mathlib/Data/Polynomial/Inductions.lean b/Mathlib/Data/Polynomial/Inductions.lean index 210a7cc5fa6c4..75e97d585c597 100644 --- a/Mathlib/Data/Polynomial/Inductions.lean +++ b/Mathlib/Data/Polynomial/Inductions.lean @@ -116,7 +116,7 @@ noncomputable def recOnHorner {M : R[X] → Sort _} (p : R[X]) (M0 : M 0) MC _ _ (coeff_mul_X_zero _) hcp0 (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0 else MX (divX p) hpX0 (recOnHorner _ M0 MC MX)) -termination_by' invImage PSigma.fst ⟨_, degree_lt_wf⟩ +termination_by _ => p.degree #align polynomial.rec_on_horner Polynomial.recOnHorner /-- A property holds for all polynomials of positive `degree` with coefficients in a semiring `R` diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index aa2967a23e0c1..8131a54110964 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -529,32 +529,30 @@ theorem IsCycle.swap_mul {α : Type _} [DecidableEq α] {f : Perm α} (hf : IsCy isCycle_swap_mul_aux₂ (i - 1) hy hi⟩ #align equiv.perm.is_cycle.swap_mul Equiv.Perm.IsCycle.swap_mul -theorem IsCycle.sign : ∀ {f : Perm α} (hf : IsCycle f), sign f = -(-1) ^ f.support.card - | f => fun hf => - let ⟨x, hx⟩ := hf - calc - Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by - {rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]} - _ = -(-1) ^ f.support.card := - if h1 : f (f x) = x then by - have h : swap x (f x) * f = 1 := by - simp only [mul_def, one_def] - rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap] - dsimp only - rw [sign_mul, sign_swap hx.1.symm, h, sign_one, - hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm] - rfl - else by - have h : card (support (swap x (f x) * f)) + 1 = card (support f) := by - rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1, - card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase] - have : card (support (swap x (f x) * f)) < card (support f) := - card_support_swap_mul hx.1 - dsimp only - rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h] - simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one] - termination_by' - ⟨_, (measure fun f => f.support.card).wf ⟩ +theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support.card := + let ⟨x, hx⟩ := hf + calc + Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by + {rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]} + _ = -(-1) ^ f.support.card := + if h1 : f (f x) = x then by + have h : swap x (f x) * f = 1 := by + simp only [mul_def, one_def] + rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap] + dsimp only + rw [sign_mul, sign_swap hx.1.symm, h, sign_one, + hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm] + rfl + else by + have h : card (support (swap x (f x) * f)) + 1 = card (support f) := by + rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1, + card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase] + have : card (support (swap x (f x) * f)) < card (support f) := + card_support_swap_mul hx.1 + dsimp only + rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h] + simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one] +termination_by _ => f.support.card #align equiv.perm.is_cycle.sign Equiv.Perm.IsCycle.sign theorem IsCycle.of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) : diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean index e5d6e2a4861d8..c2b626399dfc5 100644 --- a/Mathlib/RingTheory/PowerSeries/Basic.lean +++ b/Mathlib/RingTheory/PowerSeries/Basic.lean @@ -820,7 +820,7 @@ protected noncomputable def inv.aux (a : R) (φ : MvPowerSeries σ R) : MvPowerS else -a * ∑ x in n.antidiagonal, if _ : x.2 < n then coeff R x.1 φ * inv.aux a φ x.2 else 0 - termination_by' ⟨_, Finsupp.lt_wf σ⟩ +termination_by _ n => n #align mv_power_series.inv.aux MvPowerSeries.inv.aux theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean index 3b32067c2e586..ec4ce866511b9 100644 --- a/Mathlib/SetTheory/Lists.lean +++ b/Mathlib/SetTheory/Lists.lean @@ -359,7 +359,7 @@ instance : Setoid (Lists α) := section Decidable /-- Auxiliary function to prove termination of decidability checking -/ -@[simp] +@[simp, deprecated] -- porting note: replaced by termination_by def Equiv.decidableMeas : (PSum (Σ' _l₁ : Lists α, Lists α) <| PSum (Σ' _l₁ : Lists' α true, Lists' α true) (Σ' _a : Lists α, Lists' α true)) → @@ -430,7 +430,11 @@ mutual mem.decidable a l₂ refine' decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) _ rw [← Lists'.mem_cons]; rfl -end termination_by' ⟨_, InvImage.wf Equiv.decidableMeas Nat.lt_wfRel.wf⟩ +end +termination_by + Subset.decidable x y => sizeOf x + sizeOf y + Equiv.decidable x y => sizeOf x + sizeOf y + mem.decidable x y => sizeOf x + sizeOf y #align lists.equiv.decidable Lists.Equiv.decidable #align lists.subset.decidable Lists.Subset.decidable #align lists.mem.decidable Lists.mem.decidable diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean index c8bb145c4a042..5f3d7c9a56c9d 100644 --- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean +++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean @@ -270,15 +270,14 @@ theorem blsub_nadd_of_mono {f : ∀ c < a ♯ b, Ordinal.{max u v}} apply mem_brange_self #align ordinal.blsub_nadd_of_mono Ordinal.blsub_nadd_of_mono -theorem nadd_assoc : ∀ a b c, a ♯ b ♯ c = a ♯ (b ♯ c) - | a, b, c => by - rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc] - · congr <;> ext (d hd) <;> apply nadd_assoc - · exact fun _ _ h => nadd_le_nadd_left h a - · exact fun _ _ h => nadd_le_nadd_right h c - termination_by' PSigma.lex (inferInstance) (fun _ ↦ inferInstance) - -- Porting note: above lines replaces - -- decreasing_by solve_by_elim [PSigma.Lex.left, PSigma.Lex.right] +theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c) := by + rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc] + · congr <;> ext (d hd) <;> apply nadd_assoc + · exact fun _ _ h => nadd_le_nadd_left h a + · exact fun _ _ h => nadd_le_nadd_right h c +termination_by _ => (a, b, c) +-- Porting note: above lines replaces +-- decreasing_by solve_by_elim [PSigma.Lex.left, PSigma.Lex.right] #align ordinal.nadd_assoc Ordinal.nadd_assoc @[simp] diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean index d6e325b177127..66a05e04155ff 100644 --- a/Mathlib/SetTheory/ZFC/Basic.lean +++ b/Mathlib/SetTheory/ZFC/Basic.lean @@ -1407,9 +1407,9 @@ theorem map_isFunc {f : ZFSet → ZFSet} [Definable 1 f] {x y : ZFSet} : /-- Given a predicate `p` on ZFC sets. `hereditarily p x` means that `x` has property `p` and the members of `x` are all `hereditarily p`. -/ -def Hereditarily (p : ZFSet → Prop) : ZFSet → Prop - | x => p x ∧ ∀ y ∈ x, Hereditarily p y -termination_by' ⟨_, mem_wf⟩ +def Hereditarily (p : ZFSet → Prop) (x : ZFSet) : Prop := + p x ∧ ∀ y ∈ x, Hereditarily p y +termination_by _ => x #align Set.hereditarily ZFSet.Hereditarily section Hereditarily