mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] [inst_7 : SizeOf R]
  [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toAlgHom : A →ₐ[R] B)
  (map_star' : ∀ (x : A), (↑↑toAlgHom.toRingHom).toFun (star x) = star ((↑↑toAlgHom.toRingHom).toFun x)),
  sizeOf { toAlgHom := toAlgHom, map_star' := map_star' } = 1 + sizeOf toAlgHom
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.ReflectsEpimorphisms.iso_iff : ∀ {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} (α : F ≅ G), F.ReflectsEpimorphisms ↔ G.ReflectsEpimorphisms
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Product of affine spaces is commutative up to continuous affine isomorphism.  -/
ContinuousAffineEquiv.prodComm : (k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → P₁ × P₂ ≃ᴬ[k] P₂ × P₁
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.inr f g) g')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f (CategoryTheory.CategoryStruct.comp g g')) h
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj.eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → ∀ (x : α), f (ga x) = gb (f x)
-- Init.Data.String.Lemmas.Basic
String.empty_eq_iff : ∀ {s : String}, "" = s ↔ s = ""
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The lemma  -/
Mathlib.Tactic.ClickSuggestions.ApplyLemma.name : Mathlib.Tactic.ClickSuggestions.ApplyLemma → Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.dist_pow_map_zero_mul_translationNumber_le : ∀ (f : CircleDeg1Lift) (n : ℕ), dist ((f ^ n) 0) (↑n * f.translationNumber) ≤ 1
-- Mathlib.Topology.Compactness.Lindelof
/-- The empty set is a Lindelof set.  -/
isLindelof_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsLindelof ∅
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.lt : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → r < s → x < y
-- Mathlib.Logic.Denumerable
/-- Returns the `n`-th element of `α` indexed by the decoding.  -/
Denumerable.ofNat : (α : Type u_3) → [Denumerable α] → ℕ → α
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Ioo_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.Ioo i.castSucc j.castSucc = Set.Ioo i j
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- Turn an exact functor into an additive functor.  -/
CategoryTheory.AdditiveFunctor.ofExact : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [CategoryTheory.Limits.HasZeroObject C] →
              [CategoryTheory.Limits.HasZeroObject D] →
                [CategoryTheory.Limits.HasBinaryBiproducts C] → CategoryTheory.Functor (C ⥤ₑ D) (C ⥤+ D)
-- Init.NotationExtra
unexpandIte : Lean.PrettyPrinter.Unexpander
-- Mathlib.Order.Hom.Basic
/-- Convert an `OrderEmbedding` to an `OrderHom`.  -/
OrderEmbedding.toOrderHom : {X : Type u_6} → {Y : Type u_7} → [inst : Preorder X] → [inst_1 : Preorder Y] → X ↪o Y → X →o Y
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)) {Z : ↑(G.obj c)}
  (h : (G.map (CategoryTheory.CategoryStruct.comp f g)).toFunctor.obj ((α.app a).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((α.naturality (CategoryTheory.CategoryStruct.comp f g)).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((α.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((α.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X))
        (CategoryTheory.CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).hom.toNatTrans.app X))
          (CategoryTheory.CategoryStruct.comp ((G.mapComp f g).inv.toNatTrans.app ((α.app a).toFunctor.obj X)) h)))
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_inv_mul_nhds_one : ∀ (Gₗ : Type u_2) [inst : UniformSpace Gₗ] [inst_1 : Group Gₗ] [IsLeftUniformGroup Gₗ],
  uniformity Gₗ = Filter.comap (fun x => x.1⁻¹ * x.2) (nhds 1)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The space of continuous affine maps from a topological vector space to a topological affine
space is affinely isomorphic to the product of the codomain with the space of linear maps, by taking
the value of the affine map at `(0 : V)` and the linear part.  -/
ContinuousAffineMap.decompAffineEquiv : (R : Type u_1) →
  (S : Type u_2) →
    (V : Type u_3) →
      {W : Type u_4} →
        (Q : Type u_5) →
          [inst : Ring S] →
            [inst_1 : Ring R] →
              [inst_2 : AddCommGroup V] →
                [inst_3 : Module R V] →
                  [inst_4 : TopologicalSpace V] →
                    [IsTopologicalAddGroup V] →
                      [inst_6 : AddCommGroup W] →
                        [inst_7 : Module R W] →
                          [inst_8 : TopologicalSpace W] →
                            [inst_9 : Module S W] →
                              [inst_10 : SMulCommClass R S W] →
                                [inst_11 : ContinuousConstSMul S W] →
                                  [inst_12 : AddTorsor W Q] →
                                    [inst_13 : TopologicalSpace Q] →
                                      [inst_14 : IsTopologicalAddGroup W] →
                                        [inst_15 : IsTopologicalAddTorsor Q] → (V →ᴬ[R] Q) ≃ᵃ[S] Q × (V →L[R] W)
-- Mathlib.Order.Heyting.Hom
OrderIsoClass.toHeytingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : HeytingAlgebra α]
  {x : HeytingAlgebra β} [OrderIsoClass F α β], HeytingHomClass F α β
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.of.eq_1 : ∀ (M : Type u) [inst : AddMonoid M], AddMonCat.of M = { carrier := M, str := inst }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_le_size_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {f : Option β → Option β}, t.size - 1 ≤ (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size
-- Mathlib.Data.List.Sigma
List.head?_lookupAll : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)),
  (List.lookupAll a l).head? = List.dlookup a l
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_mul : ∀ {a b : EReal},
  a ≠ 0 ∨ b ≠ ⊥ →
    a ≠ 0 ∨ b ≠ ⊤ → a ≠ ⊥ ∨ b ≠ 0 → a ≠ ⊤ ∨ b ≠ 0 → Filter.Tendsto (fun p => p.1 * p.2) (nhds (a, b)) (nhds (a * b))
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L), x ∈ ⊥ ↔ x = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {fallback v : β},
      (m.insertIfNew k v).getD a fallback = if (k == a) = true ∧ k ∉ m then v else m.getD a fallback
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (u : H →L[𝕜] K),
  (∀ (x y : H), inner 𝕜 (u x) (u y) = inner 𝕜 x y) ↔ ContinuousLinearMap.adjoint u ∘SL u = 1
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.dist_pointReflection_self_real : ∀ {V : Type u_2} {P : Type u_10} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : NormedSpace ℝ V] (x y : P),
  dist ((AffineIsometryEquiv.pointReflection ℝ x) y) y = 2 * dist x y
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : Group Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] (f : X →ₜ* Y),
  ProfiniteGrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Init.Data.SInt.Lemmas
Int64.ofInt_toInt : ∀ (x : Int64), Int64.ofInt x.toInt = x
-- Init.Data.String.Basic
/-- Returns the character at the position `pos` of a string, or panics if the position is the
past-the-end position.

This function is overridden with an efficient implementation in runtime code.
 -/
String.Pos.get! : {s : String} → s.Pos → Char
-- Mathlib.Data.EReal.Operations
EReal.coe_neg : ∀ (x : ℝ), ↑(-x) = -↑x
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.isPrincipal_opow_omega : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) (Ordinal.omega o)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.getNameOfIdent' : Lean.Syntax → Lean.Name
-- Mathlib.Logic.Equiv.Sum
Equiv.sumAssoc_apply_inr : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ), (Equiv.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
-- Mathlib.GroupTheory.Nilpotent
AddGroup.isNilpotent_of_subsingleton : ∀ {G : Type u_1} [inst : AddGroup G] [Subsingleton G], AddGroup.IsNilpotent G
-- Mathlib.Algebra.Group.Defs
Semigroup.ext : ∀ {G : Type u} {x y : Semigroup G}, Mul.mul = Mul.mul → x = y
-- Mathlib.Logic.Equiv.PartialEquiv
/-- A bijection between two sets `s : Set α` and `t : Set β` provides a partial equivalence
between `α` and `β`.  -/
Set.BijOn.toPartialEquiv : {α : Type u_1} →
  {β : Type u_2} → [Nonempty α] → (f : α → β) → (s : Set α) → (t : Set β) → Set.BijOn f s t → PartialEquiv α β
-- Mathlib.Analysis.SpecificLimits.Basic
sum_geometric_two_le : ∀ (n : ℕ), ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X X' : C}
  (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X'),
  (e.uniqueUpToIso e').hom =
    (CategoryTheory.Coyoneda.fullyFaithful.preimage
        (CategoryTheory.NatIso.ofComponents
            (fun Z =>
              { hom := TypeCat.ofHom (⇑e.homEquiv.symm ∘ ⇑e'.homEquiv),
                inv := TypeCat.ofHom (⇑e'.homEquiv.symm ∘ ⇑e.homEquiv), hom_inv_id := ⋯, inv_hom_id := ⋯ })
            ⋯).hom).unop
-- Mathlib.RepresentationTheory.Rep.Res
Rep.full_res : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G),
  Function.Surjective ⇑f → (Rep.resFunctor f).Full
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Given a set `E`, a function `f : C_c(X, ℝ)`, `0 < ε` and `∀ x ∈ E, f x < c`, there exists an
open set `V` such that `E ⊆ V` and the sets are similar in measure and `∀ x ∈ V, f x < c`.  -/
RealRMK.exists_open_approx : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (f : CompactlySupportedContinuousMap X ℝ) {ε : ℝ},
  0 < ε →
    ∀ (E : Set X) {μ : MeasureTheory.Content X},
      μ.outerMeasure E ≠ ⊤ →
        MeasurableSet E →
          ∀ {c : ℝ},
            (∀ x ∈ E, f x < c) → ∃ V, E ⊆ ↑V ∧ (∀ x ∈ V, f x < c) ∧ μ.measure ↑V ≤ μ.measure E + ENNReal.ofReal ε
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.IsRkFinite X = (M.restrict X).RankFinite
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKey! k = if (f (t.get? k)).isSome = true then k else default
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ref : IO.Ref (Lean.Meta.RefinedDiscrTree α)), sizeOf { ref := ref } = 1 + sizeOf ref
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.le_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α},
  s ≤ t ↔ ↑s ⊆ ↑t
-- Init.Sym.DSimp.DSimprocDSL
/-- Beta reduction  -/
Lean.Parser.Sym.DSimp.beta : Lean.ParserDescr
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_eq_bot_iff : ∀ {R : Type u} [inst : CommSemiring R] (f : R), PrimeSpectrum.basicOpen f = ⊥ ↔ IsNilpotent f
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_inv : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeGroup α), x⁻¹.toWord = FreeGroup.invRev x.toWord
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.mk_dest : ∀ {F : PFunctor.{uA, uB}} (x : F.M), PFunctor.M.mk x.dest = x
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.self_complex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [inst_3 : CategoryTheory.Projective Z],
  (CategoryTheory.ProjectiveResolution.self Z).complex = (ChainComplex.single₀ C).obj Z
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.add : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → μ.Integrable g → μ.Integrable (f + g)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.instMonoidWithZeroHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β], MonoidWithZeroHomClass (α →*₀o β) α β
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- `p.lastStep` is the first ordinal where the construction stops making sense, i.e., `f` returns
garbage since there is no point left to be chosen. We will only use ordinals before this step.  -/
Besicovitch.TauPackage.lastStep : {α : Type u_1} → [MetricSpace α] → {β : Type u} → [Nonempty β] → Besicovitch.TauPackage β α → Ordinal.{u}
-- Mathlib.Order.CompleteLattice.Defs
/-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`.  -/
CompleteLinearOrder.compare_eq_compareOfLessAndEq : ∀ {α : Type u_8} [self : CompleteLinearOrder α] (a b : α), compare a b = compareOfLessAndEq a b
-- Mathlib.Geometry.Manifold.StructureGroupoid
instMinStructureGroupoid : {H : Type u_1} → [inst : TopologicalSpace H] → Min (StructureGroupoid H)
-- Mathlib.Data.ENat.Basic
ENat.natCast_lt_natCast : ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
-- Init.Data.Int.Pow
Int.pow_succ' : ∀ (b : ℤ) (e : ℕ), b ^ (e + 1) = b * b ^ e
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsFibered.toIsPreFibered : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} [self : p.IsFibered], p.IsPreFibered
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable, `f` has a top element, and `f =O[atBot] g`, for some
`g` integrable at `atBot`, then `f` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : LinearOrder α] [CompactIccSpace α] [Filter.atBot.IsMeasurablyGenerated]
  [OrderTop α],
  MeasureTheory.LocallyIntegrable f μ →
    f =O[Filter.atBot] g → MeasureTheory.IntegrableAtFilter g Filter.atBot μ → MeasureTheory.Integrable f μ
-- Init.Data.Array.Lemmas
Array.foldr_congr : ∀ {α : Type u_1} {β : Type u_2} {as bs : Array α},
  as = bs →
    ∀ {f g : α → β → β},
      f = g →
        ∀ {a b : β},
          a = b →
            ∀ {start start' stop stop' : ℕ},
              start = start' → stop = stop' → Array.foldr f a as start stop = Array.foldr g b bs start' stop'
-- Mathlib.SetTheory.Ordinal.Family
not_surjective_of_ordinal : ∀ {α : Type u_1} [Small.{u, u_1} α] (f : α → Ordinal.{u}), ¬Function.Surjective f
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_associator_inv_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).inv.1 = (CategoryTheory.Bicategory.associator f.1 g.1 h.1).inv
-- Mathlib.CategoryTheory.IsConnected
/-- In a connected category, any two objects are related by `Zigzag`.  -/
CategoryTheory.isPreconnected_zigzag : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] (j₁ j₂ : J),
  CategoryTheory.Zigzag j₁ j₂
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_injective : Function.Injective pentagonal
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.smul_mul : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} {l : Type u_7} [inst : Fintype n] [inst_1 : Monoid R]
  [inst_2 : AddCommMonoid A] [inst_3 : Mul A] [inst_4 : DistribMulAction R A] [IsScalarTower R A A] (a : R)
  (M : CStarMatrix m n A) (N : CStarMatrix n l A), a • M * N = a • (M * N)
-- Mathlib.Algebra.Order.Monoid.Lex
AddMonoidHom.inl_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddMonoid β] [inst_3 : Preorder β],
  StrictMono ⇑(AddMonoidHom.inl α β)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Algebra.IsAlgebraic.isDomain_of_adjoin_range : ∀ (R : Type u_1) {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Set A)
  [NoZeroDivisors A] [Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A], IsDomain A
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorCotangentOfFlat.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T],
  P.tensorCotangentOfFlat T = P.tensorCotangentOfFlat T
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f p x → f =ᶠ[nhds x] g → HasFPowerSeriesAt g p x
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- For `x` not in `f`'s domain, there is an infinite chain of `y` from `f`'s domain
that keeps getting closer to `x` in terms of Archimedean classes.  -/
HahnEmbedding.Partial.exists_sub_mem_ball : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) (y : ↥(↑f).domain),
  ∃ z, ↑z - x ∈ FiniteArchimedeanClass.ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.finrank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℝ (NumberField.mixedEmbedding.mixedSpace K) = Module.finrank ℚ K
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- A complex differentiable function `f : ℂ → E` is analytic at every point.  -/
Differentiable.analyticAt : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E},
  Differentiable ℂ f → ∀ (z : ℂ), AnalyticAt ℂ f z
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_closure_iff : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {x : R},
  x ∈ Subsemiring.closure s ↔ x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.OfComp.map_iso_hom_app_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H)
  [inst_3 : G.Full] [inst_4 : G.Faithful] {A : Type u_5} [inst_5 : AddMonoid A] [inst_6 : CategoryTheory.HasShift C A]
  [inst_7 : CategoryTheory.HasShift D A] [inst_8 : CategoryTheory.HasShift E A] [inst_9 : G.CommShift A]
  [inst_10 : H.CommShift A] (a : A) (X : C) {Z : E} (h : G.obj ((CategoryTheory.shiftFunctor D a).obj (F.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.CommShift.OfComp.iso e a).hom.app X)) h =
    CategoryTheory.CategoryStruct.comp (e.hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso H a).hom.app X)
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E a).map (e.inv.app X))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G a).inv.app (F.obj X)) h)))
-- Init.Data.Vector.Lemmas
Vector.append_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector β n} {n_1 : ℕ} {ys : Vector β n_1} {zs : Vector α (n + n_1)}
  {f : α → β}, xs ++ ys = Vector.map f zs ↔ ∃ as bs, zs = as ++ bs ∧ Vector.map f as = xs ∧ Vector.map f bs = ys
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.pow_disjoint_pow : ∀ {α : Type u_1} {σ τ : Equiv.Perm α}, σ.Disjoint τ → ∀ (m n : ℕ), (σ ^ m).Disjoint (τ ^ n)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsLocalizedFullyFaithfulOfIsLocalizedEquivalence : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsLocalizedEquivalence],
  Φ.IsLocalizedFullyFaithful