mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.withMDataOptions : {α : Type} → [Inhabited α] → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mem_subring_iff : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {x : ℚ_[p]}, x ∈ PadicInt.subring p ↔ ‖x‖ ≤ 1
-- Init.Data.Nat.Div.Basic
/-- An induction principle customized for reasoning about the recursion pattern of natural number
division by iterated subtraction.
 -/
Nat.div.inductionOn : {motive : ℕ → ℕ → Sort u} →
  (x y : ℕ) →
    ((x y : ℕ) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) →
      ((x y : ℕ) → ¬(0 < y ∧ y ≤ x) → motive x y) → motive x y
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_list_prod : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (l : List (TrivSqZeroExt R M)),
  l.prod.fst = (List.map TrivSqZeroExt.fst l).prod
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ}
  {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (f : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.uliftYonedaEquiv f) =
    CategoryTheory.uliftYonedaEquiv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map g.unop) f)
-- Mathlib.Data.Finset.Grade
Multiset.grade_eq : ∀ {α : Type u_1} (m : Multiset α), grade ℕ m = m.card
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  Measurable f →
    (∀ (a : α) {q r : ℚ}, q ≤ r → ∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ f (a, c) r) →
      (∀ (a : α) (q : ℚ), ∀ᵐ (c : β) ∂ν a, 0 ≤ f (a, c) q) →
        (∀ (a : α) (q : ℚ), ∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ 1) →
          (∀ (a : α) (seq : ℕ → ℚ),
              Antitone seq →
                Filter.Tendsto seq Filter.atTop Filter.atBot →
                  Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop (nhds 0)) →
            (∀ (a : α) (seq : ℕ → ℚ),
                Monotone seq →
                  Filter.Tendsto seq Filter.atTop Filter.atTop →
                    Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop
                      (nhds ((ν a).real Set.univ))) →
              (∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun c => f (a, c) q) (ν a)) →
                (∀ (a : α) {A : Set β},
                    MeasurableSet A → ∀ (q : ℚ), ∫ (c : β) in A, f (a, c) q ∂ν a = (κ a).real (A ×ˢ Set.Iic ↑q)) →
                  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν
-- Std.Do.Triple.SpecLemmas
readThe.eq_1 : ∀ (ρ : Type u) {m : Type u → Type v} [inst : MonadReaderOf ρ m], readThe ρ = MonadReaderOf.read
-- Lean.Meta.Hint
/-- The granularity at which to display an inline diff for a suggested edit.  -/
Lean.Meta.Hint.DiffGranularity : Type
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_piEquivPiSubtypeProd_symm : ∀ {δ : Type u_4} (X : δ → Type u_6) [inst : (a : δ) → MeasurableSpace (X a)] (p : δ → Prop) [inst_1 : DecidablePred p],
  Measurable ⇑(Equiv.piEquivPiSubtypeProd p X).symm
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.compContinuousLinearMapL_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] {E₁ : ι → Type u_5} [inst_8 : (i : ι) → TopologicalSpace (E₁ i)]
  [inst_9 : ContinuousConstSMul 𝕜 F] [inst_10 : (i : ι) → AddCommGroup (E₁ i)] [inst_11 : (i : ι) → Module 𝕜 (E₁ i)]
  (f : (i : ι) → E i →L[𝕜] E₁ i) (g : ContinuousMultilinearMap 𝕜 E₁ F),
  (ContinuousMultilinearMap.compContinuousLinearMapL f) g = g.compContinuousLinearMap f
-- Mathlib.Data.Finset.Union
Finset.coe_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {h : (↑s).PairwiseDisjoint t},
  ↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
at `a`, the inverse function (produced by `ContDiff.toOpenPartialHomeomorph`) is
also `ContDiff`.  -/
ContDiffAt.to_localInverse : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕂 E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕂 F] [inst_5 : CompleteSpace E] {f : E → F}
  {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0),
  ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)
-- Lean.Message
Lean.MessageData.nest.injEq : ∀ (a : ℕ) (a_1 : Lean.MessageData) (a_2 : ℕ) (a_3 : Lean.MessageData),
  (Lean.MessageData.nest a a_1 = Lean.MessageData.nest a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.toInvariantForm.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic], P.toInvariantForm = P.toInvariantForm
-- Mathlib.Order.Filter.Map
Filter.comap_inf_principal_neBot_of_image_mem : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β},
  f.NeBot → ∀ {s : Set α}, m '' s ∈ f → (Filter.comap m f ⊓ Filter.principal s).NeBot
-- Lean.Elab.DocString
/-- Adds a builtin documentation code suggestion provider.

Should be run during initialization.
 -/
Lean.Doc.addBuiltinCodeSuggestion : Lean.Name → Lean.Doc.CodeSuggester → IO Unit
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedState.mk.sizeOf_spec : ∀ (cmdState : Lean.Elab.Command.State)
  (firstCmdSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot),
  sizeOf { cmdState := cmdState, firstCmdSnap := firstCmdSnap } = 1 + sizeOf cmdState + sizeOf firstCmdSnap
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- The star subalgebra generated by polynomials functions is dense in `C(s, 𝕜)` when `s` is
compact and `𝕜` is either `ℝ` or `ℂ`.  -/
polynomialFunctions.starClosure_topologicalClosure : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : CompactSpace ↑s],
  (polynomialFunctions s).starClosure.topologicalClosure = ⊤
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `orthogonal` gives a `GaloisConnection` between
`Submodule 𝕜 E` and its `OrderDual`.  -/
Submodule.orthogonal_gc : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  GaloisConnection Submodule.orthogonal Submodule.orthogonal
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.pow_right : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {n : ℕ}, IsCoprime x y → IsCoprime x (y ^ n)
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Given `Finite α`, `linearEquivFunOnFinite R` is the natural `R`-linear equivalence between
`α →₀ β` and `α → β`.  -/
Finsupp.linearEquivFunOnFinite : (R : Type u_9) →
  (M : Type u_11) →
    (α : Type u_12) →
      [Finite α] → [inst : AddCommMonoid M] → [inst_1 : Semiring R] → [inst_2 : Module R M] → (α →₀ M) ≃ₗ[R] α → M
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.mk : ℕ → ℕ → ℕ → ℕ → Lean.PersistentHashMap.Stats
-- Lean.Parser.Term.Basic
Lean.Parser.Term.instBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {Δ' Δ : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ'),
  AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ =
    CategoryTheory.Limits.Sigma.desc fun A =>
      CategoryTheory.CategoryStruct.comp
        (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K
          (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)))
        (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ))
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.exists_eq_singleton_append : ∀ {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.endPos), p.Splits t₁ t₂ → ∃ t₂', t₂ = String.singleton (p.get hp) ++ t₂'
-- Mathlib.Data.Prod.Lex
/-- Dictionary / lexicographic partial order for pairs.  -/
Prod.Lex.instPartialOrder : (α : Type u_3) → (β : Type u_4) → [PartialOrder α] → [PartialOrder β] → PartialOrder (Lex (α × β))
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
wellFounded_dvdNotUnit : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [h : WfDvdMonoid α], WellFounded DvdNotUnit
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.GRewriteResult.mk : Lean.Expr → Lean.Expr → List Lean.MVarId → Option Lean.LocalContext → Mathlib.Tactic.GRewrite.GRewriteResult
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex)
  (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2))
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g +
        CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w)
      (Q.complex.d (n + 3) (n + 2)) =
    f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'
-- Init.Data.Vector.Lemmas
Vector.findSome?_toList : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n},
  List.findSome? f xs.toList = Vector.findSome? f xs
-- Mathlib.Topology.Category.Profinite.Basic
/-- The `connectedComponents` functor from compact Hausdorff spaces to profinite spaces,
left adjoint to the inclusion functor.
 -/
CompHaus.toProfinite : CategoryTheory.Functor CompHaus Profinite
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_congr : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.Rxi.IsAlwaysFinite α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  {m : Type u → Type w} [inst_5 : Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rii α}
  {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Mathlib.Analysis.SpecialFunctions.PolynomialExp
Polynomial.tendsto_div_exp_atTop : ∀ (p : Polynomial ℝ), Filter.Tendsto (fun x => Polynomial.eval x p / Real.exp x) Filter.atTop (nhds 0)
-- Mathlib.Topology.Algebra.Field
affineHomeomorph_symm_apply : ∀ {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : IsTopologicalRing 𝕜] (a b : 𝕜) (h : a ≠ 0)
  (y : 𝕜), (affineHomeomorph a b h).symm y = (y - b) / a
-- Init.Data.SInt.Bitwise
Int16.or_eq_zero_iff : ∀ {a b : Int16}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_map : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] [inst_7 : AddCommGroup V₃]
  [inst_8 : Module k V₃] [inst_9 : AddTorsor V₃ P₃] (s : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃),
  AffineSubspace.map g (AffineSubspace.map f s) = AffineSubspace.map (g.comp f) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.neg_def : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P : W.Point), -P = P.neg
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
_private.Mathlib.Analysis.InnerProductSpace.Orthonormal.0.«term⟪_,_⟫_2» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Basic
sub_add_cancel_right : ∀ {G : Type u_3} [inst : AddGroup G] (a b : G), a - (b + a) = -b
-- Init.Data.Option.Basic
Option.instLawfulBEq : ∀ (α : Type u_1) [inst : BEq α] [LawfulBEq α], LawfulBEq (Option α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.instHasCokernelInr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.HasCokernel CategoryTheory.Limits.biprod.inr
-- Init.Data.SInt.Bitwise
ISize.ne_not_self : ∀ {a : ISize}, a ≠ ~~~a
-- Mathlib.Data.Finset.Slice
Set.sized_empty : ∀ {α : Type u_1} {r : ℕ}, Set.Sized r ∅
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Continuous multilinear maps from `G^1` to `G'` are isomorphic with continuous linear maps from
`G` to `G'`.  -/
continuousMultilinearCurryFin1 : (𝕜 : Type u) →
  (G : Type wG) →
    (G' : Type wG') →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : NormedAddCommGroup G'] → [inst_4 : NormedSpace 𝕜 G'] → (G [×1]→L[𝕜] G') ≃ₗᵢ[𝕜] G →L[𝕜] G'
-- Mathlib.LinearAlgebra.Quotient.Card
Submodule.card_eq_card_quotient_mul_card : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submodule R M),
  Nat.card M = Nat.card ↥S * Nat.card (M ⧸ S)
-- Mathlib.Data.Sum.Order
/-- `Equiv.emptySum` as an `OrderIso` with the lexicographic sum.  -/
OrderIso.emptySumLex : {α : Type u_1} → {β : Type u_2} → [inst : LE α] → [inst_1 : LE β] → [IsEmpty β] → β ⊕ₗ α ≃o α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {a : α}, ∅.getKey! a = default
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.mk.injEq : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {L : SummationFilter β} (basis : β → X) (coord : β → StrongDual 𝕜 X)
  (ortho : ∀ (i j : β), (coord i) (basis j) = Pi.single j 1 i)
  (expansion : ∀ (x : X), HasSum (fun i => (coord i) x • basis i) x L) (basis_1 : β → X) (coord_1 : β → StrongDual 𝕜 X)
  (ortho_1 : ∀ (i j : β), (coord_1 i) (basis_1 j) = Pi.single j 1 i)
  (expansion_1 : ∀ (x : X), HasSum (fun i => (coord_1 i) x • basis_1 i) x L),
  ({ basis := basis, coord := coord, ortho := ortho, expansion := expansion } =
      { basis := basis_1, coord := coord_1, ortho := ortho_1, expansion := expansion_1 }) =
    (basis = basis_1 ∧ coord = coord_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCocone.inl φ =
    (CochainComplex.mappingCone.inl φ).rightShift (-1) 0 CochainComplex.mappingCocone.snd._proof_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {k : α}
  {v : β k}, (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Mathlib.Data.ENat.Basic
ENat.le_sub_one_of_lt : ∀ {a b : ℕ∞}, a < b → a ≤ b - 1
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- If a reflective subcategory is an exponential ideal, then the reflector preserves binary products.
This is the converse of `exponentialIdeal_of_preserves_binary_products`.
 -/
CategoryTheory.preservesBinaryProducts_of_exponentialIdeal : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.ExponentialIdeal i] [CategoryTheory.BraidedCategory C],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
    (CategoryTheory.reflector i)
-- Mathlib.NumberTheory.MulChar.Basic
/-- The equivalence between multiplicative characters and homomorphisms of unit groups
as a multiplicative equivalence.  -/
MulChar.mulEquivToUnitHom : {R : Type u_1} →
  [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → MulChar R R' ≃* (Rˣ →* R'ˣ)
-- Mathlib.Topology.Constructible
IsRetrocompact.union : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, IsRetrocompact s → IsRetrocompact t → IsRetrocompact (s ∪ t)
-- Init.Data.List.MinMaxOn
List.maxOn?.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [i : LE β] {inst : DecidableLE β} [inst_1 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (l l_1 : List α), l = l_1 → List.maxOn? f l = List.maxOn? f_1 l_1
-- Init.Data.Vector.Lemmas
Vector.append_eq_append_iff : ∀ {α : Type u_1} {n m k l : ℕ} {ws : Vector α n} {xs : Vector α m} {ys : Vector α k} {zs : Vector α l}
  (w : k + l = n + m),
  ws ++ xs = Vector.cast w (ys ++ zs) ↔
    if h : n ≤ k then ∃ as, ys = Vector.cast ⋯ (ws ++ as) ∧ xs = Vector.cast ⋯ (as ++ zs)
    else ∃ cs, ws = Vector.cast ⋯ (ys ++ cs) ∧ zs = Vector.cast ⋯ (cs ++ xs)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.bicone_ι_π_self_assoc : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) {Z : C}
  (h : F j ⟶ Z), CategoryTheory.CategoryStruct.comp (B.ι j) (CategoryTheory.CategoryStruct.comp (B.π j) h) = h
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial

If `f : MvPowerSeries σ R` and `n : σ →₀ ℕ` is a (finitely-supported) function from `σ`
to the naturals, then `trunc R n f` is the multivariable polynomial obtained from `f`
by keeping only the monomials $c\prod_i X_i^{a_i}$ where `a i ≤ n i` for all `i`
and `a i < n i` for some `i`.  -/
MvPowerSeries.trunc : {σ : Type u_1} →
  [DecidableEq σ] → (R : Type u_4) → [inst : CommSemiring R] → (σ →₀ ℕ) → MvPowerSeries σ R →ₗ[R] MvPolynomial σ R
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.nontrivial : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Nontrivial (Polynomial R)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey! k = m₁.getKey! k
-- Mathlib.Data.FinEnum
FinEnum.card_Int64 : FinEnum.card Int64 = 2 ^ 64
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.insert₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.insert ⟨m, h⟩ a b)).WF
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The regularized Gaussian hypergeometric function.  -/
Complex.regularizedGaussHGFun : ℂ → ℂ → ℂ → ℂ → ℂ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffAt_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type uE) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] (i : ι) (f : ι → E),
  ContDiffAt 𝕜 n (fun f => f i) f
-- Mathlib.Order.Hom.Basic
OrderHom.instOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β], OrderHomClass (α →o β) α β
-- Init.Core
iff_false_left : ∀ {a b : Prop}, ¬a → ((a ↔ b) ↔ ¬b)
-- Mathlib.Order.WellFounded
WellFounded.mem_of_lt_min_compl : ∀ {α : Type u_1} {r : α → α → Prop} {wf : WellFounded r} {s : Set α} {hs : sᶜ.Nonempty} {x : α},
  r x (wf.min sᶜ hs) → x ∈ s
-- Mathlib.Data.PEquiv
PEquiv.eq_symm_apply : ∀ {α : Type u} {β : Type v} (f : α ≃. β) {x : β} {y : α}, some y = f.symm x ↔ f y = some x
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toAddEquiv_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  ↑e.symm = (↑e).symm
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_zero_of_firstNonzeroIsNeg : ∀ {coef : ℝ} {exps : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length exps = List.length basis →
      exps.FirstNonzeroIsNeg →
        have t := { coef := coef, unit := exps };
        Filter.Tendsto (t.toFun basis) Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.instIsFiniteMeasureProdVariationProdOfCompleteSpace : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G]
  [MeasureTheory.IsFiniteMeasure μ.variation] [MeasureTheory.IsFiniteMeasure ν.variation],
  MeasureTheory.IsFiniteMeasure (μ.prod ν B).variation
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjObjMap_π_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W W' : CategoryTheory.Functor J (Type w)} (g : W ⟶ W') (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W' F] ⦃j : J⦄
  (x : W.obj j) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.weightedLimFlipObjMap g F)
      (CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F x) h) =
    CategoryTheory.CategoryStruct.comp (W'.weightedLimObjObjπ F ((CategoryTheory.ConcreteCategory.hom (g.app j)) x)) h
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : Add α} {inst_3 : Add β}
  {toAddEquiv : α ≃+ β} {map_le_map_iff' : ∀ {a b : α}, toAddEquiv.toFun a ≤ toAddEquiv.toFun b ↔ a ≤ b}
  {toAddEquiv_1 : α ≃+ β} {map_le_map_iff'_1 : ∀ {a b : α}, toAddEquiv_1.toFun a ≤ toAddEquiv_1.toFun b ↔ a ≤ b},
  { toAddEquiv := toAddEquiv, map_le_map_iff' := map_le_map_iff' } =
      { toAddEquiv := toAddEquiv_1, map_le_map_iff' := map_le_map_iff'_1 } →
    toAddEquiv = toAddEquiv_1
-- Mathlib.GroupTheory.Torsion
MulEquiv.submonoidCongr.congr_simp : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S = T),
  MulEquiv.submonoidCongr h = MulEquiv.submonoidCongr h
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.coe_vecMulLinear : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] (M : Matrix m n R),
  ⇑M.vecMulLinear = fun v => Matrix.vecMul v M
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.natDegree_hermite : ∀ {n : ℕ}, (Polynomial.hermite n).natDegree = n