mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.Extend
/-- Composition of a semilinear map `f` with the left inverse of a linear map `g` as a continuous
linear map provided that the norm estimate `‖f x‖ ≤ C * ‖g x‖` holds for all `x : E`.  -/
LinearMap.compLeftInverse : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          [inst : DivisionRing 𝕜] →
            [inst_1 : DivisionRing 𝕜₂] →
              {σ₁₂ : 𝕜 →+* 𝕜₂} →
                [inst_2 : AddCommGroup E] →
                  [inst_3 : NormedAddCommGroup F] →
                    [inst_4 : SeminormedAddCommGroup Eₗ] →
                      [inst_5 : Module 𝕜 E] →
                        [inst_6 : Module 𝕜₂ F] →
                          [inst_7 : Module 𝕜 Eₗ] → (E →ₛₗ[σ₁₂] F) → (g : E →ₗ[𝕜] Eₗ) → ↥g.range →SL[σ₁₂] F
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- Functoriality of `TrivSqZeroExt` when the ring is commutative: a linear map
`f : M →ₗ[R'] N` induces a morphism of `R'`-algebras from `TrivSqZeroExt R' M` to
`TrivSqZeroExt R' N`.

Note that we cannot neatly state the non-commutative case, as we do not have morphisms of bimodules.
 -/
TrivSqZeroExt.map : {R' : Type u} →
  {M : Type v} →
    [inst : CommSemiring R'] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R' M] →
          [inst_3 : Module R'ᵐᵒᵖ M] →
            [inst_4 : IsCentralScalar R' M] →
              {N : Type u_3} →
                [inst_5 : AddCommMonoid N] →
                  [inst_6 : Module R' N] →
                    [inst_7 : Module R'ᵐᵒᵖ N] →
                      [inst_8 : IsCentralScalar R' N] → (M →ₗ[R'] N) → TrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R (n - 1) = 2 * Polynomial.X * Polynomial.Chebyshev.T R n - Polynomial.Chebyshev.T R (n + 1)
-- Aesop.Forward.State
/-- Update the pattern substitutions after the goal's target changed.
`goal` is the new goal. `newPatSubsts` are the new target's pattern
substitutions.  -/
Aesop.ForwardState.enqueueTargetPatSubsts : Array (Aesop.ForwardRule × Aesop.Substitution) → Aesop.ForwardState → Aesop.ForwardState
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k fallback : α},
  k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKeyD k fallback = fallback
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.of_mul_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : CommSemigroup α] [MulLeftMono α] {a b : α},
  MulLECancellable (a * b) → MulLECancellable a
-- Mathlib.CategoryTheory.Enriched.Opposite
CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] (C : Type u) [inst_3 : CategoryTheory.EnrichedCategory V C],
  (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse V C).comp
                (CategoryTheory.forgetEnrichmentOppositeEquivalence.functor V C)).obj
            x))
      ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap'_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) h₂.g' =
    CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃
-- Lean.DocString.Extension
Lean.VersoModuleDocs.terminalNesting : Lean.VersoModuleDocs → Option ℕ
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.homCategory_id_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (Γ : F ⟶ G) (a : B),
  (CategoryTheory.CategoryStruct.id Γ).as.app a = CategoryTheory.CategoryStruct.id (Γ.app a)
-- Mathlib.Algebra.DirectSum.Basic
DFinsupp.comapDomain.congr_simp : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h)
  (f f_1 : Π₀ (i : ι), β i), f = f_1 → DFinsupp.comapDomain h hh f = DFinsupp.comapDomain h hh f_1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.mem_support_iff_mem_support_of_mem_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {x : α},
  x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
-- Mathlib.Topology.Algebra.Group.Pointwise
add_singleton_mem_nhds_of_nhds_zero : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α),
  s ∈ nhds 0 → s + {a} ∈ nhds a
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_bitwise_distrib : ∀ {f : Bool → Bool → Bool} {i a b : ℕ},
  autoParam (f false false = false) Nat.shiftLeft_bitwise_distrib._auto_5 →
    Nat.bitwise f a b <<< i = Nat.bitwise f (a <<< i) (b <<< i)
-- Mathlib.Order.Monotone.Defs
StrictMono.comp_strictAnti : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, StrictMono g → StrictAnti f → StrictAnti (g ∘ f)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.StrongEpiMonoFactorisation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (toMonoFactorisation : CategoryTheory.Limits.MonoFactorisation f)
  [e_strong_epi : CategoryTheory.StrongEpi toMonoFactorisation.e]
  (toMonoFactorisation_1 : CategoryTheory.Limits.MonoFactorisation f)
  (e_strong_epi_1 : CategoryTheory.StrongEpi toMonoFactorisation_1.e),
  ({ toMonoFactorisation := toMonoFactorisation, e_strong_epi := e_strong_epi } =
      { toMonoFactorisation := toMonoFactorisation_1, e_strong_epi := e_strong_epi_1 }) =
    (toMonoFactorisation = toMonoFactorisation_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.instMonoidalCategory : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategory (CoalgCat R)
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.coe_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), ⇑(AlgEquiv.restrictScalars R f) = ⇑f
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.refl_invLHom : ∀ (L : FirstOrder.Language), (FirstOrder.Language.LEquiv.refl L).invLHom = FirstOrder.Language.LHom.id L
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.min_le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, min ↑a ↑b ≤ ↑c ↔ min a b ≤ c
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.map_toCotangent_ker : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), Submodule.map (Submodule.subtype I) I.toCotangent.ker = I ^ 2
-- Init.Prelude
/-- Return the underlying `Nat` that represents a bitvector.

This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`.
 -/
BitVec.toNat : {w : ℕ} → BitVec w → ℕ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackId.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)],
  CategoryTheory.ChosenPullbacksAlong.pullbackId X =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).rightAdjointUniq
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Algebra.Torsor.Basic
Set.zero_mem_vsub_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {s t : Set P}, 0 ∈ s -ᵥ t ↔ ¬Disjoint s t
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.toLinearMap : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} → {B₂ : LinearMap.BilinForm R M₂} → (B₁ →bᵢ B₂) → M₁ →ₗ[R] M₂
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.length_toList_roc : ∀ {a b : ℕ}, (a<...=b).toList.length = b - a
-- Init.Data.List.Sublist
List.IsInfix.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁ <:+: l₂ → a ∈ l₂
-- Mathlib.Topology.Separation.Connected
PreconnectedSpace.infinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PreconnectedSpace X] [Nontrivial X] [T1Space X], Infinite X
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.toPreZeroHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreOneHypercover S → CategoryTheory.PreZeroHypercover S
-- Mathlib.Analysis.InnerProductSpace.Calculus
Differentiable.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E},
  Differentiable ℝ f → Differentiable ℝ fun y => ‖f y‖ ^ 2
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom_monomial : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a) (e : σ →₀ ℕ) (r : R),
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.monomial e) r) =
    (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n => a s ^ n
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.mulRec.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (s : ℕ) (h_1 : Unit → motive 0) (h_2 : (s : ℕ) → motive s.succ),
  (match s.succ with
    | 0 => h_1 ()
    | s.succ => h_2 s) =
    h_2 s
-- Lean.Parser.Extra
Lean.Parser.notSymbol.formatter : String → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.commRing : {R : Type u_1} → {M : Type u_4} → [inst : CommRing R] → [AddCommMonoid M] → CommRing (AddMonoidAlgebra R M)
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_zero : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B]
  [FiniteDimensional (FractionRing A) (FractionRing B)], (Algebra.intNorm A B) 0 = 0
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- One of the components of the iterated derivative of a multilinear map. Given a bijection `e`
between a type `α` (typically `Fin k`) and a subset `s` of `ι`, this component is a multilinear map
of `k` vectors `v₁, ..., vₖ`, mapping them to `f (x₁, (v_{e.symm 2})₂, x₃, ...)`, where at
indices `i` in `s` one uses the `i`-th coordinate of the vector `v_{e.symm i}` and otherwise one
uses the `i`-th coordinate of a reference vector `x`.
This is multilinear in the components of `x` outside of `s`, and in the `v_j`.  -/
MultilinearMap.iteratedFDerivComponent : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  {α : Type u_1} →
                    MultilinearMap R M₁ M₂ →
                      {s : Set ι} →
                        α ≃ ↑s →
                          [DecidablePred fun x => x ∈ s] →
                            MultilinearMap R (fun i => M₁ ↑i) (MultilinearMap R (fun x => (i : ι) → M₁ i) M₂)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), (∀ t ∈ I, t ⊆ s) → ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = s
-- Mathlib.Analysis.Normed.Group.Basic
norm_zpow_isUnit : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E) {n : ℤ}, IsUnit n → ‖a ^ n‖ = ‖a‖
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.enorm_toContinuousMultilinearMap : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F), ‖f.toContinuousMultilinearMap‖ₑ = ‖f‖ₑ
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The product of two affine maps is an affine map.  -/
AffineMap.prod : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          {V3 : Type u_6} →
            {P3 : Type u_7} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V1] →
                  [inst_2 : Module k V1] →
                    [inst_3 : AddTorsor V1 P1] →
                      [inst_4 : AddCommGroup V2] →
                        [inst_5 : Module k V2] →
                          [inst_6 : AddTorsor V2 P2] →
                            [inst_7 : AddCommGroup V3] →
                              [inst_8 : Module k V3] →
                                [inst_9 : AddTorsor V3 P3] → (P1 →ᵃ[k] P2) → (P1 →ᵃ[k] P3) → P1 →ᵃ[k] P2 × P3
-- Mathlib.Testing.Plausible.Functions
Plausible.instInhabitedInjectiveFunction : {α : Type u} → Inhabited (Plausible.InjectiveFunction α)
-- Init.Data.SInt.Lemmas
Int16.lt_iff_toBitVec_slt : ∀ {a b : Int16}, a < b ↔ a.toBitVec.slt b.toBitVec = true
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.spanning_iff_exists_isBase_subset : ∀ {α : Type u_2} {M : Matroid α} {S : Set α},
  autoParam (S ⊆ M.E) Matroid.spanning_iff_exists_isBase_subset._auto_1 → (M.Spanning S ↔ ∃ B, M.IsBase B ∧ B ⊆ S)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.mk.injEq : ∀ (carrier : Type u) [str : CommMonoid carrier] (carrier_1 : Type u) (str_1 : CommMonoid carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.factorₐ_comp_liftAdicCompletionAux_of_le : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (I : Ideal S) (f : A →ₐ[R] S ⧸ I) [inst_5 : Algebra.FormallySmooth R A]
  {m n : ℕ} (hn : m ≤ n),
  (Ideal.Quotient.factorₐ R ⋯).comp (Algebra.FormallySmooth.liftAdicCompletionAux✝ I f n) =
    Algebra.FormallySmooth.liftAdicCompletionAux✝ I f m
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.ordConnected_setOfPred_eball_subset`. -/
Metric.ordConnected_setOf_eball_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), {r | Metric.eball x r ⊆ s}.OrdConnected
-- Init.Data.List.Basic
List.isPrefixOf.eq_2 : ∀ {α : Type u} [inst : BEq α] (x : List α), (x = [] → False) → x.isPrefixOf [] = false
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
Differentiable.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} [Finite ι],
  Differentiable 𝕜 c → ∀ (u : (i : ι) → M i), Differentiable 𝕜 fun y => (c y) u
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.left : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop}, Nat.RecursiveIn.below ⋯
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.codRestrict_apply_coe : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ (v : ι → M), f v ∈ p)
  (v : (i : ι) → (fun x => M) i), ↑((f.codRestrict p h) v) = f v
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.testBit_succ_zero : ∀ {x : ℕ}, (x + 1).testBit 0 = !x.testBit 0
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.instInhabitedEntry.default : Lean.Compiler.CSimp.Entry
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.iso_hom : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y),
  (CategoryTheory.PreservesImage.iso L f).hom =
    CategoryTheory.Limits.image.lift
      { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯,
        e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯ }
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.length_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.toList.length = m.size
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (start : ℕ) (x : aig.RefVec w)
  (start_1 : ℕ) (x_1 : aig.RefVec w),
  ({ start := start, x := x } = { start := start_1, x := x_1 }) = (start = start_1 ∧ x = x_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The bijection `(stdSimplex.obj n).op.obj d ≃ (stdSimplex.obj n).obj d` for any
`n : ℕ` and `d : ℕ`. See also `stdSimplex.opIso`.  -/
SSet.stdSimplex.opObjEquiv : {n : SimplexCategory} → {d : SimplexCategoryᵒᵖ} → (SSet.stdSimplex.obj n).op.obj d ≃ (SSet.stdSimplex.obj n).obj d
-- Init.Data.BitVec.Lemmas
BitVec.mul_one : ∀ {w : ℕ} (x : BitVec w), x * 1#w = x
-- Lean.Message
Lean.MessageData.tagged.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : Lean.MessageData), sizeOf (Lean.MessageData.tagged a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP.go_acc : ∀ {α : Type u_1} {p : α → Bool} {xs acc : List α},
  List.splitOnPPrepend p xs acc = List.modifyHead (fun x => acc.reverse ++ x) (List.splitOnP p xs)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeleton_mono : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  {n m : ℕ∞}, m ≤ n → ↑(Topology.RelCWComplex.skeleton C m) ⊆ ↑(Topology.RelCWComplex.skeleton C n)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseQuarterNarrow : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Month.Quarter
-- Lean.Meta.ArgsPacker.Basic
Lean.Meta.ArgsPacker.mk : Array (Array Lean.Name) → Lean.Meta.ArgsPacker
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toEquiv_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective BialgEquiv.toEquiv
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.orderTop_hsum_binomialFamily_pos : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] {x : HahnSeries Γ A},
  0 < (x - 1).orderTop → ∀ (r : R), 0 < ((HahnSeries.SummableFamily.binomialFamily x r).hsum - 1).orderTop
-- Mathlib.Data.Finsupp.Basic
Rat.cast_finsuppProd : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_10} [inst : Zero M] (f : α →₀ M) [inst_1 : Field R] [CharZero R]
  (g : α → M → ℚ), ↑(f.prod g) = f.prod fun a b => ↑(g a b)
-- Mathlib.Algebra.Star.Basic
star_ofNat : ∀ {R : Type u} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (n : ℕ) [inst_2 : n.AtLeastTwo],
  star (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
_private.Mathlib.LinearAlgebra.RootSystem.BaseExists.0.RootPairing.baseOf_root_eq_baseOf_coroot_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] (f : M →+ ℚ) (g : N →+ ℚ),
  (∀ (i : ι), f (P.root i) ≠ 0) →
    (∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)) →
      IsAddIndecomposable.baseOf (⇑P.root) f ⊆ IsAddIndecomposable.baseOf (⇑P.coroot) g
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The odd Hurwitz zeta function is differentiable everywhere.  -/
HurwitzZeta.differentiable_hurwitzZetaOdd : ∀ (a : UnitAddCircle), Differentiable ℂ (HurwitzZeta.hurwitzZetaOdd a)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The refl quiver underlying a nerve is naturally isomorphic to the refl quiver underlying the
category.  -/
SSet.OneTruncation₂.ofNerve₂.natIso : CategoryTheory.Nerve.nerveFunctor₂.comp SSet.oneTruncation₂ ≅ CategoryTheory.ReflQuiv.forget
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.toInt : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.homotopyEquiv_homotopyHomInvId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  (HomologicalComplex.pathObject.homotopyEquiv K hc).homotopyHomInvId = Homotopy.ofEq ⋯
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.funLike : {α : Type u_1} → {β : Type u_2} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → FunLike (α →ᵈ β) α β
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Auxiliary function for the construction of the reverse direction of the stereographic
projection.  This is a map from the orthogonal complement of a unit vector `v` in an inner product
space `E` to `E`; we will later prove that it takes values in the unit sphere.

For most purposes, use `stereoInvFun`, not `stereoInvFunAux`.  -/
stereoInvFunAux : {E : Type u_1} → [inst : NormedAddCommGroup E] → [InnerProductSpace ℝ E] → E → E → E