mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Another formulation of the reflection formula in terms of `Gammaℝ`.  -/
Complex.Gammaℝ_div_Gammaℝ_one_sub : ∀ {s : ℂ}, (∀ (n : ℕ), s ≠ -(2 * ↑n + 1)) → s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * Complex.cos (↑Real.pi * s / 2)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The kernel of `biproduct.π f i` is the inclusion from the biproduct which omits `i`
from the index set `J` into the biproduct over `J`.  -/
CategoryTheory.Limits.biproduct.isLimitFromSubtype : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          (i : J) →
            [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
              [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)] →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f fun j => j ≠ i)
                    ⋯)
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.PrecheckM : Type → Type
-- Mathlib.Control.Bitraversable.Instances
instBitraversableBicompl : {t : Type u → Type u → Type u} →
  [Bitraversable t] →
    (F G : Type u → Type u) → [Traversable F] → [Traversable G] → Bitraversable (Function.bicompl t F G)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank.eq_1 : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  p.spanFinrank = Cardinal.toNat p.spanRank
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Implementation of the tensor product for `CartesianMonoidalCategory.ofChosenFiniteProducts`.  -/
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    ((X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) → C → C → C
-- Batteries.Data.List.Basic
/-- Auxiliary for `zipWithLeftTR`: `zipWithLeftTR.go l acc = acc.toList ++ zipWithLeft l`.  -/
List.zipWithLeftTR.go : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → Array γ → List γ
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.mk : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_4} [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B],
  FaithfulSMul G B → SMulCommClass G A B → Algebra.IsInvariant A B G → IsGaloisGroup G A B
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPCOfShape.of_equiv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C] {ι' : Type u_3}
  [inst_2 : CategoryTheory.Limits.HasProductsOfShape ι' C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C]
  (e : ι ≃ ι'), CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_1, u_1} ι' C
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_refl : ∀ {R : Type u_4} [inst : Mul R] [inst_1 : Add R], (RingEquiv.refl R).symm = RingEquiv.refl R
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.mem_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e → e ∈ M.E
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unop_comp : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z},
  (CategoryTheory.CategoryStruct.comp f g).unop = CategoryTheory.CategoryStruct.comp g.unop f.unop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instCompleteSemilatticeSup : {X : AlgebraicGeometry.Scheme} → CompleteSemilatticeSup X.IdealSheafData
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.exists_of_closure_ssubset : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α}, M.closure X ⊂ M.closure Y → ∃ e ∈ Y, e ∉ M.closure X
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.mapsTo_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → K ≠ 0 → ∀ (x : α) (r : ℝ), Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) (↑K * r))
-- Mathlib.Data.Set.Semiring
SetSemiring.instOne : {α : Type u_1} → [One α] → One (SetSemiring α)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_comp : ∀ {X Y : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (SSet.yonedaEquiv.symm x) f =
    SSet.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op n))) x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_erase_eq_of_not_compare_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, ¬cmp k (t.minKey ⋯) = Ordering.eq → (t.erase k).minKey he = t.minKey ⋯
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.comp_mk₀_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] [inst_5 : W.IsCompatibleWithShift M]
  {m : M} (α : CategoryTheory.Localization.SmallShiftedHom W X Y m) (m₀ : M) (hm₀ : m₀ = 0),
  α.comp (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ (CategoryTheory.CategoryStruct.id Y)) ⋯ = α
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.bihimp : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
  MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (bihimp s₁ s₂)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.restrict : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn f s (μ.restrict t)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.id_lift_eqToHom_codomain : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} (hRS : R = S) {b : 𝒳},
  p.obj b = S → p.IsHomLift (CategoryTheory.eqToHom hRS) (CategoryTheory.CategoryStruct.id b)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.IsArithmetic.is_commensurable : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [self : 𝒢.IsArithmetic], 𝒢.Commensurable (Matrix.SpecialLinearGroup.mapGL ℝ).range
-- Mathlib.Analysis.SpecificLimits.Basic
summable_geometric_two' : ∀ (a : ℝ), Summable fun n => a / 2 / 2 ^ n
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.toPushforwardOfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) {ℱ : TopCat.Presheaf C X}
  {𝒢 : TopCat.Presheaf C Y} (α : (TopCat.Presheaf.pushforward C H.hom).obj ℱ ⟶ 𝒢),
  TopCat.Presheaf.toPushforwardOfIso H α = ((TopCat.Presheaf.presheafEquivOfIso C H).toAdjunction.homEquiv ℱ 𝒢) α
-- Mathlib.Data.Finset.MulAntidiagonal
Set.IsWF.add : ∀ {α : Type u_1} {s t : Set α} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedCancelAddMonoid α],
  s.IsWF → t.IsWF → (s + t).IsWF
-- Mathlib.Algebra.Module.PointwisePi
vadd_univ_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → VAdd K (R i)] (r : K) (t : (i : ι) → Set (R i)),
  r +ᵥ Set.univ.pi t = Set.univ.pi (r +ᵥ t)
-- Mathlib.Algebra.GroupWithZero.Associated
/-- See also `Irreducible.coprime_iff_not_dvd`.  -/
Irreducible.isRelPrime_iff_not_dvd : ∀ {M : Type u_1} [inst : Monoid M] {p n : M}, Irreducible p → (IsRelPrime p n ↔ ¬p ∣ n)
-- Lean.Meta.PProdN
/-- Essentially a form of `foldrM1`. Underlies `pack` and `mk`, and is useful to construct proofs
that should follow the structure of `pack` and `mk` (e.g. admissibility proofs)
 -/
Lean.Meta.PProdN.genMk : {α : Type} → [Inhabited α] → (α → α → Lean.MetaM α) → Array α → Lean.MetaM α
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable on `[a, ∞)`, and `f =O[atTop] g`, for some
`g` integrable at `atTop`, then `f` is integrable on `[a, ∞)`.  -/
MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F} {a : α}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : LinearOrder α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated],
  MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ →
    f =O[Filter.atTop] g →
      MeasureTheory.IntegrableAtFilter g Filter.atTop μ → MeasureTheory.IntegrableOn f (Set.Ici a) μ
-- Init.Control.Lawful.MonadLift.Basic
LawfulMonadLift.mk : ∀ {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n]
  [inst_2 : MonadLift m n],
  (∀ {α : Type u} (a : α), MonadLift.monadLift (pure a) = pure a) →
    (∀ {α β : Type u} (ma : m α) (f : α → m β),
        MonadLift.monadLift (ma >>= f) = do
          let x ← MonadLift.monadLift ma
          MonadLift.monadLift (f x)) →
      LawfulMonadLift m n
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C} (f : X ⟶ Y),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.map f).right =
    f.app (Opposite.op CategoryTheory.WithInitial.star)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F]
  (G : CategoryTheory.Functor D H) (α : F ⟶ L.comp G) (Y : D),
  ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
      (L.costructuredArrowMapCocone F G α Y)
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.instMonadAttachExceptTOfMonad.match_1.eq_2 : ∀ {m : Type (max u_1 u_2) → Type u_3} {ε : Type (max u_1 u_2)} [inst : MonadAttach m] {α : Type (max u_1 u_2)}
  (x : ExceptT ε m α) (motive : (a : Except ε α) → MonadAttach.CanReturn x a → Sort u_4) (e : ε)
  (h : MonadAttach.CanReturn x (Except.error e))
  (h_1 : (a : α) → (h : MonadAttach.CanReturn x (Except.ok a)) → motive (Except.ok a) h)
  (h_2 : (e : ε) → (h : MonadAttach.CanReturn x (Except.error e)) → motive (Except.error e) h),
  (match Except.error e, h with
    | Except.ok a, h => h_1 a h
    | Except.error e, h => h_2 e h) =
    h_2 e h
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_zsmul : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℤ), (n • α).app X = n • α.app X
-- Mathlib.Data.Nat.Choose.Vandermonde
/-- The sum of entries squared in a row of Pascal's triangle  -/
Nat.sum_range_choose_sq : ∀ (n : ℕ), ∑ i ∈ Finset.range (n + 1), n.choose i ^ 2 = (2 * n).choose n
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- `Fix F` is a functor  -/
MvQPF.Fix.map : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α β : TypeVec.{u} n} → α.Arrow β → MvQPF.Fix F α → MvQPF.Fix F β
-- Mathlib.RingTheory.EssentialFiniteness
/-- A submonoid of `EssFiniteType.subalgebra R S`, whose localization is the whole algebra `S`.  -/
Algebra.EssFiniteType.submonoid : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [inst_3 : Algebra.EssFiniteType R S] → Submonoid ↥(Algebra.EssFiniteType.subalgebra R S)
-- Mathlib.Order.Monotone.Basic
_private.Mathlib.Order.Monotone.Basic.0.Nat.stabilises_of_monotone.strictMono : ∀ {f : ℕ → ℕ} {b : ℕ}, Monotone f → (∀ m ≤ b, f m ≠ f (m + 1)) → ∀ m ≤ b + 1, m ≤ f m
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.le_comap_map : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C),
  S ≤ CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.map φ hφ S)
-- Init.MetaTypes
Lean.Meta.Simp.ConfigCtx.mk.injEq : ∀ (toConfig toConfig_1 : Lean.Meta.Simp.Config),
  ({ toConfig := toConfig } = { toConfig := toConfig_1 }) = (toConfig = toConfig_1)
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Entry.mk.injEq : ∀ (declName optionName declName_1 optionName_1 : Lean.Name),
  ({ declName := declName, optionName := optionName } = { declName := declName_1, optionName := optionName_1 }) =
    (declName = declName_1 ∧ optionName = optionName_1)
-- Lean.Language.Basic
/-- Context of an input processing invocation.  -/
Lean.Language.ProcessingContext : Type
-- Mathlib.RingTheory.PicardGroup
Submodule.ker_unitsToPic : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A], (Submodule.unitsToPic R A).ker = (Units.map ↑(Submodule.spanSingleton R)).range
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isUVar : Lean.Name → Bool
-- Batteries.Data.Fin.Fold
Fin.dfoldrM_zero : ∀ {m : Type u_1 → Type u_2} {α : Fin (0 + 1) → Type u_1} [inst : Monad m]
  (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α (Fin.last 0)), Fin.dfoldrM 0 α f x = pure x
-- Std.Http.Server.Connection
Std.Http.Server.Connection.mk.inj : ∀ {α : Type} {socket : α} {machine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving}
  {extensions : Std.Http.Extensions} {socket_1 : α}
  {machine_1 : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving}
  {extensions_1 : Std.Http.Extensions},
  { socket := socket, machine := machine, extensions := extensions } =
      { socket := socket_1, machine := machine_1, extensions := extensions_1 } →
    socket = socket_1 ∧ machine = machine_1 ∧ extensions = extensions_1
-- Mathlib.Data.Set.Card
Set.Infinite.exists_superset_ncard_eq : ∀ {α : Type u_1} {s t : Set α},
  t.Infinite → s ⊆ t → s.Finite → ∀ {k : ℕ}, s.ncard ≤ k → ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
-- Lean.Meta.Basic
Lean.Meta.mkFreshLevelMVarsFor : Lean.ConstantInfo → Lean.MetaM (List Lean.Level)
-- Init.Data.String.Lemmas.Order
String.Pos.le_startPos : ∀ {s : String} (p : s.Pos), p ≤ s.startPos ↔ p = s.startPos
-- Aesop.Search.Main
Aesop.getProof? : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q (Option Lean.Expr)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.mk : Mathlib.Linter.TextBased.StyleError✝ → ℕ → System.FilePath → Mathlib.Linter.TextBased.ErrorContext✝
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.rightHom_comp_inl_eq_id : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q],
  RegularWreathProduct.rightHom.comp RegularWreathProduct.inl = MonoidHom.id Q
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier)
  (contentChanges : Array Lean.Lsp.TextDocumentContentChangeEvent),
  sizeOf { textDocument := textDocument, contentChanges := contentChanges } =
    1 + sizeOf textDocument + sizeOf contentChanges
-- Mathlib.Topology.Algebra.Monoid
monoidHomOfTendsto_apply : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂]
  [inst_2 : MulOneClass M₁] [inst_3 : MulOneClass M₂] [inst_4 : ContinuousMul M₂] {F : Type u_8}
  [inst_5 : FunLike F M₁ M₂] [inst_6 : MonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F)
  [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)), ⇑(monoidHomOfTendsto f g h) = f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List (α × β)} {k : α}, (m.insertMany l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.lift_comp_of : ∀ {α : Type u} {R : Type v} [inst : CommRing R] (f : FreeCommRing α →+* R), FreeCommRing.lift (⇑f ∘ FreeCommRing.of) = f
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- A normed field is either nontrivially normed or has a discrete topology.
In the discrete topology case, all the norms are 1, by `norm_eq_one_iff_ne_zero_of_discrete`.
The nontrivially normed field instance is provided by a subtype with a proof that the
forgetful inheritance to the existing `NormedField` instance is definitionally true.
This allows one to have the new `NontriviallyNormedField` instance without data clashes.  -/
NormedField.discreteTopology_or_nontriviallyNormedField : ∀ (𝕜 : Type u_4) [h : NormedField 𝕜], DiscreteTopology 𝕜 ∨ Nonempty { h' // h'.toNormedField = h }
-- Mathlib.Algebra.Lie.Submodule
/-- For an injective morphism of Lie modules, any Lie submodule is equivalent to its image.  -/
LieSubmodule.equivMapOfInjective : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {M' : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup M'] →
                    [inst_6 : Module R M'] →
                      [inst_7 : LieRingModule L M'] →
                        {f : M →ₗ⁅R,L⁆ M'} →
                          (N : LieSubmodule R L M) → Function.Injective ⇑f → ↥N ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map f N)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocMod hp (a + ↑m * p) b = toIocMod hp a b + ↑m * p
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.toPrefunctor : {V : Type u₁} →
  [inst : CategoryTheory.ReflQuiver V] → {W : Type u₂} → [inst_1 : CategoryTheory.ReflQuiver W] → V ⥤rq W → V ⥤q W
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.polynomial_comp_attachBound : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A)
  (g : Polynomial ℝ), (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound = ↑((Polynomial.aeval f) g)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_single_aux : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  (f : SkewMonoidAlgebra k G) {r : k} {x y z : G},
  (∀ (a : G), a * x = z ↔ a = y) → (f * SkewMonoidAlgebra.single x r).coeff z = f.coeff y * y • r
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Detects `Decidable*` instance hypotheses in the types of theorems which are not used in the
remainder of the type, and suggests replacing them with a use of `classical` in the proof or
`open scoped Classical in` at the term level.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.unusedDecidableInType : Lean.Linter
-- Init.Core
BEq.refl : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] (a : α), (a == a) = true
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.linearMap_comp : ∀ (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {X : Type u_7}
  {Y : Type u_8} {Z : Type u_9} [inst_3 : Finite X] [inst_4 : Finite Y] [inst_5 : Finite Z] (f : X → Y) (g : Y → Z),
  FunOnFinite.linearMap R M (g ∘ f) = FunOnFinite.linearMap R M g ∘ₗ FunOnFinite.linearMap R M f
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C],
  ((HomotopyCategory.quotient C c).comp HomologicalComplexUpToQuasiIso.Qh).IsLocalization
    (HomologicalComplex.quasiIso C c)
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite : ∀ (X : SSet) [X.Finite] (n : ℕ), Finite ↑(X.nonDegenerate n)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.mul_counit_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.new : BaseIO Lean.Server.RequestCancellationToken
-- Mathlib.Topology.Algebra.Module.FiniteDimension
isClosedEmbedding_smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space E]
  {c : E}, c ≠ 0 → Topology.IsClosedEmbedding fun x => x • c
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.brecOn.eq : ∀ {α : Type u} {motive : RBTree.RBNode.Path α → Sort u_1} (t : RBTree.RBNode.Path α)
  (F_1 : (t : RBTree.RBNode.Path α) → RBTree.RBNode.Path.below t → motive t),
  RBTree.RBNode.Path.brecOn t F_1 = F_1 t (RBTree.RBNode.Path.brecOn.go t F_1).2
-- Lean.Environment
/-- True if generated by `realizeConst`.  -/
_private.Lean.Environment.0.Lean.AsyncConst.isRealized : Lean.AsyncConst✝ → Bool
-- Init.Data.ToString.Basic
instToStringUInt64 : ToString UInt64
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Real.Gamma_mul_Gamma_add_half : ∀ (s : ℝ), Real.Gamma s * Real.Gamma (s + 1 / 2) = Real.Gamma (2 * s) * 2 ^ (1 - 2 * s) * √Real.pi
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol is multiplicative in `a` for `p` fixed.  -/
legendreSym.mul : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a b : ℤ), legendreSym p (a * b) = legendreSym p a * legendreSym p b
-- Mathlib.RingTheory.Ideal.Operations
Submodule.mem_ideal_smul_span_iff_exists_sum' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I : Ideal R)
  [I.IsTwoSided] {ι : Type u_4} (s : Set ι) (f : ι → M) (x : M),
  x ∈ I • Submodule.span R (f '' s) ↔ ∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun i c => c • f ↑i) = x
-- Init.Data.Iterators.Consumers.Partial
Std.Iter.Partial.mk.injEq : ∀ {α β : Type w} (it it_1 : Std.Iter β), ({ it := it } = { it := it_1 }) = (it = it_1)