mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mk_id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W X X] (α : CategoryTheory.Localization.SmallHom W X Y),
  (CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id X)).comp α = α
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cone postcomposed with a natural isomorphism is a limit cone
if and only if the original cone is.
 -/
CategoryTheory.Limits.IsLimit.postcomposeHomEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (α : F ≅ G) →
            (c : CategoryTheory.Limits.Cone F) →
              CategoryTheory.Limits.IsLimit ((CategoryTheory.Limits.Cone.postcompose α.hom).obj c) ≃
                CategoryTheory.Limits.IsLimit c
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.Gamma_mul_Gamma_add_half : ∀ (s : ℂ), Complex.Gamma s * Complex.Gamma (s + 1 / 2) = Complex.Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√Real.pi
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_op_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹
-- Mathlib.CategoryTheory.EpiMono
/-- When `f` is an isomorphism, `f ≫ g` is monic iff `g` is.  -/
CategoryTheory.mono_comp_iff_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (g : Z ⟶ Y) [CategoryTheory.IsIso g]
  (f : Y ⟶ X), CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f) ↔ CategoryTheory.Mono f
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalRing.map_maximalIdeal_lt_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [inst_2 : CommSemiring S]
  [IsLocalRing S] (f : R →+* S) [IsLocalHom f], Ideal.map f (IsLocalRing.maximalIdeal R) < ⊤
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_nonempty_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFinitaryElemRestrictSubtype : ∀ {α : Type u_1} {M : Matroid α} [M.Finitary] {X : Set α}, (M.restrictSubtype X).Finitary
-- Mathlib.Algebra.Symmetrized
SymAlg.instUnique : {α : Type u_1} → [Unique α] → Unique αˢʸᵐ
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps from `Empty` is equivalent to `PUnit`.  -/
Equiv.emptyArrowEquivPUnit : (α : Sort u_1) → (Empty → α) ≃ PUnit.{u}
-- Mathlib.Algebra.Quaternion
Quaternion.im_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (star a).im = -a.im
-- Init.Data.SInt.Basic
/-- The smallest number that `Int16` can represent: `-2^15 = -32768`.  -/
Int16.minValue : Int16
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a filtered category `J`, the colimit of `F` (computed in `C`) gives
a subobject of `F` which is a supremum of the subobjects corresponding to
the objects in the image of the functor `F`.  -/
CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w}
  [inst_3 : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X))
  [inst_4 : CategoryTheory.IsFiltered J]
  {c : CategoryTheory.Limits.Cocone (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))}
  (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X)
  (hf : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom),
  CategoryTheory.Subobject.mk f = ⨆ j, CategoryTheory.Subobject.mk (F.obj j).obj.hom
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.star_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Star (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] (i : ι) (x : G i), star ⟦⟨i, x⟩⟧ = ⟦⟨i, star x⟩⟧
-- Lean.Meta.Sym.SymM
/-- Fallback used by `shareCommon` and `shareCommonInc` after a check violation:
repairs the term and re-runs the full hash-consing pass with checks disabled, so
this second pass always succeeds. In the exotic case where the repair does not
eliminate all violations (e.g., a reducible definition that cannot be unfolded because
of smart-unfolding blocking reduction), the term is admitted as-is; other parts of the
system report this kind of issue.
 -/
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.repairAndShare : Lean.Expr → Lean.Meta.Sym.AlphaShareCommon.Cache → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.coe_addLeft : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : SeparatelyContinuousAdd X] (x : X),
  ⇑(ContinuousMap.addLeft x) = fun y => x + y
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.sub_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), a - 0 = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ φ' φ'' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') (θ' : φ' ⟶ φ''),
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.CategoryStruct.comp θ θ') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ)
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ')
-- Mathlib.Order.Lattice
inf_ind : ∀ {α : Type u} [inst : LinearOrder α] (a b : α) {p : α → Prop}, p a → p b → p (min a b)
-- Init.Data.UInt.Bitwise
instAssociativeUSizeHOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.Computability.PartrecCode
/-- Helper lemma for the evaluation of `prec` in the base case.  -/
Nat.Partrec.Code.eval_prec_zero : ∀ (cf cg : Nat.Partrec.Code) (a : ℕ), (cf.prec cg).eval (Nat.pair a 0) = cf.eval a
-- Mathlib.Analysis.Complex.Basic
Complex.conjCLE_toLinearEquiv : ↑Complex.conjCLE = ↑Complex.conjAe
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getD : {α : Type u} → {β : Type v} → [BEq α] → α → β → (Std.DHashMap.Internal.AssocList α fun x => β) → β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.BVPred.bitblast.eq_2 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (w : ℕ)
  (expr : Std.Tactic.BVDecide.BVExpr w) (idx : ℕ),
  Std.Tactic.BVDecide.BVPred.bitblast aig { val := Std.Tactic.BVDecide.BVPred.getLsbD expr idx, cache := cache } =
    match Std.Tactic.BVDecide.BVExpr.bitblast aig { val := expr, cache := cache } with
    | { result := ⟨{ aig := aig_1, vec := refs }, hrefs⟩, cache := cache } =>
      have res := Std.Tactic.BVDecide.BVPred.blastGetLsbD aig_1 { w := w, vec := refs, idx := idx };
      { result := ⟨{ aig := aig_1, ref := res }, hrefs⟩, cache := cache }
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.IsArithmetic.inter : ∀ {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] [Γ'.IsArithmetic], (Γ ⊓ Γ').IsArithmetic
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_neighborSet : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), w ∈ G.neighborSet v ↔ G.Adj v w
-- Lean.Parser.Basic
Lean.Parser.scientificLitNoAntiquot : Lean.Parser.Parser
-- Mathlib.Analysis.Convex.Basic
convex_hyperplane : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w | f w = r}
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.mk.sizeOf_spec : ∀ {R : Type u} [inst : LE R] [inst_1 : AddCommMonoid R] [inst_2 : One R] {M : Type v} [inst_3 : SizeOf R]
  [inst_4 : SizeOf M] (weights : M →₀ R) (nonneg : 0 ≤ weights) (total : (weights.sum fun x r => r) = 1),
  sizeOf { weights := weights, nonneg := nonneg, total := total } = 1 + sizeOf weights + sizeOf total
-- Mathlib.Topology.Algebra.Group.Basic
toUnits_homeomorph.eq_1 : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : ContinuousInv G],
  toUnits_homeomorph = { toEquiv := toUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.encard_inv : ∀ {G : Type u_1} [inst : InvolutiveInv G] (s : Set G), s⁻¹.encard = s.encard
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The canonical (bundled) continuous map from the underlying topological
space of `X` to the prime spectrum of its global sections.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase : (X : AlgebraicGeometry.LocallyRingedSpace) →
  X.toTopCat ⟶ AlgebraicGeometry.Spec.topObj (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mem_toAddSubgroup : ∀ {K : Type u} [inst : DivisionRing K] {s : Subfield K} {x : K}, x ∈ s.toAddSubgroup ↔ x ∈ s
-- Init.Sym.Lemmas
Lean.Sym.UInt16.eq_eq_true : ∀ (a b : UInt16), decide (a = b) = true → (a = b) = True
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.whiskerLeft_id : ∀ {C : Type u} (X Y : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X (CategoryTheory.FreeMonoidalCategory.Hom.id Y))
    (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor Y))
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_mem_vadd_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β} {a : α} {x : β},
  a +ᵥ x ∈ a +ᵥ s ↔ x ∈ s
-- Mathlib.Analysis.Convex.Mul
ConvexOn.mul : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConvexOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → MonovaryOn f g s → ConvexOn 𝕜 s (f * g)
-- Init.Core
Thunk.mk.inj : ∀ {α : Type u} {fn fn_1 : Unit → α}, { fn := fn } = { fn := fn_1 } → fn = fn_1
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.sub_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  AntivaryOn f₁ g s → MonovaryOn f₂ g s → AntivaryOn (f₁ - f₂) g s
-- Mathlib.Algebra.Group.Center
IsAddCentral.left_comm : ∀ {M : Type u_1} {a : M} [inst : Add M], IsAddCentral a → ∀ (b c : M), a + (b + c) = b + (a + c)
-- Mathlib.FieldTheory.Normal.Basic
AlgEquiv.restrict_liftNormal : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K₁ E] [inst_6 : IsScalarTower F K₁ E] (χ : Gal(K₁/F))
  [inst_7 : Normal F K₁] [inst_8 : Normal F E], (χ.liftNormal E).restrictNormal K₁ = χ
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.map_effectiveEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpis] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f], CategoryTheory.EffectiveEpi (F.map f)
-- Mathlib.Algebra.Field.Defs
/-- `a / b := a * b⁻¹`  -/
DivisionSemiring.div_eq_mul_inv : ∀ {K : Type u_2} [self : DivisionSemiring K] (a b : K), a / b = a * b⁻¹
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- This delaborator tries to elide functions which are known coercions.
For example, `Int.ofNat` is a coercion, so instead of printing `ofNat n` we just print `↑n`,
and when re-parsing this we can (usually) recover the specific coercion being used.
 -/
Lean.PrettyPrinter.Delaborator.coeDelaborator : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Lex
/-- A type synonym to equip a type with its lexicographic order.  -/
Lex : Type u_2 → Type u_2
-- Init.Data.String.Lemmas.Pattern.Find.Basic
List.findSome?.match_1.congr_eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (x : Option β) (h_1 : (b : β) → motive (some b))
  (h_2 : Unit → motive none) (b : β),
  x = some b →
    (match x with
      | some b => h_1 b
      | none => h_2 ()) ≍
      h_1 b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over
the two morphisms `∏ᶜ I.left ⇉ ∏ᶜ I.right`. This is the diagram of the latter for limiting fans.
 -/
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        CategoryTheory.Limits.Fan I.left →
          {d : CategoryTheory.Limits.Fan I.right} →
            CategoryTheory.Limits.IsLimit d → CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
-- Lean.Elab.Tactic.Conv.Pattern
/-- Assuming `isReady` returned false, this advances to the next match.  -/
Lean.Elab.Tactic.Conv.PatternMatchState.skip : Lean.Elab.Tactic.Conv.PatternMatchState → Lean.Elab.Tactic.Conv.PatternMatchState
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.toCodeDecl! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.CodeDecl pu
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km : α},
  t.max? = some km → t.contains km = true
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- A non-computable version of `AddMonoidHom.liftOfRightInverse` for when no
computable right inverse is available.  -/
AddMonoidHom.liftOfSurjective : {G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : AddGroup G₁] →
        [inst_1 : AddGroup G₂] →
          [inst_2 : AddGroup G₃] → (f : G₁ →+ G₂) → Function.Surjective ⇑f → { g // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.eq' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {x y : M}, Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ -x + y ∈ p
-- Lean.Meta.Closure
Lean.Meta.Closure.Context.mk.injEq : ∀ (zetaDelta zetaDelta_1 : Bool),
  ({ zetaDelta := zetaDelta } = { zetaDelta := zetaDelta_1 }) = (zetaDelta = zetaDelta_1)
-- Init.Data.String.Lemmas.IsEmpty
String.copy_sliceTo_startPos : ∀ {s : String}, (s.sliceTo s.startPos).copy = ""
-- Mathlib.Topology.QuasiSeparated
Topology.IsOpenEmbedding.isQuasiSeparated_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsOpenEmbedding f → ∀ {s : Set α}, IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.IsGaussian.charFun_eq : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (t : E),
  MeasureTheory.charFun μ t =
    Complex.exp
      ((∫ (x : E), ↑((fun x => inner ℝ t x) x) ∂μ) * Complex.I -
        ↑(ProbabilityTheory.variance (fun x => inner ℝ t x) μ) / 2)
-- Mathlib.Algebra.Ring.Parity
Nat.two_dvd_mul_add_one : ∀ (k : ℕ), 2 ∣ k * (k + 1)
-- Mathlib.CategoryTheory.CatCommSq
/-- Horizontal inverse of a 2-commutative square  -/
CategoryTheory.CatCommSq.hInv : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (T : C₁ ≌ C₂) →
                  (L : CategoryTheory.Functor C₁ C₃) →
                    (R : CategoryTheory.Functor C₂ C₄) →
                      (B : C₃ ≌ C₄) →
                        CategoryTheory.CatCommSq T.functor L R B.functor →
                          CategoryTheory.CatCommSq T.inverse R L B.inverse
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulAddMonoidHom : {A : Type u_5} →
  {B : Type u_6} →
    {M : Type u_7} → [inst : AddMonoid A] → [DistribSMul M A] → [inst_2 : AddZeroClass B] → SMul Mᵈᵐᵃ (A →+ B)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eq_zero_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α},
  eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- Prove that a category is connected by supplying an explicit initial object.  -/
CategoryTheory.isConnected_of_isInitial : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {x : C} (h : CategoryTheory.Limits.IsInitial x),
  CategoryTheory.IsConnected C
-- Mathlib.Tactic.Abel
/-- Elaborator for the `abel_nf` tactic.  -/
Mathlib.Tactic.Abel.elabAbelNFConv : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.isoOfIso_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon C} {P Q : Bimod X Y} (f : P.X ≅ Q.X)
  (f_left_act_hom :
    CategoryTheory.CategoryStruct.comp P.actLeft f.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom) Q.actLeft)
  (f_right_act_hom :
    CategoryTheory.CategoryStruct.comp P.actRight f.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) Q.actRight),
  (Bimod.isoOfIso f f_left_act_hom f_right_act_hom).inv.hom = f.inv
-- Init.Data.UInt.Lemmas
UInt16.le_antisymm : ∀ {a b : UInt16}, a ≤ b → b ≤ a → a = b
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isCycle_of_prime_order' : ∀ {α : Type u_1} [inst : Fintype α] {σ : Equiv.Perm α},
  Nat.Prime (orderOf σ) → Fintype.card α < 2 * orderOf σ → σ.IsCycle
-- Init.Data.List.Lemmas
List.map_eq_map_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {g : α → α_1},
  List.map f l = List.map g l ↔ ∀ a ∈ l, f a = g a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  k ∉ t → (f (Std.DTreeMap.Const.get? t k)).isNone = true → (Std.DTreeMap.Const.alter t k f).size = t.size
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.mk.injEq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (toHomotopy : f₀.Homotopy f₁)
  (prop' : ∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy.toFun (t, x), continuous_toFun := ⋯ })
  (toHomotopy_1 : f₀.Homotopy f₁)
  (prop'_1 : ∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy_1.toFun (t, x), continuous_toFun := ⋯ }),
  ({ toHomotopy := toHomotopy, prop' := prop' } = { toHomotopy := toHomotopy_1, prop' := prop'_1 }) =
    (toHomotopy = toHomotopy_1)
-- Mathlib.RepresentationTheory.Basic
Representation.self_inv_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (x : V), (ρ g) ((ρ g⁻¹) x) = x
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.congr_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i ≃ₗ[R] t i) (m : (i : ι) → s i),
  (PiTensorProduct.congr f) ((PiTensorProduct.tprod R) m) = ⨂ₜ[R] (i : ι), (f i) (m i)
-- Lean.Meta.IndPredBelow
/-- A new declaration of type `∀ x y z, indName ... (h x y z)` for all `h ∈ vars`  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.below : Lean.LocalDecl → Lean.Name → Array Lean.FVarId → Lean.Meta.IndPredBelow.NewDecl✝
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- The algebra equivalence underlying a bialgebra equivalence.  -/
BialgEquiv.toAlgEquiv : {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] → (A ≃ₐc[R] B) → A ≃ₐ[R] B
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `h.χ m` is the characteristic map of monomorphism `m` given by the bijection `h.homEquiv`.  -/
CategoryTheory.SubobjectRepresentableBy.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} → CategoryTheory.SubobjectRepresentableBy Ω → {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.star_eigenvectorUnitary_mulVec : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (j : n), (star ↑hA.eigenvectorUnitary).mulVec (hA.eigenvectorBasis j).ofLp = Pi.single j 1
-- Mathlib.Topology.Connected.TotallyDisconnected
totallyDisconnectedSpace_subtype_iff : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_map_iff_exists_tendsto : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter β} {f : β → α} [l.NeBot],
  Cauchy (Filter.map f l) ↔ ∃ x, Filter.Tendsto f l (nhds x)
-- Mathlib.Computability.Partrec
Partrec.some : ∀ {α : Type u_1} [inst : Primcodable α], Partrec Part.some
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.addEquiv_coe_eq : ∀ {X Y : Type u_1} [inst : Add X] [inst_1 : Add Y] (e : X ≃+ Y), AddMagmaCat.Hom.hom (AddMagmaCat.ofHom ↑e) = ↑e