feat: add Bool.dand and Ordering.dthen along with more lemmas

src/Init/Data/Ord/Basic.lean

@@ -96,6 +96,15 @@ Ordering.lt
   | .eq => b
   | a => a
 
+/--
+Dependent version of `Ordering.then`.
+-/
+@[macro_inline, expose, implicit_reducible]
+def dthen (a : Ordering) (b : a = .eq → Ordering) : Ordering :=
+  match a with
+  | .eq => b rfl
+  | a => a
+
 /-- Version of `Ordering.then'` for proof by reflection. -/
 @[expose] noncomputable def then' (a b : Ordering) : Ordering :=
   Ordering.rec a b a a
@@ -252,6 +261,7 @@ theorem isGE_eq_isGT_or_isEq : ∀ {o : Ordering}, o.isGE = (o.isGT || o.isEq) :
 theorem isEq_eq_beq_eq : ∀ {o : Ordering}, o.isEq = (o == .eq) := by decide
 theorem isNe_eq_not_beq_eq : ∀ {o : Ordering}, o.isNe = (!o == .eq) := by decide
 theorem isNe_eq_isLT_or_isGT : ∀ {o : Ordering}, o.isNe = (o.isLT || o.isGT) := by decide
+theorem isLE_and_isGE_eq : ∀ {o : Ordering}, (o.isLE && o.isGE) = o.isEq := by decide
 
 @[simp] theorem not_isLT_eq_isGE : ∀ {o : Ordering}, (!o.isLT) = o.isGE := by decide
 @[simp] theorem not_isLE_eq_isGT : ∀ {o : Ordering}, (!o.isLE) = o.isGT := by decide
@@ -271,6 +281,9 @@ theorem swap_then : ∀ (o₁ o₂ : Ordering), (o₁.then o₂).swap = o₁.swa
 theorem then_eq_lt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by decide
 theorem then_eq_gt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by decide
 @[simp] theorem then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by decide
+theorem then_eq_eq_of_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁ = eq → o₂ = eq → o₁.then o₂ = eq := by decide
+theorem left_eq_eq_of_then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq → o₁ = eq := by decide
+theorem right_eq_eq_of_then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq → o₂ = eq := by decide
 
 theorem isLT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLT = (o₁.isLT || o₁.isEq && o₂.isLT) := by decide
 theorem isEq_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq) := by decide
@@ -290,7 +303,37 @@ theorem isLE_then_iff_and : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE 
 theorem isLE_left_of_isLE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE → o₁.isLE := by decide
 theorem isGE_left_of_isGE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGE → o₁.isGE := by decide
 
-theorem isLE_and_isGE_eq : ∀ {o : Ordering}, (o.isLE && o.isGE) = o.isEq := by decide
+theorem then_eq_left_iff : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = o₁ ↔ (o₁ = .eq → o₂ = o₁) := by decide
+theorem then_eq_right_iff : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = o₂ ↔ (o₁ ≠ .eq → o₂ = o₁) := by decide
+
+@[congr] theorem dthen_congr {x x' : Ordering}
+    {y : x = eq → Ordering} {y' : x' = eq → Ordering}
+    (hx : x = x') (hy : ∀ h, y (hx ▸ h) = y' h) :
+    x.dthen y = x'.dthen y' := by cases hx; cases funext hy; rfl
+
+@[simp] theorem dthen_eq_then : ∀ {o₁ o₂ : Ordering}, o₁.dthen (fun _ => o₂) = o₁.then o₂ := by decide
+
+theorem swap_dthen : ∀ (o₁ : Ordering) (o₂), (o₁.dthen o₂).swap = o₁.swap.dthen (fun h => (o₂ (swap_eq_eq.mp h)).swap) := by decide
+
+theorem dthen_eq_lt : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = lt ↔ o₁ = lt ∨ ∃ h : o₁ = eq, o₂ h = lt := by decide
+theorem dthen_eq_gt : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = gt ↔ o₁ = gt ∨ ∃ h : o₁ = eq, o₂ h = gt := by decide
+@[simp] theorem dthen_eq_eq : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = eq ↔ ∃ h : o₁ = eq, o₂ h = eq := by decide
+theorem dthen_eq_eq_of_eq_eq : ∀ {o₁ : Ordering} {o₂}, (h₁ : o₁ = .eq) → o₂ h₁ = .eq → o₁.dthen o₂ = .eq := by decide
+theorem left_eq_eq_of_dthen_eq_eq : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = .eq → o₁ = .eq := by decide
+theorem right_eq_eq_of_dthen_eq_eq : ∀ {o₁ : Ordering} {o₂}, (h : o₁.dthen o₂ = .eq) → o₂ (left_eq_eq_of_dthen_eq_eq h) = .eq := by decide
+
+@[simp] theorem lt_dthen {o} : lt.dthen o = lt := rfl
+@[simp] theorem gt_dthen {o} : gt.dthen o = gt := rfl
+@[simp] theorem eq_dthen {o} : eq.dthen o = o rfl := rfl
+
+theorem dthen_assoc : ∀ (o₁ : Ordering) (o₂ o₃), (o₁.dthen o₂).dthen o₃ =
+  o₁.dthen (fun h => (o₂ h).dthen fun h' => o₃ (dthen_eq_eq_of_eq_eq h h')) := by decide
+
+theorem isLE_dthen_iff_or : ∀ {o₁ : Ordering} {o₂}, (o₁.dthen o₂).isLE ↔ o₁ = lt ∨ (∃ h, (o₂ h).isLE) := by decide
+theorem isLE_left_of_isLE_dthen : ∀ {o₁ : Ordering} {o₂}, (o₁.dthen o₂).isLE → o₁.isLE := by decide
+theorem isGE_left_of_isGE_dthen : ∀ {o₁ : Ordering} {o₂}, (o₁.dthen o₂).isGE → o₁.isGE := by decide
+
+theorem dthen_eq_left_iff : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = o₁ ↔ (∀ h, o₂ h = o₁) := by decide
 
 instance : Std.Associative Ordering.then := ⟨then_assoc⟩
 instance : Std.IdempotentOp Ordering.then := ⟨fun _ => then_self⟩

src/Init/Prelude.lean

@@ -1076,6 +1076,14 @@ noncomputable def Bool.and (x y : Bool) : Bool :=
   | false => false
   | true  => y
 
+/--
+The dependent version of `a && b`.
+-/
+@[macro_inline, implicit_reducible] def Bool.dand (a : Bool) (b : Eq a true → Bool) : Bool :=
+  match a with
+  | false => false
+  | true => b rfl
+
 /--
 Boolean negation, also known as Boolean complement. `not x` can be written `!x`.
 
@@ -1264,6 +1272,12 @@ instance [dp : Decidable p] : Decidable (Not p) where
     | isTrue  hp => absurd hp
     | isFalse hp => hp
 
+theorem Bool.Reflects.of_imp {x : Bool} {p : Prop} (h₁ : Eq x true → p) (h₂ : p → Eq x true) :
+    x.Reflects p :=
+  match x with
+  | false => fun hp => Bool.noConfusion (h₂ hp)
+  | true => h₁ rfl
+
 /--
 Decides whether two Booleans are equal.
 

src/Init/PropLemmas.lean

@@ -542,6 +542,22 @@ instance forall_prop_decidable {p} (P : p → Prop)
       | isFalse h2 => fun al => absurd (al h) h2
     | isFalse h => fun h2 => absurd h2 h
 
+@[inline]
+instance forall_forall_prop_decidable {p} {α : Sort u} (P : (p → α) → Prop)
+    [hp : Decidable p] [hP : ∀ f, Decidable (P f)]
+    [hα : ∀ Q : α → Bool, Decidable (∀ x, Q x = true)] : Decidable (∀ f, P f) where
+  decide := if h : p then decide (∀ a, decide <| P fun _ => a) else decide (P h.elim)
+  reflects_decide :=
+    match hp with
+    | isTrue h =>
+      match hα (fun a => decide <| P fun _ => a) with
+      | isTrue h2 => fun f => of_decide_eq_true (h2 (f h))
+      | isFalse h2 => fun h' => h2 fun _ => decide_eq_true (h' _)
+    | isFalse h => show (decide (P h.elim)).Reflects (∀ h, P h) from
+      match hP h.elim with
+      | isTrue h2 => fun f => (funext (fun h' => absurd h' h) : f = h.elim) ▸ h2
+      | isFalse h2 => fun h' => absurd (h' _) h2
+
 @[bool_to_prop] theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) ↔ p := by simp
 
 @[simp, bool_to_prop] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
@@ -942,4 +958,3 @@ theorem Bool.dite_else_true {p : Prop} [Decidable p] {x : p → Bool} : (if h :
 
 @[deprecated Bool.dite_false_right_eq_false (since := "2026-07-21")]
 theorem Bool.dite_else_false_eq_false {p : Prop} [Decidable p] {x : p → Bool} : (if h : p then x h else Bool.false) = Bool.false ↔ ∀ (h : p), x h = Bool.false := Bool.dite_false_right_eq_false
-

src/Init/SimpLemmas.lean

@@ -377,6 +377,30 @@ instance : Std.LawfulIdentity (· && ·) true where
 instance : Std.IdempotentOp (· && ·) := ⟨Bool.and_self⟩
 @[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by
   cases a <;> cases b <;> decide
+theorem Bool.and_eq_true_of_eq_true {x y : Bool} (hx : x = true) (hy : y = true) :
+    (x && y) = true := and_eq_true x y ▸ ⟨hx, hy⟩
+theorem Bool.left_eq_true_of_and_eq_true {x y : Bool} (h : (x && y) = true) :
+    x = true := (and_eq_true x y ▸ h).1
+theorem Bool.right_eq_true_of_and_eq_true {x y : Bool} (h : (x && y) = true) :
+    y = true := (and_eq_true x y ▸ h).2
+
+@[congr] theorem Bool.dand_congr {x x' : Bool} {y : x = true → Bool} {y' : x' = true → Bool}
+    (hx : x = x') (hy : ∀ h, y (hx ▸ h) = y' h) :
+    x.dand y = x'.dand y' := by cases hx; cases funext hy; rfl
+@[simp] theorem Bool.false_dand {y : false = true → Bool} : false.dand y = false := rfl
+@[simp] theorem Bool.true_dand {y : true = true → Bool} : true.dand y = y rfl := rfl
+@[simp] theorem Bool.dand_eq_and {x y : Bool} : x.dand (fun _ => y) = (x && y) := by cases x <;> rfl
+@[simp] theorem Bool.dand_eq_true_iff {x : Bool} {y : x = true → Bool} :
+    x.dand y = true ↔ Exists fun h : x = true => y h = true :=
+  match x with
+  | false => iff_of_false nofun nofun
+  | true => ⟨fun hy => ⟨rfl, hy⟩, fun ⟨_, hy⟩ => hy⟩
+theorem Bool.dand_eq_true_of_eq_true {x : Bool} {y : x = true → Bool}
+    (hx : x = true) (hy : y hx = true) : x.dand y = true := dand_eq_true_iff.mpr ⟨hx, hy⟩
+theorem Bool.left_eq_true_of_dand_eq_true {x : Bool} {y : x = true → Bool} (h : x.dand y = true) :
+    x = true := (dand_eq_true_iff.mp h).1
+theorem Bool.right_eq_true_of_dand_eq_true {x : Bool} {y : x = true → Bool} (h : x.dand y = true) :
+    y (left_eq_true_of_dand_eq_true h) = true := (dand_eq_true_iff.mp h).2
 
 theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c)) := by
   cases a <;> cases b <;> cases c <;> decide