mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
MeasureTheory.AddContent.measure.eq_1 : ∀ {α : Type u_1} {C : Set (Set α)} [mα : MeasurableSpace α] (m : MeasureTheory.AddContent ENNReal C)
  (hC : MeasureTheory.IsSetSemiring C) (hC_gen : mα ≤ MeasurableSpace.generateFrom C)
  (m_sigma_subadd : m.IsSigmaSubadditive),
  m.measure hC hC_gen m_sigma_subadd = (m.measureCaratheodory hC m_sigma_subadd).trim ⋯
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} (s : Finset ι)
  (X : ι → Ω → ENNReal),
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), Measurable (X i)) → ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.σ j.succ) =
      CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i)
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- A cocone on `F` with cocone point `X` is the same as an element of `lim Hom(F·, X)`,
naturally in `F` and `X`.  -/
CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones : (J : Type v) →
  [inst : CategoryTheory.SmallCategory J] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (CategoryTheory.Functor.opHom J C).comp
            ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).comp
              (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v))
                        (CategoryTheory.Functor Jᵒᵖ (Type v)) (Type v)).obj
                    CategoryTheory.Limits.lim).comp
                ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v)).obj
                  CategoryTheory.yoneda))) ≅
          CategoryTheory.cocones J C
-- Mathlib.GroupTheory.Exponent
Group.exponent_dvd_card : ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G], Monoid.exponent G ∣ Fintype.card G
-- Mathlib.AlgebraicGeometry.Modules.Presheaf
/-- The underlying sheaf of rings of a scheme.  -/
AlgebraicGeometry.Scheme.ringCatSheaf : (X : AlgebraicGeometry.Scheme) → TopCat.Sheaf RingCat ↑X.toPresheafedSpace
-- Mathlib.RingTheory.Polynomial.Bernstein
/-- The Bernstein polynomials are linearly independent.

We prove by induction that the collection of `bernsteinPolynomial n ν` for `ν = 0, ..., k`
are linearly independent.
The inductive step relies on the observation that the `(n-k)`-th derivative, evaluated at 1,
annihilates `bernsteinPolynomial n ν` for `ν < k`, but has a nonzero value at `ν = k`.
 -/
bernsteinPolynomial.linearIndependent : ∀ (n : ℕ), LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
UpperSemicontinuousOn.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  UpperSemicontinuousOn f s →
    UpperSemicontinuousOn g s →
      (∀ x ∈ s, ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → UpperSemicontinuousOn (fun z => f z + g z) s
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.measure_compl_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], μ μ.supportᶜ = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
inhomogeneousCochains.d_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  inhomogeneousCochains.d A n =
    CategoryTheory.CategoryStruct.comp (Rep.freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv
      (CategoryTheory.CategoryStruct.comp (((Rep.barComplex k G).linearYonedaObj k A).d n (n + 1))
        (Rep.freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom)
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
/-- A cochain complex `K` is K-projective if any morphism `K ⟶ L`
with `L` acyclic is homotopic to zero.  -/
CochainComplex.IsKProjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [inst_1 : CategoryTheory.Abelian C] → CochainComplex C ℤ → Prop
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.toRatAlgEquiv_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S],
  Function.Injective RingEquiv.toRatAlgEquiv
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.smul_mem_pointwise_smul : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (a : A) (m : M)
  (S : AddSubmonoid A), a ∈ S → m • a ∈ m • S
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm.eq_1 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : PadicSeq p),
  f.norm = if hf : f ≈ 0 then 0 else padicNorm p (↑f (PadicSeq.stationaryPoint hf))
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRciSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Rci.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RciSlice α β)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.HasForget₂ (TopModuleCat R) TopCat
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`-th root of unity in `K`, then
`cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ)`. ∈ particular,
`cyclotomic n K = cyclotomic' n K`  -/
Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
  IsPrimitiveRoot ζ n → Polynomial.cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (Polynomial.X - Polynomial.C μ)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- Functor translating a functor into the category of commutative monoid objects
to a commutative monoid object in the functor category
 -/
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [inst_3 : CategoryTheory.BraidedCategory D] →
            CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.CommMon D))
              (CategoryTheory.CommMon (CategoryTheory.Functor C D))
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.map_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.PositiveCompacts α),
  TopologicalSpace.PositiveCompacts.map id ⋯ ⋯ K = K
-- Mathlib.Computability.Ackermann
ack_pair_lt : ∀ (m n k : ℕ), ack m (Nat.pair n k) < ack (m + 4) (max n k)
-- Mathlib.Topology.Separation.Basic
nhdsNE_le_cofinite : ∀ {α : Type u_3} [inst : TopologicalSpace α] [T1Space α] (a : α), nhdsWithin a {a}ᶜ ≤ Filter.cofinite
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_comm : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] (v w : Projectivization F (Fin 3 → F)), v.cross w = w.cross v
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_smul : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) [NoZeroDivisors R] (a : R), (a • p).mirror = a • p.mirror
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.absoluteForm.inj : ∀ {uri uri_1 : Std.Http.URI},
  Std.Http.RequestTarget.absoluteForm uri = Std.Http.RequestTarget.absoluteForm uri_1 → uri = uri_1
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Imp.instReflBoundedFormula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ}, Std.Refl T.Imp
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.DevosMulRel.eq_1 : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α],
  DevosMulRel✝ =
    Function.onFun (Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 > x2) fun x1 x2 => x1 < x2)) fun x =>
      ((x.1 * x.2).card, x.1.card + x.2.card, x.1.card)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- `tensorDistrib` as an equivalence.  -/
LinearMap.BilinForm.tensorDistribEquiv : (R : Type uR) →
  {M₁ : Type uM₁} →
    {M₂ : Type uM₂} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                [Module.Free R M₁] →
                  [Module.Finite R M₁] →
                    [Module.Free R M₂] →
                      [Module.Finite R M₂] →
                        TensorProduct R (LinearMap.BilinForm R M₁) (LinearMap.BilinForm R M₂) ≃ₗ[R]
                          LinearMap.BilinForm R (TensorProduct R M₁ M₂)
-- Mathlib.Algebra.Polynomial.GroupRingAction
Polynomial.instMulSemiringAction : (M : Type u_1) →
  [inst : Monoid M] →
    (R : Type u_2) → [inst_1 : Semiring R] → [MulSemiringAction M R] → MulSemiringAction M (Polynomial R)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_add_right_eq_map : ∀ {m n : ℕ}, (m...m + n).toList = List.map (fun x => x + m) (0...n).toList
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  IsTopologicalGroup (CategoryTheory.Aut F)
-- Mathlib.Data.Set.MulAntidiagonal
/-- `Set.mulAntidiagonal s t a` is the set of all pairs of an element in `s` and an element in `t`
that multiply to `a`.  -/
Set.mulAntidiagonal : {α : Type u_1} → [Mul α] → Set α → Set α → α → Set (α × α)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- Let `f : β → α` be a summable function and let `b ∈ β` be an index.
Lemma `tsum_eq_add_tsum_ite` writes `Σ' n, f n` as `f b` plus the sum of the
remaining terms.  -/
Summable.tsum_eq_add_tsum_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} [T2Space α] [inst_4 : DecidableEq β],
  Summable f → ∀ (b : β), ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.instSliceableListSliceNat.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → (Unit → motive none) → ((stop : ℕ) → motive (some stop)) → motive x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Pack two `BVExpr` of equivalent width into one parameter-less structure.
 -/
Std.Tactic.BVDecide.BVPred.ExprPair : Type
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- If `f` is a normal mono, then any map `k : W ⟶ Y` such that `k ≫ normal_mono.g = 0` induces
a morphism `l : W ⟶ X` such that `l ≫ f = k`.  -/
CategoryTheory.NormalMono.lift' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {W : C} →
          (f : X ⟶ Y) →
            [hf : CategoryTheory.NormalMono f] →
              (k : W ⟶ Y) →
                CategoryTheory.CategoryStruct.comp k CategoryTheory.NormalMono.g = 0 →
                  { l // CategoryTheory.CategoryStruct.comp l f = k }
-- Std.Time.Format.Modifier
Std.Time.instInhabitedFraction : Inhabited Std.Time.Fraction
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation): Use `Hom.toImage` instead which has better def-eqs.  -/
AlgebraicGeometry.Scheme.Hom.toImageAux : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → X ⟶ AlgebraicGeometry.Scheme.Hom.image f
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.map_lift_piComparison_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (P : C)
  (g : (j : β) → P ⟶ f j) {Z : D} (h : (∏ᶜ fun b => G.obj (f b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift fun j => G.map (g j)) h
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instIsTrivialTrivial : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {V : Type w} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V], (Rep.trivial k G V).IsTrivial
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₇_det : CartanMatrix.E₇.det = 2
-- Init.Data.Nat.Lcm
Nat.lcm_le_mul : ∀ {m n : ℕ}, 0 < m → 0 < n → m.lcm n ≤ m * n
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.mk : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g fg : X.PtSimplex n x} →
        {i : Fin n} →
          (map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X) →
            autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map = g.map)
                SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map = fg.map)
                  SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam →
                autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map = f.map)
                    SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam →
                  autoParam
                      (∀ j < i.castSucc.castSucc,
                        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
                      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam →
                    autoParam
                        (∀ (j : Fin (n + 2)),
                          i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
                        SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam →
                      f.MulStruct g fg i
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDerivAux_nonneg : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ], κ ≤ η → ∀ {a : α} {x : γ}, 0 ≤ κ.rnDerivAux η a x
-- Mathlib.Algebra.Lie.Submodule
LieSubalgebra.coe_toLieSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  ↑K.toLieSubmodule = K.toSubmodule
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_eq_of_mem : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)] {i : ι},
  i ∈ s → s.piecewise f g i = f i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastSub : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastSub
-- Mathlib.Order.CompleteLattice.Lemmas
sup_biInf_le_biInf_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (s : Set β) (a : α),
  a ⊔ ⨅ i ∈ s, f i ≤ ⨅ i ∈ s, a ⊔ f i
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.sum_zero_pow : (Cardinal.sum fun n => 0 ^ n) = 1
-- Mathlib.Algebra.RingQuot
RingQuot.preLiftAlgHom.congr_simp : ∀ (S : Type u_1) [inst : CommSemiring S] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u_3}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] {s : A → A → Prop} {f f_1 : A →ₐ[S] B} (e_f : f = f_1)
  (h : ∀ ⦃x y : A⦄, s x y → f x = f y), RingQuot.preLiftAlgHom S h = RingQuot.preLiftAlgHom S ⋯
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.monotone : ∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}},
  a.IsFundamentalSequence o f → ∀ {i j : Ordinal.{u}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_lpPiLpₗᵢ_symm : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Fintype α]
  {𝕜 : Type u_3} [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : α) → NormedSpace 𝕜 (E i)] [inst_4 : Fact (1 ≤ p)]
  (f : PiLp p E), ↑((lpPiLpₗᵢ E 𝕜).symm f) = f.ofLp
-- Mathlib.GroupTheory.Solvable
IsSimpleGroup.derivedSeries_succ : ∀ {G : Type u_1} [inst : Group G] [IsSimpleGroup G] {n : ℕ}, derivedSeries G n.succ = commutator G
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- The extremal number of a natural number `n` and a simple graph `H` is the maximum number of
edges in a `H`-free simple graph on `n` vertices.

If `H` is contained in all simple graphs on `n` vertices, then this is `0`.  -/
SimpleGraph.extremalNumber : ℕ → {W : Type u_1} → SimpleGraph W → ℕ
-- Mathlib.Order.Monotone.Basic
strictMonoOn_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn (⇑OrderDual.toDual ∘ f) s ↔ StrictAntiOn f s
-- Init.Omega.IntList
Lean.Omega.IntList.smul_get : ∀ (xs : Lean.Omega.IntList) (a : ℤ) (i : ℕ), (a * xs).get i = a * xs.get i
-- Mathlib.LinearAlgebra.DFinsupp
Submodule.mem_biSup_iff_exists_dfinsupp : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Prop) [inst_4 : DecidablePred p] (S : ι → Submodule R N) (x : N),
  x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ f, ((DFinsupp.lsum ℕ) fun i => (S i).subtype) (DFinsupp.filter p f) = x
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_nhds_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β},
  Asymptotics.IsEquivalent l u v → (Filter.Tendsto u l (nhds c) ↔ Filter.Tendsto v l (nhds c))
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, Set.Ioc a ⊤ = Set.Ioi a
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instExistsAddOfLE : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [ExistsAddOfLE α], ExistsAddOfLE (WithZero α)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Ref for the key.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandler.ref : Lean.Elab.ConfigEval.EvalConfigItemHandler → Lean.Syntax
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_of_right_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β),
  b ≤ x → Set.IccExtend h f x = f ⟨b, ⋯⟩
-- Batteries.Data.UInt
instLawfulOrdUInt8 : Std.LawfulOrd UInt8
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_vecCons_sub : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] {n : ℕ}
  (f : M [⋀^Fin (n + 1)]→L[R] N) (x y : M) (v : Fin n → M),
  f (Matrix.vecCons (x - y) v) = f (Matrix.vecCons x v) - f (Matrix.vecCons y v)
-- Init.Data.Float.Model.Unpacked.Basic
/-- Finite floats consisting of a sign bit, a positive natural mantissa and an exponent.  -/
Float.Model.UnpackedFloat.finite : Float.Model.UnpackedFloat.Sign → (mantissa : ℕ) → ℤ → 0 < mantissa → Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂)
  (gh : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W) {Z : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) gh))
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₂) gh) h_1))
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_biInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_5} {s : Set ι} {H : ι → AddSubgroup G},
  (∀ i ∈ s, (H i).Characteristic) → (⨅ i ∈ s, H i).Characteristic
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.ne_zero : ∀ (p q : ENNReal) [p.HolderConjugate q], p ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getKey? k = some k
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), ⊥.strictMap F = ⊥
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] (f : β → α) {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂)
  (h₁ : s₁.Nonempty), s₁.sup' h₁ f ≤ s₂.sup' ⋯ f
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ofHom_injective : ∀ {X Y : Type u} [inst : Group X] [inst_1 : Group Y], Function.Injective fun f => GrpCat.ofHom f
-- Mathlib.Util.TermReduce
/-- `zeta% t` elaborates to a zeta and zeta-delta reduced version of `t`.  -/
Mathlib.Util.TermReduce.zetaStx : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.ret.inj : ∀ {a : Turing.ToPartrec.Cont} {a_1 : List ℕ} {a_2 : Turing.ToPartrec.Cont} {a_3 : List ℕ},
  Turing.ToPartrec.Cfg.ret a a_1 = Turing.ToPartrec.Cfg.ret a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Data.Nat.Bitwise
/-- The ith bit is the ith element of `n.bits`.  -/
Nat.testBit_eq_inth : ∀ (n i : ℕ), n.testBit i = n.bits.getI i
-- Mathlib.Data.Finset.Card
Finset.strongDownwardInduction.eq_1 : ∀ {α : Type u_1} {p : Finset α → Sort u_4} {n : ℕ}
  (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (x : Finset α),
  Finset.strongDownwardInduction H x =
    H x fun {t} ht h =>
      have this := ⋯;
      have this := ⋯;
      Finset.strongDownwardInduction H t ht
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.const_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Mul β] [ContinuousMul β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : β), MeasureTheory.AEStronglyMeasurable (fun x => c * f x) μ
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.mk : Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr →
  Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.AbstractM.State✝