mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- In a star ring (i.e., a non-unital, non-associative, semiring with an additive,
antimultiplicative, involutive star operation), a star-closed non-unital subsemiring is itself a
star ring.  -/
StarMemClass.instStarRing : {S : Type u_1} →
  {R : Type u_2} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : SetLike S R] → [inst_3 : NonUnitalSubsemiringClass S R] → [StarMemClass S R] → (s : S) → StarRing ↥s
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasProd.tprod_fiberwise : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α]
  [CompleteSpace α] [T2Space α] {f : β → α} {a : α},
  HasProd f a → ∀ (g : β → γ), HasProd (fun c => ∏' (b : ↑(g ⁻¹' {c})), f ↑b) a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_rpow_of_exponent_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (x y : ℝ),
  0 ≤ x → 0 ≤ y → autoParam (0 ≤ a) CFC.rpow_rpow_of_exponent_nonneg._auto_1 → (a ^ x) ^ y = a ^ (x * y)
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.instIsCartesianCompOfIsFibered : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [p.IsFibered] {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c)
  [p.IsCartesian f φ] [p.IsCartesian g ψ],
  p.IsCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.isClosed : {α : Type} → Std.CloseableChannel.Unbounded✝ α → BaseIO Bool
-- Init.Data.List.Lemmas
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`.  -/
List.map_id' : ∀ {α : Type u_1} (l : List α), List.map (fun a => a) l = l
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instFinallySmallProd : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {J' : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J'] [CategoryTheory.FinallySmall J] [CategoryTheory.FinallySmall J'],
  CategoryTheory.FinallySmall (J × J')
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableOn.finsum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B}
  {ι : Type u_9} {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) → (∀ (i : ι), MDiff[u] (T% t)) → MDiff[u] fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩
-- Mathlib.Order.InitialSeg
InitialSeg.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : InitialSeg r s},
  (∀ (x : α), f x = g x) → f = g
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfDom_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M}
  (H : AddSubmonoid.map k.toAddMonoidHom T = S),
  (f.ofAddEquivOfDom H).toAddMonoidHom = f.toAddMonoidHom.comp k.toAddMonoidHom
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.iUnion_sdiff`. -/
Set.iUnion_diff : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), (⋃ i, t i) \ s = ⋃ i, t i \ s
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.toIsNormalMonoCategory : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.IsNormalMonoCategory C
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get!.eq_def : ∀ {α : Type u} {δ : Type w} [inst : Ord α] [inst_1 : Inhabited δ] (t : Std.DTreeMap.Internal.Impl α fun x => δ) (k : α),
  Std.DTreeMap.Internal.Impl.Const.get! t k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.get!" 227 13
        "Key is not present in map"
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get! l k
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get! r k
      | Ordering.eq => v'
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ιOfLE_μ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C}
  [inst_3 : P'.IsMonoidal] (h : P ≤ P') (X Y : P.FullSubcategory),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.ObjectProperty.ιOfLE h) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)
        ((CategoryTheory.ObjectProperty.ιOfLE h).obj Y))
-- Init.Data.Int.Lemmas
Int.mul_comm : ∀ (a b : ℤ), a * b = b * a
-- Mathlib.RingTheory.Adjoin.Singleton
/-- If the `algebraMap` injective then we have a Ring isomorphism between A[b] and A[↑b].  -/
Algebra.RingHom.adjoinAlgebraMapEquiv : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : CommSemiring C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] →
                  [IsScalarTower A B C] → (b : B) → [FaithfulSMul B C] → ↥A[b] ≃+* ↥A[(algebraMap B C) b]
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
RingHom.FaithfullyFlat.codescendsAlong_bijective : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f)
  fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.Order.Partition.Finpartition
Finpartition.exists_subset_part_bijOn : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts
-- Init.Data.Array.Basic
Array.Mem.mk : ∀ {α : Type u} {as : Array α} {a : α}, a ∈ as.toList → as.Mem a
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.IsMultiplyPreprimitive.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {n : ℕ},
  MulAction.IsMultiplyPretransitive M α n →
    (∀ {s : Set α},
        s.encard + 1 = ↑n → MulAction.IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)) →
      MulAction.IsMultiplyPreprimitive M α n
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index_mono : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {K K' V : Set G},
  IsCompact K' →
    K ⊆ K' → (interior V).Nonempty → MeasureTheory.Measure.haar.index K V ≤ MeasureTheory.Measure.haar.index K' V
-- Mathlib.MeasureTheory.Integral.Prod
/-- Double integrals commute with addition. This is the version with `(f + g) (x, y)`
(instead of `f (x, y) + g (x, y)`) in the LHS.  -/
MeasureTheory.integral_integral_add' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f g : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ =
        ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
-- Mathlib.Order.Category.Frm
Frm.ext_iff : ∀ {X Y : Frm} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.instMonoSimplexCategoryMonoOfLE : ∀ {X : SSet} [inst : X.Nonsingular] {x y : X.N} (h : x ≤ y), CategoryTheory.Mono (SSet.N.monoOfLE h)
-- Lean.Environment
Lean.instInhabitedEffectiveImport.default : Lean.EffectiveImport
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_append : ∀ {n m i : ℕ} {x : BitVec n} {y : BitVec m}, (x ++ y).getLsbD i = if i < m then y.getLsbD i else x.getLsbD (i - m)
-- Init.Data.Option.Basic
/-- For verification purposes, we replace `mapA` with `mapM`.  -/
Option.mapA_eq_mapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {o : Option α} [inst : Applicative m] {f : α → m β},
  Option.mapA f o = Option.mapM f o
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_mem_range : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p : AddMonoidAlgebra R A} (D : A → B), p ≠ 0 → AddMonoidAlgebra.supDegree D p ∈ Set.range D
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.revlexWF.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (p : Lean.Grind.CommRing.Power)
  (m : Lean.Grind.CommRing.Mon) (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
    | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) =
    h_2 p m
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_const : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β},
  s.Nonempty → ∀ (c : α), (s.inf fun x => c) = c
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_iInf : ∀ {ι : Sort u_1} (f : ι → Cardinal.{v}), Cardinal.lift.{u, v} (iInf f) = ⨅ i, Cardinal.lift.{u, v} (f i)
-- Mathlib.Algebra.Group.Even
isSquare_toMul_iff : ∀ {α : Type u_2} [inst : Mul α] {a : Additive α}, IsSquare (Additive.toMul a) ↔ Even a
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk_surjective : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {w : CategoryTheory.TwoSquare T L R B} {X₂ : C₂}
  {X₃ : C₃} {g : R.obj X₂ ⟶ B.obj X₃} (f : w.CostructuredArrowDownwards g),
  ∃ X₁ a b,
    ∃ (comm :
      CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g),
      f = CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g X₁ a b comm
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- If `checkCoeffDvd` is `true`, then when using a polynomial `k*m - p`
to simplify `.. + k'*m*m_2 + ...`, the substitution is performed IF
- `k` divides `k'`, OR
- Ring implements `NoNatZeroDivisors`.

We need this check when simplifying disequalities. In this case, if we perform
the simplification anyway, we may end up with a proof that `k * q = 0`, but
we cannot deduce `q = 0` since the ring does not implement `NoNatZeroDivisors`
See comment at `PolyDerivation`.

We also need it when destructively simplifying equations, i.e., when *replacing* an
equation with its simplified form (`EqCnstr.simplify` and `EqCnstr.simplifyBasis`):
the rewrite multiplies the equation by `k₁ = k/gcd k k'`, and the result is weaker than
the original equation when `k₁ ≠ ±1`. See **Note** at `EqCnstr.simplify`.
 -/
Lean.Meta.Grind.Arith.CommRing.RingM.Context.checkCoeffDvd : Lean.Meta.Grind.Arith.CommRing.RingM.Context → Bool
-- Mathlib.Topology.Sheaves.Alexandrov
/-- The main theorem of this file.
If `X` is a topological space and preorder whose topology is the `UpperSet` topology associated
with the preorder, `F : X ⥤ C` is a functor into a complete category from the preorder category,
and `P : (Opens X)ᵒᵖ ⥤ C` denotes the right Kan extension of `F` along the
functor `X ⥤ (Open X)ᵒᵖ` which sends `x : X` to `{y | x ≤ y}`, then `P` is a sheaf.
 -/
Topology.IsUpperSet.isSheaf_of_isRightKanExtension : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (F : CategoryTheory.Functor X C)
  (P : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C) (η : (Alexandrov.principals X).comp P ⟶ F)
  [P.IsRightKanExtension η], CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P
-- Mathlib.Data.Finset.Image
Finset.map_toFinset : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} [inst : DecidableEq α] [inst_1 : DecidableEq β] {s : Multiset α},
  Finset.map f s.toFinset = (Multiset.map (⇑f) s).toFinset
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S)
  {Y : C} {g : Y ⟶ S} {P : ι → C} {p₁ : (i : ι) → P i ⟶ Y} {p₂ : (i : ι) → P i ⟶ X i},
  (∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) →
    CategoryTheory.Sieve.ofArrows P p₁ = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.orderHom_top : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] (f : M →+o N),
  (ArchimedeanClass.orderHom f) ⊤ = ⊤
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSortM : Type → Type
-- Lean.Parser.Types
Lean.Parser.FirstTokens.tokens.injEq : ∀ (a a_1 : List Lean.Parser.Token), (Lean.Parser.FirstTokens.tokens a = Lean.Parser.FirstTokens.tokens a_1) = (a = a_1)
-- Init.Data.List.Erase
List.eraseP_filterMap : ∀ {α : Type u_1} {β : Type u_2} {p : β → Bool} {f : α → Option β} {l : List α},
  List.eraseP p (List.filterMap f l) =
    List.filterMap f
      (List.eraseP
        (fun x =>
          match f x with
          | some y => p y
          | none => false)
        l)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.localizedMap_surjective_iff_subsingleton_localized_coker : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) (φ : M →ₗ[R] N),
  Function.Surjective ⇑((LocalizedModule.map S) φ) ↔ Subsingleton (LocalizedModule S (N ⧸ φ.range))
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_one : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : AddCommMonoidWithOne R],
  Matrix.trace 1 = ↑(Fintype.card n)
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instIsScalarTower : ∀ (n : ℕ) (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K],
  IsScalarTower A K (CyclotomicField n K)
-- Init.GrindInstances.ToInt
Lean.Grind.instPowIntIi : Lean.Grind.ToInt.Pow ℤ Lean.Grind.IntInterval.ii
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.invalid.sizeOf_spec : sizeOf Std.Http.Internal.UnquoteState.invalid✝ = 1
-- Lean.Meta.SizeOf
/-- Auxiliary function for constructing an `_sizeOf_<idx>` for `ys`,
where `ys` are the indices + major.
Recall that if `info.name` is part of a mutually inductive declaration, then the resulting application
is not necessarily a `lhs.getAppFn` application.
The result is an application of one of the `(← read),sizeOfFns` functions.
We use this auxiliary function to builtin the motive of the recursor.  -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.mkSizeOfAuxLemmaProof.mkSizeOf : Subarray Lean.Expr → List Lean.Level → Array Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- Coercion from `X` to `OnePoint X`.  -/
OnePoint.some : {X : Type u_1} → X → OnePoint X
-- Init.Data.Array.Lemmas
Array.foldlM_append : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {f : β → α → m β} {b : β}
  {xs xs' : Array α},
  Array.foldlM f b (xs ++ xs') = do
    let init ← Array.foldlM f b xs
    Array.foldlM f init xs'
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.N.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) (x : G), B.N x = Filter.map (fun y => x + y) B.filter
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_right_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (z * x + y) ↔ IsRelPrime x y
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is maximized when `f` and
`g` monovary together. Stated by permuting the entries of `g`.  -/
Monovary.sum_mul_comp_perm_le_sum_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι], Monovary f g → ∑ i, f i * g (σ i) ≤ ∑ i, f i * g i
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K) =ᵐ[MeasureTheory.volume]
    interior (NumberField.mixedEmbedding.fundamentalCone.paramSet K)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.rowLens.eq_1 : ∀ (μ : YoungDiagram), μ.rowLens = List.map μ.rowLen (List.range (μ.colLen 0))
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type u_1}
  (D D_1 : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ),
  D = D_1 →
    ∀ (hι : HasCardinalLT ι κ),
      CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup D hι =
        CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup D_1 hι
-- Mathlib.Data.Seq.Computation
Computation.Results.length : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ} [_T : s.Terminates], s.Results a n → s.length = n
-- Mathlib.LinearAlgebra.Matrix.WithConv
instMulOneClassWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [MulOneClass α] → MulOneClass (WithConv (Matrix m n α))
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isPlot_iff_contDiff : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace ℝ X]
  [Diffeology.IsContDiffCompatible X] {p : EuclideanSpace ℝ (Fin n) → X}, Diffeology.IsPlot p ↔ ContDiff ℝ (↑⊤) p
-- Mathlib.Order.Category.BoolAlg
BoolAlg.comp_apply : ∀ {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.IsTrail
-- Mathlib.Order.Closure
ClosureOperator.id_apply : ∀ (α : Type u_1) [inst : Preorder α] (a : α), (ClosureOperator.id α) a = a
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.formatCategory : Lean.Name → Lean.Syntax → Lean.CoreM Std.Format
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `SummableLocallyUniformlyOn f s` means that `∑' i, f i b` converges locally
uniformly on `s` to something.  -/
SummableLocallyUniformlyOn : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → Set β → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Init.Data.Vector.Lemmas
Vector.getElem_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n} {i : ℕ}
  (hi : i < n), (Vector.zipWith f as bs)[i] = f as[i] bs[i]
-- Mathlib.Algebra.Algebra.Tower
Algebra.lsmul_eq_smul_one : ∀ (R : Type u) {A : Type w} (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] (a : A),
  (Algebra.lsmul R R M) a = a • 1
-- Mathlib.Data.Complex.Basic
Complex.ofReal_ne_one : ∀ {z : ℝ}, ↑z ≠ 1 ↔ z ≠ 1
-- Mathlib.Topology.EMetricSpace.Defs
edist_toAdd : ∀ {X : Type u_1} [inst : EDist X] (a b : Multiplicative X),
  edist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = edist a b
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_apply_pos : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M) {a : α},
  p a → (Finsupp.filter p f) a = f a
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function is asymptotically non-negative.
 -/
ValueDistribution.logCounting_eventually_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {e : WithTop E},
  0 ≤ᶠ[Filter.atTop] ValueDistribution.logCounting f e
-- Mathlib.Topology.MetricSpace.Infsep
/-- The "infimum separation" of a set with an edist function.  -/
Set.infsep : {α : Type u_1} → [EDist α] → Set α → ℝ
-- Mathlib.Algebra.Group.Defs
npowBinRec.eq_1 : ∀ {M : Type u_2} [inst : One M] [inst_1 : Mul M] (k : ℕ), npowBinRec k = npowBinRec.go k 1
-- Std.Internal.Parsec.ByteArray
/-- Skip a single byte equal to `b`, fails if different.
 -/
Std.Internal.Parsec.ByteArray.skipByte : UInt8 → Std.Internal.Parsec.ByteArray.Parser Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_constToList_perm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β},
  (Std.DHashMap.Raw.Const.toList m₁).Perm (Std.DHashMap.Raw.Const.toList m₂) → m₁.Equiv m₂
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.regular_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C), (Bimod.regular A).X = A.X
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
instIsAddKleinFourAdditiveOfIsKleinFour : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G], IsAddKleinFour (Additive G)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.foldl : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → {β : Type u_2} → (β → α → β) → β → Aesop.OrderedHashSet α → β
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mrange_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N], MonoidHom.mrange Monoid.Coprod.mk = ⊤