mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Similarity
/-- Scales distance with positive ratio. Forward direction of
`similar_iff_exists_pos_dist_eq`.  -/
Similar.exists_pos_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.diagram.eq_1 : ∀ (P : ProfiniteGrp.{u}),
  P.diagram = P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
-- Mathlib.Order.FixedPoints
OrderHom.le_prevFixed : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) {y : ↑(Function.fixedPoints ⇑f)},
  ↑y ≤ x → y ≤ f.prevFixed x hx
-- Aesop.Util.UnorderedArraySet
/-- O(1)  -/
Aesop.UnorderedArraySet.singleton : {α : Type u_1} → [inst : BEq α] → α → Aesop.UnorderedArraySet α
-- Mathlib.Topology.IsLocalHomeomorph
/-- The point `f x` lies in the source of `localInverseAt x`.  -/
IsLocalHomeomorph.apply_self_mem_localInverseAt_source : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsLocalHomeomorph f) {x : X}, f x ∈ (hf.localInverseAt x).source
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesColimitsOfShape.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {F : CategoryTheory.Functor C D} →
              autoParam ({K : CategoryTheory.Functor J C} → CategoryTheory.CreatesColimit K F)
                  CategoryTheory.CreatesColimitsOfShape.CreatesColimit._autoParam →
                CategoryTheory.CreatesColimitsOfShape J F
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sum_congr : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {s : Finset ι} {B : ι → α → ℝ}, (∀ i ∈ s, A i =o[l] B i) → (fun H => ∑ i ∈ s, A i H) =o[l] fun H => ∑ i ∈ s, ‖B i H‖
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure : Type
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_inl : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃), f.coprod g ∘ₗ LinearMap.inl R M M₂ = f
-- Mathlib.Data.Finsupp.AList
Finsupp.toAList_lookupFinsupp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M), f.toAList.lookupFinsupp = f
-- Mathlib.ModelTheory.PartialEquiv
/-- Maps to the symmetric finitely-generated partial equivalence.  -/
FirstOrder.Language.FGEquiv.symm : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.FGEquiv M N → L.FGEquiv N M
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.hasSum_expZeta_of_one_lt_re : ∀ (a : ℝ) {s : ℂ},
  1 < s.re → HasSum (fun n => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑n ^ s) (HurwitzZeta.expZeta (↑a) s)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.left_top_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {V : Submodule R N},
  p.IsPerfectCompl ⊤ V ↔ V = ⊤
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.of_forall_mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.diff : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Std.Http.Internal.Char
/-- Checks if a character is valid for use in a domain name.
Valid characters are ASCII alphanumeric, hyphens, and dots.
 -/
Std.Http.Internal.Char.isValidDomainNameChar : Char → Bool
-- Mathlib.Data.Set.Pairwise.List
List.Nodup.pairwise_coe : ∀ {α : Type u_1} {r : α → α → Prop} {l : List α} [Std.Symm r], l.Nodup → ({a | a ∈ l}.Pairwise r ↔ List.Pairwise r l)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesLeftHomologyOf.congr_simp : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_4 : F.PreservesZeroMorphisms] (S S_1 : CategoryTheory.ShortComplex C),
  S = S_1 → F.PreservesLeftHomologyOf S = F_1.PreservesLeftHomologyOf S_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.pp : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.GoalM Lean.MessageData
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.invert_flip : ∀ {v : Bool} (f : Std.Sat.AIG.Fanin), (decide ((f.flip v).invert = f.invert) ^^ v) = true
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.strictMonoOn_rpow_Ici_of_exponent_pos : ∀ {r : ℝ}, 0 < r → StrictMonoOn (fun x => x ^ r) (Set.Ici 0)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.subtype_injective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [inst_2 : NonUnitalSubsemiringClass S R] (s : S), Function.Injective ⇑(NonUnitalSubsemiringClass.subtype s)
-- Mathlib.AlgebraicGeometry.Cover.Sigma
/-- If `𝒰` is a cover of `S`, this is the single object cover where the covering
object is the disjoint union.  -/
AlgebraicGeometry.Scheme.Cover.sigma : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [UnivLE.{v, u}] →
        AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S →
          AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S
-- Lean.Elab.Util
Lean.Elab.MacroStackElem.before : Lean.Elab.MacroStackElem → Lean.Syntax
-- Mathlib.Analysis.Analytic.Constructions
analyticOnNhd_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {v : F} {s : Set E},
  AnalyticOnNhd 𝕜 (fun x => v) s
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v', u'} D}
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)}
  {app : (c : C) → A.obj c → (F.obj c ⟶ G.obj c)}
  {naturality :
    autoParam
      (∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
        CategoryTheory.CategoryStruct.comp (F.map f) (app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
          CategoryTheory.CategoryStruct.comp (app c a) (G.map f))
      CategoryTheory.Functor.HomObj.naturality._autoParam}
  {app_1 : (c : C) → A.obj c → (F.obj c ⟶ G.obj c)}
  {naturality_1 :
    autoParam
      (∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
        CategoryTheory.CategoryStruct.comp (F.map f) (app_1 d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
          CategoryTheory.CategoryStruct.comp (app_1 c a) (G.map f))
      CategoryTheory.Functor.HomObj.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' → (Std.ExtTreeMap.map f t).getD k fallback = (Option.map (f k') t[k]?).getD fallback
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.zero_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (m : ↑(A.obj.obj X)), PresheafOfModules.Sheafify.smul α φ 0 m = 0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- `negAt` is its own inverse.  -/
NumberField.mixedEmbedding.negAt_symm : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }},
  (NumberField.mixedEmbedding.negAt s).symm = NumberField.mixedEmbedding.negAt s
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection], Uᗮ.starProjection = 1 - U.starProjection
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instTransOrdOffset : Std.TransOrd Std.Time.Nanosecond.Offset
-- Batteries.Data.List.Lemmas
List.diff_subset : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ : List α), l₁.diff l₂ ⊆ l₁
-- Mathlib.Data.List.Perm.Basic
List.map_append_flatMap_perm : ∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) (g : α → List β),
  (List.map f l ++ List.flatMap g l).Perm (List.flatMap (fun x => f x :: g x) l)
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_succ_right_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  ¬IsMax b → Set.Ioo a (Order.succ b) = Set.Ioc a b
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α ≪≫ CategoryTheory.Iso.refl Y = α
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapId_inv_app_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T) (X : CategoryTheory.Under Y),
  ((CategoryTheory.Under.mapId Y).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.isOrderedCancelAddMonoid : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommMonoid (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)],
  IsOrderedCancelAddMonoid (Lex (Π₀ (i : ι), α i))
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mul_X_cancel : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R}, φ * PowerSeries.X = ψ * PowerSeries.X → φ = ψ
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instInf : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Min β] → Min (MeasureTheory.SimpleFunc α β)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Add-sub-add version.  -/
Finset.ruzsa_triangle_inequality_add_sub_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  B.card * (A + C).card ≤ (B - A).card * (B + C).card
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.brecOn.go : {motive_1 : Lean.IR.IRType → Sort u} →
  {motive_2 : Array Lean.IR.IRType → Sort u} →
    {motive_3 : List Lean.IR.IRType → Sort u} →
      (t : Lean.IR.IRType) →
        ((t : Lean.IR.IRType) → t.below → motive_1 t) →
          ((t : Array Lean.IR.IRType) → Lean.IR.IRType.below_1 t → motive_2 t) →
            ((t : List Lean.IR.IRType) → Lean.IR.IRType.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Init.Data.Bool
Bool.le_trans : ∀ {x y z : Bool}, x ≤ y → y ≤ z → x ≤ z
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_cons : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} (h : t.WF)
  {l : List (α × β)} {k : α} {v : β},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t ((k, v) :: l) ⋯) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertMany (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl l ⋯)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ [Inhabited α] {k : α} {f : β k → β k} {hc : k ∈ t.modify k f}, (t.modify k f).getKey k hc = k
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_ric : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) (Std.Slice.size xs)
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.fiberInclusion_mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {a : 𝒳} (ha : p.obj a = S),
  CategoryTheory.Functor.Fiber.fiberInclusion.obj (CategoryTheory.Functor.Fiber.mk ha) = a
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling.  -/
AddSubgroup.nsmul : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → SMul ℕ ↥H
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.add.injEq : ∀ (a a_1 a_2 a_3 : Mathlib.Tactic.Linarith.CompSource), (a.add a_1 = a_2.add a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A space is a compactly coherent space if the topology is generated by the compact sets.  -/
CompactlyCoherentSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.LinearAlgebra.Matrix.Module
LinearMap.mapMatrixModule_comp_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Ring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : AddCommGroup P] [inst_8 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (v : ι → M),
  (LinearMap.mapMatrixModule ι (g ∘ₗ f)) v = (LinearMap.mapMatrixModule ι g) ((LinearMap.mapMatrixModule ι f) v)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
and `B ⟶ X` is an arrow of `S`. This is the hom `A ⟶ B`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} → {S : J.Cover X} → {T : (I : S.Arrow) → J.Cover I.Y} → (I : (S.bind T).Arrow) → I.Y ⟶ I.middle
-- Mathlib.Algebra.Homology.SingleHomology
/-- The canonical isomorphism `((single C c j).obj A).homology j ≅ A`  -/
HomologicalComplex.singleObjHomologySelfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) → (j : ι) → (A : C) → ((HomologicalComplex.single C c j).obj A).homology j ≅ A
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X} [AlgebraicGeometry.IsOpenImmersion f],
  Y.IsGermInjectiveAt (f x) ↔ X.IsGermInjectiveAt x
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source : ∀ {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [Q.IsLocal] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
  (𝒰 : X.OpenCover) [inst : ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)] [inst_1 : AlgebraicGeometry.IsAffine Y],
  (∀ (i j : 𝒰.I₀), Q (CategoryTheory.Limits.pullback.mapDesc (𝒰.f i) (𝒰.f j) f)) → Q.diagonal f
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isIso_iff₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 2} (f : F ⟶ G),
  CategoryTheory.IsIso f ↔
    CategoryTheory.IsIso (f.app 0) ∧ CategoryTheory.IsIso (f.app 1) ∧ CategoryTheory.IsIso (f.app 2)
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def
/-- A stochastic process is a Gaussian process if all its finite dimensional distributions are
Gaussian.  -/
ProbabilityTheory.IsGaussianProcess : {Ω : Type u_1} →
  {E : Type u_2} →
    {T : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        [MeasurableSpace E] →
          [TopologicalSpace E] →
            [inst : AddCommMonoid E] →
              [Module ℝ E] →
                (T → Ω → E) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsGaussianProcess._auto_1 → Prop
-- Init.Data.SInt.Basic
instHashableInt64 : Hashable Int64
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Bounding the Hausdorff edistance by bounding the edistance of any point
in each set to the other set  -/
Metric.hausdorffEDist_le_of_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
  (∀ x ∈ s, Metric.infEDist x t ≤ r) → (∀ x ∈ t, Metric.infEDist x s ≤ r) → Metric.hausdorffEDist s t ≤ r
-- Batteries.Data.Fin.Lemmas
Fin.find?_eq_findRev?_iff : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.find? p = Fin.findRev? p ↔ ∀ (i j : Fin n), p i = true → p j = true → i = j
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Turn a subgraph of a `SimpleGraph` into a member of its subgraph type.  -/
SimpleGraph.toSubgraph : {V : Type u} → {G : SimpleGraph V} → (H : SimpleGraph V) → H ≤ G → G.Subgraph
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.maxKey? = none ↔ t.isEmpty = true)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.defaultRatCDF_le_one : ∀ (q : ℚ), ProbabilityTheory.defaultRatCDF q ≤ 1
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.OLeanEntry.mk.injEq : ∀ (key : Lean.KeyedDeclsAttribute.Key) (declName : Lean.Name) (key_1 : Lean.KeyedDeclsAttribute.Key)
  (declName_1 : Lean.Name),
  ({ key := key, declName := declName } = { key := key_1, declName := declName_1 }) =
    (key = key_1 ∧ declName = declName_1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.comp_toFun : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B)
  (x : A), (g.comp f) x = g (f x)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The (exact) short complex `A.ρ.invariants ⟶ A ⟶ (G → A)`.  -/
groupCohomology.shortComplexH0 : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → Rep.{max u u_1, u, u} k G → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- **Alias** of `CategoryTheory.Functor.Faithful.of_comp_eq`. -/
Eq.faithful_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [ℋ : H.Faithful], F.comp G = H → F.Faithful
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- The Kahler form on an oriented real inner product space of dimension 2 can be evaluated in terms
of a complex-number representation of the space.  -/
Orientation.kahler_map_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ),
  (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
    ∀ (x y : E), (o.kahler x) y = f y * (starRingEnd ℂ) (f x)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_refl : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (g : L.Equiv M N), g.comp (FirstOrder.Language.Equiv.refl L M) = g
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- If we're compressed by all useful compressions, then we're an initial segment. This is the other
key Kruskal-Katona part.  -/
Finset.UV.isInitSeg_of_compressed : ∀ {α : Type u_1} [inst : LinearOrder α] {ℬ : Finset (Finset α)} {r : ℕ},
  Set.Sized r ↑ℬ →
    (∀ (U V : Finset α), Finset.UV.UsefulCompression✝ U V → UV.IsCompressed U V ℬ) → Finset.Colex.IsInitSeg ℬ r
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.mul_omega0_dvd : ∀ {a : Ordinal.{u}}, 0 < a → a < Ordinal.omega0 → ∀ {b : Ordinal.{u}}, Ordinal.omega0 ∣ b → a * b = b
-- Lean.Exception
/-- Convert exception into a structured message.  -/
Lean.Exception.toMessageData : Lean.Exception → Lean.MessageData
-- Aesop.Options.Internal
Aesop.Options' : Type
-- Mathlib.RingTheory.Extension.Basic
/-- The identity hom.  -/
Algebra.Extension.Hom.id : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → P.Hom P
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff.inj : ∀ {k : ℕ} {c : Lean.Meta.Grind.Arith.Linear.EqCnstr} {k_1 : ℕ} {c_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr},
  Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff k c = Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff k_1 c_1 →
    k = k_1 ∧ c = c_1
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.t0Space : ∀ (X : CpltSepUniformSpace), T0Space X.toUniformSpace.carrier
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (l : α →₀ M) (b : β),
  (Finsupp.equivMapDomain f l) b = l (f.symm b)
-- Mathlib.Order.Category.Semilat
/-- Construct a bundled `SemilatInfCat` from a `SemilatticeInf`.  -/
SemilatInfCat.of : (X : Type u) → [isSemilatticeInf : SemilatticeInf X] → [isOrderTop : OrderTop X] → SemilatInfCat
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.edgeDensity_chunk_aux : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {G : SimpleGraph α}
  [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α] (hP : P.IsEquipartition),
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ∀ (hU : U ∈ P.parts) (hV : V ∈ P.parts),
        ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
          ((∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts,
                ↑(G.edgeDensity ab.1 ab.2)) /
              16 ^ P.parts.card) ^
            2
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Tensor product of two bimodule objects as a bimodule object.  -/
Bimod.tensorBimod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.Limits.HasCoequalizers C] →
        [∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {X Y Z : CategoryTheory.Mon C} → Bimod X Y → Bimod Y Z → Bimod X Z