feat: 158 new lemmas discovered by a weightless verifier-mediated learner

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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