mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Internal.Order.MonadTail
Lean.Order.MonadTail.monotone_bind_right : ∀ (m : Type u → Type v) [inst : Monad m] [inst_1 : Lean.Order.MonadTail m] {α β : Type u} [inst_2 : Nonempty β]
  {γ : Sort w} [inst_3 : Lean.Order.PartialOrder γ] (f : m α) (g : γ → α → m β),
  Lean.Order.monotone g → Lean.Order.monotone fun x => f >>= g x
-- Mathlib.Data.Finset.Prod
Finset.nonempty_product : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainNonUnitalRingHom_comp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N]
  [inst_3 : Mul O] (f : N →ₙ* O) (g : M →ₙ* N),
  MonoidAlgebra.mapDomainNonUnitalRingHom R (f.comp g) =
    (MonoidAlgebra.mapDomainNonUnitalRingHom R f).comp (MonoidAlgebra.mapDomainNonUnitalRingHom R g)
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.mk.inj : ∀ {k : Lean.SyntaxNodeKinds} {ref : Lean.Syntax} {patterns : Array Lean.Syntax} {lhs : Lean.Syntax}
  {rhs : Lean.TSyntax k} {ref_1 : Lean.Syntax} {patterns_1 : Array Lean.Syntax} {lhs_1 : Lean.Syntax}
  {rhs_1 : Lean.TSyntax k},
  { ref := ref, patterns := patterns, lhs := lhs, rhs := rhs } =
      { ref := ref_1, patterns := patterns_1, lhs := lhs_1, rhs := rhs_1 } →
    ref = ref_1 ∧ patterns = patterns_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.tendsto_of_ne_zero : ∀ {α : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : α → Γ₀} {γ : Γ₀},
  γ ≠ 0 → (Filter.Tendsto f l (nhds γ) ↔ ∀ᶠ (x : α) in l, f x = γ)
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal),
  h.toLaxMonoidal =
    { ε := h.εIso.hom, μ := fun X Y => (h.μIso X Y).hom, μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯,
      left_unitality := ⋯, right_unitality := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.norm_le_convexBodySumFun : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  ‖x‖ ≤ NumberField.mixedEmbedding.convexBodySumFun x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the objects in the covering of `S`  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.X : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} → {S : C} → (self : F.PreOneHypercoverDenseData S) → self.I₀ → C₀
-- Std.Data.HashSet.Lemmas
Std.HashSet.any_eq_true_iff_exists_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulHashable α] [EquivBEq α] {p : α → Bool},
  m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p (m.get a h) = true
-- Mathlib.Data.Int.Cast.Basic
Int.cast_natCast : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ), ↑↑n = ↑n
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f = O[l] g` on measurably generated `l`, `f` is strongly measurable at `l`,
and `g` is integrable at `l`, then `f` is integrable at `l`.  -/
Asymptotics.IsBigO.integrableAtFilter : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F} {l : Filter α}
  [inst_1 : MeasurableSpace α] [inst_2 : NormedAddCommGroup F] {μ : MeasureTheory.Measure α} [l.IsMeasurablyGenerated],
  f =O[l] g →
    StronglyMeasurableAtFilter f l μ → MeasureTheory.IntegrableAtFilter g l μ → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom`  -/
SkewMonoidAlgebra.liftNCAlgHom : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] →
        {A : Type u_4} →
          {B : Type u_5} →
            [inst_2 : Semiring A] →
              [inst_3 : Algebra k A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra k B] →
                    [inst_6 : MulSemiringAction G A] →
                      [inst_7 : SMulCommClass G k A] →
                        (f : A →ₐ[k] B) →
                          (g : G →* B) →
                            (∀ {x : A} {y : G}, f (y • x) * g y = g y * f x) → SkewMonoidAlgebra A G →ₐ[k] B
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_two_mul : ∀ (x : ℝ), Real.sin (2 * x) = 2 * Real.sin x * Real.cos x
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.coe_of : ∀ {X : Type u_1} (point : X), (Pointed.of point).X = X
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.instDecidableEqWalkingReflexivePair : DecidableEq CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Given the existence of the appropriate (possibly finite) coproducts and coequalizers,
we know a colimit of `F` exists.
(This assumes the existence of all coequalizers, which is technically stronger than needed.)
 -/
CategoryTheory.Limits.hasColimit_of_coequalizer_and_coproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)]
  [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.1)]
  [CategoryTheory.Limits.HasCoequalizers C], CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Order.Group.Cone
/-- `AddGroupConeClass S G` says that `S` is a type of cones in `G`.  -/
AddGroupConeClass : (S : Type u_1) → (G : outParam (Type u_2)) → [AddCommGroup G] → [SetLike S G] → Prop
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mem_carrier : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} {x : M}, x ∈ p.carrier ↔ x ∈ ↑p
-- Mathlib.Topology.Basic
isClosed_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosed ∅
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.le_mul_iff_one_le_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : MulOneClass α] [MulLeftMono α] {a b : α},
  MulLECancellable a → (a ≤ a * b ↔ 1 ≤ b)
-- Init.Data.Nat.Basic
Nat.add_sub_cancel : ∀ (n m : ℕ), n + m - m = n
-- Mathlib.Algebra.Notation
/-- The *negative part* of an element `a`.  -/
«term_⁻ᵐ» : Lean.TrailingParserDescr
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.newArgs : Lean.Elab.Term.CollectPatternVars.Context → Array Lean.Term
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup of an `AddGroup` inherits an inverse.  -/
NegMemClass.neg : {G : Type u_5} → {S : Type u_6} → [inst : Neg G] → [inst_1 : SetLike S G] → [NegMemClass S G] → {H : S} → Neg ↥H
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_whiskerLeft : ∀ {R : Type u} [inst : CommRing R] (L : ModuleCat R) {M N : ModuleCat R} (f : M ⟶ N),
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) =
    LinearMap.lTensor (↑L) (ModuleCat.Hom.hom f)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.map_rel : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.Embedding M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.desc.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.InjectiveResolution.desc f I J =
    J.cocomplex.mkHom I.cocomplex (CategoryTheory.InjectiveResolution.descFZero f I J)
      (CategoryTheory.InjectiveResolution.descFOne f I J) ⋯ fun n x =>
      match x with
      | ⟨g, ⟨g', w⟩⟩ => ⟨(I.descFSucc J n g g' ⋯).fst, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- Morphisms of Hopf monoids are just morphisms of the underlying bimonoids.
In fact they automatically intertwine the antipodes, proved below.
 -/
CategoryTheory.Hopf.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Hopf C)
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_8 : {α : Type u} → Std.Rii.Sliceable (Subarray α) ℕ (Subarray α)
-- Init.Data.SInt.Lemmas
ISize.toUSize_ofNat : ∀ {n : ℕ}, ISize.toUSize (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Order.WithBot
Equiv.withBotCongr_refl : ∀ {α : Type u_1}, (Equiv.refl α).withBotCongr = Equiv.refl (WithBot α)
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Return the consecutive unfoldings of `e` that are user friendly.  -/
_private.Mathlib.Tactic.ClickSuggestions.Unfold.0.Mathlib.Tactic.ClickSuggestions.filteredUnfolds : Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Topology.Inseparable
SeparationQuotient.lift.congr_simp : ∀ {X : Type u_1} {α : Type u_4} [inst : TopologicalSpace X] (f f_1 : X → α) (e_f : f = f_1)
  (hf : ∀ (x y : X), Inseparable x y → f x = f y) (a a_1 : SeparationQuotient X),
  a = a_1 → SeparationQuotient.lift f hf a = SeparationQuotient.lift f_1 ⋯ a_1
-- Mathlib.Topology.MetricSpace.Similarity
/-- Change the index set ι to an index ι' that maps to ι.  -/
Similar.index_map : ∀ {ι : Type u_1} {ι' : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂],
  Similar v₁ v₂ → ∀ (f : ι' → ι), Similar (v₁ ∘ f) (v₂ ∘ f)
-- Mathlib.MeasureTheory.Topology
/-- Under reasonable assumptions, sets that are codiscrete within `U` are contained in the "almost
everywhere" filter of co-null sets.  -/
ae_restrict_le_codiscreteWithin : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] {U : Set α},
  MeasurableSet U → MeasureTheory.ae (μ.restrict U) ≤ Filter.codiscreteWithin U
-- Mathlib.Algebra.Ring.Action.Pointwise.Finset
Finset.neg_smul_finset : ∀ {R : Type u_1} {G : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup G] [inst_2 : Module R G] [inst_3 : DecidableEq G]
  {t : Finset G} {a : R}, -a • t = -(a • t)
-- Mathlib.RingTheory.FreeCommRing
FreeRing.castFreeCommRing.eq_1 : ∀ {α : Type u_1}, FreeRing.castFreeCommRing = ⇑FreeRing.toFreeCommRing
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- A topological additive group is nonarchimedean if every neighborhood of 0
contains an open subgroup.  -/
NonarchimedeanAddGroup : (G : Type u_1) → [AddGroup G] → [TopologicalSpace G] → Prop
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.uncurry_ihomCurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.MonoidalClosed.ihomCurry x y z) =
    CategoryTheory.MonoidalClosed.curry
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator x y
            (CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z)).inv
        ((CategoryTheory.ihom.ev (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)).app z))
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- A map from a measurable space to the Cantor space `ℕ → Bool` induced by a countable
sequence of sets generating the measurable space.  -/
MeasurableSpace.mapNatBool : (α : Type u_1) → [inst : MeasurableSpace α] → [MeasurableSpace.CountablyGenerated α] → α → ℕ → Bool
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_xor : ∀ {w : ℕ} {y x : BitVec w} {hi lo : ℕ},
  BitVec.extractLsb lo hi (x ^^^ y) = BitVec.extractLsb lo hi x ^^^ BitVec.extractLsb lo hi y
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Ideal.IsMaximal.ne_bot_of_isIntegral_int : ∀ {R : Type u_1} [inst : CommRing R] [CharZero R] [Algebra.IsIntegral ℤ R] (I : Ideal R) [I.IsMaximal], I ≠ ⊥
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Localizing a ring homogeneously at a prime ideal.  -/
HomogeneousLocalization.AtPrime : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} → [inst : CommRing A] → [SetLike σ A] → (ι → σ) → (𝔭 : Ideal A) → [𝔭.IsPrime] → Type (max u_1 u_2)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.sSup_le : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {c : Set (E →ₛₗ.[σ] F)}
  (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c) {g : E →ₛₗ.[σ] F}, (∀ f ∈ c, f ≤ g) → LinearPMap.sSup c hc ≤ g
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.of_pow : ∀ {R : Type u_3} [inst : MonoidWithZero R] {x : R} {m : ℕ}, IsNilpotent (x ^ m) → IsNilpotent x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.mapM.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [inst_1 : Monad n]
  [inst_2 : MonadAttach n] [inst_3 : MonadLiftT m n] (f : β → n γ) (it : Std.IterM m β),
  Std.IterM.mapM f it = Std.IterM.mapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The categorical product of rings is the Cartesian product of rings.
 -/
CommRingCat.piFanIsLimit : {ι : Type u} → (R : ι → CommRingCat) → CategoryTheory.Limits.IsLimit (CommRingCat.piFan R)
-- Mathlib.Topology.UnitInterval
unitInterval.symm_lt_comm : ∀ {i j : ↑unitInterval}, unitInterval.symm i < j ↔ unitInterval.symm j < i
-- Mathlib.Algebra.DirectSum.Basic
/-- `fromAddMonoid φ` is the natural homomorphism from `γ` to `⨁ i, β i`
induced by a family `φ` of homomorphisms `γ → β i`.

Note that this is not an isomorphism. Not every homomorphism `γ →+ ⨁ i, β i` arises in this way.  -/
DirectSum.fromAddMonoid : {ι : Type v} →
  {β : ι → Type w} →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] →
        {γ : Type u₁} → [inst_2 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β i
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.eq_one : ∀ {M : Type u_1} [inst : Monoid M] {a : M} [Subsingleton Mˣ], IsUnit a → a = 1
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (γ : (ValuativeRel.ValueGroupWithZero R)ˣ),
  ∃ a b, (ValuativeRel.valuation R) ↑a / (ValuativeRel.valuation R) ↑b = ↑γ
-- Mathlib.Algebra.Group.Defs
AddCommGroup.toDivisionAddCommMonoid.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G],
  AddCommGroup.toDivisionAddCommMonoid =
    { toSubNegMonoid := inst.toSubNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯, add_comm := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Any monoid homomorphism `M →* A` can be lifted to an algebra homomorphism `R[M] →ₐ[R] A`.  -/
MonoidAlgebra.lift : (R : Type u_1) →
  (A : Type u_4) →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Monoid M] → (M →* A) ≃ (MonoidAlgebra R M →ₐ[R] A)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (α.naturality (CategoryTheory.CategoryStruct.comp f g)).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapComp f g).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (α.app a) (G.map f) (G.map g)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (α.naturality f).inv (G.map g))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (α.app b) (G.map g)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (α.naturality g).inv)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (α.app c)).inv
                (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (α.app c)))))))
-- Mathlib.Algebra.Star.Unitary
Unitary.map_comp : ∀ {R : Type u_2} {S : Type u_3} {T : Type u_4} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S]
  [inst_3 : StarMul S] [inst_4 : Monoid T] [inst_5 : StarMul T] (g : S →⋆* T) (f : R →⋆* S),
  Unitary.map (g.comp f) = (Unitary.map g).comp (Unitary.map f)
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_pair : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (i j : ι) (w : ι → R) (z : ι → E) [inst_3 : DecidableEq ι],
  i ≠ j → {i, j}.centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι],
  MeasureTheory.stoppedValue (MeasureTheory.stoppedProcess u τ) σ = fun ω =>
    if σ ω ≠ ⊤ then MeasureTheory.stoppedValue u (fun ω => min (σ ω) (τ ω)) ω
    else MeasureTheory.stoppedValue u (fun ω => min (↑(Classical.arbitrary ι)) (τ ω)) ω
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nonempty_image_addRight_neg_inter_iff : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s t : Set α} {a : α},
  ((fun x => x + -a) '' s ∩ t).Nonempty ↔ ((fun x => a + x) '' (-s) ∩ -t).Nonempty
-- Init.Data.Slice.Lemmas
Std.Slice.foldlM_toArray : ∀ {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] [LawfulMonad m] {s : Std.Slice γ} {init : δ}
  {f : δ → β → m δ}, Array.foldlM f init s.toArray = Std.Slice.foldlM f init s
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.toGaloisCoinsertion.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (gc : GaloisConnection u l) (h : ∀ (b : β), l (u b) ≤ b),
  gc.toGaloisCoinsertion h = { choice := fun x x_1 => l x, gc := gc, u_l_le := h, choice_eq := ⋯ }
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.IsMarkovKernel.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsMarkovKernel η]
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.IsMarkovKernel (η.comp κ)
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointIdIso_hom_app : ∀ {C₀ : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C₀] {F G : CategoryTheory.Functor C₀ C₀} (adj : F ⊣ G)
  (e : G ≅ CategoryTheory.Functor.id C₀) (X : C₀),
  (adj.leftAdjointIdIso e).hom.app X = CategoryTheory.CategoryStruct.comp (F.map (e.inv.app X)) (adj.counit.app X)
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_wbtw_left_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Sbtw R w y z → Wbtw R w x y → x ≠ z
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `y - X`
has Gaussian law with mean `y - μ` and variance `v`.  -/
ProbabilityTheory.gaussianReal_const_sub : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (y : ℝ), ProbabilityTheory.HasLaw (fun ω => y - X ω) (ProbabilityTheory.gaussianReal (y - μ) v) P
-- Aesop.Stats.Basic
Aesop.RuleStats.mk.injEq : ∀ (rule : Aesop.DisplayRuleName) (elapsed : Aesop.Nanos) (successful : Bool) (rule_1 : Aesop.DisplayRuleName)
  (elapsed_1 : Aesop.Nanos) (successful_1 : Bool),
  ({ rule := rule, elapsed := elapsed, successful := successful } =
      { rule := rule_1, elapsed := elapsed_1, successful := successful_1 }) =
    (rule = rule_1 ∧ elapsed = elapsed_1 ∧ successful = successful_1)
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_iff_bddAbove_bddBelow : ∀ {α : Type u_3} {s : Set α} [Nonempty α] [inst : Lattice α] [LocallyFiniteOrder α], s.Finite ↔ BddAbove s ∧ BddBelow s
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.inv_mul_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ σ' : S.Section) (g : G), (σ g)⁻¹ * σ' g ∈ S.inl.range
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_zero : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α],
  Matrix.blockDiagonal' 0 = 0
-- Mathlib.Algebra.Star.Module
/-- The self-adjoint elements of a star module, as a submodule.  -/
selfAdjoint.submodule : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] → [inst_5 : StarAddMonoid A] → [StarModule R A] → Submodule R A
-- Mathlib.Algebra.Lie.Basic
LieEquiv.coe_toLieHom : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), ⇑e.toLieHom = ⇑e
-- Init.Data.List.Sublist
List.subset_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, n ≠ 0 → (l ⊆ List.replicate n a ↔ ∀ x ∈ l, x = a)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map f).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)) h =
    CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h)
-- Batteries.Data.List.Lemmas
List.getElem_swap_of_ne : ∀ {α : Type u_1} {xs : List α} {i j k : ℕ}, k ≠ i → k ≠ j → ∀ (hk : k < (xs.swap i j).length), (xs.swap i j)[k] = xs[k]
-- Mathlib.Data.Finset.Card
Finset.fiber_card_ne_zero_iff_mem_image : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → β) [inst : DecidableEq β] (y : β),
  {x ∈ s | f x = y}.card ≠ 0 ↔ y ∈ Finset.image f s
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `R` is of characteristic `p` and `¬p ∣ m`, then `ζ` is a root of `cyclotomic (p ^ k * m) R`
if and only if it is a primitive `m`-th root of unity.  -/
Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP : ∀ {m k p : ℕ} {R : Type u_1} [inst : CommRing R] [IsDomain R] [hp : Fact (Nat.Prime p)] [hchar : CharP R p] {μ : R}
  [NeZero ↑m], (Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
-- Mathlib.Logic.Equiv.Nat
/-- An equivalence between `ℕ ⊕ ℕ` and `ℕ`, by mapping `(Sum.inl x)` to `2 * x` and `(Sum.inr x)` to
`2 * x + 1`.
 -/
Equiv.natSumNatEquivNat : ℕ ⊕ ℕ ≃ ℕ