mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.CartanCriterion
/-- An auxiliary lemma used to prove `LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero`
which proves the same result except without the algebraically closed assumption.  -/
_private.Mathlib.Algebra.Lie.CartanCriterion.0.LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_aux : ∀ {L : Type u_2} {M : Type u_3} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {K : Type u_4}
  [inst_3 : Field K] [CharZero K] [IsAlgClosed K] [inst_6 : LieAlgebra K L] [inst_7 : Module K M]
  [inst_8 : LieModule K L M] [FiniteDimensional K M],
  LieModule.traceForm K L M = 0 → LieModule.IsNilpotent (↥(LieAlgebra.derivedSeries K L 1)) M
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.pow_totalWeight_sub_one_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (NumberField.InfinitePlace K)] {n : ℕ},
  n ≠ 0 →
    ∀ (v : NumberField.InfinitePlace K),
      ↑n ^ (Height.totalWeight K - 1) = (∏ w ∈ Finset.univ.erase v, ↑n ^ w.mult) * ↑n ^ (v.mult - 1)
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.OreSet.mk : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) →
        (oreNum : R → ↥S → R) →
          (oreDenom : R → ↥S → ↥S) →
            (∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s) → OreLocalization.OreSet S
-- Init.Data.UInt.Lemmas
USize.ofBitVec_ofFin : ∀ (n : Fin (2 ^ System.Platform.numBits)), { toBitVec := { toFin := n } } = USize.ofFin n
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.alter : {α : Type u} →
  [BEq α] →
    [Hashable α] →
      {β : Type v} →
        (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → (Option β → Option β) → Std.DHashMap.Internal.Raw₀ α fun x => β
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.toPreAbstractSimplicialComplex_injective : ∀ {ι : Type u_1}, Function.Injective AbstractSimplicialComplex.toPreAbstractSimplicialComplex
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.map.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
  FundamentalGroupoid.map f =
    { obj := fun x => { as := f x.as }, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.map p f, map_id := ⋯,
      map_comp := ⋯ }
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.mem_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {a : α},
  a ∈ aig ↔ Std.Sat.AIG.Decl.atom a ∈ aig.decls
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.lexOrder_eq_top_iff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  (φ : MvPowerSeries σ R), φ.lexOrder = ⊤ ↔ φ = 0
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.eraseIfExists : Lean.Meta.SimpTheorems → Lean.Meta.Origin → Lean.Meta.SimpTheorems
-- Mathlib.GroupTheory.PGroup
IsPGroup.commutative_of_card_eq_prime_sq : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)], Nat.card G = p ^ 2 → ∀ (a b : G), a * b = b * a
-- Lean.Elab.Term.TermElabM
/-- Main function for elaborating terms.
It extracts the elaboration methods from the environment using the node kind.
Recall that the environment has a mapping from `SyntaxNodeKind` to `TermElab` methods.
It creates a fresh macro scope for executing the elaboration method.
All unlogged trace messages produced by the elaboration method are logged using
the position information at `stx`. If the elaboration method throws an `Exception.error` and `errToSorry == true`,
the error is logged and a synthetic sorry expression is returned.
If the elaboration throws `Exception.postpone` and `catchExPostpone == true`,
a new synthetic metavariable of kind `SyntheticMVarKind.postponed` is created, registered,
and returned.
The option `catchExPostpone == false` is used to implement `resumeElabTerm`
to prevent the creation of another synthetic metavariable when resuming the elaboration.

If `implicitLambda == false`, then disable implicit lambdas feature for the given syntax, but not for its subterms.
We use this flag to implement, for example, the `@` modifier. If `Context.implicitLambda == false`, then this parameter has no effect.
 -/
Lean.Elab.Term.elabTerm : Lean.Syntax → Option Lean.Expr → optParam Bool true → optParam Bool true → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.LinearAlgebra.Complex.Module
Complex.liftAux_I : Complex.liftAux Complex.I Complex.I_mul_I = AlgHom.id ℝ ℂ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Mul Mᵐᵒᵖ], DomMulAct.instMulOfMulOpposite = inst
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- The sum of an (arbitrary) collection of outer measures.  -/
MeasureTheory.OuterMeasure.sum : {α : Type u_1} → {ι : Type u_3} → (ι → MeasureTheory.OuterMeasure α) → MeasureTheory.OuterMeasure α
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
alternatingGroup.isSimpleGroup_five : IsSimpleGroup ↥(alternatingGroup (Fin 5))
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- `true` if the filter corresponds to a Riemann-style integral,
i.e. in the definition of integrability we require a constant upper estimate `r` on the size of
boxes of a tagged partition; the value `false` means that the estimate may depend on the position
of the tag.  -/
BoxIntegral.IntegrationParams.bRiemann : BoxIntegral.IntegrationParams → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union! m₂).getKey? k = m₂.getKey? k
-- Lean.Elab.DefView
Lean.Elab.HeaderProcessedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {view : Lean.Elab.DefViewElabHeaderData} {state : Lean.Elab.Term.SavedState}
  {tacStx? : Option Lean.Syntax} {tacSnap? : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)}
  {bodyStx : Lean.Syntax} {bodySnap : Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot)}
  {moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)} {toSnapshot_1 : Lean.Language.Snapshot}
  {view_1 : Lean.Elab.DefViewElabHeaderData} {state_1 : Lean.Elab.Term.SavedState} {tacStx?_1 : Option Lean.Syntax}
  {tacSnap?_1 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)} {bodyStx_1 : Lean.Syntax}
  {bodySnap_1 : Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot)}
  {moreSnaps_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)},
  { toSnapshot := toSnapshot, view := view, state := state, tacStx? := tacStx?, tacSnap? := tacSnap?,
        bodyStx := bodyStx, bodySnap := bodySnap, moreSnaps := moreSnaps } =
      { toSnapshot := toSnapshot_1, view := view_1, state := state_1, tacStx? := tacStx?_1, tacSnap? := tacSnap?_1,
        bodyStx := bodyStx_1, bodySnap := bodySnap_1, moreSnaps := moreSnaps_1 } →
    toSnapshot = toSnapshot_1 ∧
      view = view_1 ∧
        state = state_1 ∧
          tacStx? = tacStx?_1 ∧
            tacSnap? = tacSnap?_1 ∧ bodyStx = bodyStx_1 ∧ bodySnap = bodySnap_1 ∧ moreSnaps = moreSnaps_1
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_inv : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : DivisionCommMonoid γ] {f : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ}, (f.prod fun i b => (h i b)⁻¹) = (f.prod h)⁻¹
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- Composing `F₁ × F₂` with `G₁ ⊠ G₂` is isomorphic to `(F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂)`.  -/
CategoryTheory.MonoidalCategory.prodCompExternalProduct : {J₁ : Type u₁} →
  {J₂ : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              {I₁ : Type u₃} →
                {I₂ : Type u₄} →
                  [inst_4 : CategoryTheory.Category.{v₃, u₃} I₁] →
                    [inst_5 : CategoryTheory.Category.{v₄, u₄} I₂] →
                      (F₁ : CategoryTheory.Functor I₁ J₁) →
                        (G₁ : CategoryTheory.Functor J₁ C) →
                          (F₂ : CategoryTheory.Functor I₂ J₂) →
                            (G₂ : CategoryTheory.Functor J₂ C) →
                              (F₁.prod F₂).comp (CategoryTheory.MonoidalCategory.externalProduct G₁ G₂) ≅
                                CategoryTheory.MonoidalCategory.externalProduct (F₁.comp G₁) (F₂.comp G₂)
-- Init.Control.Lawful.Instances
OptionT.bind.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α β : Type u} (x : OptionT m α) (f : α → OptionT m β),
  x.bind f =
    OptionT.mk do
      let __do_lift ← x
      match __do_lift with
        | some a => f a
        | none => pure none
-- Init.Data.Vector.Attach
Vector.mem_attachWith : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {q : α → Prop} (H : ∀ x ∈ xs, q x) (x : { x // q x }),
  x ∈ xs.attachWith q H ↔ ↑x ∈ xs
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.sdiff_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ M.E → X \ Y ⊆ M.E
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.isClosed_closedBall : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, IsClosed (Euclidean.closedBall x r)
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntIntIi : Lean.Grind.ToInt ℤ Lean.Grind.IntInterval.ii
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_le_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b : α}, a⁻¹ * b ≤ 1 ↔ b ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.EdgeDisjointTriangles.farFromTriangleFree : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [inst_5 : DecidableEq α],
  G.EdgeDisjointTriangles → ε * ↑(Fintype.card α ^ 2) ≤ ↑(G.cliqueFinset 3).card → G.FarFromTriangleFree ε
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.currPos : {ρ : Type} →
  {pat : ρ} → {s : String.Slice} → String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s → s.Pos
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
Frullani.norm_integral_inv_smul_sub_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        ∀ {V : E} {δ : ℝ},
          0 ≤ δ →
            (∀ x ∈ Set.uIoc a b, ‖f x - V‖ ≤ δ) →
              ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - Real.log (b / a) • V‖ ≤ δ * |Real.log (b / a)|
-- Mathlib.Data.FunLike.Group
FunLike.divisionCommMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Inv F] [inst_5 : Div F] [inst_6 : Pow F ℤ] [inst_7 : DivisionCommMonoid β]
  [inst_8 : IsOneApply F α β] [inst_9 : IsMulApply F α β] [inst_10 : IsInvApply F α β] [inst_11 : IsDivApply F α β]
  [inst_12 : IsPowApply ℕ F α β] [inst_13 : IsPowApply ℤ F α β],
  FunLike.divisionCommMonoid = Function.Injective.divisionCommMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α} {hc : t.minKeyD fallback ∈ t}, t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Enters the body of the current expression, which must be a lambda or forall.
The binding variable is passed to `d` as `Syntax`, and it is an identifier that has been annotated with the fvar expression
for the variable.

If `pp.safeShadowing` is true, then the name is allowed to shadow a name in the local context
if the name does not appear in the body or in the `avoid` set.
(The `avoid` set is assumed to be a subset of the names used by the local context.)

If `preserveName` is `false` (the default), gives the binder an unused name.
Otherwise, it tries to preserve the textual form of the name, preserving whether it is hygienic.
 -/
Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName : {α : Type} →
  (Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM α) →
    optParam Bool false → optParam Lean.NameSet ∅ → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Data.Finset.Sigma
Finset.sup_sigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α i → β)
  [inst : SemilatticeSup β] [inst_1 : OrderBot β], (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The ring isomorphism between the endomorphisms of an object `M` in `TopModuleCat R` and the
continuous `R`-linear endomorphisms of `M`.  -/
TopModuleCat.endRingEquiv : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      (M : TopModuleCat R) → CategoryTheory.End M ≃+* (↑M.toModuleCat →L[R] ↑M.toModuleCat)
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- The number of generators.  -/
FGAlgCatSkeleton.n : {R : Type u} → [inst : CommRing R] → FGAlgCatSkeleton R → ℕ
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.lift_of' : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι],
  AddCommGroup.DirectLimit.lift G f (AddCommGroup.DirectLimit G f) (AddCommGroup.DirectLimit.of G f) ⋯ =
    AddMonoidHom.id (AddCommGroup.DirectLimit G f)
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedProj_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y : ↑s},
  s.ordConnectedProj x = s.ordConnectedProj y ↔ Set.uIcc ↑x ↑y ⊆ s
-- Init.Data.UInt.Lemmas
USize.right_eq_add : ∀ {a b : USize}, b = a + b ↔ a = 0
-- Mathlib.GroupTheory.Nilpotent
AddGroup.isNilpotent_top : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.IsNilpotent ↥⊤ ↔ AddGroup.IsNilpotent G
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is `π` if and only if they are nonzero and the first is
on the same ray as the negation of the second.  -/
Orientation.oangle_eq_pi_iff_sameRay_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑Real.pi ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
-- Mathlib.Analysis.Complex.Exponential
Real.norm_exp_sub_one_sub_id_le : ∀ {x : ℝ}, ‖x‖ ≤ 1 → ‖Real.exp x - 1 - x‖ ≤ ‖x‖ ^ 2
-- Init.Data.Int.Order
Int.neg_nonneg_of_nonpos : ∀ {a : ℤ}, a ≤ 0 → 0 ≤ -a
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Turn a non-unital subalgebra containing `1` into a subalgebra.  -/
NonUnitalSubalgebra.toSubalgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : NonUnitalSubalgebra R A) → 1 ∈ S → Subalgebra R A
-- Mathlib.Tactic.SplitIfs
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition.hyp.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Mathlib.Tactic.SplitPosition.hyp✝ fvarId) = 1 + sizeOf fvarId
-- Aesop.Builder.Forward
Aesop.RuleBuilder.forwardCore₂ : Aesop.ElabRuleTerm →
  Option (Array Lean.Name) → Option Aesop.RulePattern → Aesop.PhaseSpec → Bool → Lean.MetaM Aesop.ForwardRule
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke
versions for `ℝ≥0`, `ℝ`, and `ℂ`.  -/
Unitization.cfcₙ_eq_cfc_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {R : Type u_2} [inst_1 : Semifield R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : Module R A]
  [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A] [inst_9 : Algebra R ℂ] [inst_10 : IsScalarTower R ℂ A]
  {p : A → Prop} {p' : Unitization ℂ A → Prop} [inst_11 : NonUnitalContinuousFunctionalCalculus R A p]
  [inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'] [ContinuousMapZero.UniqueHom R (Unitization ℂ A)],
  (∀ {a : A}, p' ↑a ↔ p a) →
    ∀ (a : A) (f : R → R), autoParam (f 0 = 0) Unitization.cfcₙ_eq_cfc_inr._auto_1 → ↑(cfcₙ f a) = cfc f ↑a
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.mulIndicator_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : One β] {s : Set α},
  Filter.EventuallyConst s l → ∀ (c : β), Filter.EventuallyConst (s.mulIndicator fun x => c) l
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b}, CurveIntegrable ω₁ γ → CurveIntegrable ω₂ γ → CurveIntegrable (ω₁ + ω₂) γ
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ⟶ Z) [CategoryTheory.IsIso f], CategoryTheory.IsIso (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite limits, then `F.unop : C ⥤ D` reflects finite
colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteLimits F],
  CategoryTheory.Limits.ReflectsFiniteColimits F.unop
-- Init.Data.Vector.Lemmas
Vector.foldrM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → β → m β} {init : β}
  {xs : Vector α n}, Array.foldrM f init xs.toArray = Vector.foldrM f init xs
-- Mathlib.RingTheory.Flat.Basic
Submodule.toBaseChange.toLinearEquiv_symm_apply : ∀ {R : Type u_1} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Module.Flat R A] {M : Type u_5} [inst_4 : AddCommMonoid M] [inst_5 : Module R M] (p : Submodule R M) (a : A)
  (m : ↥p), (Submodule.toBaseChange.toLinearEquiv A p).symm ⟨a ⊗ₜ[R] ↑m, ⋯⟩ = a ⊗ₜ[R] m
-- Mathlib.Data.Finset.Max
Finset.mem_of_min : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a : α}, s.min = ↑a → a ∈ s
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- If a morphism `q : Z ⟶ X i` belongs to `sieve f f' i`, this is a choice of
index `j` such that there exists a factorization `hom ≫ f' j = q ≫ f i` for
some `hom`.  -/
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.idx : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type t} →
      {S : C} →
        {X : ι → C} →
          {f : (i : ι) → X i ⟶ S} →
            {ι' : Type t'} →
              {X' : ι' → C} →
                {f' : (j : ι') → X' j ⟶ S} →
                  {i : ι} →
                    {Z : C} →
                      {q : Z ⟶ X i} →
                        (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows
                            (CategoryTheory.Over.homMk q ⋯) →
                          ι'
-- Init.Data.String.Pattern.Basic
/-- Builds an iterator of `SearchStep` corresponding to matches of `pat` along the slice
  `s`. The `SearchStep`s returned by this iterator must contain ranges that are
  adjacent, non-overlapping and cover all of `s`.
   -/
String.Slice.Pattern.ToForwardSearcher.toSearcher : {ρ : Type} →
  (pat : ρ) →
    {σ : outParam (String.Slice → Type)} →
      [self : String.Slice.Pattern.ToForwardSearcher pat σ] →
        (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
-- Mathlib.Algebra.Group.Prod
Prod.instAddZeroClass : {M : Type u_3} → {N : Type u_4} → [AddZeroClass M] → [AddZeroClass N] → AddZeroClass (M × N)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_right_mul : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x - y * z, y} = Ideal.span {x, y}
-- Std.Data.HashMap.AdditionalOperations
/-- Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.HashMap.filterMap : {α : Type u} →
  {β : Type v} →
    {γ : Type w} → [inst : BEq α] → [inst_1 : Hashable α] → (α → β → Option γ) → Std.HashMap α β → Std.HashMap α γ
-- Batteries.Data.String.Legacy
/-- Checks whether the Boolean predicate `p` returns `true` for every character in a substring.

Short-circuits at the first character for which `p` returns `false`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
Substring.Raw.Legacy.all : Substring.Raw → (Char → Bool) → Bool
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.sub : ∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] {φ ψ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → ψ.IsHomogeneous n → (φ - ψ).IsHomogeneous n
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Compatibility with the structure morphism, for a morphism of coalgebras.  -/
CategoryTheory.Comonad.Coalgebra.Hom.h_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (self : A.Hom B) {Z : C} (h : G.obj B.A ⟶ Z),
  CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp (G.map self.f) h) =
    CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp B.a h)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommSemigroupOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : CommSemigroup Mᵐᵒᵖ], DomMulAct.instCommSemigroupOfMulOpposite = inst
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_L₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.L₀ = S.L₃.op
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.zeroKernelFork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C], (CategoryTheory.Limits.kernel.zeroKernelFork f).pt = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- If `H` is a characteristic subgroup of `G`, then every automorphism of `G` induces an
automorphism of `H`.  -/
MulAut.characteristic : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → [H.Characteristic] → MulAut G →* MulAut ↥H
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
GrpCat.μ_forget_apply : ∀ {G H : GrpCat} (p : ↑G) (q : ↑H),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget GrpCat) G H))
      (p, q) =
    (p, q)
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.integrable_binomial : ∀ {n : ℕ} {p : ↑unitInterval} {E : Type u_3} [inst : NormedAddCommGroup E] (f : ℕ → E),
  MeasureTheory.Integrable f (ProbabilityTheory.binomial n p)