mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_or : ∀ (a b : UInt8), (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n)
      (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i.succ) =
    CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i
-- Mathlib.Topology.CompactOpen
ContinuousMap.coev_apply : ∀ (X : Type u_2) (Y : Type u_3) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (b : Y),
  ⇑(ContinuousMap.coev X Y b) = Prod.mk b
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split_ineq_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (k a : ℤ) (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_right_split_ineq_cert p₁ p₂ k a p' =
    (p₁.leadCoeff.beq' a).and'
      (p'.beq' ((Int.Internal.Linear.Poly.combine_mul_k p₂.leadCoeff (-a) p₁.tail p₂.tail).addConst_k (-a * k)))
-- Mathlib.Analysis.Normed.Group.Uniform
dist_sub_eq_dist_add_right : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a b c : E), dist a (b - c) = dist (a + c) b
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectEpimorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [∀ (i : I), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (F i)]
      [CategoryTheory.Limits.HasPushouts C], CategoryTheory.JointlyReflectEpimorphisms F
-- Mathlib.Probability.Kernel.Composition.Comp
/-- A version of the Chapman-Kolmogorov equation useful for paths.  -/
ProbabilityTheory.Kernel.pow_succ_apply_eq_lintegral : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel α α) (n : ℕ) (a : α) {s : Set α},
  MeasurableSet s → ((κ ^ (n + 1)) a) s = ∫⁻ (b : α), (κ b) s ∂(κ ^ n) a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_eq_of_eq_cos : ∀ {x y : ℝ}, 0 ≤ y → y ≤ Real.pi → x = Real.cos y → Real.arccos x = y
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_fun : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [inst_1 : NormedAddCommGroup F] {g : ℝ → F},
  IntervalIntegrable f μ a b →
    MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b)) →
      ((fun x => ‖g x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun x => ‖f x‖) → IntervalIntegrable g μ a b
-- Mathlib.Order.Defs.Unbundled
UpperSet.mk : {α : Type u_1} → [inst : LE α] → (carrier : Set α) → IsUpperSet carrier → UpperSet α
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.toPresheaf.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  PresheafOfModules.toPresheaf R =
    { obj := fun M => M.presheaf,
      map := fun {X Y} f =>
        { app := fun X_1 => AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(CategoryTheory.ConcreteCategory.hom (f.app X_1)) ⋯),
          naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.BitVec
BitVec.ofFin_intCast : ∀ {w : ℕ} (z : ℤ), { toFin := ↑z } = ↑z
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves binary biproducts of `X` and `Y` if `F` maps every bilimit bicone over
`X` and `Y` to a bilimit bicone over `F.obj X` and `F.obj Y`.  -/
CategoryTheory.Limits.isBinaryBilimitOfPreserves : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] →
                    {b : CategoryTheory.Limits.BinaryBicone X Y} → b.IsBilimit → (F.mapBinaryBicone b).IsBilimit
-- Lean.Meta.Basic
/-- Similar to `forallMetaTelescope`, but if `e = forall ..xs, A`
it will reduce `A` to construct further mvars.   -/
Lean.Meta.forallMetaTelescopeReducing : Lean.Expr →
  optParam (Option ℕ) none →
    optParam Lean.MetavarKind Lean.MetavarKind.natural →
      Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.Topology.Separation.Basic
/-- In an R₁ space, the closure of a compact set is the union of the closures of its points.  -/
IsCompact.closure_eq_biUnion_closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K : Set X}, IsCompact K → closure K = ⋃ x ∈ K, closure {x}
-- Aesop.Options.Public
/-- Maximum total number of rule applications in the search tree. When this limit
is exceeded, the search ends. 0 means no limit.
 -/
Aesop.Options.maxRuleApplications : Aesop.Options → ℕ
-- Lean.Meta.WHNF
Lean.Meta.reduceBinNatPred : (ℕ → ℕ → Bool) → Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.warning.sizeOf_spec : sizeOf Lean.Lsp.DiagnosticSeverity.warning = 1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagSource.ematch.injEq : ∀ (origin : Lean.Meta.Grind.Origin) (inst : Lean.Expr) (origin_1 : Lean.Meta.Grind.Origin) (inst_1 : Lean.Expr),
  (Lean.Meta.Grind.EMatchDiagSource.ematch origin inst = Lean.Meta.Grind.EMatchDiagSource.ematch origin_1 inst_1) =
    (origin = origin_1 ∧ inst = inst_1)
-- Aesop.Frontend.Saturate
Aesop.Frontend.mkHypImplicationRule? : Lean.FVarId → Aesop.ElabM (Option Aesop.LocalRuleSetMember)
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_eq_zero_iff : ∀ {w n : ℕ} {x : BitVec w},
  (∀ (i : ℕ), n < i → x.getLsbD i = false) → ∀ (hw : 0 < w), (x.clzAuxRec n).toNat = 0 ↔ x[w - 1] = true
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.iterate : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {L : Filter (𝕜 × 𝕜)} {f : 𝕜 → 𝕜} {f' : 𝕜},
  HasDerivAtFilter f f' L → Filter.Tendsto (Prod.map f f) L L → ∀ (n : ℕ), HasDerivAtFilter f^[n] (f' ^ n) L
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- The characteristic function is asymptotically non-negative.
 -/
ValueDistribution.characteristic_eventually_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E},
  0 ≤ᶠ[Filter.atTop] ValueDistribution.characteristic f a
-- Init.Data.Int.DivMod.Lemmas
Int.eq_mul_of_tdiv_eq_left : ∀ {a b c : ℤ}, b ∣ a → a.tdiv b = c → a = c * b
-- Mathlib.Algebra.Star.StarAlgHom
/-- The second projection of a product is a non-unital ⋆-algebra homomorphism.  -/
NonUnitalStarAlgHom.snd : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : Star A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : Star B] → A × B →⋆ₙₐ[R] B
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_eq_Icc_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b = Set.Icc a b ↔ ¬a ≤ b
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_natCast : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (n : ℕ), (↑n).coeff = fun₀ | 0 => ↑n
-- Mathlib.Algebra.Module.Lattice
/-- Any lattice over a PID is a free `R`-module.
Note that under our conditions, `Module.IsTorsionFree R K` simply says that `algebraMap R K` is
injective.  -/
Submodule.IsLattice.free : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module K V] [inst_5 : Module R V] [inst_6 : IsScalarTower R K V] [IsDomain R]
  [IsPrincipalIdealRing R] [Module.IsTorsionFree R K] (M : Submodule R V) [Submodule.IsLattice K M], Module.Free R ↥M
-- Init.Data.Vector.Attach
Vector.attachWith_congr : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {H : ∀ x ∈ xs, P x},
  xs.attachWith P H = ys.attachWith P ⋯
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeBack_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.coconeBack✝.obj t).pt = CategoryTheory.Under.mk (t.ι.app CategoryTheory.WithInitial.star)
-- Mathlib.Data.ENat.Pow
ENat.one_le_epow : ∀ {x y : ℕ∞}, x ≠ 0 → 1 ≤ x ^ y
-- Mathlib.Data.Part
Part.assert_pos : ∀ {α : Type u_1} {p : Prop} {f : p → Part α} (h : p), Part.assert p f = f h
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- An uncurried version of `Finset.sum_product_right`  -/
Finset.sum_product_right' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β),
  ∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ y ∈ t, ∑ x ∈ s, f x y
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- Continuous functors send covering sieves to covering sieves.
The converse is false, see [SGA4, III, Exemple 1.9.3][sga-4-tome-1].  -/
CategoryTheory.CoverPreserving.of_isContinuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K], CategoryTheory.CoverPreserving J K F
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubgroup_strictMono : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M},
  StrictMono Submodule.toAddSubgroup
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.liftHomology_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : A ⟶ S.opcycles)
  (hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0),
  CategoryTheory.CategoryStruct.comp (S.liftHomology k hk) S.homologyι = k
-- Mathlib.GroupTheory.Goursat
/-- **Goursat's lemma** for a subgroup of a product with surjective projections.

If `I` is a subgroup of `G × H` which projects fully on both factors, then there exist normal
subgroups `M ≤ G` and `N ≤ H` such that `G' × H' ≤ I` and the image of `I` in `G ⧸ M × H ⧸ N` is the
graph of an isomorphism `G ⧸ M ≃ H ⧸ N'`.

`G'` and `H'` can be explicitly constructed as `I.goursatFst` and `I.goursatSnd` respectively.  -/
Subgroup.goursat_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)}
  (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)),
  have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.lift_comp_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] (P : Type u_4) [inst_3 : AddCommMonoid P]
  (F : AddCommGroup.DirectLimit G f →+ P),
  AddCommGroup.DirectLimit.lift G f P (fun i => F.comp (AddCommGroup.DirectLimit.of G f i)) ⋯ = F
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ (k : α), t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isTree_iff_minimal_connected : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree ↔ Minimal SimpleGraph.Connected G
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctor_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [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₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5)
  {X Y : CategoryTheory.GradedObject I C₁} (φ : X ⟶ Y) (Y_1 : CategoryTheory.GradedObject J C₂) (ij : I × J),
  ((CategoryTheory.GradedObject.mapBifunctor F I J).map φ).app Y_1 ij = (F.map (φ ij.1)).app (Y_1 ij.2)
-- Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
iteratedDerivWithin_one_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (k : ℕ),
  IsOpen s → Set.EqOn (iteratedDerivWithin k (fun y => 1 / y) s) (fun y => (-1) ^ k * ↑k.factorial * y ^ (-1 - ↑k)) s
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.mem_ker_modByMonic : ∀ {R : Type u} [inst : CommRing R] {q : Polynomial R}, q.Monic → ∀ {p : Polynomial R}, p ∈ q.modByMonicHom.ker ↔ q ∣ p
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)},
  CategoryTheory.Presieve.IsSeparatedFor F E.presieve₀ →
    (∀ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j),
        CategoryTheory.CategoryStruct.comp p₁ (E.f i) = CategoryTheory.CategoryStruct.comp p₂ (E.f j) →
          CategoryTheory.Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows) →
      E.IsStronglySeparatedFor F
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.Finite.mk : ∀ {X : SSet}, Finite X.N → X.Finite
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.mu'_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a b : α),
  (IncidenceAlgebra.mu'✝ 𝕜) a b = if a = b then 1 else -∑ x ∈ Finset.Ioc a b, (IncidenceAlgebra.mu'✝ 𝕜) x b
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.div_mul_cancel'` for a stronger version.  -/
ENNReal.div_mul_cancel : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → b / a * a = b
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic.0.IsCovariantDerivativeOn.difference.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M}
  (hcov : IsCovariantDerivativeOn F cov s) (hcov' : IsCovariantDerivativeOn F cov' s) [inst_15 : CompleteSpace 𝕜]
  [inst_16 : FiniteDimensional 𝕜 F] [inst_17 : VectorBundle 𝕜 F V] [inst_18 : ContMDiffVectorBundle 1 F V I] (x : M),
  hcov.difference hcov' x =
    if hxs : x ∈ s then TensorialAt.mkHom (fun x_1 => IsCovariantDerivativeOn.differenceAux✝ cov cov' x_1 x) x ⋯ else 0
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- Exponential monomials in `d` variables.  -/
UnitAddTorus.mFourier : {d : Type u_1} → [Fintype d] → (d → ℤ) → C(UnitAddTorus d, ℂ)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.counit_comul_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t]
  {Z : a ⟶ a} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) t ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.counit t) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor t).inv h
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.algebra''' : {K : Type v} →
  [inst : Field K] →
    {n : ℕ} → {f : Polynomial K} → Algebra (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `Real.sinh` as an `Equiv`.  -/
Real.sinhEquiv : ℝ ≃ ℝ
-- Mathlib.Data.Nat.Count
/-- **Alias** of the reverse direction of `Nat.count_succ_eq_succ_count_iff`. -/
Nat.count_succ_eq_succ_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, p n → Nat.count p (n + 1) = Nat.count p n + 1
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.uniqueProd_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Unique M₂] (a : M₂ × M), LinearEquiv.uniqueProd a = a.2
-- Mathlib.Order.Filter.Cofinite
/-- Every filter is the disjoint supremum of
a principal filter and a free filter in a unique way.  -/
existsUnique_eq_principal_sup_free : ∀ {α : Type u_2} (f : Filter α),
  ∃! p, p.2 ≤ Filter.cofinite ∧ Disjoint (Filter.principal p.1) p.2 ∧ f = Filter.principal p.1 ⊔ p.2
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofClosedSubgroup.eq_1 : ∀ {G : ProfiniteGrp.{u_1}} (H : ClosedSubgroup ↑G.toProfinite.toTop),
  ProfiniteGrp.ofClosedSubgroup H = ProfiniteGrp.of ↥↑H
-- Mathlib.Data.Finsupp.Order
Finsupp.isOrderedAddMonoid : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α],
  IsOrderedAddMonoid (ι →₀ α)
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- A base of a root system yields a basis of the root space.  -/
RootPairing.Base.toWeightBasis : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} → (b : P.Base) → [P.IsRootSystem] → Module.Basis (↥b.support) R M
-- Mathlib.ModelTheory.Substructures
/-- Indicates that a set in a given structure is a closed under a function symbol.  -/
FirstOrder.Language.ClosedUnder : {L : FirstOrder.Language} → {M : Type w} → [L.Structure M] → {n : ℕ} → L.Functions n → Set M → Prop
-- Mathlib.Tactic.FunProp.Types
/-- Pretty print `FunProp.Origin`.  -/
Mathlib.Meta.FunProp.ppOrigin : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Mathlib.Meta.FunProp.Origin → m Lean.MessageData
-- Std.Data.DTreeMap.Basic
/-- Removes all mappings of the map for which the given function returns `false`.  -/
Std.DTreeMap.filter : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → ((a : α) → β a → Bool) → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
dvd_nsmul_of_dvd : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {x y : R} (n : ℕ), x ∣ y → x ∣ n • y
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.instFinCategoryOfLOfDecidableEqR.match_7.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive :
      (b : J.R) →
        (a : J.L) →
          (CategoryTheory.Limits.WalkingMulticospan.left a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b) →
            J.fst b = a → J.snd b = a → Sort u_3) →
    (b : J.R) →
      (a : J.L) →
        (x : CategoryTheory.Limits.WalkingMulticospan.left a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b) →
          (h₁ : J.fst b = a) →
            (h₂ : J.snd b = a) →
              ((a : J.R) →
                  (h₁ : J.fst a = J.fst a) →
                    (h₂ : J.snd a = J.fst a) →
                      motive a (J.fst a) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst a) h₁ h₂) →
                ((a : J.R) →
                    (h₁ : J.fst a = J.snd a) →
                      (h₂ : J.snd a = J.snd a) →
                        motive a (J.snd a) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd a) h₁ h₂) →
                  motive b a x h₁ h₂
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.checkAux.checkLambdaLet : Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Unit Lean.MetaM Unit
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles_naturality : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L)
  (i j : ι) [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology i] [inst_5 : L.HasHomology j],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (L.opcyclesToCycles i j) =
    CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (HomologicalComplex.cyclesMap φ j)
-- Lean.Meta.AppBuilder
Lean.Meta.mkEqMPR : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visit : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.smul : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] {R : Type u_4} [inst_2 : AddGroup E] [inst_3 : DistribSMul R E]
  [MeasurableConstSMul R E],
  ProbabilityTheory.HasIndepIncrements X P → ∀ (c : R), ProbabilityTheory.HasIndepIncrements (fun t ω => c • X t ω) P
-- Mathlib.Order.Filter.Bases.Basic
/-- A set `t` belongs to a filter `l` iff it includes an element of the basis.  -/
Filter.HasBasis.mem_iff' : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
-- Mathlib.Order.RelIso.Set
Subrel.instTrichotomousSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Trichotomous r] (p : α → Prop), Std.Trichotomous (Subrel r p)
-- Mathlib.Dynamics.FixedPoints.Prufer
/-- Let `n : ℤ` and `s` a subset of an additive commutative group `G` that is invariant
under preimage for the map `x ↦ n • x`. Then `s` is invariant under the pointwise action of
the additive subgroup of elements `g : G` such that `(n^j) • g = 0` for some `j : ℕ`.
(This additive subgroup is called the Prüfer subgroup when `G` is the `AddCircle` and `n` is
prime.)  -/
vadd_eq_self_of_preimage_zsmul_eq_self : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℤ} {s : Set G},
  (fun x => n • x) ⁻¹' s = s → ∀ {g : G} {j : ℕ}, n ^ j • g = 0 → g +ᵥ s = s
-- Mathlib.Data.W.Constructions
WType.toList.eq_2 : ∀ (γ : Type u) (hd : γ) (f : WType.Listβ γ (WType.Listα.cons hd) → WType (WType.Listβ γ)),
  WType.toList γ (WType.mk (WType.Listα.cons hd) f) = hd :: WType.toList γ (f PUnit.unit)
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If a function defined on a topological group has compact support, then either
the function is trivial or the group is locally compact.  -/
HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] [inst_4 : Zero α] [T1Space α] {f : G → α},
  HasCompactSupport f → Continuous f → f = 0 ∨ LocallyCompactSpace G