mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.PiLex
/-- **Alias** of `Pi.trichotomous_lex`. -/
Pi.isTrichotomous_lex : ∀ {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), Std.Trichotomous s],
  WellFounded r → Std.Trichotomous (Pi.Lex r s)
-- Mathlib.Topology.Compactness.SigmaCompact
/-- The union of all sets in a compact exhaustion equals the entire space.  -/
CompactExhaustion.iUnion_eq' : ∀ {X : Type u_4} [inst : TopologicalSpace X] (self : CompactExhaustion X), ⋃ n, self.toFun n = Set.univ
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod_size : ∀ (n : UInt8), n.toNat % UInt8.size = n.toNat
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel.congr_simp : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n m : ℕ} (hm : n ∣ m),
  DirichletCharacter.changeLevel hm = DirichletCharacter.changeLevel hm
-- Init.Meta.Defs
/-- Use the head atom/identifier of the current `ref` as the `ref`  -/
Lean.withHeadRefOnly : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → {α : Type} → m α → m α
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_comp_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G H : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)
-- Mathlib.Data.Set.Lattice
Set.nonempty_of_nonempty_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α}, (⋃ i, s i).Nonempty → Nonempty ι
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsModuleFiltration.mk : ∀ {ι : Type u_1} {ιM : Type u_2} {R : Type u_3} {M : Type u_4} {σ : Type u_5} {σM : Type u_6} [inst : AddMonoid ι]
  [inst_1 : PartialOrder ι] [inst_2 : PartialOrder ιM] [inst_3 : VAdd ι ιM] [inst_4 : Preorder σ] [inst_5 : Semiring R]
  [inst_6 : SetLike σ R] [inst_7 : Preorder σM] [inst_8 : AddCommMonoid M] [inst_9 : Module R M]
  [inst_10 : SetLike σM M] {F : ι → σ} {F_lt : outParam (ι → σ)} [inst_11 : IsRingFiltration F F_lt] {F' : ιM → σM}
  {F'_lt : outParam (ιM → σM)} [toIsFiltration : IsFiltration F' F'_lt] [toGradedSMul : SetLike.GradedSMul F F'],
  IsModuleFiltration F F_lt F' F'_lt
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.instReprState.repr : Std.Http.Protocol.H1.Writer.State → ℕ → Std.Format
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiable_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E], Differentiable 𝕜 id
-- Mathlib.Algebra.Group.Pi.Lemmas
AddSemiconjBy.pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {x y z : (i : I) → f i},
  (∀ (i : I), AddSemiconjBy (x i) (y i) (z i)) → AddSemiconjBy x y z
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
iterateInduction.eq_1 : ∀ {X : ℕ → Type u_1} {a : ℕ} (x : (i : ↥(Finset.Iic a)) → X ↑i)
  (ind : (n : ℕ) → ((i : ↥(Finset.Iic n)) → X ↑i) → X (n + 1)), iterateInduction x ind 0 = x ⟨0, ⋯⟩
-- Mathlib.Algebra.DirectSum.Ring
/-- The zeroth power will yield 1  -/
DirectSum.GSemiring.gnpow_zero' : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A] (a : GradedMonoid A),
  GradedMonoid.mk (0 • a.fst) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_nonneg_of_nonneg : ∀ {K : Type u_1} [inst : RCLike K] {x : K}, IsSelfAdjoint x → (0 ≤ RCLike.re x ↔ 0 ≤ x)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance2.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d)))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d))
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
      b = RBTree.RBNode.node RBTree.RBColor.red b_1 y (RBTree.RBNode.node RBTree.RBColor.red c z d) → False) →
    (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
        b = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b_1 y c) z d → False) →
      (match a, x, b with
        | a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) =>
          h_1 a x b y c z d
        | a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d =>
          h_2 a x b y c z d
        | a, x, b => h_3 a x b) =
        h_3 a x b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams.toJson : Lean.Lsp.CallHierarchyIncomingCallsParams → Lean.Json
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the left adjoint is full, then each component of the unit is a split epimorphism.  -/
CategoryTheory.Adjunction.unitSplitEpiOfLFull : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → [L.Full] → (X : C) → CategoryTheory.SplitEpi (h.unit.app X)
-- Mathlib.CategoryTheory.Limits.Cones
/-- To give an isomorphism between cones, it suffices to give an
isomorphism between their vertices which commutes with the cone maps.  -/
CategoryTheory.Limits.Cone.extInv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j)
                  CategoryTheory.Limits.Cone.extInv._auto_1 →
                (c ≅ c')
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous
endomorphism.  -/
LipschitzWith.list_prod : ∀ {α : Type u} {ι : Type x} [inst : PseudoEMetricSpace α] (f : ι → Function.End α) (K : ι → NNReal),
  (∀ (i : ι), LipschitzWith (K i) (f i)) → ∀ (l : List ι), LipschitzWith (List.map K l).prod (List.map f l).prod
-- Std.Internal.Parsec.Basic
/-- Represents any other kind of parsing error with an associated message.
 -/
Std.Internal.Parsec.Error.other : String → Std.Internal.Parsec.Error
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Convert a `HeapNode` to a `Heap` by reversing the order of the nodes
along the `sibling` spine.
 -/
Batteries.BinomialHeap.Imp.HeapNode.toHeap : {α : Type u_1} → Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_updateRow_smul : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] (M : Matrix n n R)
  (j : n) (c : R) (u : n → R), (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.IsDynNetIn.card_le_netMaxcard : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {F : Set X} {s : Finset X},
  Dynamics.IsDynNetIn T F U n ↑s → ↑s.card ≤ Dynamics.netMaxcard T F U n
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {M N : CategoryTheory.Mod D A} {x y : M.Hom N}, x = y ↔ x.hom = y.hom
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ (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)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isoOverPullback_hom_left_comp_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong g] {P : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  (h : CategoryTheory.IsPullback fst snd f g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left h.isoOverPullback.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h_1) =
    CategoryTheory.CategoryStruct.comp snd h_1
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.prod_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {f : β × α → X},
  MeasureTheory.AEStronglyMeasurable f (ν.prod μ) → MeasureTheory.AEStronglyMeasurable (fun z => f z.swap) (μ.prod ν)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → t.minKey? = none
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableOn.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.cosh (f x)) s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k}
  [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → ⟨k, v⟩ ∈ l → (t.insertMany l).get! k' = cast ⋯ v
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.mono_measure : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ ν : MeasureTheory.Measure α}, AEMeasurable f μ → ν ≤ μ → AEMeasurable f ν
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The isomorphism `R ⧸ p ^ n ≃ₐ[R] Rₚ ⧸ maximalIdeal Rₚ ^ n`, where `Rₚ` satisfies
`IsLocalization.AtPrime Rₚ p`.  -/
IsLocalization.AtPrime.equivQuotMaximalIdealPow : {R : Type u_7} →
  [inst : CommRing R] →
    (p : Ideal R) →
      [inst_1 : p.IsMaximal] →
        (Rₚ : Type u_8) →
          [inst_2 : CommRing Rₚ] →
            [inst_3 : Algebra R Rₚ] →
              [IsLocalization.AtPrime Rₚ p] →
                [inst_5 : IsLocalRing Rₚ] → (n : ℕ) → (R ⧸ p ^ n) ≃ₐ[R] Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ ^ n
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.instInitialOfHasInitialOfPreservesColimitDiscretePEmptyEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F], F.Initial
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
_private.Mathlib.Algebra.Homology.Embedding.ExtendHomotopy.0.Homotopy.extend.homAux.match_1.eq_3 : ∀ {ι : Type u_1} (motive : Option ι → Option ι → Sort u_2) (i j : ι) (h_1 : (x : Option ι) → motive none x)
  (h_2 : (x : Option ι) → motive x none) (h_3 : (i j : ι) → motive (some i) (some j)),
  (match some i, some j with
    | none, x => h_1 x
    | x, none => h_2 x
    | some i, some j => h_3 i j) =
    h_3 i j
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice.eq_def : ∀ (s : String.Slice) (p : String.Pos.Raw),
  String.Pos.Raw.isValidForSlice s p =
    if h : p < s.rawEndPos then decide (s.getUTF8Byte p h).IsUTF8FirstByte else decide (p = s.rawEndPos)
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_zsmul : ∀ {α : Type u} [inst : SubNegMonoid α] (z : ℤ) (a : α), Multiplicative.ofAdd (z • a) = Multiplicative.ofAdd a ^ z
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The projection from the limit object to a value of the functor.  -/
CategoryTheory.Limits.limit.π : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] → (j : J) → CategoryTheory.Limits.limit F ⟶ F.obj j
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂) {Z : C}
  (h_1 : (K.total c₁₂).X i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).hom
      (CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ y₁ y₂ i₁₂ h) h_1) =
    CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯) h_1
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverEntropy_restrict_subset : ∀ {X : Type u_1} [inst : UniformSpace X] {T : X → X} {F G : Set X},
  F ⊆ G →
    ∀ (hG : Set.MapsTo T G G),
      Dynamics.coverEntropy (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropy T F
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.left : CategoryTheory.Limits.WalkingPair
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_comp_apply : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) (x : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom
        (groupHomology.mapCycles₁ (g.comp f) (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ))))
      x =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ g ψ))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ f φ)) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableCoproducts C]
  (J : Type u_3) [Countable J], CategoryTheory.Limits.HasCoproductsOfShape J C
-- Mathlib.Data.FunLike.IsApply
/-- `IsPowApply M F α β` states for all `f : F`, `n : M` and `x : α`, `(f ^ n) x = (f x) ^ n`.  -/
IsPowApply : (M : Type u_1) →
  (F : Type u_2) →
    (α : outParam (Type u_3)) → (β : outParam (Type u_4)) → [FunLike F α β] → [Pow β M] → [Pow F M] → Prop
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
instSMulFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : ContinuousAdd E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : ContinuousAdd F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] →
                            (𝕜' : Type u_1) →
                              [inst_11 : Semiring 𝕜'] →
                                [inst_12 : Module 𝕜' F] →
                                  [ContinuousConstSMul 𝕜' F] →
                                    [SMulCommClass 𝕜 𝕜' F] → SMul 𝕜' (FormalMultilinearSeries 𝕜 E F)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instIsScalarTower : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {𝕜 : Type u_5} {𝕜' : Type u_6} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] [inst_4 : SMul 𝕜' γ]
  [inst_5 : ContinuousConstSMul 𝕜' γ] [inst_6 : SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' γ], IsScalarTower 𝕜 𝕜' (α →ₘ[μ] γ)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- For `X : C`, the cokernel cofork `CokernelCofork.ofπ (Φ.π.app X) (Φ.ι_π_app X)` exhibits
`Φ.π.app X : X ⟶ Φ.quotient.obj X` as the cokernel of `Φ.ι.app X : Φ.r.obj X ⟶ X`.  -/
CategoryTheory.Abelian.Preradical.isColimitCokernelCoforkObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) →
        (X : C) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (Φ.π.app X) ⋯)
-- Mathlib.Algebra.CharP.Defs
/-- The definition of the exponential characteristic of a semiring.  -/
ExpChar : (R : Type u_1) → [AddMonoidWithOne R] → ℕ → Prop
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_of_not_memLp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E},
  ¬MeasureTheory.MemLp id 2 μ → ProbabilityTheory.covarianceBilin μ = 0
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror = p.reverse * Polynomial.X ^ p.natTrailingDegree
-- Mathlib.Combinatorics.HalesJewett
/-- The type of combinatorial lines. A line `l : Line α ι` in the hypercube `ι → α` defines a
function `α → ι → α` from `α` to the hypercube, such that for each coordinate `i : ι`, the function
`fun x ↦ l x i` is either `id` or constant. We require lines to be nontrivial in the sense that
`fun x ↦ l x i` is `id` for at least one `i`.

Formally, a line is represented by a word `l.idxFun : ι → Option α` which says whether
`fun x ↦ l x i` is `id` (corresponding to `l.idxFun i = none`) or constantly `y` (corresponding to
`l.idxFun i = some y`).

When `α` has size `1` there can be many elements of `Line α ι` defining the same function.  -/
Combinatorics.Line : Type u_5 → Type u_6 → Type (max u_5 u_6)
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Return the tactic string that does the unfolding.  -/
_private.Mathlib.Tactic.ClickSuggestions.Unfold.0.Mathlib.Tactic.ClickSuggestions.tacticSyntax : Lean.Expr →
  Lean.Expr →
    Mathlib.Tactic.ClickSuggestions.RwKind → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Lean.TSyntax `tactic)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v
-- Mathlib.CategoryTheory.Join.Sum
_private.Mathlib.CategoryTheory.Join.Sum.0.CategoryTheory.sum.match_3.splitter : (C : Type u_1) →
  (D : Type u_2) →
    (motive : C ⊕ D → Sort u_3) →
      (X : C ⊕ D) → ((X : C) → motive (Sum.inl X)) → ((X : D) → motive (Sum.inr X)) → motive X
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq : {J : Type u_1} →
  {a a_1 : CategoryTheory.Limits.WidePullbackShape J} → [DecidableEq J] → (x x_1 : a.Hom a_1) → Decidable (x = x_1)
-- Mathlib.Topology.Order.Lattice
Continuous.sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L}, Continuous f → Continuous g → Continuous fun x => f x ⊔ g x
-- Init.Data.Int.Order
Int.mul_lt_mul' : ∀ {a b c d : ℤ}, a ≤ c → b < d → 0 ≤ b → 0 < c → a * b < c * d
-- Init.Data.Random
IO.stdGenRef : IO.Ref StdGen
-- Mathlib.Order.PiLex
Pi.le_toColex_update_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedGT ι], toColex x ≤ toColex (Function.update x i a) ↔ x i ≤ a
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.IsStableUnderRetracts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g), P g → P f) → P.IsStableUnderRetracts
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Algebra.Star.Unitary
Unitary.mapEquiv_refl : ∀ {R : Type u_2} [inst : Monoid R] [inst_1 : StarMul R],
  Unitary.mapEquiv (StarMulEquiv.refl R) = StarMulEquiv.refl ↥(unitary R)
-- Init.Data.Range.Polymorphic.NatLemmas
Std.PRange.Nat.succ_eq : ∀ {n : ℕ}, Std.PRange.succ n = n + 1
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpi.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y W : C} (f : Y ⟶ X)
  [inst_1 : CategoryTheory.EffectiveEpi f] (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.EffectiveEpi.desc f e ⋯) = e
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.Truncated.rightExtensionInclusion_right_as : ∀ (X : SSet) (n : ℕ), (SSet.Truncated.rightExtensionInclusion X n).right.as = PUnit.unit
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.ext_functor_iff : ∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {X : Type v} [inst_2 : Group X]
  {f g : CategoryTheory.Functor G (CategoryTheory.SingleObj X)},
  f = g ↔ ∀ (a b : IsFreeGroupoid.Generators G) (e : a ⟶ b), f.map (IsFreeGroupoid.of e) = g.map (IsFreeGroupoid.of e)
-- Mathlib.SetTheory.ZFC.Class
/-- Coerce a ZFC set into a class  -/
Class.ofSet : ZFSet.{u} → Class.{u}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m},
  Std.DHashMap.Const.get m a h' = Std.DHashMap.Const.get m b ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.rightHomologyData_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.rightHomologyData.Q = S.X₃
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.equivWithAbs_equiv_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  {v w : AbsoluteValue R S} {x : R},
  (WithAbs.congr v w (RingEquiv.refl R)) ((WithAbs.equiv v).symm x) = (WithAbs.equiv w).symm x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData.range : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.RiiSliceData α β → Std.Rii α