diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
index e27c84a71918b3..c238dd5178aae0 100644
--- a/Mathlib/Algebra/Algebra/Hom.lean
+++ b/Mathlib/Algebra/Algebra/Hom.lean
@@ -541,3 +541,19 @@ lemma AlgHom.default_apply (x : S) : (default : S →ₐ[R] T) x = 0 :=
   rfl
 
 end
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem RingCon.inf_def : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (c d : RingCon R), c ⊓ d = ringConGen (⇑c ⊓ ⇑d) := by
+  open RingCon in
+    intro R inst inst_1 c d
+    exact (RingCon.gi R |>.l_inf_u _ _ |>.symm)
+
+theorem RingCon.sInf_def : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)), sInf S = ringConGen (sInf (DFunLike.coe '' S)) := by
+  open RingCon in
+    intro R inst inst_1 S
+    exact (RingCon.gi R |>.l_sInf_u_image _ |>.symm)
+
+end
diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean
index 66cd3bf80c06aa..6a8cb859f1f537 100644
--- a/Mathlib/Algebra/Algebra/Prod.lean
+++ b/Mathlib/Algebra/Algebra/Prod.lean
@@ -160,3 +160,14 @@ def uniqueProd [Unique B] : (B × A) ≃ₐ[R] A where
   commutes' _ := rfl
 
 end AlgEquiv
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem LinearMap.inf_range_inl_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : _root_.Module R M] [inst_4 : _root_.Module R M₂], (LinearMap.inl R M M₂).range ⊓ (LinearMap.inr R M M₂).range = ⊥ := by
+  open LinearMap Submodule in
+    intro R M M₂ inst inst_1 inst_2 inst_3 inst_4
+    exact (IsCompl.inf_eq_bot isCompl_range_inl_inr)
+
+end
diff --git a/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean b/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean
index 1063de3e49fe92..fa7e155be69e04 100644
--- a/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean
@@ -672,3 +672,14 @@ variable {ι M N : Type*} [CommMonoid M] [Zero N]
     unop (f.prod g) = f.prod fun i n ↦ unop (g i n) := unop_prod ..
 
 end AddOpposite
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem NNReal.iInf_div : ∀ {ι : Sort u_3} (f : ι → NNReal) (a : NNReal), (⨅ i, f i) / a = ⨅ i, f i / a := by
+  open NNReal Function Set Real in
+    intro ι f a
+    simp only [div_eq_mul_inv, iInf_mul]
+
+end
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index b162815dd0a236..5391dfe31d4076 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -1068,3 +1068,16 @@ end
 end ModuleCat
 
 end ModuleCat
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ModuleCat.preservesFiniteLimits_tensorRight_of_ringHomFlat : ∀ {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B}, f.Flat → CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorRight ((ModuleCat.restrictScalars f).obj (ModuleCat.of B B))) := by
+  open ModuleCat CategoryTheory Comonad Limits MonoidalCategory in
+    intro A B inst inst_1 f hf
+    algebraize [f]
+    change PreservesFiniteLimits <| tensorRight (ModuleCat.of A B)
+    infer_instance
+
+end
diff --git a/Mathlib/Algebra/Divisibility/Basic.lean b/Mathlib/Algebra/Divisibility/Basic.lean
index 97120cd19c3273..6c13cc94c9dba3 100644
--- a/Mathlib/Algebra/Divisibility/Basic.lean
+++ b/Mathlib/Algebra/Divisibility/Basic.lean
@@ -210,3 +210,14 @@ lemma pow_dvd_pow_of_dvd_of_le {m n : ℕ} (hab : a ∣ b) (hmn : m ≤ n) : a ^
   trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]
 
 end CommMonoid
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem SaturatedSubmonoid.iInf_def : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_2} {f : ι → SaturatedSubmonoid M}, iInf f = (⨅ i, (f i).toSubmonoid).saturation := by
+  open SaturatedSubmonoid in
+    intro M inst ι f
+    exact ((Submonoid.giSaturation M).l_iInf_u f |>.symm)
+
+end
diff --git a/Mathlib/Algebra/Exact/Basic.lean b/Mathlib/Algebra/Exact/Basic.lean
index c06babd2e4c995..935764bce54379 100644
--- a/Mathlib/Algebra/Exact/Basic.lean
+++ b/Mathlib/Algebra/Exact/Basic.lean
@@ -589,3 +589,15 @@ lemma Function.Exact.linearEquivOfSurjective_symm_apply (h : Function.Exact f g)
   simp [LinearEquiv.symm_apply_eq]
 
 end Ring
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem LieAlgebra.Extension.lie_apply_proj_of_rightInverse_eq : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [IsLieAbelian M] (E : LieAlgebra.Extension R M L) {s : L →ₗ[R] E.L}, Function.RightInverse ⇑E.proj ⇑s → ∀ (x : E.L) (y : ↥E.proj.ker), ⁅s (E.proj x), y⁆ = ⁅x, y⁆ := by
+  open LieAlgebra LieAlgebra.Extension Function LieModule.Cohomology in
+    intro R L M inst inst_1 inst_2 inst_3 inst_4 _ E s hs x y
+    rw [← sub_eq_zero, ← sub_lie]
+    exact trivial_lie_zero E.proj.ker E.proj.ker ⟨_, (by simp [hs.eq])⟩ y
+
+end
diff --git a/Mathlib/Algebra/Group/Action/Defs.lean b/Mathlib/Algebra/Group/Action/Defs.lean
index 54914db1eafdfb..5ddd14f6234779 100644
--- a/Mathlib/Algebra/Group/Action/Defs.lean
+++ b/Mathlib/Algebra/Group/Action/Defs.lean
@@ -717,3 +717,54 @@ instance [Group G] [MulAction G P] : IsLeftCancelSMul G P where
   left_cancel' a b c h := by rw [← inv_smul_smul a b, h, inv_smul_smul]
 
 end IsCancelSMul
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.preimage_inv_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α), Inv.inv ⁻¹' Set.Icc a b = Set.Icc b⁻¹ a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a b
+    simp
+
+theorem Set.preimage_inv_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), Inv.inv ⁻¹' Set.Ici a = Set.Iic a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a
+    simp
+
+theorem Set.preimage_inv_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), Inv.inv ⁻¹' Set.Iic a = Set.Ici a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a
+    simp
+
+theorem Set.preimage_inv_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α), Inv.inv ⁻¹' Set.Ico a b = Set.Ioc b⁻¹ a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a b
+    simp
+
+theorem Set.preimage_inv_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), Inv.inv ⁻¹' Set.Iio a = Set.Ioi a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a
+    simp
+
+theorem Set.preimage_inv_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α), Inv.inv ⁻¹' Set.Ioc a b = Set.Ico b⁻¹ a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a b
+    simp
+
+theorem Set.preimage_inv_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α), Inv.inv ⁻¹' Set.Ioo a b = Set.Ioo b⁻¹ a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a b
+    simp
+
+theorem Set.preimage_inv_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), Inv.inv ⁻¹' Set.Ioi a = Set.Iio a⁻¹ := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a
+    simp
+
+theorem Set.preimage_neg_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b : α), Neg.neg ⁻¹' Set.uIcc a b = Set.uIcc (-a) (-b) := by
+  open Set Interval Pointwise in
+    intro α inst inst_1 _ a b
+    simp
+
+end
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index c28a5efa016538..4d0abf66c04d8b 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -1094,3 +1094,14 @@ instance AddCommGroup.toGrindIntModule [s : AddCommGroup α] :
 instance IsRightCancelAdd.toGrindAddRightCancel [AddSemigroup α] [IsRightCancelAdd α] :
     Grind.AddRightCancel α where
   add_right_cancel _ _ _ := add_right_cancel
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.mulIndicator_inter_mul_union_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (f : α → M) (s t : Set α) (a : α), (s ∩ t).mulIndicator f a * (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a := by
+  open Set Function in
+    intro α M inst f s t a
+    by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]
+
+end
diff --git a/Mathlib/Algebra/Group/Conj.lean b/Mathlib/Algebra/Group/Conj.lean
index 691ab9ca1ead6b..08c5353644bc3c 100644
--- a/Mathlib/Algebra/Group/Conj.lean
+++ b/Mathlib/Algebra/Group/Conj.lean
@@ -295,3 +295,14 @@ theorem carrier_eq_preimage_mk {a : ConjClasses α} : a.carrier = ConjClasses.mk
   Set.ext fun _ => mem_carrier_iff_mk_eq
 
 end ConjClasses
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Subgroup.prod_eq_top_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup G} {K : Subgroup N}, H.prod K = ⊤ ↔ H = ⊤ ∧ K = ⊤ := by
+  open Subgroup Function Set in
+    intro G inst N inst_1 H K
+    simpa only [← Subgroup.toSubmonoid_inj] using! Submonoid.prod_eq_top_iff
+
+end
diff --git a/Mathlib/Algebra/Group/EvenFunction.lean b/Mathlib/Algebra/Group/EvenFunction.lean
index fac96be08157c8..79f8997afda9f3 100644
--- a/Mathlib/Algebra/Group/EvenFunction.lean
+++ b/Mathlib/Algebra/Group/EvenFunction.lean
@@ -166,3 +166,20 @@ lemma Odd.map_zero [NegZeroClass α] (hf : f.Odd) : f 0 = 0 := by simp [← neg_
 end torsionfree
 
 end Function
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem tprod_iInf_decode₂ : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4} [inst_2 : Encodable β] [inst_3 : CompleteLattice α] (m : α → M), m ⊤ = 1 → ∀ (s : β → α), ∏' (i : ℕ), m (⨅ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b) := by
+  open Filter Finset Function Encodable in
+    intro M inst inst_1 α β inst_2 inst_3 m m0 s
+    rw [← tprod_extend_one (@encode_injective β _)]
+    refine tprod_congr fun n ↦ ?_
+    rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
+    · simp [encode_injective.extend_apply]
+    · rw [extend_apply' _ _ _ hn]
+      rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn
+      simp [hn, m0]
+
+end
diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean
index e843f06764b73c..8f82c6d618f154 100644
--- a/Mathlib/Algebra/Group/InjSurj.lean
+++ b/Mathlib/Algebra/Group/InjSurj.lean
@@ -432,3 +432,19 @@ protected abbrev commGroup [CommGroup M₁] (f : M₁ → M₂) (hf : Surjective
 end Surjective
 
 end Function
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Con.inf_def : ∀ {M : Type u_1} [inst : Mul M] (c d : Con M), c ⊓ d = conGen (⇑c ⊓ ⇑d) := by
+  open Con Function Setoid in
+    intro M inst c d
+    exact (Con.gi M |>.l_inf_u _ _ |>.symm)
+
+theorem Con.sInf_def : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), sInf S = conGen (sInf (DFunLike.coe '' S)) := by
+  open Con Function Setoid in
+    intro M inst S
+    exact (Con.gi M |>.l_sInf_u_image _ |>.symm)
+
+end
diff --git a/Mathlib/Algebra/Group/Nat/Units.lean b/Mathlib/Algebra/Group/Nat/Units.lean
index 85297dcecd5c0e..da401e29449e3b 100644
--- a/Mathlib/Algebra/Group/Nat/Units.lean
+++ b/Mathlib/Algebra/Group/Nat/Units.lean
@@ -41,3 +41,29 @@ protected lemma isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1 := isUnit_iff_eq_one
 protected lemma isAddUnit_iff {n : ℕ} : IsAddUnit n ↔ n = 0 := isAddUnit_iff_eq_zero
 
 end Nat
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ENat.WithTop.natCast_add_cancel : ∀ {a b : WithTop ℕ∞} {c : ℕ}, ↑c + a = ↑c + b ↔ a = b := by
+  open ENat ENat.WithBot Function in
+    intro a b c
+    exact ((IsAddLeftRegular.all c).withBot.withTop.eq_iff)
+
+theorem ENat.WithTop.one_add_cancel : ∀ {a b : WithTop ℕ∞}, 1 + a = 1 + b ↔ a = b := by
+  open ENat ENat.WithBot Function in
+    intro a b
+    exact ((IsAddLeftRegular.all 1).withBot.withTop.eq_iff)
+
+theorem ENat.WithTop.add_natCast_cancel : ∀ {a b : WithTop ℕ∞} {c : ℕ}, a + ↑c = b + ↑c ↔ a = b := by
+  open ENat ENat.WithBot Function in
+    intro a b c
+    exact ((IsAddRightRegular.all c).withBot.withTop.eq_iff)
+
+theorem ENat.WithTop.add_one_cancel : ∀ {a b : WithTop ℕ∞}, a + 1 = b + 1 ↔ a = b := by
+  open ENat ENat.WithBot Function in
+    intro a b
+    exact ((IsAddRightRegular.all 1).withBot.withTop.eq_iff)
+
+end
diff --git a/Mathlib/Algebra/Group/Subgroup/Lattice.lean b/Mathlib/Algebra/Group/Subgroup/Lattice.lean
index 04aeb1ddde5112..453ec2f55375fa 100644
--- a/Mathlib/Algebra/Group/Subgroup/Lattice.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Lattice.lean
@@ -692,3 +692,14 @@ theorem mul_injective_of_disjoint {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H
     Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
 
 end Subgroup
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Submodule.toAddSubgroup_eq_bot : ∀ {R : Type u_4} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : _root_.Module R M] {p : Submodule R M}, p.toAddSubgroup = ⊥ ↔ p = ⊥ := by
+  open Submodule in
+    intro R M inst inst_1 inst_2 p
+    simp [← toAddSubgroup_inj]
+
+end
diff --git a/Mathlib/Algebra/Group/WithOne/Map.lean b/Mathlib/Algebra/Group/WithOne/Map.lean
index b7af9151f5b235..075fd60e26b3bf 100644
--- a/Mathlib/Algebra/Group/WithOne/Map.lean
+++ b/Mathlib/Algebra/Group/WithOne/Map.lean
@@ -63,3 +63,21 @@ lemma map₂_eq_bot_iff {f : α → β → γ} {a : WithOne α} {b : WithOne β}
     map₂ f a b = 1 ↔ a = 1 ∨ b = 1 := Option.map₂_eq_none_iff
 
 end WithOne
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem WithZero.instMulRightReflectLT : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Mul α] [MulRightReflectLT α], MulRightReflectLT (WithZero α) := by
+  open WithZero Multiplicative in
+    intro α inst inst_1 _
+    refine ⟨fun a b c h => ?_⟩
+    have := h.ne_zero
+    induction a
+    · simp at this
+    induction c
+    · simp at this
+    induction b
+    exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_right' <| coe_lt_coe.mp h)]
+
+end
diff --git a/Mathlib/Algebra/GroupWithZero/Regular.lean b/Mathlib/Algebra/GroupWithZero/Regular.lean
index cc8c99501f7f19..0b369a88bf3fc6 100644
--- a/Mathlib/Algebra/GroupWithZero/Regular.lean
+++ b/Mathlib/Algebra/GroupWithZero/Regular.lean
@@ -109,3 +109,14 @@ theorem isRegular_iff_ne_zero [Nontrivial R] : IsRegular a ↔ a ≠ 0 :=
   ⟨IsRegular.ne_zero, .of_ne_zero⟩
 
 end CancelMonoidWithZero
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem AbsoluteValue.map_one_of_isRightRegular : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S] (abv : AbsoluteValue R S), IsRightRegular (abv 1) → abv 1 = 1 := by
+  open AbsoluteValue in
+    intro R S inst inst_1 inst_2 abv h
+    exact (h <| by simp [← abv.map_mul])
+
+end
diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean
index 82a263fbcad7bd..fda2633eb55648 100644
--- a/Mathlib/Algebra/Lie/Submodule.lean
+++ b/Mathlib/Algebra/Lie/Submodule.lean
@@ -1023,3 +1023,14 @@ theorem LieSubalgebra.topEquiv_apply (x : (⊤ : LieSubalgebra R L)) : LieSubalg
   rfl
 
 end TopEquiv
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem LieIdeal.bot_toLieSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], LieIdeal.toLieSubalgebra R L ⊥ = ⊥ := by
+  open LieIdeal in
+    intro R L inst inst_1 inst_2
+    exact (rfl)
+
+end
diff --git a/Mathlib/Algebra/Order/AddGroupWithTop.lean b/Mathlib/Algebra/Order/AddGroupWithTop.lean
index 4ed0b10b0c5ca3..659d98fd7995bb 100644
--- a/Mathlib/Algebra/Order/AddGroupWithTop.lean
+++ b/Mathlib/Algebra/Order/AddGroupWithTop.lean
@@ -285,3 +285,19 @@ instance [LinearOrder G] [IsOrderedAddMonoid G] : LinearOrderedAddCommGroupWithT
   add_neg_cancel_of_ne_top | (a : G), _ => mod_cast add_neg_cancel a
 
 end WithTop.LinearOrderedAddCommGroup
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Tropical.trop_min_def : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R), min x y = Tropical.trop (min (Tropical.untrop x) (Tropical.untrop y)) := by
+  open Tropical in
+    intro R inst x y
+    exact (rfl)
+
+theorem Tropical.untrop_min : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R), Tropical.untrop (min x y) = min (Tropical.untrop x) (Tropical.untrop y) := by
+  open Tropical in
+    intro R inst x y
+    exact (rfl)
+
+end
diff --git a/Mathlib/Algebra/Order/Kleene.lean b/Mathlib/Algebra/Order/Kleene.lean
index 31cfca05053b33..4a4ca16d88ed28 100644
--- a/Mathlib/Algebra/Order/Kleene.lean
+++ b/Mathlib/Algebra/Order/Kleene.lean
@@ -376,3 +376,14 @@ protected abbrev kleeneAlgebra [KleeneAlgebra α] [LE β] [LT β] [Zero β] [One
     exact kstar_mul_le_self h
 
 end Function.Injective
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Language.sub_iInf : ∀ {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α), m - ⨅ i, l i = ⨆ i, m - l i := by
+  open Language List Set Computability in
+    intro α ι _ l m
+    exact (sdiff_iInter _ _)
+
+end
diff --git a/Mathlib/Algebra/Order/Monoid/Basic.lean b/Mathlib/Algebra/Order/Monoid/Basic.lean
index 6faa3142c6a982..fcd3a32bee14e8 100644
--- a/Mathlib/Algebra/Order/Monoid/Basic.lean
+++ b/Mathlib/Algebra/Order/Monoid/Basic.lean
@@ -76,3 +76,29 @@ See also `OrderIso.mulRight` when working in an ordered group. -/
 def OrderEmbedding.mulRight {α : Type*} [Mul α] [LinearOrder α]
     [MulRightStrictMono α] (m : α) : α ↪o α :=
   OrderEmbedding.ofStrictMono (fun n => n * m) mul_left_strictMono
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Cardinal.aleph_min : ∀ (o₁ o₂ : Ordinal.{u_1}), Cardinal.aleph (min o₁ o₂) = min (Cardinal.aleph o₁) (Cardinal.aleph o₂) := by
+  open Cardinal Function Set Equiv Order Ordinal in
+    intro o₁ o₂
+    exact (aleph.monotone.map_min)
+
+theorem Ordinal.omega_min : ∀ (o₁ o₂ : Ordinal.{u_1}), Ordinal.omega (min o₁ o₂) = min (Ordinal.omega o₁) (Ordinal.omega o₂) := by
+  open Ordinal Function Set Cardinal Equiv Order in
+    intro o₁ o₂
+    exact (omega.monotone.map_min)
+
+theorem Cardinal.preAleph_min : ∀ (o₁ o₂ : Ordinal.{u_1}), Cardinal.preAleph (min o₁ o₂) = min (Cardinal.preAleph o₁) (Cardinal.preAleph o₂) := by
+  open Cardinal Function Set Equiv Order Ordinal in
+    intro o₁ o₂
+    exact (preAleph.monotone.map_min)
+
+theorem Ordinal.preOmega_min : ∀ (o₁ o₂ : Ordinal.{u_1}), Ordinal.preOmega (min o₁ o₂) = min (Ordinal.preOmega o₁) (Ordinal.preOmega o₂) := by
+  open Ordinal Function Set Cardinal Equiv Order in
+    intro o₁ o₂
+    exact (preOmega.monotone.map_min)
+
+end
diff --git a/Mathlib/Algebra/Order/Ring/WithTop.lean b/Mathlib/Algebra/Order/Ring/WithTop.lean
index a7a8bc4d82a7bd..42ba539f046ff0 100644
--- a/Mathlib/Algebra/Order/Ring/WithTop.lean
+++ b/Mathlib/Algebra/Order/Ring/WithTop.lean
@@ -496,3 +496,14 @@ instance instIsOrderedRing [CommSemiring α] [PartialOrder α] [IsOrderedRing α
     IsOrderedRing (WithBot α) where
 
 end WithBot
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ENNReal.coe_mem_lowerBounds : ∀ {r : NNReal} {s : Set NNReal}, ↑r ∈ lowerBounds (ENNReal.ofNNReal '' s) ↔ r ∈ lowerBounds s := by
+  open ENNReal Function Set NNReal in
+    intro r s
+    simp +contextual [lowerBounds, forall_mem_image, -mem_image, *]
+
+end
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
index 5bcb9b4e73ec77..3b21d7cb927196 100644
--- a/Mathlib/Algebra/Ring/Defs.lean
+++ b/Mathlib/Algebra/Ring/Defs.lean
@@ -529,3 +529,14 @@ scoped instance (priority := 50) [Ring R] [IsMulCommutative R] :
     CommRing R where
 
 end IsMulCommutative
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem SimpleGraph.deleteEdges_inf : ∀ {V : Type u_1} (G H : SimpleGraph V) (s : Set (Sym2 V)), (G ⊓ H).deleteEdges s = G.deleteEdges s ⊓ H.deleteEdges s := by
+  open SimpleGraph Finset Fintype in
+    intro V G H s
+    exact (inf_sdiff)
+
+end
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
index 26d5fefa8013e3..25e73f543f1d79 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
@@ -332,3 +332,15 @@ lemma Scheme.zeroLocus_eq_univ_iff_subset_nilradical {X : Scheme.{u}}
   zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact (U := ⊤) (CompactSpace.isCompact_univ) s
 
 end AlgebraicGeometry
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_biSup : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) {s : Set ι}, s.Finite → (⨆ i ∈ s, I i).ideal = ⨆ i ∈ s, (I i).ideal := by
+  open AlgebraicGeometry AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData CategoryTheory TopologicalSpace in
+    intro X ι I s hs
+    refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_
+    simp only [iSup_insert, e, ideal_sup]
+
+end
diff --git a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean
index d4ecbe96fb3ba6..74cd273c8af1c1 100644
--- a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean
+++ b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean
@@ -486,3 +486,14 @@ end Distortion
 end Box
 
 end BoxIntegral
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem BoxIntegral.Box.lower_sub_upper_splitCenterBox : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι) (i : ι), (I.splitCenterBox s).lower i - (I.splitCenterBox s).upper i = (I.lower i - I.upper i) / 2 := by
+  open BoxIntegral BoxIntegral.Box Set Function Filter Topology Classical in
+    intro ι I s i
+    by_cases i ∈ s <;> simp [field, splitCenterBox, *] <;> ring
+
+end
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Const.lean b/Mathlib/Analysis/Calculus/FDeriv/Const.lean
index a35d81e96fb6e0..3ca53db68bf314 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Const.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Const.lean
@@ -397,3 +397,15 @@ end Support
 
 
 end
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem differentiableWithinAt_Iio_iff_Iic : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [inst_3 : PartialOrder 𝕜], DifferentiableWithinAt 𝕜 f (Set.Iio x) x ↔ DifferentiableWithinAt 𝕜 f (Set.Iic x) x := by
+  open Filter Asymptotics Set in
+    intro 𝕜 inst F inst_1 inst_2 f x inst_3
+    exact (⟨fun h => h.hasDerivWithinAt.Iic_of_Iio.differentiableWithinAt, fun h =>
+      h.hasDerivWithinAt.Iio_of_Iic.differentiableWithinAt⟩)
+
+end
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
index 09797f0b3d9bc8..d2cace594992f3 100644
--- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
@@ -667,3 +667,17 @@ lemma re_inner_starProjection_nonneg [K.HasOrthogonalProjection] (v : E) :
 end
 
 end Submodule
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Submodule.topologicalClosure_eq_bot_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [CompleteSpace E], K.topologicalClosure = ⊥ ↔ Kᗮ = ⊤ := by
+  open Submodule Topology Finsupp RCLike Real Filter in
+    intro 𝕜 E inst inst_1 inst_2 K _
+    rw [← K.orthogonal_orthogonal_eq_closure]
+    constructor <;> intro h
+    · rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.bot_orthogonal_eq_top]
+    · rw [h, Submodule.top_orthogonal_eq_bot]
+
+end
diff --git a/Mathlib/CategoryTheory/Comma/Arrow.lean b/Mathlib/CategoryTheory/Comma/Arrow.lean
index 5ea218a8f31358..0f6e8b48f51642 100644
--- a/Mathlib/CategoryTheory/Comma/Arrow.lean
+++ b/Mathlib/CategoryTheory/Comma/Arrow.lean
@@ -445,3 +445,20 @@ lemma Arrow.functor_ext {F G : C ⥤ D} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
     tauto)
 
 end CategoryTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem CategoryTheory.MorphismProperty.toSet_min : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty C), (W₁ ⊓ W₂).toSet = W₁.toSet ∩ W₂.toSet := by
+  open CategoryTheory CategoryTheory.MorphismProperty Opposite in
+    intro C inst W₁ W₂
+    exact (rfl)
+
+theorem CategoryTheory.MorphismProperty.toSet_iInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} (W : ι → CategoryTheory.MorphismProperty C), (⨅ i, W i).toSet = ⋂ i, (W i).toSet := by
+  open CategoryTheory CategoryTheory.MorphismProperty Opposite in
+    intro C inst ι W
+    ext
+    simp [mem_toSet_iff]
+
+end
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Creates/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Preserves/Creates/Pullbacks.lean
index 5e71b76d7448b6..c4ae431f0d887e 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Creates/Pullbacks.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Creates/Pullbacks.lean
@@ -33,3 +33,14 @@ lemma HasPushout.of_createsColimit (F : C ⥤ D) {X Y S : C} (f : S ⟶ X) (g :
   hasColimit_of_created _ F
 
 end CategoryTheory.Limits
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem CategoryTheory.Precoverage.comap_sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {J K : CategoryTheory.Precoverage D}, CategoryTheory.Precoverage.comap F (J ⊔ K) = CategoryTheory.Precoverage.comap F J ⊔ CategoryTheory.Precoverage.comap F K := by
+  open CategoryTheory CategoryTheory.Precoverage Limits in
+    intro C inst D inst_1 F J K
+    exact (rfl)
+
+end
diff --git a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean
index 6152f84f2e3d72..f86e1d70875419 100644
--- a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean
+++ b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean
@@ -128,3 +128,21 @@ lemma ι_map_top (P : ObjectProperty C) :
     exact ⟨⟨Y, hY⟩, by simp, ⟨e.symm⟩⟩
 
 end CategoryTheory.ObjectProperty
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem CategoryTheory.ObjectProperty.shift_iInf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] {ι : Sort u_4} (P : ι → CategoryTheory.ObjectProperty C) (a : A), (⨅ i, P i).shift a = ⨅ i, (P i).shift a := by
+  open CategoryTheory CategoryTheory.ObjectProperty Category in
+    intro C inst A inst_1 inst_2 ι P a
+    ext
+    simp [prop_shift_iff]
+
+theorem CategoryTheory.ObjectProperty.shift_inf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {A : Type u_2} [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A), (P ⊓ Q).shift a = P.shift a ⊓ Q.shift a := by
+  open CategoryTheory CategoryTheory.ObjectProperty Category in
+    intro C inst P Q A inst_1 inst_2 a
+    ext
+    simp [prop_shift_iff]
+
+end
diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
index 45cd429c4147d0..b187e14a0e581a 100644
--- a/Mathlib/CategoryTheory/Sites/Sieves.lean
+++ b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -1486,3 +1486,16 @@ lemma Presieve.functorPushforward_overForget
   (Sieve.arrows_generate_map_eq_functorPushforward (Over.forget S)).symm
 
 end CategoryTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem CategoryTheory.GrothendieckTopology.eq_bot_of_isEmpty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [IsEmpty C] (J : CategoryTheory.GrothendieckTopology C), J = ⊥ := by
+  open CategoryTheory CategoryTheory.GrothendieckTopology Category in
+    intro C inst _ J
+    rw [eq_bot_iff]
+    intro X
+    exact IsEmpty.elim ‹IsEmpty C› X
+
+end
diff --git a/Mathlib/CategoryTheory/Subfunctor/Basic.lean b/Mathlib/CategoryTheory/Subfunctor/Basic.lean
index 741777bea72237..51a1cc8aced527 100644
--- a/Mathlib/CategoryTheory/Subfunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Subfunctor/Basic.lean
@@ -215,3 +215,14 @@ theorem nat_trans_naturality (f : F' ⟶ G.toFunctor) {U V : C} (i : U ⟶ V)
 end Subfunctor
 
 end CategoryTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem CategoryTheory.Subfunctor.image_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (G : CategoryTheory.Subfunctor F), G.image (CategoryTheory.CategoryStruct.id F) = G := by
+  open CategoryTheory CategoryTheory.Subfunctor in
+    intro C inst F G
+    aesop
+
+end
diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 79ec4ae0442ef6..2a410fb3d8f6f8 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -700,3 +700,16 @@ TODO
 -/
 
 end SimpleGraph
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem SimpleGraph.IsClique.sdiff_of_inf_edge : ∀ {α : Type u_1} {G : SimpleGraph α} {v w : α} {s : Set α}, (G ⊓ SimpleGraph.edge v w).IsClique s → G.IsClique (s \ {v}) := by
+  open SimpleGraph SimpleGraph.IsClique Finset Fintype Function SimpleGraph.Walk in
+    intro α G v w s hc
+    intro _ hx _ hy hxy
+    have := hc hx.1 hy.1 hxy
+    simp_all [inf_adj, edge_adj]
+
+end
diff --git a/Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean b/Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean
index 5e901085b73c54..cd19980b9f960b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean
@@ -248,3 +248,19 @@ lemma DeleteFar.le_card_edgeFinset (h : G.DeleteFar p r) (hp : p ⊥) : r ≤ #G
 end DeleteFar
 
 end SimpleGraph
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem SimpleGraph.Subgraph.comap_equiv_bot : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (f : G →g H), SimpleGraph.Subgraph.comap f ⊥ = ⊥ := by
+  open SimpleGraph SimpleGraph.Subgraph in
+    intro V W G H f
+    ext <;> simp +contextual [f.map_adj]
+
+theorem SimpleGraph.Subgraph.map_iso_bot : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H), SimpleGraph.Subgraph.map e.toHom ⊥ = ⊥ := by
+  open SimpleGraph SimpleGraph.Subgraph in
+    intro V W G H e
+    ext <;> simp [Relation.Map, e.apply_eq_iff_eq_symm_apply, ← e.map_rel_iff]
+
+end
diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean
index 28d51e727e65df..59dfd73a09ceaa 100644
--- a/Mathlib/Computability/PartrecCode.lean
+++ b/Mathlib/Computability/PartrecCode.lean
@@ -1038,3 +1038,19 @@ instance : Countable {f : ℕ → ℕ // Computable f} :=
     (fun _ _ h => Subtype.val_inj.1 (PFun.lift_injective (by simpa using h)))
 
 end Nat.Partrec.Code
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem min_ack_left : ∀ (m₁ m₂ n : ℕ), ack (min m₁ m₂) n = min (ack m₁ n) (ack m₂ n) := by
+  open Nat in
+    intro m₁ m₂ n
+    exact ((ack_mono_left n).map_min)
+
+theorem min_ack_right : ∀ (m n₁ n₂ : ℕ), ack m (min n₁ n₂) = min (ack m n₁) (ack m n₂) := by
+  open Nat in
+    intro m n₁ n₂
+    exact ((ack_mono_right m).map_min)
+
+end
diff --git a/Mathlib/Control/Basic.lean b/Mathlib/Control/Basic.lean
index 64a01e338c85b4..0454b0b391959d 100644
--- a/Mathlib/Control/Basic.lean
+++ b/Mathlib/Control/Basic.lean
@@ -221,3 +221,19 @@ theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative
       rw [@CommApplicative.commutative_prod m h]
       simp [map_seq, map_map]
       rfl
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Filter.comap_sInf : ∀ {α : Type u_1} {β : Type u_2} {s : Set (Filter β)} {m : α → β}, Filter.comap m (sInf s) = ⨅ f ∈ s, Filter.comap m f := by
+  open Filter Function Set Order in
+    intro α β s m
+    simp only [sInf_eq_iInf, comap_iInf]
+
+theorem Filter.codisjoint_comap : ∀ {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β}, Codisjoint g₁ g₂ → Codisjoint (Filter.comap m g₁) (Filter.comap m g₂) := by
+  open Filter Function Set Order in
+    intro α β g₁ g₂ m h
+    simp only [codisjoint_iff, ← comap_sup, h.eq_top, comap_top]
+
+end
diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean
index 218392836d7fad..f9f40930d1818f 100644
--- a/Mathlib/Data/ENNReal/Basic.lean
+++ b/Mathlib/Data/ENNReal/Basic.lean
@@ -769,3 +769,19 @@ meta def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα pα? e :=
   | _, _, _ => throwError "not ENNReal.ofNNReal"
 
 end Mathlib.Meta.Positivity
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ENNReal.toNNReal_mul_bot : ∀ (a : ENNReal), (a * ⊥).toNNReal = 0 := by
+  open ENNReal Set NNReal in
+    intro a
+    simp
+
+theorem ENNReal.toNNReal_bot_mul : ∀ (a : ENNReal), (⊥ * a).toNNReal = 0 := by
+  open ENNReal Set NNReal in
+    intro a
+    simp
+
+end
diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean
index 2aeca7a1b8dabf..80db46a362f0f2 100644
--- a/Mathlib/Data/ENNReal/Real.lean
+++ b/Mathlib/Data/ENNReal/Real.lean
@@ -403,3 +403,39 @@ meta def evalENNRealOfReal : PositivityExt where eval {u α} _zα pα? e :=
     | _ => pure .none
   | _, _, _ => throwError "not ENNReal.ofReal"
 end Mathlib.Meta.Positivity
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ENNReal.preimage_coe_Ioo : ∀ (x y : NNReal), ENNReal.ofNNReal ⁻¹' Set.Ioo x y = Set.Ioo ↑x ↑y := by
+  open ENNReal Set NNReal in
+    intro x y
+    exact (WithTop.preimage_coe_Ioo)
+
+theorem ENNReal.preimage_coe_Icc : ∀ (x y : NNReal), ENNReal.ofNNReal ⁻¹' Set.Icc x y = Set.Icc ↑x ↑y := by
+  open ENNReal Set NNReal in
+    intro x y
+    exact (WithTop.preimage_coe_Icc)
+
+theorem ENNReal.preimage_coe_Ico : ∀ (x y : NNReal), ENNReal.ofNNReal ⁻¹' Set.Ico x y = Set.Ico ↑x ↑y := by
+  open ENNReal Set NNReal in
+    intro x y
+    exact (WithTop.preimage_coe_Ico)
+
+theorem ENNReal.preimage_coe_Iic : ∀ (x : NNReal), ENNReal.ofNNReal ⁻¹' Set.Iic x = Set.Iic ↑x := by
+  open ENNReal Set NNReal in
+    intro x
+    exact (WithTop.preimage_coe_Iic)
+
+theorem ENNReal.preimage_coe_Iio : ∀ (x : NNReal), ENNReal.ofNNReal ⁻¹' Set.Iio x = Set.Iio ↑x := by
+  open ENNReal Set NNReal in
+    intro x
+    exact (WithTop.preimage_coe_Iio)
+
+theorem ENNReal.preimage_coe_Ioc : ∀ (x y : NNReal), ENNReal.ofNNReal ⁻¹' Set.Ioc x y = Set.Ioc ↑x ↑y := by
+  open ENNReal Set NNReal in
+    intro x y
+    exact (WithTop.preimage_coe_Ioc)
+
+end
diff --git a/Mathlib/Data/Finset/Attach.lean b/Mathlib/Data/Finset/Attach.lean
index 2823309d9bee2d..7c12cfd26b27d2 100644
--- a/Mathlib/Data/Finset/Attach.lean
+++ b/Mathlib/Data/Finset/Attach.lean
@@ -58,3 +58,14 @@ theorem mem_attach (s : Finset α) : ∀ x, x ∈ s.attach :=
 theorem coe_attach (s : Finset α) : (s.attach : Set s) = Set.univ := by ext; simp
 
 end Finset
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Finset.erase_inter_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), (s ∩ t).erase a = s.erase a ∩ t.erase a := by
+  open Finset Multiset Subtype Function in
+    intro α inst s t a
+    grind
+
+end
diff --git a/Mathlib/Data/Finset/Defs.lean b/Mathlib/Data/Finset/Defs.lean
index 4421e55d0a0215..3c51929b29efbc 100644
--- a/Mathlib/Data/Finset/Defs.lean
+++ b/Mathlib/Data/Finset/Defs.lean
@@ -380,3 +380,19 @@ theorem pairwise_subtype_iff_pairwise_finset (r : α → α → Prop) :
 end Pairwise
 
 end Finset
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Finset.inter_union_cancel_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∩ t) ∪ s = s := by
+  open Finset Multiset Subtype Function in
+    intro α inst s t
+    grind
+
+theorem Finset.inter_union_cancel_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∩ t) ∪ t = t := by
+  open Finset Multiset Subtype Function in
+    intro α inst s t
+    grind
+
+end
diff --git a/Mathlib/Data/Finset/Lattice/Fold.lean b/Mathlib/Data/Finset/Lattice/Fold.lean
index 6b25b519cddedc..e70eab331f43a8 100644
--- a/Mathlib/Data/Finset/Lattice/Fold.lean
+++ b/Mathlib/Data/Finset/Lattice/Fold.lean
@@ -807,3 +807,19 @@ theorem sup_singleton_eq_self (s : Finset α) : s.sup singleton = s :=
   (s.sup_singleton_apply _).trans image_id
 
 end Finset
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem InfIrred.not_isMax : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfIrred a → ¬IsMax a := by
+  open SupIrred Finset OrderDual in
+    intro α inst a ha
+    exact (ha.1)
+
+theorem InfPrime.not_isMax : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfPrime a → ¬IsMax a := by
+  open SupPrime Finset OrderDual in
+    intro α inst a ha
+    exact (ha.1)
+
+end
diff --git a/Mathlib/Data/Finset/Sym.lean b/Mathlib/Data/Finset/Sym.lean
index 0d798e170847a4..8fd2fef3b2bfdb 100644
--- a/Mathlib/Data/Finset/Sym.lean
+++ b/Mathlib/Data/Finset/Sym.lean
@@ -302,3 +302,14 @@ theorem val_prod_eq_prod_count_pow [CommMonoid α] {n : ℕ} {k : Sym α n}
 end Sym
 
 end Finset
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem LinearMap.BilinForm.separatingRight_of_anisotropic : ∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : _root_.Module R M] {B : LinearMap.BilinForm R M}, (LinearMap.BilinMap.toQuadraticMap B).Anisotropic → LinearMap.SeparatingRight B := by
+  open LinearMap LinearMap.BilinForm QuadraticMap Matrix Module in
+    intro R M inst inst_1 inst_2 B hB
+    exact (fun x hx => hB _ (hx x))
+
+end
diff --git a/Mathlib/Data/Finsupp/Lex.lean b/Mathlib/Data/Finsupp/Lex.lean
index 3aa7a80b5988c4..921e4225190d48 100644
--- a/Mathlib/Data/Finsupp/Lex.lean
+++ b/Mathlib/Data/Finsupp/Lex.lean
@@ -254,3 +254,19 @@ instance Colex.isOrderedCancelAddMonoid
 end OrderedAddMonoid
 
 end Finsupp
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem MonomialOrder.preimage_leadingTerm_insert_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (B : Set (MvPolynomial σ R)), m.leadingTerm ⁻¹' insert 0 B = insert 0 (m.leadingTerm ⁻¹' B) := by
+  open MonomialOrder MvPolynomial in
+    intro σ m R inst B
+    aesop
+
+theorem MonomialOrder.preimage_leadingTerm_sdiff_singleton_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (B : Set (MvPolynomial σ R)), m.leadingTerm ⁻¹' (B \ {0}) = m.leadingTerm ⁻¹' B \ {0} := by
+  open MonomialOrder MvPolynomial in
+    intro σ m R inst B
+    aesop
+
+end
diff --git a/Mathlib/Data/NNReal/Basic.lean b/Mathlib/Data/NNReal/Basic.lean
index 06bdfc1b60931d..2b1a77a21a1541 100644
--- a/Mathlib/Data/NNReal/Basic.lean
+++ b/Mathlib/Data/NNReal/Basic.lean
@@ -280,3 +280,19 @@ theorem image_coe_uIoo (x y : ℝ≥0) : toReal '' uIoo x y = uIoo ↑x ↑y :=
   image_subtype_val_uIoo (s := Ici 0) ..
 
 end NNReal
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ENNReal.iInf_pow_of_ne_zero : ∀ {ι : Sort u_1} {n : ℕ}, n ≠ 0 → ∀ (f : ι → ENNReal), (⨅ i, f i) ^ n = ⨅ i, f i ^ n := by
+  open ENNReal Filter Metric Set TopologicalSpace Topology Finset in
+    intro ι n hn f
+    exact ((powOrderIso n hn).map_iInf _)
+
+theorem ENNReal.iInf₂_pow_of_ne_zero : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal) {n : ℕ}, n ≠ 0 → (⨅ i, ⨅ j, f i j) ^ n = ⨅ i, ⨅ j, f i j ^ n := by
+  open ENNReal Filter Metric Set TopologicalSpace Topology Finset in
+    intro ι κ f n hn
+    exact ((powOrderIso n hn).map_iInf₂ f)
+
+end
diff --git a/Mathlib/Data/Nat/Cast/WithTop.lean b/Mathlib/Data/Nat/Cast/WithTop.lean
index 99b71bb61593b9..403273c9456352 100644
--- a/Mathlib/Data/Nat/Cast/WithTop.lean
+++ b/Mathlib/Data/Nat/Cast/WithTop.lean
@@ -26,3 +26,36 @@ theorem Nat.cast_withTop (n : ℕ) : Nat.cast n = WithTop.some n :=
 
 theorem Nat.cast_withBot (n : ℕ) : Nat.cast n = WithBot.some n :=
   rfl
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Nat.WithTop.add_eq_one_iff : ∀ {n m : WithTop ℕ}, n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by
+  open Nat Nat.WithBot in
+    intro n m
+    cases n
+    · simp
+    cases m
+    · simp [WithTop.add_top]
+    simp [← WithTop.coe_add, Nat.add_eq_one_iff]
+
+theorem Nat.WithTop.add_eq_two_iff : ∀ {n m : WithTop ℕ}, n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 := by
+  open Nat Nat.WithBot in
+    intro n m
+    cases n
+    · simp [WithTop.top_add]
+    cases m
+    · simp [WithTop.add_top]
+    simp [← WithTop.coe_add, Nat.add_eq_two_iff]
+
+theorem Nat.WithTop.add_eq_three_iff : ∀ {n m : WithTop ℕ}, n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0 := by
+  open Nat Nat.WithBot in
+    intro n m
+    cases n
+    · simp [WithTop.top_add]
+    cases m
+    · simp [WithTop.add_top]
+    simp [← WithTop.coe_add, Nat.add_eq_three_iff]
+
+end
diff --git a/Mathlib/Data/Rel.lean b/Mathlib/Data/Rel.lean
index 010eadd374f95a..6e660dfa675f77 100644
--- a/Mathlib/Data/Rel.lean
+++ b/Mathlib/Data/Rel.lean
@@ -607,3 +607,14 @@ end Set
 
 Consider using `SetRel` instead if you want extra API for relations. -/
 abbrev Rel (α β : Type*) : Type _ := α → β → Prop
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem SetRel.gc_rightDual_leftDual : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β), GaloisConnection (⇑OrderDual.toDual ∘ R.rightDual) (R.leftDual ∘ ⇑OrderDual.ofDual) := by
+  open SetRel OrderDual in
+    intro α β R
+    exact (fun _ _ ↦ ⟨fun h _ ha _ hb ↦ h (by simpa) ha, fun h _ hb _ ha ↦ h (by simpa) hb⟩)
+
+end
diff --git a/Mathlib/Data/Rel/Cover.lean b/Mathlib/Data/Rel/Cover.lean
index c2dd4502b33f27..74c3df8cbad2ae 100644
--- a/Mathlib/Data/Rel/Cover.lean
+++ b/Mathlib/Data/Rel/Cover.lean
@@ -83,3 +83,19 @@ lemma IsCover.of_maximal_isSeparated [U.IsRefl] [U.IsSymm]
 @[deprecated (since := "2025-12-19")] alias isCover_relId := isCover_id
 
 end SetRel
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem UniformSpace.ball_union : ∀ {β : Type ub} (x : β) (V W : Set (β × β)), UniformSpace.ball x (V ∪ W) = UniformSpace.ball x V ∪ UniformSpace.ball x W := by
+  open UniformSpace Set Filter Topology in
+    intro β x V W
+    exact (preimage_union)
+
+theorem UniformSpace.ball_iUnion : ∀ {β : Type ub} {ι : Sort u_1} {x : β} {V : ι → Set (β × β)}, UniformSpace.ball x (⋃ i, V i) = ⋃ i, UniformSpace.ball x (V i) := by
+  open UniformSpace Set Filter Topology in
+    intro β ι x V
+    exact (preimage_iUnion)
+
+end
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index f351d53127ac98..5394d90f462de2 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -1088,3 +1088,79 @@ protected lemma setSubtypeComm_symm_apply (p : α → Prop) (s : {s // ∀ a ∈
   rfl
 
 end Equiv
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.codisjoint_empty : ∀ {α : Type u} {s : Set α}, Codisjoint s ∅ ↔ s = Set.univ := by
+  open Set Function in
+    intro α s
+    exact (codisjoint_bot)
+
+theorem Set.empty_codisjoint : ∀ {α : Type u} {s : Set α}, Codisjoint ∅ s ↔ s = Set.univ := by
+  open Set Function in
+    intro α s
+    exact (bot_codisjoint)
+
+theorem Codisjoint.union_left : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Codisjoint s t → Codisjoint (s ∪ u) t := by
+  open Disjoint Function in
+    intro α s t u h
+    exact (h.sup_left _)
+
+theorem Set.codisjoint_iff_union_eq_univ : ∀ {α : Type u} {s t : Set α}, Codisjoint s t ↔ s ∪ t = Set.univ := by
+  open Set Function in
+    intro α s t
+    exact (codisjoint_iff)
+
+theorem Codisjoint.union_left' : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Codisjoint s t → Codisjoint (u ∪ s) t := by
+  open Disjoint Function in
+    intro α s t u h
+    exact (h.sup_left' _)
+
+theorem Codisjoint.union_right : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Codisjoint s t → Codisjoint s (t ∪ u) := by
+  open Disjoint Function in
+    intro α s t u h
+    exact (h.sup_right _)
+
+theorem Codisjoint.union_right' : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Codisjoint s t → Codisjoint s (u ∪ t) := by
+  open Disjoint Function in
+    intro α s t u h
+    exact (h.sup_right' _)
+
+theorem Codisjoint.inter_left : ∀ {α : Type u_1} {s t u : Set α}, Codisjoint s u → Codisjoint t u → Codisjoint (s ∩ t) u := by
+  open Disjoint Function in
+    intro α s t u hs ht
+    exact (hs.inf_left ht)
+
+theorem Codisjoint.union_eq : ∀ {α : Type u} {s t : Set α}, Codisjoint s t → s ∪ t = Set.univ := by
+  open Disjoint Function in
+    intro α s t
+    exact (Codisjoint.eq_top)
+
+theorem Codisjoint.inter_right : ∀ {α : Type u_1} {s t u : Set α}, Codisjoint s t → Codisjoint s u → Codisjoint s (t ∩ u) := by
+  open Disjoint Function in
+    intro α s t u ht hu
+    exact (ht.inf_right hu)
+
+theorem Set.codisjoint_inter_left : ∀ {α : Type u} {s t u : Set α}, Codisjoint (s ∩ t) u ↔ Codisjoint s u ∧ Codisjoint t u := by
+  open Set Function in
+    intro α s t u
+    exact (codisjoint_inf_left)
+
+theorem Set.univ_codisjoint : ∀ {α : Type u} (s : Set α), Codisjoint Set.univ s := by
+  open Set Function in
+    intro α s
+    exact (codisjoint_top_left)
+
+theorem Set.codisjoint_univ : ∀ {α : Type u} (s : Set α), Codisjoint s Set.univ := by
+  open Set Function in
+    intro α s
+    exact (codisjoint_top_right)
+
+theorem Set.codisjoint_inter_right : ∀ {α : Type u} {s t u : Set α}, Codisjoint s (t ∩ u) ↔ Codisjoint s t ∧ Codisjoint s u := by
+  open Set Function in
+    intro α s t u
+    exact (codisjoint_inf_right)
+
+end
diff --git a/Mathlib/Data/Set/Constructions.lean b/Mathlib/Data/Set/Constructions.lean
index 1fde47d3e54a09..6b338a93c1479b 100644
--- a/Mathlib/Data/Set/Constructions.lean
+++ b/Mathlib/Data/Set/Constructions.lean
@@ -95,3 +95,15 @@ the empty finset, but `s` is a family of sets, not finsets). -/
 theorem Set.biUnion_empty_finset {ι X : Type*} {s : ι → Set X} :
     ⋃ i ∈ (∅ : Finset ι), s i = ∅ := by
   simp
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem TopologicalSpace.IsTopologicalBasis.insert_univ : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)}, TopologicalSpace.IsTopologicalBasis s → TopologicalSpace.IsTopologicalBasis (insert Set.univ s) := by
+  open TopologicalSpace TopologicalSpace.IsTopologicalBasis Set Filter Function Topology in
+    intro α t s h
+    exact (h.of_isOpen_of_subset (by rintro _ (rfl | hu); exacts [isOpen_univ, h.isOpen hu])
+      (subset_insert ..))
+
+end
diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
index 409e09c29778d0..82599c73d1bce3 100644
--- a/Mathlib/Data/Set/Function.lean
+++ b/Mathlib/Data/Set/Function.lean
@@ -1366,3 +1366,19 @@ lemma bijOn_swap (ha : a ∈ s) (hb : b ∈ s) : BijOn (swap a b) s s :=
     simp [*, swap_apply_of_ne_of_ne]
 
 end Equiv
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Pairwise.codisjoint_extend_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PartialOrder γ] [inst_1 : OrderTop γ] {e : α → β} {f : α → γ}, Pairwise (Function.onFun Codisjoint f) → Function.FactorsThrough f e → Pairwise (Function.onFun Codisjoint (Function.extend e f ⊤)) := by
+  open Pairwise Function Order Set in
+    intro α β γ inst inst_1 e f hf he
+    intro b₁ b₂ hne
+    rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁
+    · rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
+      · simpa only [onFun, he.extend_apply] using! hf (ne_of_apply_ne e hne)
+      · simpa only [onFun, extend_apply' _ _ _ hb₂] using! codisjoint_top_right
+    · simpa only [onFun, extend_apply' _ _ _ hb₁] using! codisjoint_top_left
+
+end
diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean
index cfd6250f5185c2..0872b192a77f2b 100644
--- a/Mathlib/Data/Set/Image.lean
+++ b/Mathlib/Data/Set/Image.lean
@@ -1412,3 +1412,29 @@ lemma sigma_mk_preimage_image_eq_self : Sigma.mk i ⁻¹' Sigma.mk i '' s = s :=
   simp [image]
 
 end Sigma
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.inter_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t : (i : ι) → Set (α i)}, (s₁ ∩ s₂).sigma t = s₁.sigma t ∩ s₂.sigma t := by
+  open Set in
+    intro ι α s₁ s₂ t
+    grind
+
+theorem Nat.zero_inter_range_succ : {0} ∩ Set.range Nat.succ = ∅ := by
+  open Nat Set in
+    ext n
+    cases n <;> simp
+
+theorem isOpen_iUnion₂ : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsOpen (f i j)) → IsOpen (⋃ i, ⋃ j, f i j) := by
+  open Filter Set TopologicalSpace Topology in
+    intro ι κ α inst _ f hf
+    exact (isOpen_iUnion fun _ ↦ isOpen_iUnion <| hf _)
+
+theorem isClosed_iInter₂ : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsClosed (f i j)) → IsClosed (⋂ i, ⋂ j, f i j) := by
+  open Filter Set TopologicalSpace Topology in
+    intro ι κ α inst _ f hf
+    exact (isClosed_iInter fun _ ↦ isClosed_iInter <| hf _)
+
+end
diff --git a/Mathlib/Data/Set/Insert.lean b/Mathlib/Data/Set/Insert.lean
index 74410133de73aa..8f69996f0cc337 100644
--- a/Mathlib/Data/Set/Insert.lean
+++ b/Mathlib/Data/Set/Insert.lean
@@ -414,3 +414,17 @@ open Set
 
 @[simp] theorem Prop.compl_singleton (p : Prop) : ({p}ᶜ : Set Prop) = {¬p} :=
   ext fun q ↦ by simpa [@Iff.comm q] using not_iff
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.ite_union_union : ∀ {α : Type u_1} (t s₁ s₂ s₁' s₂' : Set α), t.ite (s₁ ∪ s₂) (s₁' ∪ s₂') = t.ite s₁ s₁' ∪ t.ite s₂ s₂' := by
+  open Set Function in
+    intro α t s₁ s₂ s₁' s₂'
+    ext x
+    unfold Set.ite
+    push _ ∈ _
+    tauto
+
+end
diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean
index f83b4087cb7c9f..e3ac674399fb56 100644
--- a/Mathlib/Data/Set/Lattice.lean
+++ b/Mathlib/Data/Set/Lattice.lean
@@ -1474,3 +1474,24 @@ lemma forall_sUnion {S : Set (Set α)} {p : α → Prop} :
 lemma exists_sUnion {S : Set (Set α)} {p : α → Prop} :
     (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x := by
   simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.iInter_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γ → Set α), ⋂ x, f x = ⋂ i, ⋂ j, f (i, j) := by
+  open Set Function in
+    intro α β γ f
+    exact (iInf_prod)
+
+theorem Set.biInter_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set β) (t : Set γ) (f : β × γ → Set α), ⋂ x ∈ s ×ˢ t, f x = ⋂ i ∈ s, ⋂ j ∈ t, f (i, j) := by
+  open Set Function in
+    intro α β γ s t f
+    exact (biInf_prod)
+
+theorem Pi.eq_top_iff : ∀ {ι : Type u_4} {π : ι → Type u} [inst : (i : ι) → Top (π i)] {f : (i : ι) → π i}, f = ⊤ ↔ ∀ (i : ι), f i = ⊤ := by
+  open Pi Order Classical in
+    intro ι π inst f
+    exact (funext_iff)
+
+end
diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 14341437454387..ec29537a9253ea 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -1025,3 +1025,14 @@ lemma exists_eq_mgraphOn_univ {s : Set (β × γ)}
     fun a b h ↦ congr_arg (Prod.snd ∘ (Subtype.val : s → β × γ)) (hs₁.injective h)
 
 end Set
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem FirstOrder.Language.Formula.equivSentence_sup : ∀ {L : FirstOrder.Language} {α : Type u'} (φ ψ : L.Formula α), FirstOrder.Language.Formula.equivSentence (φ ⊔ ψ) = FirstOrder.Language.Formula.equivSentence φ ⊔ FirstOrder.Language.Formula.equivSentence ψ := by
+  open FirstOrder FirstOrder.Language FirstOrder.Language.Formula Structure Fin Finset Term BoundedFormula in
+    intro L α φ ψ
+    exact (rfl)
+
+end
diff --git a/Mathlib/FieldTheory/Finiteness.lean b/Mathlib/FieldTheory/Finiteness.lean
index 6b9a563f1beab9..736fb44e64d5e0 100644
--- a/Mathlib/FieldTheory/Finiteness.lean
+++ b/Mathlib/FieldTheory/Finiteness.lean
@@ -104,3 +104,16 @@ theorem iff_fg : IsNoetherian K V ↔ Module.Finite K V :=
   ⟨fun _ ↦ IsNoetherian.finite _ _, fun _ ↦ isNoetherian_of_isNoetherianRing_of_finite _ _⟩
 
 end IsNoetherian
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem IntermediateField.adjoin_eq_bot_iff_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E}, (∀ x ∈ S, IsAlgebraic F x) → (IntermediateField.adjoin F S = ⊥ ↔ Algebra.adjoin F S = ⊥) := by
+  open IntermediateField Module Polynomial Algebra in
+    intro F inst E inst_1 inst_2 S hS
+    rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic hS,
+    ← IntermediateField.toSubalgebra_inj,
+    IntermediateField.bot_toSubalgebra]
+
+end
diff --git a/Mathlib/Geometry/Convex/Cone/Pointed.lean b/Mathlib/Geometry/Convex/Cone/Pointed.lean
index f2370255b2ba01..2f246bc9536031 100644
--- a/Mathlib/Geometry/Convex/Cone/Pointed.lean
+++ b/Mathlib/Geometry/Convex/Cone/Pointed.lean
@@ -370,3 +370,14 @@ lemma salient_iff_inter_neg_eq_singleton (C : PointedCone R E) :
 end Salient
 
 end PointedCone
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem PointedCone.dual_inf : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2} [inst_3 : AddCommMonoid M] [inst_4 : _root_.Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : _root_.Module R N] {p : M →ₗ[R] N →ₗ[R] R} (C D : PointedCone R M), PointedCone.dual p ↑(C ⊓ D) = PointedCone.dual p (↑C ∩ ↑D) := by
+  open PointedCone Function LinearMap Pointwise Set in
+    intro R inst inst_1 inst_2 M inst_3 inst_4 N inst_5 inst_6 p C D
+    simp [← dual_hull]
+
+end
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
index c4a9815c985c17..9fc864b4987d83 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
@@ -923,3 +923,14 @@ theorem contMDiffOn_of_locally_contMDiffOn
 theorem contMDiff_of_locally_contMDiffOn (h : ∀ x, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f u) :
     ContMDiff I I' n f :=
   (contDiffWithinAt_localInvariantProp n).liftProp_of_locally_liftPropOn h
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ContMDiff.piecewise_Ici : ∀ {n : WithBot ℕ∞} {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_12} [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_13} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {f g : ℝ → M} {s : ℝ}, ContMDiff (modelWithCornersSelf ℝ ℝ) I n f → ContMDiff (modelWithCornersSelf ℝ ℝ) I n g → f =ᶠ[nhds s] g → ContMDiff (modelWithCornersSelf ℝ ℝ) I n ((Set.Ici s).piecewise f g) := by
+  open ContMDiff Filter Function Set Topology in
+    intro n E inst inst_1 H inst_2 I M inst_3 inst_4 f g s hf hg hfg
+    exact (hf.piecewise hg (by simpa using hfg))
+
+end
diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean
index b3c6fd0d028d22..ba4b9fa82921e8 100644
--- a/Mathlib/GroupTheory/Index.lean
+++ b/Mathlib/GroupTheory/Index.lean
@@ -909,3 +909,19 @@ lemma index_smul (a : G) (S : AddSubgroup A) : (a • S).index = S.index :=
   index_map_of_bijective (MulAction.bijective _) _
 
 end AddSubgroup
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Subgroup.IsComplement'.codisjoint : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → Codisjoint H K := by
+  open Subgroup Subgroup.IsComplement' Function Set MulAction in
+    intro G inst H K h
+    exact (h.isCompl.codisjoint)
+
+theorem Subgroup.IsComplement'.inf_eq_bot : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → H ⊓ K = ⊥ := by
+  open Subgroup Subgroup.IsComplement' Function Set MulAction in
+    intro G inst H K h
+    exact (h.isCompl.inf_eq_bot)
+
+end
diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean
index fde00ab331897f..f124d9eed3e598 100644
--- a/Mathlib/LinearAlgebra/Alternating/Basic.lean
+++ b/Mathlib/LinearAlgebra/Alternating/Basic.lean
@@ -932,3 +932,19 @@ def AlternatingMap.constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M''
   map_smul' _ _ := rfl
   invFun f := f 0
   right_inv f := ext fun _ => AlternatingMap.congr_arg f <| Subsingleton.elim _ _
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem AlternatingMap.curryRight_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : _root_.Module R M] [inst_4 : _root_.Module R N] {n : ℕ} (f g : M [⋀^Fin n.succ]→ₗ[R] N), (f + g).curryRight = f.curryRight + g.curryRight := by
+  open AlternatingMap in
+    intro R M N inst inst_1 inst_2 inst_3 inst_4 n f g
+    exact (rfl)
+
+theorem AlternatingMap.curryRight_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : _root_.Module R M] [inst_4 : _root_.Module R N] {n : ℕ} (r : R) (f : M [⋀^Fin n.succ]→ₗ[R] N), (r • f).curryRight = r • f.curryRight := by
+  open AlternatingMap in
+    intro R M N inst inst_1 inst_2 inst_3 inst_4 n r f
+    exact (rfl)
+
+end
diff --git a/Mathlib/LinearAlgebra/Alternating/Curry.lean b/Mathlib/LinearAlgebra/Alternating/Curry.lean
index 6ea44434cd4d94..b16f52c77de947 100644
--- a/Mathlib/LinearAlgebra/Alternating/Curry.lean
+++ b/Mathlib/LinearAlgebra/Alternating/Curry.lean
@@ -85,3 +85,24 @@ theorem curryLeft_compLinearMap (g : M₂ →ₗ[R] M) (f : M [⋀^Fin n.succ]
   ext fun v ↦ congr_arg f <| funext fun i ↦ by cases i using Fin.cases <;> simp
 
 end AlternatingMap
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ContinuousAlternatingMap.curryRight_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} (f g : E [⋀^Fin (n + 1)]→L[𝕜] F), (f + g).curryRight = f.curryRight + g.curryRight := by
+  open ContinuousAlternatingMap in
+    intro 𝕜 E F inst inst_1 inst_2 inst_3 inst_4 n f g
+    exact (rfl)
+
+theorem ContinuousAlternatingMap.curryRight_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} (r : 𝕜) (f : E [⋀^Fin (n + 1)]→L[𝕜] F), (r • f).curryRight = r • f.curryRight := by
+  open ContinuousAlternatingMap in
+    intro 𝕜 E F inst inst_1 inst_2 inst_3 inst_4 n r f
+    exact (rfl)
+
+theorem ContinuousAlternatingMap.norm_curryRight : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F), ‖f.curryRight‖ = ‖f‖ := by
+  open ContinuousAlternatingMap in
+    intro 𝕜 E F inst inst_1 inst_2 inst_3 inst_4 n f
+    exact (f.toContinuousMultilinearMap.curryRight_norm)
+
+end
diff --git a/Mathlib/LinearAlgebra/Basis/Basic.lean b/Mathlib/LinearAlgebra/Basis/Basic.lean
index 9bf07fec3e2dbe..6d35f8c44e1d50 100644
--- a/Mathlib/LinearAlgebra/Basis/Basic.lean
+++ b/Mathlib/LinearAlgebra/Basis/Basic.lean
@@ -332,3 +332,19 @@ lemma card_fintype [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b :
       _ = card R ^ card ι := by simp
 
 end Module
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem LinearMap.IsRefl.ker_eq_top_iff_ker_flip_eq_top : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : _root_.Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : _root_.Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → (B.ker = ⊤ ↔ B.flip.ker = ⊤) := by
+  open LinearMap LinearMap.IsRefl Module in
+    intro R R₁ M M₁ inst inst_1 inst_2 inst_3 inst_4 inst_5 I₁ I₂ B H
+    rwa [ker_flip]
+
+theorem LinearMap.IsRefl.ker_flip_eq_top : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : _root_.Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : _root_.Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → B.ker = ⊤ → B.flip.ker = ⊤ := by
+  open LinearMap LinearMap.IsRefl Module in
+    intro R R₁ M M₁ inst inst_1 inst_2 inst_3 inst_4 inst_5 I₁ I₂ B H h
+    rwa [H.ker_flip]
+
+end
diff --git a/Mathlib/LinearAlgebra/Dual/Lemmas.lean b/Mathlib/LinearAlgebra/Dual/Lemmas.lean
index 5e885ee7021604..8e80b333a7792e 100644
--- a/Mathlib/LinearAlgebra/Dual/Lemmas.lean
+++ b/Mathlib/LinearAlgebra/Dual/Lemmas.lean
@@ -1193,3 +1193,19 @@ noncomputable def dualDistribEquiv : Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (
   dualDistribEquivOfBasis (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R N)
 
 end TensorProduct
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem LinearMap.IsPerfectCompl.left_bot_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : _root_.Module R M] [inst_3 : AddCommGroup N] [inst_4 : _root_.Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {V : Submodule R N}, p.IsPerfectCompl ⊥ V ↔ V = ⊥ := by
+  open LinearMap LinearMap.IsPerfectCompl Function Module in
+    intro R M N inst inst_1 inst_2 inst_3 inst_4 p inst_5 V
+    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+    · exact eq_bot_of_isCompl_top <| by simpa using h.isCompl_right
+    · rw [h]
+      exact
+        { isCompl_left := by simpa using isCompl_bot_top
+          isCompl_right := by simpa using isCompl_bot_top }
+
+end
diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index 33da624467b19e..5fea2f47e1ab70 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -621,3 +621,15 @@ def encodableQuotient : Encodable (Quotient s) :=
     rintro ⟨l⟩; dsimp; rw [encodek]; exact congr_arg some ⟦l⟧.rep_spec⟩
 
 end Quotient
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Encodable.iInf_decode₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable β] [inst_1 : CompleteLattice α] (f : β → α), ⨅ i, ⨅ b ∈ Encodable.decode₂ β i, f b = ⨅ b, f b := by
+  open Encodable Set in
+    intro α β inst inst_1 f
+    rw [iInf_comm]
+    simp only [mem_decode₂, iInf_iInf_eq_right]
+
+end
diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean
index b430f0e1e4d1cf..feeafbf5236f27 100644
--- a/Mathlib/Logic/Equiv/Set.lean
+++ b/Mathlib/Logic/Equiv/Set.lean
@@ -624,3 +624,19 @@ theorem Equiv.swap_bijOn_exchange (ha : a ∈ s) (hb : b ∉ s) :
   grind [Equiv.bijOn]
 
 end Swap
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem iInf_codisjoint_iff : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] {a : α} {f : ι → α}, Codisjoint (⨅ i, f i) a ↔ ∀ (i : ι), Codisjoint (f i) a := by
+  open Function Set Order in
+    intro α ι inst a f
+    simp only [codisjoint_iff, iInf_sup_eq, iInf_eq_top]
+
+theorem sInf_codisjoint_iff : ∀ {α : Type u} [inst : Order.Coframe α] {a : α} {s : Set α}, Codisjoint (sInf s) a ↔ ∀ b ∈ s, Codisjoint b a := by
+  open Function Set Order in
+    intro α inst a s
+    simp only [codisjoint_iff, sInf_sup_eq, iInf_eq_top]
+
+end
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index d2d3f67f4f10da..81dee6084ef0ce 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -1243,3 +1243,13 @@ theorem map_comp_map {α β γ : ι → Type*} (f : ∀ i, α i → β i) (g : 
   rfl
 
 end Pi
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem not_isRight_and_isLeft : ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬(x.isRight = true ∧ x.isLeft = true) := by
+  intro α β x
+  simp
+
+end
diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean
index 0c3098fed6abe8..b2f817dc2b0161 100644
--- a/Mathlib/Logic/Function/Defs.lean
+++ b/Mathlib/Logic/Function/Defs.lean
@@ -205,3 +205,14 @@ protected def map (f : ∀ i, α i → β i) : (∀ i, α i) → (∀ i, β i) :
 lemma map_apply (f : ∀ i, α i → β i) (a : ∀ i, α i) (i : ι) : Pi.map f a i = f i (a i) := rfl
 
 end Pi
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Relator.RightUnique.flip : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Relator.RightUnique r → Relator.LeftUnique (flip r) := by
+  open Relator Relator.LeftUnique in
+    intro α β r h
+    exact (fun _ _ _ h₁ h₂ => h h₁ h₂)
+
+end
diff --git a/Mathlib/Logic/Pairwise.lean b/Mathlib/Logic/Pairwise.lean
index fca700806c5b0a..a5b637f8ef2bd8 100644
--- a/Mathlib/Logic/Pairwise.lean
+++ b/Mathlib/Logic/Pairwise.lean
@@ -112,3 +112,15 @@ end Set
 theorem Pairwise.set_pairwise (h : Pairwise r) (s : Set α) : s.Pairwise r := fun _ _ _ _ w => h w
 
 end Pairwise
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.iInter_sumElim : ∀ {α : Type u_1} {ι : Type u_12} {σ : Type u_13} (s : ι → Set α) (t : σ → Set α), ⋂ x, Sum.elim s t x = (⋂ x, s x) ∩ ⋂ x, t x := by
+  open Set Function in
+    intro α ι σ s t
+    ext
+    simp
+
+end
diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
index 20c22dc9b98969..5c0465ee8bc815 100644
--- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
+++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
@@ -1118,3 +1118,14 @@ theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type*} {mα
   rw [A, B, C, add_assoc]
 
 end ENNReal
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem StieltjesFunction.id_rightLim : ∀ (x : ℝ), Function.rightLim (↑StieltjesFunction.id) x = x := by
+  open StieltjesFunction Set Filter Function ENNReal NNReal Topology MeasureTheory in
+    intro x
+    exact (continuousWithinAt_id.rightLim_eq)
+
+end
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean b/Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
index e199fd48bbffd0..15eda4badb0523 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
@@ -119,3 +119,14 @@ theorem Measurable.eventuallyMeasurable_of_eventuallyEq
   hf.eventuallyMeasurable.congr hgf
 
 end EventuallyMeasurable
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem MeasureTheory.NullMeasurableSet.inter_null : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasureTheory.NullMeasurableSet s μ → μ t = 0 → MeasureTheory.NullMeasurableSet (s ∩ t) μ := by
+  open MeasureTheory MeasureTheory.NullMeasurableSet Filter Set Encodable in
+    intro α m0 μ s t hs ht
+    exact (hs.inter (of_null ht))
+
+end
diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean
index 3905185f5bf840..dc60a147528413 100644
--- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean
+++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean
@@ -458,3 +458,14 @@ instance (μ : Measure α) (f : α → β) [SFinite μ] : SFinite (μ.map f) :=
 
 end Measure
 end MeasureTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Finset.measurable_inf' : ∀ {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [inst : MeasurableSpace δ] [inst_1 : SemilatticeInf α] [MeasurableInf₂ α] {ι : Type u_4} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}, (∀ n ∈ s, Measurable (f n)) → Measurable (s.inf' hs f) := by
+  open Finset MeasureTheory in
+    intro α m δ inst inst_1 _ ι s hs f hf
+    exact (Finset.inf'_induction hs _ (fun _f hf _g hg => hf.inf hg) fun n hn => hf n hn)
+
+end
diff --git a/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
index 810ec64d0ba490..95d5c11de85a0f 100644
--- a/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
+++ b/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
@@ -1084,3 +1084,14 @@ lemma add_sub_of_mutuallySingular {ξ : Measure α} (h : μ ⟂ₘ ξ) : μ + (
 end Measure
 
 end MeasureTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem MeasureTheory.Measure.compProd_apply_empty : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsMarkovKernel κ], (μ.compProd κ) ∅ = μ ∅ := by
+  open MeasureTheory MeasureTheory.Measure ProbabilityTheory Set in
+    intro α β mα mβ μ κ _ _
+    simp [compProd]
+
+end
diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean
index 2f3c5ca3e1db60..0e8ee367ba5e31 100644
--- a/Mathlib/MeasureTheory/Measure/Prod.lean
+++ b/Mathlib/MeasureTheory/Measure/Prod.lean
@@ -1246,3 +1246,15 @@ theorem _root_.MeasureTheory.volume_preserving_prodAssoc {α₁ β₁ γ₁ : Ty
 end MeasurePreserving
 
 end MeasureTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ProbabilityTheory.Kernel.parallelComp_apply_empty : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel γ δ} {x : α × γ} [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η], ((κ.parallelComp η) x) ∅ = (κ x.1) ∅ * (η x.2) ∅ := by
+  open ProbabilityTheory ProbabilityTheory.Kernel MeasureTheory Classical in
+    intro α β γ δ mα mβ mγ mδ κ η x _ _
+    rw [parallelComp_apply, Measure.prod_apply .empty, mul_comm]
+    simp
+
+end
diff --git a/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean b/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
index 42836f08747de6..a86dd58b3b96db 100644
--- a/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
+++ b/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
@@ -465,3 +465,14 @@ end sInfGen
 end OuterMeasure
 
 end MeasureTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem MeasureTheory.OuterMeasure.isCaratheodory_univ : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α), m.IsCaratheodory Set.univ := by
+  open MeasureTheory MeasureTheory.OuterMeasure Set Function Filter in
+    intro α m
+    simp [IsCaratheodory, sdiff_univ]
+
+end
diff --git a/Mathlib/MeasureTheory/OuterMeasure/Operations.lean b/Mathlib/MeasureTheory/OuterMeasure/Operations.lean
index e928f1711c0649..64da572f13fea4 100644
--- a/Mathlib/MeasureTheory/OuterMeasure/Operations.lean
+++ b/Mathlib/MeasureTheory/OuterMeasure/Operations.lean
@@ -361,3 +361,16 @@ end Basic
 end OuterMeasure
 
 end MeasureTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem MeasureTheory.OuterMeasure.restrict_biSup : ∀ {α : Type u_1} {ι : Type u_2} {I : Set ι}, I.Nonempty → ∀ (s : Set α) (m : ι → MeasureTheory.OuterMeasure α), (MeasureTheory.OuterMeasure.restrict s) (⨆ i ∈ I, m i) = ⨆ i ∈ I, (MeasureTheory.OuterMeasure.restrict s) (m i) := by
+  open MeasureTheory MeasureTheory.OuterMeasure Set Function Filter in
+    intro α ι I hI s m
+    haveI := hI.to_subtype
+    rw [← iSup_subtype'', ← iSup_subtype'']
+    exact restrict_iSup _ _
+
+end
diff --git a/Mathlib/Order/Atoms.lean b/Mathlib/Order/Atoms.lean
index 626c404ca544a2..5d463b92d1e732 100644
--- a/Mathlib/Order/Atoms.lean
+++ b/Mathlib/Order/Atoms.lean
@@ -1313,3 +1313,14 @@ instance : IsAtomistic (Set α) := inferInstance
 instance : IsCoatomistic (Set α) := inferInstance
 
 end Set
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem AffineSubspace.vectorSpan_eq_bot_of_affineSpan_eq_bot : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : _root_.Module k V] [S : AddTorsor V P] {s : Set P}, affineSpan k s = ⊥ → vectorSpan k s = ⊥ := by
+  open AffineSubspace Affine Set in
+    intro k V P inst inst_1 inst_2 S s h
+    rw [← direction_affineSpan, h, direction_bot]
+
+end
diff --git a/Mathlib/Order/BooleanSubalgebra.lean b/Mathlib/Order/BooleanSubalgebra.lean
index 007c6eb3cc2f3f..e17aafdcf1605e 100644
--- a/Mathlib/Order/BooleanSubalgebra.lean
+++ b/Mathlib/Order/BooleanSubalgebra.lean
@@ -435,3 +435,14 @@ lemma biInf_mem {ι : Type*} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf :
 
 end CompleteBooleanAlgebra
 end BooleanSubalgebra
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Topology.IsLocallyConstructible.biInter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {f : ι → Set X} {s : Set ι}, s.Finite → (∀ i ∈ s, Topology.IsLocallyConstructible (f i)) → Topology.IsLocallyConstructible (⋂ i ∈ s, f i) := by
+  open Topology Topology.IsLocallyConstructible Set TopologicalSpace in
+    intro X inst ι f s hs hf
+    exact (InfClosed.biInf_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.inter) hs .univ hf)
+
+end
diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean
index 12fbb67bd29471..3e935290aa55b3 100644
--- a/Mathlib/Order/Bounds/Basic.lean
+++ b/Mathlib/Order/Bounds/Basic.lean
@@ -911,3 +911,14 @@ def Lattice.ofIsLUBofIsGLB [PartialOrder α] (sup inf : α → α → α)
     Lattice α where
   __ := SemilatticeSup.ofIsLUB sup isLUB_pair
   __ := SemilatticeInf.ofIsGLB inf isGLB_pair
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.Ici.eq_bot_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {x : ↑(Set.Ici a)}, x = ⊥ ↔ ↑x = a := by
+  open Set Set.Iic in
+    intro α a inst x
+    simp [Subtype.ext_iff]
+
+end
diff --git a/Mathlib/Order/Filter/AtTopBot/Disjoint.lean b/Mathlib/Order/Filter/AtTopBot/Disjoint.lean
index 9567ca1eb588ac..f5af23dd10eff6 100644
--- a/Mathlib/Order/Filter/AtTopBot/Disjoint.lean
+++ b/Mathlib/Order/Filter/AtTopBot/Disjoint.lean
@@ -48,3 +48,14 @@ theorem disjoint_atBot_atTop [PartialOrder α] [Nontrivial α] :
     exact Iic_disjoint_Ici.2 hle
 
 end Filter
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Filter.Tendsto.eventually_ne_atBot' : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α}, Filter.Tendsto f l Filter.atBot → ∀ (c : α), ∀ᶠ (x : α) in l, x ≠ c := by
+  open Filter Filter.Tendsto Set in
+    intro α β inst _ f l hf c
+    exact ((hf.eventually_ne_atBot (f c)).mono fun _ => ne_of_apply_ne f)
+
+end
diff --git a/Mathlib/Order/Filter/Prod.lean b/Mathlib/Order/Filter/Prod.lean
index e6f62fd24324e3..3863511f121854 100644
--- a/Mathlib/Order/Filter/Prod.lean
+++ b/Mathlib/Order/Filter/Prod.lean
@@ -555,3 +555,15 @@ lemma Tendsto.coprod_of_prod_top_left {f : α × β → γ} {la : Filter α} {lb
 end Coprod
 
 end Filter
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Filter.sUnion_lift_sets : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β}, Monotone g → ⋃₀ {s | s ∈ f.lift g} = ⋃ s ∈ f, ⋃₀ {t | t ∈ g s} := by
+  open Filter Set Function in
+    intro α β f g hg
+    simp only [sUnion_eq_biUnion, mem_setOf_eq, mem_lift_sets hg, iUnion_exists,
+    iUnion_and, @iUnion_comm _ (Set β)]
+
+end
diff --git a/Mathlib/Order/Fin/Basic.lean b/Mathlib/Order/Fin/Basic.lean
index 84f14489c0d9eb..fe984f0e227d03 100644
--- a/Mathlib/Order/Fin/Basic.lean
+++ b/Mathlib/Order/Fin/Basic.lean
@@ -405,3 +405,59 @@ map. In this lemma we state that for each `i : Fin n` we have `(e i : ℕ) = (i
   · rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]
 
 end Fin
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Fin.image_rev_uIoo : ∀ {n : ℕ} (i j : Fin n), Fin.rev '' Set.uIoo i j = Set.uIoo i.rev j.rev := by
+  open Fin Function Set in
+    intro n i j
+    simp [uIoo, ← rev_anti.map_min, ← rev_anti.map_max]
+
+theorem Fin.image_rev_Ici : ∀ {n : ℕ} (i : Fin n), Fin.rev '' Set.Ici i = Set.Iic i.rev := by
+  open Fin Function Set in
+    intro n i
+    ext; simp [le_rev_iff]
+
+theorem Fin.image_rev_Iic : ∀ {n : ℕ} (i : Fin n), Fin.rev '' Set.Iic i = Set.Ici i.rev := by
+  open Fin Function Set in
+    intro n i
+    ext; simp [rev_le_iff]
+
+theorem Fin.image_rev_Iio : ∀ {n : ℕ} (i : Fin n), Fin.rev '' Set.Iio i = Set.Ioi i.rev := by
+  open Fin Function Set in
+    intro n i
+    ext; simp [rev_lt_iff]
+
+theorem Fin.image_rev_Ioi : ∀ {n : ℕ} (i : Fin n), Fin.rev '' Set.Ioi i = Set.Iio i.rev := by
+  open Fin Function Set in
+    intro n i
+    ext; simp [lt_rev_iff]
+
+theorem Fin.image_rev_Icc : ∀ {n : ℕ} (i j : Fin n), Fin.rev '' Set.Icc i j = Set.Icc j.rev i.rev := by
+  open Fin Function Set in
+    intro n i j
+    ext; simp [le_rev_iff, rev_le_iff, and_comm]
+
+theorem Fin.image_rev_Ico : ∀ {n : ℕ} (i j : Fin n), Fin.rev '' Set.Ico i j = Set.Ioc j.rev i.rev := by
+  open Fin Function Set in
+    intro n i j
+    ext; simp [le_rev_iff, rev_lt_iff, and_comm]
+
+theorem Fin.image_rev_Ioc : ∀ {n : ℕ} (i j : Fin n), Fin.rev '' Set.Ioc i j = Set.Ico j.rev i.rev := by
+  open Fin Function Set in
+    intro n i j
+    ext; simp [lt_rev_iff, rev_le_iff, and_comm]
+
+theorem Fin.image_rev_Ioo : ∀ {n : ℕ} (i j : Fin n), Fin.rev '' Set.Ioo i j = Set.Ioo j.rev i.rev := by
+  open Fin Function Set in
+    intro n i j
+    ext; simp [lt_rev_iff, rev_lt_iff, and_comm]
+
+theorem Fin.image_rev_uIcc : ∀ {n : ℕ} (i j : Fin n), Fin.rev '' Set.uIcc i j = Set.uIcc i.rev j.rev := by
+  open Fin Function Set in
+    intro n i j
+    simp [uIcc, ← rev_anti.map_min, ← rev_anti.map_max]
+
+end
diff --git a/Mathlib/Order/Interval/Set/Basic.lean b/Mathlib/Order/Interval/Set/Basic.lean
index bc913bfeaa7fcf..790149c8f358ba 100644
--- a/Mathlib/Order/Interval/Set/Basic.lean
+++ b/Mathlib/Order/Interval/Set/Basic.lean
@@ -771,3 +771,29 @@ lemma Iio_False : Iio False = ∅ := by aesop
 lemma Ioi_True : Ioi True = ∅ := by aesop
 
 end Set
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Set.Ioc_inter_Ioc_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a c ∩ Set.Ioc b c = Set.Ioc (max a b) c := by
+  open Set Function in
+    intro α inst a b c
+    grind
+
+theorem Set.Ioc_inter_Ioc_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b ∩ Set.Ioc a c = Set.Ioc a (min b c) := by
+  open Set Function in
+    intro α inst a b c
+    grind
+
+theorem Set.Ioc_inter_Ioc_symm : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioc a b ∩ Set.Ioc b a = Set.Ioc (max a b) (min a b) := by
+  open Set Function in
+    intro α inst a b
+    grind
+
+theorem Set.Ioc_inter_Ioc_inter_Ioc_cycle : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b ∩ Set.Ioc b c ∩ Set.Ioc c a = Set.Ioc (max a (max b c)) (min a (min b c)) := by
+  open Set Function in
+    intro α inst a b c
+    grind
+
+end
diff --git a/Mathlib/Order/Interval/Set/OrdConnected.lean b/Mathlib/Order/Interval/Set/OrdConnected.lean
index 47cae5ddfedfa6..3ab2ff567741c0 100644
--- a/Mathlib/Order/Interval/Set/OrdConnected.lean
+++ b/Mathlib/Order/Interval/Set/OrdConnected.lean
@@ -333,3 +333,19 @@ theorem image_subtype_val_uIoo [OrdConnected s] (a b : s) :
 end LinearOrder
 
 end Set
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Filter.tendsto_Ico_Iic_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iic a)) := by
+  open Filter Set Function in
+    intro α inst a
+    exact (tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self)
+
+theorem Filter.tendsto_Ioc_Ici_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ici a)) := by
+  open Filter Set Function in
+    intro α inst a
+    exact (tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self)
+
+end
diff --git a/Mathlib/Probability/HasLaw.lean b/Mathlib/Probability/HasLaw.lean
index 73c46d781c40af..b137c8a72381b9 100644
--- a/Mathlib/Probability/HasLaw.lean
+++ b/Mathlib/Probability/HasLaw.lean
@@ -246,3 +246,16 @@ lemma iIndepFun_iff_hasLaw_pi_pi [IsProbabilityMeasure P] {ι : Type*} [Fintype
     simp_rw [fun i ↦ (hX i).map_eq]
 
 end ProbabilityTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem ProbabilityTheory.IdentDistrib.essInf_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ} [inst_3 : ConditionallyCompleteLinearOrder γ] [inst_4 : TopologicalSpace γ] [OpensMeasurableSpace γ] [OrderClosedTopology γ], ProbabilityTheory.IdentDistrib f g μ ν → essInf f μ = essInf g ν := by
+  open ProbabilityTheory ProbabilityTheory.IdentDistrib MeasureTheory Filter Finset TopologicalSpace in
+    intro α β γ inst inst_1 inst_2 μ ν f g inst_3 inst_4 _ _ h
+    have I : ∀ a, μ {x : α | a > f x} = ν {x : β | a > g x} := fun a =>
+      h.measure_mem_eq measurableSet_Iio
+    simp_rw [essInf_eq_sSup, I]
+
+end
diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean
index 7fd840d064c9c2..3fdcabce3d5c63 100644
--- a/Mathlib/Probability/Kernel/Basic.lean
+++ b/Mathlib/Probability/Kernel/Basic.lean
@@ -462,3 +462,14 @@ end Bool
 
 end Kernel
 end ProbabilityTheory
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem MeasureTheory.Measure.comp_apply_empty : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel κ], (μ.bind ⇑κ) ∅ = μ ∅ := by
+  open MeasureTheory MeasureTheory.Measure ProbabilityTheory in
+    intro α β mα mβ μ κ _
+    simp [bind_apply .empty κ.aemeasurable]
+
+end
diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean b/Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
index 23e037a198388a..55d33c2c84abe5 100644
--- a/Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
+++ b/Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
@@ -214,3 +214,15 @@ lemma Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes
     simpa [h1] using Ideal.comap_mono (f := Ideal.Quotient.mk (p.map (algebraMap R S))) h2
 
 end
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem PrimeSpectrum.inter_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (s s' : Set R), PrimeSpectrum.zeroLocus s ∩ PrimeSpectrum.zeroLocus s' = PrimeSpectrum.zeroLocus ↑(Ideal.span s ⊔ Ideal.span s') := by
+  open PrimeSpectrum in
+    intro R inst s s'
+    rw [zeroLocus_sup]
+    simp
+
+end
diff --git a/Mathlib/RingTheory/Ideal/Oka.lean b/Mathlib/RingTheory/Ideal/Oka.lean
index b28c6f90864576..bf58504db8417b 100644
--- a/Mathlib/RingTheory/Ideal/Oka.lean
+++ b/Mathlib/RingTheory/Ideal/Oka.lean
@@ -81,3 +81,14 @@ theorem forall_of_forall_prime'
 end IsOka
 
 end Ideal
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem IsPrincipalIdealRing.of_prime_ne_top : ∀ {R : Type u_1} [inst : CommSemiring R], (∀ (P : Ideal R), P.IsPrime → P ≠ ⊤ → Submodule.IsPrincipal P) → IsPrincipalIdealRing R := by
+  open IsPrincipalIdealRing Ideal in
+    intro R inst H
+    exact (.of_prime fun P hp ↦ (eq_or_ne P ⊤).elim (· ▸ inferInstance) <| H _ hp)
+
+end
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index 6695747a689e33..72864b75048c8b 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -1150,3 +1150,14 @@ abbrev orderBotAleph0OrdToType : OrderBot Cardinal.aleph0.{u}.ord.ToType :=
   WellFoundedLT.toOrderBot _
 
 end Cardinal
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Ordinal.iInf_eq_of_range_eq : ∀ {ι : Sort u_3} {ι' : Sort u_4} {f : ι → Ordinal.{u_5}} {g : ι' → Ordinal.{u_5}}, Set.range f = Set.range g → iInf f = iInf g := by
+  open Ordinal Function Cardinal Set Order in
+    intro ι ι' f g h
+    exact (congr_arg _ h)
+
+end
diff --git a/Mathlib/SetTheory/ZFC/Ordinal.lean b/Mathlib/SetTheory/ZFC/Ordinal.lean
index 4c6cc793d9b0a3..3c3c38e312a316 100644
--- a/Mathlib/SetTheory/ZFC/Ordinal.lean
+++ b/Mathlib/SetTheory/ZFC/Ordinal.lean
@@ -406,3 +406,13 @@ noncomputable def _root_.Ordinal.toZFSetIso : Ordinal ≃o {x // ZFSet.IsOrdinal
   map_rel_iff' {a b} := by simp
 
 end ZFSet
+
+
+-- Dual/order lemmas discovered by the Manifold Destiny verifier-mediated learner.
+-- Paper: https://github.com/sumofagents/manifold-destiny
+section
+theorem Class.congToClass_univ : Class.congToClass Set.univ = Set.univ := by
+  open Class in
+    rfl
+
+end