mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Basic
le_map_mul_map_div : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : CommMagma β]
  [inst_3 : LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b : α), f a ≤ f b * f (a / b)
-- Mathlib.Util.Notation3
/-- Delaborate the given variable's value. Fails if the variable has no value.
If `checkNot` is provided, then checks that the expression being delaborated is not
the given one (this is used to prevent infinite loops).  -/
Mathlib.Notation3.MatchState.delabVar : Mathlib.Notation3.MatchState →
  Lean.Name → optParam (Option Lean.Expr) none → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to a `CommGroup`.  -/
ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq : ∀ {R : Type u_1} [inst : CommGroup R] {f g : ℕ → R},
  (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
/-- Converting a group into a group object in `Type u`.  -/
CommGrpTypeEquivalenceCommGrp.inverse : CategoryTheory.Functor CommGrpCat (CategoryTheory.CommGrp (Type u))
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.liftₐ_algebraMap : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A) [inst_5 : I.IsPrime] (f : A →ₐ[R] B)
  (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)) (r : A),
  (Ideal.ResidueField.liftₐ I f hf₁ hf₂) ((algebraMap A I.ResidueField) r) = f r
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.coe_map : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F] [inst_6 : Module R F]
  (C : PointedCone R E) (f : E →ₗ[R] F), ↑(PointedCone.map f C) = ⇑f '' ↑C
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The quotient of a finitely presented additive group by an additive subgroup
which is finitely generated as a normal subgroup is finitely presented.  -/
AddGroup.IsFinitelyPresented.quotient : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsFinitelyPresented G] (N : AddSubgroup G) [inst_1 : N.Normal],
  N.IsFinitelyNormallyGenerated → AddGroup.IsFinitelyPresented (G ⧸ N)
-- Mathlib.Probability.Independence.Conditional
/-- **Alias** of `ProbabilityTheory.iCondIndepFun.condIndepFun_finsetProd_of_notMem`. -/
ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β}
  [inst_2 : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.CondIndepFun m' hm' (∏ j ∈ s, f j) (f i) μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → Std.ExtDHashMap.Const.get? (m₁ ∩ m₂) k = none
-- Mathlib.GroupTheory.Perm.Sign
/-- If we apply `prod_extendRight a (σ a)` for all `a : α` in turn,
we get `prod_congrRight σ`.  -/
Equiv.Perm.prod_prodExtendRight : ∀ {β : Type v} {α : Type u_1} [inst : DecidableEq α] (σ : α → Equiv.Perm β) {l : List α},
  l.Nodup →
    (∀ (a : α), a ∈ l) → (List.map (fun a => Equiv.Perm.prodExtendRight a (σ a)) l).prod = Equiv.prodCongrRight σ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.beq'.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly),
  p₁.beq' =
    Lean.Grind.CommRing.Poly.rec (motive := fun x => Lean.Grind.CommRing.Poly → Bool)
      (fun k₁ p₂ => Lean.Grind.CommRing.Poly.rec (fun k₂ => k₁.beq' k₂) (fun x x_1 x_2 x_3 => false) p₂)
      (fun k₁ v₁ x ih p₂ =>
        Lean.Grind.CommRing.Poly.rec (fun x => false) (fun k₂ v₂ p₂ x => (k₁.beq' k₂).and' ((v₁.beq' v₂).and' (ih p₂)))
          p₂)
      p₁
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeMapAux.match_1.eq_1 : ∀ {C : Type u_1}
  (motive : CategoryTheory.Discrete (CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → Sort u_2)
  (X : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  (h_1 : (X : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → motive { as := X }),
  (match { as := X } with
    | { as := X } => h_1 X) =
    h_1 X
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a : α} {μ : MeasureTheory.Measure α} [ClosedIicTopology α], MeasureTheory.NullMeasurableSet (Set.Iic a) μ
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instSMul : {ι : Type u_1} → {α : Type u_2} → {M : ι → Type u_5} → [(i : ι) → SMul α (M i)] → SMul α ((i : ι) → M i)
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Quaternion.exp_coe : ∀ (r : ℝ), NormedSpace.exp ↑r = ↑(NormedSpace.exp r)
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ico (f (Order.succ n)) (f n)` are pairwise disjoint.  -/
Antitone.pairwise_disjoint_on_Ico_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ico (f (Order.succ n)) (f n))
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Build a list of elements in descending order from the tree.

```
toRevList {1, 2, 4} = [4, 2, 1]
toRevList {2, 1, 1, 4} = [4, 2, 1]
```  -/
Ordnode.toRevList : {α : Type u_1} → Ordnode α → List α
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.symm_apply_apply : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α),
  h.symm (h x) = x
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.reflective : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful]
  [inst_5 : ∀ (F : CategoryTheory.Functor C H), L.HasPointwiseRightKanExtension F], CategoryTheory.IsIso L.ranCounit
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.instBEqAuxLemmaKey.beq : Lean.Meta.AuxLemmaKey → Lean.Meta.AuxLemmaKey → Bool
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
Set.finrank_mono : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {s t : Set V}, s ⊆ t → Set.finrank K s ≤ Set.finrank K t
-- Mathlib.RepresentationTheory.Equiv
/-- If there exists `G`-action on a trivial monoid `H` then the induced representation
on `k[H]` is equivalent to the trivial representation.  -/
Representation.ofMulActionSubsingletonEquivTrivial : (k : Type u) →
  [inst : Semiring k] →
    (G : Type v) →
      [inst_1 : Monoid G] →
        (H : Type w) →
          [Subsingleton H] →
            [MulOneClass H] →
              [inst_4 : MulAction G H] → (Representation.ofMulAction k G H).Equiv (Representation.trivial k G k)
-- Init.Prelude
/-- The number of distinct values representable by `UInt8`, that is, `2^8 = 256`.  -/
UInt8.size : ℕ
-- Mathlib.Topology.NhdsWithin
Pi.instNeBotNhdsWithinIio : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] [Nonempty ι]
  [inst_2 : (i : ι) → Preorder (X i)] {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (Set.Iio (x i))).NeBot],
  (nhdsWithin x (Set.Iio x)).NeBot
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.mk : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : Group α], (UniformContinuous fun p => p.1 / p.2) → IsUniformGroup α
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type v)} (x : F.obj.obj (Opposite.op X)) (Y : Cᵒᵖ)
  (f : Opposite.unop Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app Y)) f =
    (CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_injOn_pos : ∀ {b : ℝ}, 1 < b → Set.InjOn (Real.logb b) (Set.Ioi 0)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_comap_algEquiv : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {T : Type u_4}
  [inst_11 : CommRing T] [inst_12 : IsDedekindDomain T] [inst_13 : IsIntegrallyClosed T] [inst_14 : Algebra R T]
  [inst_15 : Module.Finite R T] [inst_16 : Module.IsTorsionFree R T] (σ : S ≃ₐ[R] T) (I : Ideal T),
  (Ideal.relNorm R) (Ideal.comap σ I) = (Ideal.relNorm R) I
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.mk.sizeOf_spec : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  [inst_2 : SizeOf J] [inst_3 : SizeOf C] (hom : A.pt ⟶ B.pt)
  (wπ :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π j) = A.π j)
      CategoryTheory.Limits.BiconeMorphism.wπ._autoParam)
  (wι :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom = B.ι j)
      CategoryTheory.Limits.BiconeMorphism.wι._autoParam),
  sizeOf { hom := hom, wπ := wπ, wι := wι } = 1 + sizeOf hom
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforward_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {D'' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D''] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_4 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {K' : CategoryTheory.GrothendieckTopology D'}
  {K'' : CategoryTheory.GrothendieckTopology D''} {G : CategoryTheory.Functor D D'}
  {R' : CategoryTheory.Sheaf K' RingCat} [inst_5 : G.IsContinuous K K']
  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') {G' : CategoryTheory.Functor D' D''}
  {R'' : CategoryTheory.Sheaf K'' RingCat} [inst_6 : G'.IsContinuous K' K''] [inst_7 : (G.comp G').IsContinuous K K'']
  [inst_8 : (F.comp G).IsContinuous J K'] (ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R''),
  (SheafOfModules.pushforward ψ').isoWhiskerLeft (SheafOfModules.pushforwardComp φ ψ) ≪≫
      SheafOfModules.pushforwardComp
        (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ)) ψ' =
    ((SheafOfModules.pushforward ψ').associator (SheafOfModules.pushforward ψ) (SheafOfModules.pushforward φ)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pushforwardComp ψ ψ') (SheafOfModules.pushforward φ) ≪≫
        SheafOfModules.pushforwardComp φ
          (CategoryTheory.CategoryStruct.comp ψ ((G.sheafPushforwardContinuous RingCat K K').map ψ'))
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- Typeclass for a convex space structure on a module to be given by weighted sums.  -/
Convexity.IsModuleConvexSpace : (R : Type u_2) →
  (M : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsStrictOrderedRing R] →
          [inst_3 : AddCommMonoid M] → [Module R M] → [Convexity.ConvexSpace R M] → Prop
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebung_coeff_succ : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  (WittVector.verschiebung x).coeff n.succ = x.coeff n
-- Mathlib.Order.Interval.Multiset
Multiset.card_Ioo_eq_card_Icc_sub_two : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Multiset.Ioo a b).card = (Multiset.Icc a b).card - 2
-- Aesop.RuleTac.Forward
Aesop.RuleTac.applyForwardRule : Lean.MVarId →
  Lean.Expr →
    Option (Array Aesop.Substitution) →
      Aesop.UnorderedArraySet Aesop.PremiseIndex → Bool → Option ℕ → Aesop.ScriptM Aesop.Subgoal
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.eq_2 : ∀ {α : Type u_1} (motive : RegularExpression α → Sort u_2) (h_1 : Unit → motive RegularExpression.zero)
  (h_2 : Unit → motive RegularExpression.epsilon) (h_3 : (a : α) → motive (RegularExpression.char a))
  (h_4 : (P Q : RegularExpression α) → motive (P.plus Q)) (h_5 : (P Q : RegularExpression α) → motive (P.comp Q))
  (h_6 : (P : RegularExpression α) → motive P.star),
  (match RegularExpression.epsilon with
    | RegularExpression.zero => h_1 ()
    | RegularExpression.epsilon => h_2 ()
    | RegularExpression.char a => h_3 a
    | P.plus Q => h_4 P Q
    | P.comp Q => h_5 P Q
    | P.star => h_6 P) =
    h_2 ()
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.noConfusionType : Sort v✝ → Lean.ReducibilityStatus → Lean.ReducibilityStatus → Sort v✝
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extension of `PolynomialLaw.zero_def`  -/
PolynomialLaw.toFun_zero : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type u_5} [inst_5 : CommSemiring S] [inst_6 : Algebra R S],
  PolynomialLaw.toFun S 0 = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k : α} {v : β k}, (m.insert k v).get k ⋯ = v
-- Mathlib.Logic.ExistsUnique
ExistsUnique.eq_1 : ∀ {α : Sort u_1} (p : α → Prop), ExistsUnique p = ∃ x, p x ∧ ∀ (y : α), p y → y = x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
_private.Mathlib.AlgebraicTopology.SimplicialSet.HornColimits.0.SSet.horn.IsCompatible.multicofork.match_1.eq_1 : ∀ {n : ℕ} {i : Fin (n + 2)} (motive : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ↑{i}ᶜ).R → Sort u_1)
  (j : Fin (n + 1 + 1)) (hj : j ∈ {i}ᶜ) (h_1 : (j : Fin (n + 1 + 1)) → (hj : j ∈ {i}ᶜ) → motive ⟨j, hj⟩),
  (match ⟨j, hj⟩ with
    | ⟨j, hj⟩ => h_1 j hj) =
    h_1 j hj
-- Mathlib.MeasureTheory.Measure.Tight
MeasureTheory.IsTightMeasureSet.inter : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [inst : TopologicalSpace 𝓧],
  MeasureTheory.IsTightMeasureSet S → ∀ (T : Set (MeasureTheory.Measure 𝓧)), MeasureTheory.IsTightMeasureSet (S ∩ T)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Ioi_val : ∀ {n : ℕ} (i : Fin n), Fin.val ⁻¹' Set.Ioi ↑i = Set.Ioi i
-- Mathlib.Analysis.Complex.Basic
Complex.conj_tsum : ∀ {α : Type u_1} {L : SummationFilter α} (f : α → ℂ),
  (starRingEnd ℂ) (∑'[L] (a : α), f a) = ∑'[L] (a : α), (starRingEnd ℂ) (f a)
-- Mathlib.Tactic.Translate.Reorder
/-- Return `true` if the reorder doesn't do anything.  -/
Mathlib.Tactic.Translate.ArgReorder.isEmpty : Mathlib.Tactic.Translate.ArgReorder → Bool
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.ext : ∀ {G : Type u_2} [inst : AddGroup G] [Finite G] [IsAddCyclic G] {d : ℕ} {a b : ZMod d},
  Nat.card G = d → (∀ (t : G), a.val • t = b.val • t) → a = b
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.σ_comp_toMk₁_of_lt : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.toMk₁ i) = SimplexCategory.toMk₁ i.succ
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Iio_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {b : α} {n : ℕ},
  ↑n ∈ Set.Iio b ↔ n ∈ Finset.Iio ⌈b⌉₊
-- Mathlib.Analysis.SumIntegralComparisons
sum_mul_Ico_le_integral_of_monotone_antitone : ∀ {a b : ℕ} {f g : ℝ → ℝ},
  a ≤ b →
    MonotoneOn f (Set.Icc ↑a ↑b) →
      AntitoneOn g (Set.Icc (↑a - 1) (↑b - 1)) →
        0 ≤ f ↑a → 0 ≤ g (↑b - 1) → ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a `k`-linear `G`-representation `A`, this is the Hom-set bijection in the adjunction
`A ⊗ - ⊣ ihom(A, -)`. It sends `f : A ⊗ B ⟶ C` to a `Rep k G` morphism defined by currying the
`k`-linear map underlying `f`, giving a map `A →ₗ[k] B →ₗ[k] C`, then flipping the arguments.  -/
Rep.tensorHomEquiv : {k : Type u} →
  [inst : CommRing k] →
    {G : Type v} →
      [inst_1 : Group G] →
        (A B C : Rep.{u, u, v} k G) → (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ (B ⟶ A.ihom.obj C)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- A local algebra homomorphism induces an algebra homomorphism on the residue fields.

See `mapAlgHom` for a variant where the base ring `R` is not quotiented.  -/
IsLocalRing.ResidueField.mapAlgHom' : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : IsLocalRing R] →
          [inst_2 : CommRing S] →
            [inst_3 : IsLocalRing S] →
              [inst_4 : CommRing T] →
                [inst_5 : IsLocalRing T] →
                  [inst_6 : Algebra R S] →
                    [inst_7 : Algebra R T] →
                      [inst_8 : IsLocalHom (algebraMap R S)] →
                        [inst_9 : IsLocalHom (algebraMap R T)] →
                          (e : S →ₐ[R] T) →
                            [IsLocalHom e] →
                              IsLocalRing.ResidueField S →ₐ[IsLocalRing.ResidueField R] IsLocalRing.ResidueField T
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_iff_lt_rowLen : ∀ {μ : YoungDiagram} {i j : ℕ}, (i, j) ∈ μ ↔ j < μ.rowLen i
-- Mathlib.Data.Set.Prod
Set.piMap_image_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {f : (i : ι) → α i → β i},
  (∀ i ∉ s, Function.Surjective (f i)) → ∀ (t : (i : ι) → Set (α i)), Pi.map f '' s.pi t = s.pi fun i => f i '' t i
-- Mathlib.Data.Finmap
Finmap.keysLookupEquiv_symm_apply_keys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }),
  (Finmap.keysLookupEquiv.symm f).keys = (↑f).1
-- Mathlib.Tactic.Linter.Style
/-- The "missing end" linter emits a warning on non-closed `section`s and `namespace`s.
It allows the "outermost" `noncomputable section` to be left open (whether or not it is named).
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.missingEnd.missingEndLinter : Lean.Linter
-- Std.Async.Select
/-- An event source together with a continuation to call on data obtained from that event source,
usually used together in conjunction with `Selectable.one`.
 -/
Std.Async.Selectable : Type → Type 1
-- Init.Data.String.Lemmas.Splits
String.copy_sliceTo_eq_iff_exists_splits : ∀ {s : String} {p : s.Pos} {t₁ : String}, (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂
-- Mathlib.Analysis.Calculus.Implicit
/-- **Alias** of `HasStrictFDerivAt.tendsto_implicitFunction`. -/
Filter.Tendsto.implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) {α : Type u_4} {l : Filter α}
  {g₁ : α → F} {g₂ : α → ↥(↑f').ker},
  Filter.Tendsto g₁ l (nhds (f a)) →
    Filter.Tendsto g₂ l (nhds 0) →
      Filter.Tendsto (fun t => HasStrictFDerivAt.implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (nhds a)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₀₁_comp_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 1 → G) → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).inv
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) 0 1)
        h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).inv h)
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying ring hom.  -/
RingCat.Hom.hom' : {R S : RingCat} → R.Hom S → ↑R →+* ↑S
-- Mathlib.MeasureTheory.Measure.Dirac
HasSum.isProbabilityMeasure_sum_dirac : ∀ {δ : Type u_3} {ι : Type u_4} {mδ : MeasurableSpace δ} {c : ι → ℝ} {d : ι → δ},
  (∀ (i : ι), 0 ≤ c i) →
    HasSum c 1 →
      MeasureTheory.IsProbabilityMeasure
        (MeasureTheory.Measure.sum fun i => ENNReal.ofReal (c i) • MeasureTheory.Measure.dirac (d i))
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The functor `C ⥤ D × E` obtained from two lax monoidal functors is lax monoidal.  -/
CategoryTheory.Functor.LaxMonoidal.prod' : {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] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor C E) → [F.LaxMonoidal] → [G.LaxMonoidal] → (F.prod' G).LaxMonoidal
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.isCongruent : Lean.Meta.Grind.Goal → Lean.Expr → Lean.Expr → Bool
-- Init.Data.Vector.Attach
Vector.attachWith_append : ∀ {α : Type u_1} {n m : ℕ} {P : α → Prop} {xs : Vector α n} {ys : Vector α m} {H : ∀ a ∈ xs ++ ys, P a},
  (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯
-- Mathlib.RingTheory.PowerBasis
PowerBasis.dim_ne_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Nontrivial S]
  (pb : PowerBasis R S), pb.dim ≠ 0
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_eq_zero_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {φ : MvPolynomial σ R}, ↑φ = 0 ↔ φ = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (∀ a ∈ t, (List.map Prod.fst l).contains a = false) →
          (Std.DTreeMap.Raw.Const.insertMany t l).size = t.size + l.length
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.toFreeMonoid.eq_1 : ∀ {α : Type u_1}, FreeSemigroup.toFreeMonoid = FreeSemigroup.lift FreeMonoid.of
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Reindexing a pullback cone preserves being limiting.  -/
CategoryTheory.Limits.WidePullbackCone.reindexIsLimitEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_2} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            (s : CategoryTheory.Limits.WidePullbackCone f) →
              {ι' : Type u_3} →
                (e : ι' ≃ ι) → CategoryTheory.Limits.IsLimit (s.reindex e) ≃ CategoryTheory.Limits.IsLimit s