feat(set_theory/ordinal/fixed_point): add missing theorem (#18323)

We add `apply_lt_nfp_bfamily` matching `apply_lt_nfp_family`, and rename the existing theorem with that name to `apply_lt_nfp_bfamily_iff`, matching `apply_lt_nfp_family_iff`.

Author: vihdzp

src/set_theory/ordinal/fixed_point.lean

@@ -237,20 +237,25 @@ sup_le
 theorem nfp_bfamily_monotone (hf : ∀ i hi, monotone (f i hi)) : monotone (nfp_bfamily o f) :=
 nfp_family_monotone (λ i, hf _ _)
 
-theorem apply_lt_nfp_bfamily (ho : o ≠ 0) (H : ∀ i hi, is_normal (f i hi)) {a b} :
-  (∀ i hi, f i hi b < nfp_bfamily o f a) ↔ b < nfp_bfamily o f a :=
+theorem apply_lt_nfp_bfamily (H : ∀ i hi, is_normal (f i hi)) {a b} (hb : b < nfp_bfamily o f a)
+  (i hi) : f i hi b < nfp_bfamily o f a :=
 begin
-  unfold nfp_bfamily,
-  rw ←@apply_lt_nfp_family_iff _ (family_of_bfamily o f) (out_nonempty_iff_ne_zero.2 ho)
-    (λ i, H _ _),
-  refine ⟨λ h i, h _ (typein_lt_self i), λ h i hio, _⟩,
   rw ←family_of_bfamily_enum o f,
-  apply h
+  apply apply_lt_nfp_family _ hb,
+  exact λ _, H _ _
 end
 
+theorem apply_lt_nfp_bfamily_iff (ho : o ≠ 0) (H : ∀ i hi, is_normal (f i hi)) {a b} :
+  (∀ i hi, f i hi b < nfp_bfamily o f a) ↔ b < nfp_bfamily o f a :=
+⟨λ h, begin
+  haveI := out_nonempty_iff_ne_zero.2 ho,
+  refine (apply_lt_nfp_family_iff _).1 (λ _, h _ _),
+  exact λ _, H _ _,
+end, apply_lt_nfp_bfamily H⟩
+
 theorem nfp_bfamily_le_apply (ho : o ≠ 0) (H : ∀ i hi, is_normal (f i hi)) {a b} :
   (∃ i hi, nfp_bfamily o f a ≤ f i hi b) ↔ nfp_bfamily o f a ≤ b :=
-by { rw ←not_iff_not, push_neg, convert apply_lt_nfp_bfamily ho H, simp only [not_le] }
+by { rw ←not_iff_not, push_neg, convert apply_lt_nfp_bfamily_iff ho H, simp only [not_le] }
 
 theorem nfp_bfamily_le_fp (H : ∀ i hi, monotone (f i hi)) {a b} (ab : a ≤ b)
   (h : ∀ i hi, f i hi b ≤ b) : nfp_bfamily o f a ≤ b :=