mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.SubExpr
/-- A position of a subexpression in an expression.

We use a simple encoding scheme for expression positions `Pos`:
every `Expr` constructor has at most 3 direct expression children. Considering an expression's type
to be one extra child as well, we can injectively map a path of `childIdxs` to a natural number
by computing the value of the 4-ary representation `1 :: childIdxs`, since n-ary representations
without leading zeros are unique. Note that `pos` is initialized to `1` (case `childIdxs == []`).

See also `SubExpr`.  -/
Lean.SubExpr.Pos : Type
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral.eq_1 : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V)
  (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W),
  VectorFourier.fourierIntegral e μ L f w = ∫ (v : V), e (-(L v) w) • f v ∂μ
-- Mathlib.NumberTheory.Harmonic.Int
/-- The 2-adic norm of the n-th harmonic number is 2 raised to the logarithm of n in base 2.  -/
padicNorm_two_harmonic : ∀ {n : ℕ}, n ≠ 0 → ‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The morphism in `Localization W` that is the formal inverse of a morphism
which belongs to `W`.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [inst_1 : W.HasLeftCalculusOfFractions] →
        {X Y : C} →
          (s : X ⟶ Y) →
            W s →
              ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y ⟶
                (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X)
-- Init.Data.List.Nat.TakeDrop
List.length_take_le' : ∀ {α : Type u_1} (i : ℕ) (l : List α), (List.take i l).length ≤ l.length
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_expEquiv_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), ↑(WithZero.expEquiv a) = WithZero.exp a
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.trans_arrowCongrLeft : ∀ {α₁ : Sort u} {α₂ : Sort v} {α₃ : Sort x} {γ : Sort w} [inst : Inhabited γ] (e₁₂ : α₁ ↪ α₂) (e₂₃ : α₂ ↪ α₃),
  e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft = (e₁₂.trans e₂₃).arrowCongrLeft
-- LeanSearchClient.Basic
leansearchclient.backend : Lean.Option String
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_ofReal_im : ∀ (x : ℝ), (Complex.tan ↑x).im = 0
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.isAcyclic_starGraph : ∀ {V : Type u_1} (r : V), (SimpleGraph.starGraph r).IsAcyclic
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v t =
    if Std.DTreeMap.Internal.Impl.contains k t = true then (true, t)
    else (false, Std.DTreeMap.Internal.Impl.insert! k v t)
-- Init.Data.Nat.ToString
Nat.b_eq_digitChar : ∀ {n : ℕ}, 'b' = n.digitChar ↔ n = 11
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.equivTree_apply : ∀ (p : DyckWord), DyckWord.equivTree p = p.toTree
-- Mathlib.LinearAlgebra.Reflection
/-- Given an element `x` in a module `M` and a linear form `f` on `M`, we define the endomorphism
of `M` for which `y ↦ y - (f y) • x`.

One is typically interested in this endomorphism when `f x = 2`; this definition exists to allow the
user defer discharging this proof obligation. See also `Module.reflection`.  -/
Module.preReflection : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M → Module.Dual R M → Module.End R M
-- Mathlib.RingTheory.Ideal.Operations
Ideal.prod_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R),
  ∏ i ∈ s, Ideal.span {I i} = Ideal.span {∏ i ∈ s, I i}
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt16HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.ClosedUnder.sInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} {f : L.Functions n} {S : Set (Set M)},
  (∀ s ∈ S, FirstOrder.Language.ClosedUnder f s) → FirstOrder.Language.ClosedUnder f (sInf S)
-- Mathlib.Data.Fintype.EquivFin
Infinite.of_not_fintype : ∀ {α : Type u_1}, (∀ (a : Fintype α), False) → Infinite α
-- Mathlib.Algebra.Polynomial.Basic
/-- Linear isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials.  -/
Polynomial.toFinsuppIsoLinear : (R : Type u) → [inst : Semiring R] → Polynomial R ≃ₗ[R] AddMonoidAlgebra R ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sq_pi_over_two_pow : ∀ (n : ℕ), Real.sin (Real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (Real.sqrtTwoAddSeries 0 n / 2) ^ 2
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.finsetProd_mem : ∀ {R : Type u_1} [inst : CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Finset ι) (f : ι → R),
  (∃ x ∈ s, f x ∈ I) → s.prod f ∈ I
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_neg : ∀ {R : Type u} (M : Type v) [inst : Neg R] [inst_1 : NegZeroClass M] (r : R),
  TrivSqZeroExt.inl (-r) = -TrivSqZeroExt.inl r
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.polarSpaceCoord K =
    (NumberField.mixedEmbedding.polarCoord K).transHomeomorph
      (NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Topology.isEmbedding_sigmoid : Topology.IsEmbedding unitInterval.sigmoid
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.instContinuousOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β], ContinuousOrderHomClass (α →Co β) α β
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : NatCast F] (n : ℕ) (x : E), DifferentiableAt 𝕜 (↑n) x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- **Alias** of `intervalIntegral.integral_finsetSum`. -/
intervalIntegral.integral_finset_sum : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {ι : Type u_8} {s : Finset ι} {f : ι → ℝ → E},
  (∀ i ∈ s, IntervalIntegrable (f i) μ a b) →
    ∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodAssoc_toAffineEquiv : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) (P₃ : Type u_4) {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃], ↑(ContinuousAffineEquiv.prodAssoc k P₁ P₂ P₃) = AffineEquiv.prodAssoc k P₁ P₂ P₃
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α}, (t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.instInhabitedMkId : {α : Type u} → [Inhabited α] → Inhabited (CategoryTheory.KleisliCat.mk id α)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (P Q : CategoryTheory.ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)}
  (h : (ChainComplex.single₀ C).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).inv (CategoryTheory.CategoryStruct.comp P.π h) =
    CategoryTheory.CategoryStruct.comp Q.π h
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyoneda.eq_1 : CommGrpCat.coyoneda =
  {
    obj := fun M =>
      { obj := fun N => CommGrpCat.of (↑(Opposite.unop M) →* ↑N),
        map := fun {X Y} f => CommGrpCat.ofHom (MonoidHom.compHom (CommGrpCat.Hom.hom f)), map_id := ⋯, map_comp := ⋯ },
    map := fun {X Y} f => { app := fun N => CommGrpCat.ofHom (CommGrpCat.Hom.hom f.unop).compHom', naturality := ⋯ },
    map_id := CommGrpCat.coyoneda._proof_4, map_comp := @CommGrpCat.coyoneda._proof_5 }
-- Mathlib.MeasureTheory.Group.Measure
/-- A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`.  -/
ContinuousLinearEquiv.isAddHaarMeasure_map : ∀ {E : Type u_3} {F : Type u_4} {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommGroup E] [inst_3 : Module R E] [inst_4 : AddCommGroup F] [inst_5 : Module S F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_8 : TopologicalSpace F] [IsTopologicalAddGroup F]
  {σ : R →+* S} {σ' : S →+* R} [inst_10 : RingHomInvPair σ σ'] [inst_11 : RingHomInvPair σ' σ]
  [inst_12 : MeasurableSpace E] [BorelSpace E] [inst_14 : MeasurableSpace F] [BorelSpace F] (L : E ≃SL[σ] F)
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure], (MeasureTheory.Measure.map (⇑L) μ).IsAddHaarMeasure
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hom_ext : ∀ {R S : SemiRingCat} {f g : R ⟶ S}, SemiRingCat.Hom.hom f = SemiRingCat.Hom.hom g → f = g
-- Mathlib.Order.Monotone.Basic
StrictAnti.wellFoundedLT : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} [WellFoundedGT β],
  StrictAnti f → WellFoundedLT α
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop_mono' : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄,
  f₁ ≤ᶠ[l] f₂ → Filter.Tendsto f₁ l Filter.atTop → Filter.Tendsto f₂ l Filter.atTop
-- Mathlib.Analysis.Convex.Segment
segment_eq_image' : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (x y : E), segment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Set.Icc 0 1
-- Init.Data.Array.MapIdx
Array.mem_mapFinIdx : ∀ {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β},
  b ∈ xs.mapFinIdx f ↔ ∃ i, ∃ (h : i < xs.size), f i xs[i] h = b
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  (homotopic C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f : ι → M), ∏ a ∈ s with p a, f a = ∏ a ∈ s, if p a then f a else 1
-- Mathlib.Data.Multiset.UnionInter
Multiset.zero_disjoint : ∀ {α : Type u_1} (l : Multiset α), Disjoint 0 l
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
/-- Abbreviation for an unbundled commutative group object. It is a group object that is a
commutative monoid object.  -/
CategoryTheory.CommGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.BraidedCategory C] → C → Type v
-- Mathlib.Data.Fintype.Basic
Fin.univ_image_get : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), Finset.image l.get Finset.univ = l.toFinset
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instUnion : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Union (Std.DTreeMap α β cmp)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.equivOp_apply_coe : ∀ {M : Type u_2} [inst : Add M] (H : AddSubsemigroup M) (a : ↥H), ↑(H.equivOp a) = AddOpposite.op ↑a
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂ : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  IsCoprime ↑(Polynomial.UniversalCoprimeFactorizationRing.factor₁ m k hn p)
    ↑(Polynomial.UniversalCoprimeFactorizationRing.factor₂ m k hn p)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.measurableEquivIoc.congr_simp : ∀ (T : ℝ) [hT : Fact (0 < T)] (a : ℝ), AddCircle.measurableEquivIoc T a = AddCircle.measurableEquivIoc T a
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.notMem_range_embeddingUpIntLE_iff : ∀ (p n : ℤ), (∀ (i : ℕ), (ComplexShape.embeddingUpIntLE p).f i ≠ n) ↔ p < n
-- Mathlib.Topology.Order.Monotone
/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set.  -/
MonotoneOn.map_sSup_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousWithinAt f s (sSup s) → MonotoneOn f s → f ⊥ = ⊥ → f (sSup s) = sSup (f '' s)
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.filter_apply_eq_zero_iff : ∀ {α : Type u_1} {p : PMF α} {s : Set α} (h : ∃ a ∈ s, a ∈ p.support) (a : α),
  (p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support
-- Mathlib.RingTheory.Coalgebra.Hom
/-- `CoalgHomClass F R A B` asserts `F` is a type of bundled coalgebra homomorphisms
from `A` to `B`.  -/
CoalgHomClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : Module R A] →
              [inst_3 : AddCommMonoid B] →
                [inst_4 : Module R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → [FunLike F A B] → Prop
-- Mathlib.Data.Tree.Basic
BinaryTree.numLeaves.eq_def : ∀ {α : Type u} (x : BinaryTree α),
  x.numLeaves =
    match x with
    | BinaryTree.nil => 1
    | BinaryTree.node value a b => a.numLeaves + b.numLeaves
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.of_mul_left : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {m n : ℕ},
  p.IsMonicOfDegree m → (p * q).IsMonicOfDegree (m + n) → q.IsMonicOfDegree n
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (G : Type u_2)
  [inst_3 : Group G] [Finite G],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G)
    (CategoryTheory.PreGaloisCategory.functorToAction F)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLM_apply_single_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : DecidableEq m] {M : CStarMatrix m n A} {i : m} {j : n} (a : A),
  (CStarMatrix.toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i a)) j = a * M i j
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalSemiring : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] → [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → NonUnitalSemiring ↥S
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.dep.visit : (Lean.FVarId → Bool) → (Lean.MVarId → Bool) → Lean.Expr → Lean.DependsOn.M✝ Bool
-- Mathlib.Order.Hom.Basic
/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `ULift α →o β` in a
higher universe.  -/
OrderHom.uliftLeftMap : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → ULift.{u_8, u_2} α →o β
-- Init.Data.Order.Lemmas
Std.not_lt_of_ge : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] {a b : α}, a ≤ b → ¬b < a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ},
  ε₁ ≤ ε₂ → Metric.closedBall x ε₁ ⊆ Metric.closedBall x ε₂
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Naturality of the associator isomorphism: `(f₁ ⊗ₘ f₂) ⊗ₘ f₃ ≃ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)`  -/
CategoryTheory.MonoidalCategory.associator_naturality_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃)) h)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.uniformContinuous : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {E₁ : Type u_9}
  {E₂ : Type u_10} [inst_2 : UniformSpace E₁] [inst_3 : UniformSpace E₂] [inst_4 : AddCommGroup E₁]
  [inst_5 : AddCommGroup E₂] [inst_6 : Module R₁ E₁] [inst_7 : Module R₂ E₂] [IsUniformAddGroup E₁]
  [IsUniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂), UniformContinuous ⇑f
-- Init.Data.Array.Extract
Array.extract_size_left : ∀ {α : Type u_1} {j : ℕ} {as : Array α}, as.extract as.size j = #[]
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.LimitBicone.mk.inj : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {bicone : CategoryTheory.Limits.Bicone F}
  {isBilimit : bicone.IsBilimit} {bicone_1 : CategoryTheory.Limits.Bicone F} {isBilimit_1 : bicone_1.IsBilimit},
  { bicone := bicone, isBilimit := isBilimit } = { bicone := bicone_1, isBilimit := isBilimit_1 } →
    bicone = bicone_1 ∧ isBilimit ≍ isBilimit_1
-- Mathlib.Data.DFinsupp.Small
DFinsupp.small : ∀ {ι : Type u} {π : ι → Type v} [inst : (i : ι) → Zero (π i)] [Small.{w, u} ι] [∀ (i : ι), Small.{w, v} (π i)],
  Small.{w, max v u} (DFinsupp π)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- If `χ` is a Dirichlet character, then `L(χ, s)` does not vanish for `s.re ≥ 1`
except when `χ` is trivial and `s = 1` (then `L(χ, s)` has a simple pole at `s = 1`).  -/
DirichletCharacter.LFunction_ne_zero_of_one_le_re : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] ⦃s : ℂ⦄,
  χ ≠ 1 ∨ s ≠ 1 → 1 ≤ s.re → DirichletCharacter.LFunction χ s ≠ 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule.mk.injEq : ∀ (toEffectiveImport : Lean.EffectiveImport) (parts irParts : Array (Lean.ModuleData × Lean.CompactedRegion))
  (needsIRTrans : Bool) (toEffectiveImport_1 : Lean.EffectiveImport)
  (parts_1 irParts_1 : Array (Lean.ModuleData × Lean.CompactedRegion)) (needsIRTrans_1 : Bool),
  ({ toEffectiveImport := toEffectiveImport, parts := parts, irParts := irParts, needsIRTrans := needsIRTrans } =
      { toEffectiveImport := toEffectiveImport_1, parts := parts_1, irParts := irParts_1,
        needsIRTrans := needsIRTrans_1 }) =
    (toEffectiveImport = toEffectiveImport_1 ∧ parts = parts_1 ∧ irParts = irParts_1 ∧ needsIRTrans = needsIRTrans_1)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (next : Option α) (upperBound : α),
  sizeOf { next := next, upperBound := upperBound } = 1 + sizeOf next + sizeOf upperBound
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- When `s : X.N` is such that `s.dim = d`, this is a term
that is equal to `s`, but whose dimension if definitionally equal to `d`.  -/
SSet.N.cast : {X : SSet} → (s : X.N) → {d : ℕ} → s.dim = d → X.N
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- In a 2-transitive action, the normal closure of stabilizers is the full group.  -/
normalClosure_of_stabilizer_eq_top : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  2 < ENat.card α →
    MulAction.IsMultiplyPretransitive G α 2 → ∀ {a : α}, Subgroup.normalClosure ↑(MulAction.stabilizer G a) = ⊤
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_containsKey_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  l₁.isEmpty = true → (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).isEmpty = true
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.exists_smul_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : IsMulCommutative ↥H] [inst_2 : H.FiniteIndex]
  [inst_3 : H.Normal], (Nat.card ↥H).Coprime H.index → ∀ (α β : H.QuotientDiff), ∃ h, h • α = β
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_apply_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.Functor Cᵒᵖ (Type u_3)) (s : (E.saturate.multicospanIndex F).sections)
  (i : E.saturate.multicospanShape.L), ↑((E.sectionsSaturateEquiv F) s) i = s.val i
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonUnitalNonAssocCommRing.mul_comm : ∀ {α : Type u} [self : NonUnitalNonAssocCommRing α] (a b : α), a * b = b * a
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The equivalence between endomorphisms of `F` and the limit over the automorphism groups
of all Galois objects.  -/
CategoryTheory.PreGaloisCategory.endEquivAutGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          CategoryTheory.End F ≃ CategoryTheory.PreGaloisCategory.AutGalois F
-- Mathlib.Logic.Relation
/-- `SymmGen r`: symmetric closure of `r`. This is also the comparability relation, such
that `SymmGen r a b` means that either `r a b` or `r b a` (see `Mathlib.Order.Comparable`).  -/
Relation.SymmGen : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spineToSimplex_interval : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path m) (j l : ℕ)
  (hjl : j + l ≤ m),
  (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.subinterval j l hjl) ⋯ h).op))
      (sx.spineToSimplex m h f) =
    sx.spineToSimplex l ⋯ (f.interval j l hjl)