mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Jensen
/-- A form of the **equality case of Jensen's equality**.

For a strictly convex function `f` and positive weights `w`, if
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)`, then the points `p` are all equal.

See also `StrictConvexOn.map_sum_eq_iff`.  -/
StrictConvexOn.eq_of_le_map_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i) → ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
-- Init.Data.Nat.Power2.Basic
_private.Init.Data.Nat.Power2.Basic.0.Nat.nextPowerOfTwo.go.eq_def : ∀ (n power : ℕ) (h : power > 0),
  Nat.nextPowerOfTwo.go✝ n power h = if power < n then Nat.nextPowerOfTwo.go✝ n (power * 2) ⋯ else power
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_of : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.RespectsIso],
  (AlgebraicGeometry.AffineTargetMorphismProperty.of P).toProperty.RespectsIso
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxHom.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S], IsLocalization.Away.auxHom✝ S r = IsLocalization.Away.auxHom✝ S r
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_eq : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R), PowerSeries.constantCoeff f = MvPowerSeries.constantCoeff f
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuous_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, edist (f x) (f a) < ε
-- Mathlib.Order.WithBot
WithBot.coe_strictMono : ∀ {α : Type u_1} [inst : Preorder α], StrictMono fun a => ↑a
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.sup_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeSup β]
  [inst_3 : ContinuousSup β] (f g : C(α, β)) (a : α), (f ⊔ g) a = f a ⊔ g a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastReverse : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse
-- Mathlib.AlgebraicGeometry.Cover.Sigma
/-- `𝒰` refines the single object cover defined by `𝒰`.  -/
AlgebraicGeometry.Scheme.Cover.toSigma : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [inst_1 : UnivLE.{v, u}] →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) → 𝒰 ⟶ 𝒰.sigma
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_mono : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ENNReal},
  X ≤ᵐ[P] Y → P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.telescope_aux : ∀ (z : ℂ) (m : ℤ) (b : ℕ),
  ∑ n ∈ Finset.Ico (-↑b) ↑b, (1 / (↑m * z + ↑n) - 1 / (↑m * z + ↑n + 1)) = 1 / (↑m * z - ↑b) - 1 / (↑m * z + ↑b)
-- Mathlib.Data.Int.Bitwise
Int.bodd_mul : ∀ (m n : ℤ), (m * n).bodd = (m.bodd && n.bodd)
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- Notation for composition of prefunctors.  -/
Prefunctor.«term_⋙q_» : Lean.TrailingParserDescr
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  (he : e ∈ a.pretrivializationAtlas), Bundle.Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.lhs : Lean.Meta.Grind.AC.DiseqCnstr → Lean.Grind.AC.Seq
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp.inj : ∀ {e : Lean.Expr} {isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift}
  {f g h i : Mathlib.Tactic.BicategoryLike.Mor₁} {α : Mathlib.Tactic.BicategoryLike.CoherenceHom}
  {η θ : Mathlib.Tactic.BicategoryLike.Mor₂} {e_1 : Lean.Expr}
  {isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f_1 g_1 h_1 i_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {α_1 : Mathlib.Tactic.BicategoryLike.CoherenceHom} {η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂},
  Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e_1 isoLift?_1 f_1 g_1 h_1 i_1 α_1 η_1 θ_1 →
    e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ i = i_1 ∧ α = α_1 ∧ η = η_1 ∧ θ = θ_1
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.inter' : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} [s.OrdConnected] [t.OrdConnected], (s ∩ t).OrdConnected
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C],
  CategoryTheory.IsFilteredOrEmpty Cᵒᵖ
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_mul : ∀ {R : Type u} [inst : Semiring R] {f g : Polynomial R},
  Polynomial.derivative (f * g) = Polynomial.derivative f * g + f * Polynomial.derivative g
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The function `UniformFun.filter α β : Filter (β × β) → Filter ((α →ᵤ β) × (α →ᵤ β))`
has a lower adjoint `l` (in the sense of `GaloisConnection`). The exact definition of `l` is not
interesting; we will only use that it exists (in `UniformFun.mono` and
`UniformFun.iInf_eq`) and that
`l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕)` for each
`𝓕 : Filter (γ × γ)` and `f : γ → α` (in `UniformFun.comap_eq`).  -/
UniformFun.gc : ∀ (α : Type u_1) (β : Type u_2),
  GaloisConnection (fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X),
  CategoryTheory.CategoryStruct.comp (e.hom.toNatTrans.app A) (e.inv.toNatTrans.app A) =
    CategoryTheory.CategoryStruct.id (F.toFunctor.obj A)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The completion of a number field at an infinite place is locally compact.  -/
NumberField.InfinitePlace.Completion.locallyCompactSpace : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), LocallyCompactSpace v.Completion
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofEq_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂),
  (CategoryTheory.ShortComplex.Homotopy.ofEq h).h₀ = 0
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_bot : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊥.op = ⊥
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.coe_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : Module.End R M), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Regular.Basic
IsAddLeftRegular.right_of_addCommute : ∀ {R : Type u_1} [inst : Add R] {a : R}, (∀ (b : R), AddCommute a b) → IsAddLeftRegular a → IsAddRightRegular a
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_bernoulli_iff : ∀ {p : NNReal} (h : p ≤ 1) (b : Bool), b ∈ (PMF.bernoulli p h).support ↔ bif b then p ≠ 0 else p ≠ 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ofBijective.symm_eq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ),
  (AffineEquiv.ofBijective hφ).symm.toEquiv = (Equiv.ofBijective (⇑φ) hφ).symm
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.Balanced.map : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.Balanced → t₁ = t₂ → t₂.Balanced
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`.  -/
MulAction.IsBlock.subgroup : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} {H : Subgroup G},
  MulAction.IsBlock G B → MulAction.IsBlock (↥H) B
-- Mathlib.Data.Rel
SetRel.preimage_inter_subset : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) {t₁ t₂ : Set β}, R.preimage (t₁ ∩ t₂) ⊆ R.preimage t₁ ∩ R.preimage t₂
-- Mathlib.Data.Num.ZNum
ZNum.to_int_inj : ∀ {m n : ZNum}, ↑m = ↑n ↔ m = n
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_le_avgRisk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  (π : MeasureTheory.Measure Θ) [hκ : ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.bayesRisk ℓ P π ≤ ProbabilityTheory.avgRisk ℓ P κ π
-- Mathlib.RingTheory.Polynomial.Basic
/-- If `P` is a prime ideal of `R`, then `P.R[x]` is a prime ideal of `R[x]`.  -/
Ideal.isPrime_map_C_of_isPrime : ∀ {R : Type u} [inst : CommRing R] {P : Ideal R} [P.IsPrime], (Ideal.map Polynomial.C P).IsPrime
-- Mathlib.Logic.Function.Basic
Function.instIsEquivSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsEquiv α r], IsEquiv α (Function.swap r)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore.isContMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [h : IsManifold I (n + 1) M],
  (tangentBundleCore I M).IsContMDiff I n
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.instInhabitedInfiniteAdeleRing : (K : Type u_1) → [inst : Field K] → Inhabited (NumberField.InfiniteAdeleRing K)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {W : C} →
          {ι : W ⟶ X} →
            (leftRetraction : X ⟶ W) →
              (rightRetraction : Y ⟶ X) →
                autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
                    CategoryTheory.IsSplitEqualizer.condition._autoParam →
                  autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction = CategoryTheory.CategoryStruct.id W)
                      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp g rightRetraction = CategoryTheory.CategoryStruct.id X)
                        CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp f rightRetraction =
                            CategoryTheory.CategoryStruct.comp leftRetraction ι)
                          CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam →
                        CategoryTheory.IsSplitEqualizer f g ι