mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.find?.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomainLinearEquiv_single : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N) (s : S) (m : M),
  (MonoidAlgebra.mapDomainLinearEquiv R S e) (MonoidAlgebra.single m s) = MonoidAlgebra.single (e m) s
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsKernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (W : CategoryTheory.MorphismProperty C), W.kernels.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.sup'_div₀ : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : SemilatticeSup G₀] {a : G₀} [MulPosReflectLT G₀],
  0 ≤ a → ∀ (f : ι → G₀) (s : Finset ι) (hs : s.Nonempty), s.sup' hs f / a = s.sup' hs fun i => f i / a
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.coe_le_norm_of_mem : ∀ {A : Type u_3} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] [NormOneClass A] {a : A}
  {r : NNReal}, r ∈ spectrum NNReal a → ↑r ≤ ‖a‖
-- Init.Grind.Ring.Basic
/-- Zero is right absorbing for multiplication.  -/
Lean.Grind.Semiring.zero_mul : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α), 0 * a = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (t.alter k f).getKey! k' =
        if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else default else t.getKey! k'
-- Batteries.Recycling.RBTree.Basic
/-- The root of the tree, which is the end of the path of parents.  -/
RBTree.RBNode.Path.root : {α : Type u} → RBTree.RBNode.Path α
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.Isocrystal.frob : {p : ℕ} →
  {inst : Fact (Nat.Prime p)} →
    {k : Type u_1} →
      {inst_1 : CommRing k} →
        {inst_2 : CharP k p} →
          {inst_3 : PerfectRing k p} →
            {V : Type u_2} →
              {inst_4 : AddCommGroup V} →
                [self : WittVector.Isocrystal p k V] → V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α) (v : β k), m₁.Equiv m₂ → (m₁.insertIfNew k v).Equiv (m₂.insertIfNew k v)
-- Init.Data.SInt.Lemmas
Int32.toInt16_sub : ∀ (a b : Int32), (a - b).toInt16 = a.toInt16 - b.toInt16
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `sq` is the quadratic map sending the vector `x : A` to `x * x`  -/
QuadraticMap.sq : {R : Type u_3} →
  {A : Type u_7} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [SMulCommClass R A A] → [IsScalarTower R A A] → QuadraticMap R A A
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.compare.eq_def : ∀ (x x_1 : Float.Model.UnpackedFloat),
  x.compare x_1 =
    match x, x_1 with
    | Float.Model.UnpackedFloat.notANumber, x => none
    | x, Float.Model.UnpackedFloat.notANumber => none
    | Float.Model.UnpackedFloat.infinity s₁, Float.Model.UnpackedFloat.infinity s₂ => some (compare s₁ s₂)
    | Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive, x => some Ordering.gt
    | Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative, x => some Ordering.lt
    | x, Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive => some Ordering.lt
    | x, Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative => some Ordering.gt
    | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos,
      Float.Model.UnpackedFloat.zero sign => some Ordering.gt
    | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos,
      Float.Model.UnpackedFloat.zero sign => some Ordering.lt
    | Float.Model.UnpackedFloat.zero sign,
      Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos =>
      some Ordering.lt
    | Float.Model.UnpackedFloat.zero sign,
      Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos =>
      some Ordering.gt
    | Float.Model.UnpackedFloat.zero sign, Float.Model.UnpackedFloat.zero sign_1 => some Ordering.eq
    | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative m₁ e₁ mantissa_pos,
      Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative m₂ e₂ mantissa_pos_1 =>
      some ((compare e₁ e₂).then (compare m₁ m₂)).swap
    | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos,
      Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa_1 exponent_1 mantissa_pos_1 =>
      some Ordering.lt
    | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos,
      Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa_1 exponent_1 mantissa_pos_1 =>
      some Ordering.gt
    | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m₁ e₁ mantissa_pos,
      Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m₂ e₂ mantissa_pos_1 =>
      some ((compare e₁ e₂).then (compare m₁ m₂))
-- Mathlib.Topology.Inseparable
SeparationQuotient.lift₂_mk : ∀ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y → α}
  (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d) (x : X) (y : Y),
  SeparationQuotient.lift₂ f hf (SeparationQuotient.mk x) (SeparationQuotient.mk y) = f x y
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- If `a ≤ 1`, then `x = O(x ^ a)` as `x → 0`, `x ≥ 0`.  -/
Asymptotics.IsBigO.id_rpow_of_le_one : ∀ {a : ℝ}, a ≤ 1 → id =O[nhdsWithin 0 (Set.Ici 0)] fun x => x ^ a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A mono factorisation of `g ≫ f`, where `g` is an isomorphism,
gives a mono factorisation of `f`.  -/
CategoryTheory.Limits.MonoFactorisation.ofIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {X' : C} →
          (g : X' ⟶ X) →
            [CategoryTheory.IsIso g] →
              CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f) →
                CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Data.Set.Sigma
Set.sigma_inter_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i => t₁ i ∩ t₂ i
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Multiplying a `CuspForm` by a `ModularForm` gives a `CuspForm` (the cusp condition is
preserved since a function tending to zero times a bounded function tends to zero).  -/
CuspForm.mulModularForm : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  [Γ.HasDetPlusMinusOne] → {k₁ k₂ : ℤ} → CuspForm Γ k₁ → ModularForm Γ k₂ → CuspForm Γ (k₁ + k₂)
-- Mathlib.Topology.Algebra.Monoid
ContinuousMul.to_continuousSMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], ContinuousSMul M M
-- Init.GetElem
outOfBounds : {α : Sort u_1} → [Inhabited α] → α
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instSubHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → Sub (T₁ ⟶ T₂)
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceFrom_le_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  String.Pos.ofSliceFrom p ≤ q ↔ ∃ (h : p₀ ≤ q), p ≤ p₀.sliceFrom q h
-- Mathlib.RingTheory.PowerSeries.Order
/-- The operation of dividing a power series by the largest possible power of `X`
preserves multiplication.  -/
PowerSeries.divXPowOrder_mul : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] {f g : PowerSeries R},
  (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.toBallPackage : {β : Type u_1} → {α : Type u_2} → Besicovitch.TauPackage β α → Besicovitch.BallPackage β α
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.instIsOrderedAddMonoidId : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  IsOrderedAddMonoid (E →ₗ[𝕜] E)
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesLimitsOfShape : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C],
  (CategoryTheory.ObjectProperty.preservesLimitsOfShape K).IsClosedUnderIsomorphisms
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot.eq_1 : ∀ (n a : ℕ), n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ ((k + n - 1) / n)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_univ : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Finset.univᶜ = ∅
-- Mathlib.GroupTheory.Coset.Basic
mem_leftAddCoset : ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → a + x ∈ a +ᵥ s
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ico_mul_Ioc_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Ico a b * Finset.Ioc c d ⊆ Finset.Ioo (a * c) (b * d)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_monoLM_eq : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E} {i : ℕ},
  n₁ = n₂ →
    K₁ ≤ K₂ →
      ∀ (f : ContDiffMapSupportedIn E F n₁ K₁),
        (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((ContDiffMapSupportedIn.monoLM 𝕜) f) =
          (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.ncard_sdiff_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → (B₁ \ B₂).ncard = (B₂ \ B₁).ncard
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coe_measurableEquivPiIoc : ∀ {ι : Type u_2} (b : ι → ℝ),
  ⇑(UnitAddTorus.measurableEquivPiIoc b) = fun x => ⟨fun i => ↑((AddCircle.equivIoc 1 (b i)) (x i)), ⋯⟩
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.IsCartanSubalgebra.mk : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {H : LieSubalgebra R L},
  LieRing.IsNilpotent ↥H → H.normalizer = H → H.IsCartanSubalgebra
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The "naive" presentation of `T = R[X₁, ..., Xₙ] / (b₁, ..., bᵣ)` over `R`.
We make sure the section `T → R[X₁, ..., Xₙ]` maps `-1` to `-1` and `0` to `0`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Algebra.Presentation R (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) ι σ
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sumInv.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι],
  AdicCompletion.sumInv I M =
    ↑(DirectSum.linearEquivFunOnFintype (AdicCompletion I R) ι fun j => AdicCompletion I (M j)).symm ∘ₗ
      AdicCompletion.pi I M ∘ₗ AdicCompletion.map I ↑(DirectSum.linearEquivFunOnFintype R ι M)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- For `j + l ≤ n`, a path of length `n` restricts to a path of length `l`, namely
the subpath spanned by the vertices `j ≤ i ≤ j + l` and edges `j ≤ i < j + l`.  -/
SSet.Path.interval : {X : SSet} → {n : ℕ} → X.Path n → (j l : ℕ) → autoParam (j + l ≤ n) SSet.Path.interval._auto_1 → X.Path l
-- Mathlib.Topology.Spectral.Hom
SpectralMap.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : SpectralMap α β},
  f.toFun = ⇑f
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Meta.transformWithCache.visit.visitForall : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            Bool →
              Bool →
                Bool →
                  (x : STWorld IO.RealWorld m) →
                    MonadLiftT (ST IO.RealWorld) m →
                      Array Lean.Expr → Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Init.Omega.Constraint
/-- Negate a constraint. `[x, y]` becomes `[-y, -x]`.
 -/
Lean.Omega.Constraint.neg : Lean.Omega.Constraint → Lean.Omega.Constraint
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))
      (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial)
        ((AlgebraicGeometry.Spec R).residue x))
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.mk.injEq : ∀ {α : Type u} (lower upper lower_1 upper_1 : α),
  ((lower<...=upper) = lower_1<...=upper_1) = (lower = lower_1 ∧ upper = upper_1)
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.mk : ∀ {X : Type u_3} [t : TopologicalSpace X],
  (∃ m, PseudoMetricSpace.toUniformSpace.toTopologicalSpace = t ∧ CompleteSpace X) →
    TopologicalSpace.IsCompletelyPseudoMetrizableSpace X
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.invalidHeader.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.invalidHeader = 1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_def : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), a⁻ = cfcₙ (fun x => x⁻) a
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- `reflectsColimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsColimitsOfSize.{w w'} F`
from some other `reflectsColimitsOfSize F`.
 -/
CategoryTheory.Limits.reflectsColimitsOfSize_shrink : ∀ {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.ReflectsColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_inv : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ), ↑r⁻¹ = (↑r)⁻¹
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.SurjectiveOnWith.surjOn : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : ℝ}, f.SurjectiveOnWith K C → Set.SurjOn (⇑f) Set.univ ↑K
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Connected.ofBoxProdLeft : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β}, (G □ H).Connected → G.Connected
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The left point of the walking span.  -/
CategoryTheory.Limits.WalkingSpan.left : CategoryTheory.Limits.WalkingSpan
-- Mathlib.Topology.Category.Profinite.Basic
/-- The pi-type of profinite spaces is profinite.  -/
Profinite.pi : {α : Type u} → (α → Profinite) → Profinite
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.enorm_lid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 𝕜 E), ‖(TensorProduct.lid 𝕜 E) x‖ₑ = ‖x‖ₑ
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_3.eq_1 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (y : Dyadic) (h_1 : (y : Dyadic) → motive Dyadic.zero y)
  (h_2 : (x : Dyadic) → motive x Dyadic.zero)
  (h_3 :
    (n₁ k₁ : ℤ) →
      (hn₁ : n₁ % 2 = 1) → (n₂ k₂ : ℤ) → (hn₂ : n₂ % 2 = 1) → motive (Dyadic.ofOdd n₁ k₁ hn₁) (Dyadic.ofOdd n₂ k₂ hn₂)),
  (match Dyadic.zero, y with
    | Dyadic.zero, y => h_1 y
    | x, Dyadic.zero => h_2 x
    | Dyadic.ofOdd n₁ k₁ hn₁, Dyadic.ofOdd n₂ k₂ hn₂ => h_3 n₁ k₁ hn₁ n₂ k₂ hn₂) =
    h_1 y
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnP_spec.flatten_zipWith : ∀ {α : Type u_1} {xs ys : List (List α)} {a : α},
  xs ≠ [] →
    ys ≠ [] →
      (List.zipWith (fun x x_1 => x ++ x_1) (List.modifyHead (List.cons a) xs) ys).flatten =
        a :: (List.zipWith (fun x x_1 => x ++ x_1) xs ys).flatten
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_or_isNonloop : ∀ {α : Type u_1} (M : Matroid α) (e : α),
  autoParam (e ∈ M.E) Matroid.isLoop_or_isNonloop._auto_1 → M.IsLoop e ∨ M.IsNonloop e
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_eq : ∀ {R : Type u_1} {a b u₀ : R} [inst : Field R],
  a ≠ 1 → ∀ (n : ℕ), arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddCommSemigroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddCommSemigroup α] → AddCommSemigroup (Shrink.{v, u_2} α)
-- Mathlib.Algebra.Group.ULift
ULift.semigroup.eq_1 : ∀ {α : Type u} [inst : Semigroup α], ULift.semigroup = Function.Injective.semigroup ⇑MulEquiv.ulift ⋯ ⋯
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_false : Nat.bit false = fun x => 2 * x
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.map_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  CategoryTheory.Epi (F.map f)
-- Mathlib.Algebra.Algebra.Unitization
/-- `starMap` is functorial:
`starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)`.  -/
Unitization.starMap_id : ∀ {R : Type u_1} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring B]
  [inst_3 : StarRing B] [inst_4 : Module R B] [inst_5 : SMulCommClass R B B] [inst_6 : IsScalarTower R B B]
  [inst_7 : StarModule R B], Unitization.starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Right Kan extensions of isomorphic functors are isomorphic.  -/
CategoryTheory.Functor.rightKanExtensionUniqueOfIso : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] →
                      {G : CategoryTheory.Functor C H} →
                        (F ≅ G) →
                          (G' : CategoryTheory.Functor D H) → (β : L.comp G' ⟶ G) → [G'.IsRightKanExtension β] → F' ≅ G'
-- Mathlib.Algebra.Group.End
AddAutAdditive_symm_apply_symm_apply : ∀ (G : Type u_3) [inst : Group G] (a : G ≃* G) (a_1 : Additive G),
  (AddEquiv.symm ((AddAutAdditive G).symm a)) a_1 = Additive.ofMul (a.symm (Additive.toMul a_1))
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodCongr_toContinuousAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [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₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄),
  (e₁.prodCongr e₂).toContinuousAffineMap = e₁.toContinuousAffineMap.prodMap e₂.toContinuousAffineMap
-- Std.Data.HashSet.Basic
/-- Computes the union of the given hash sets.

This function always merges the smaller set into the larger set, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashSet.union : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → Std.HashSet α → Std.HashSet α
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.continuousAt : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X},
  IsCoveringMapOn f s → ∀ {x : E}, f x ∈ s → ContinuousAt f x
-- Std.Do.SPred.Laws
Std.Do.SPred.and_intro : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ Q) → (P ⊢ₛ R) → P ⊢ₛ Q ∧ R
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Module.Basis.map_addHaar : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : MeasurableSpace E]
  [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace E] [inst_8 : BorelSpace F] [SecondCountableTopology F]
  [SigmaCompactSpace F] (b : Module.Basis ι ℝ E) (f : E ≃L[ℝ] F),
  MeasureTheory.Measure.map (⇑f) b.addHaar = (b.map ↑f).addHaar
-- Init.Data.Vector.Lemmas
Vector.getElem_singleton : ∀ {α : Type u_1} {i : ℕ} {a : α} (h : i < 1), #v[a][i] = a
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toBitVec = n#'hn
-- Lean.Data.KVMap
Lean.instInhabitedKVMap : Inhabited Lean.KVMap
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
instMeasurableSpaceOrderDual : {α : Type u_1} → [h : MeasurableSpace α] → MeasurableSpace αᵒᵈ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_zero : ∀ {α : Type u_2} [inst : Zero α] {a : α}, a ∈ 0 ↔ a = 0
-- Init.MetaTypes
/-- When `index` (default : `true`) is `false`, `simp` will only use the root symbol
to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
 -/
Lean.Meta.Simp.Config.index : Lean.Meta.Simp.Config → Bool