mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_fromBlocks_zero₂₁ : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₂ : Matrix n n R),
  (Matrix.fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
-- Mathlib.Data.Set.Function
Function.Semiconj.surjOn_image : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s t : Set α},
  Function.Semiconj f fa fb → Set.SurjOn fa s t → Set.SurjOn fb (f '' s) (f '' t)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousOn.div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (f / g) s
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMap_symm_apply' : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₂ e₂] {b : B},
  b ∈ e₁.baseSet ∩ e₂.baseSet →
    ∀ (L : F₁ →SL[σ] F₂),
      (Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂).symm b L =
        Bundle.Trivialization.symmL 𝕜₂ e₂ b ∘SL L ∘SL Bundle.Trivialization.continuousLinearMapAt 𝕜₁ e₁ b
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMinSealed.eq_1 : ∀ (n : ℕ), BitVec.Signed.intMinSealed✝ n = ↑(2 ^ (n - 1))
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.of_add_one_of_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f : ℤ → M},
  (Summable fun n => f (↑n + 1)) → (Summable fun n => f (-(↑n + 1))) → Summable f
-- Init.Prelude
/-- Folds a function over a list from the left, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in order, using `f`.

Examples:
 * `[a, b, c].foldl f z  = f (f (f z a) b) c`
 * `[1, 2, 3].foldl (· ++ toString ·) "" = "123"`
 * `[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"`
 -/
List.foldl : {α : Type u} → {β : Type v} → (α → β → α) → α → List β → α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The assumption that the pullback of `X i₁` and `X i₂` over `S` exists
for any `i₁` and `i₂`.  -/
CategoryTheory.PreZeroHypercover.HasPullbacks : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.PreZeroHypercover S → Prop
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- `maxTensorProduct` is functorial: the image of a maximal tensor product under
`TensorProduct.map f g` is contained in the maximal tensor product of the images.  -/
PointedCone.maxTensorProduct_map_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {G' : Type u_4} {H' : Type u_5} [inst_7 : AddCommGroup G'] [inst_8 : Module R G'] [inst_9 : AddCommGroup H']
  [inst_10 : Module R H'] (f : G →ₗ[R] G') (g : H →ₗ[R] H') (C₁ : PointedCone R G) (C₂ : PointedCone R H),
  PointedCone.map (TensorProduct.map f g) (C₁.maxTensorProduct C₂) ≤
    (PointedCone.map f C₁).maxTensorProduct (PointedCone.map g C₂)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Given `φ : F ⟶ G`, this is the cochain in `Cochain (mappingCone φ) K n` that is
constructed from two cochains `α : Cochain F K m` (with `m + 1 = n`) and `β : Cochain F K n`.  -/
CochainComplex.mappingCone.liftCochain : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              {n m : ℤ} →
                CochainComplex.HomComplex.Cochain K F m →
                  CochainComplex.HomComplex.Cochain K G n →
                    n + 1 = m → CochainComplex.HomComplex.Cochain K (CochainComplex.mappingCone φ) n
-- Mathlib.Topology.Sheaves.Flasque
TopCat.Presheaf.IsFlasque.pushforward_isFlasque : ∀ {X : TopCat} {C : Type v} [inst : CategoryTheory.Category.{w, v} C] (F : TopCat.Presheaf C X) {Y : TopCat}
  [F.IsFlasque] (f : X ⟶ Y), ((TopCat.Presheaf.pushforward C f).obj F).IsFlasque
-- Mathlib.CategoryTheory.GradedObject.Single
/-- The canonical isomorphism `(single j).obj X j ≅ X`.  -/
CategoryTheory.GradedObject.singleObjApplyIso : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Limits.HasInitial C] →
        [inst_2 : DecidableEq J] → (j : J) → (X : C) → (CategoryTheory.GradedObject.single j).obj X j ≅ X
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instMonoid.eq_1 : ∀ {α : Type u_1} [inst : Monoid α],
  Colex.instMonoid =
    { toSemigroup := Colex.instSemigroup, toOne := Colex.instOne, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow,
      npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_eq : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α} {F : Set α},
  y ∈ connectedComponentIn F x → connectedComponentIn F x = connectedComponentIn F y
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.mul_ones : ∀ {w : ℕ} (a : BitVec w), a * -1#w = -a
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_mk : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] {f : α → β}
  (hf : Continuous f) (hf' : Filter.Tendsto f (Filter.cocompact α) (nhds 0)),
  ⇑{ toFun := f, continuous_toFun := hf, zero_at_infty' := hf' } = f
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.linear_eq_sumCoords : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (i : ι), (b.coord i).linear = -(b.basisOf i).sumCoords
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivWithinAt_congr_set : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  s =ᶠ[nhds x] t → (HasMFDerivAt[s] f x f' ↔ HasMFDerivAt[t] f x f')
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.hom₁.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [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} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (j j' : J),
  HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j' =
    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalDesc fun i₁ i₂ x =>
      c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
        CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂))
          (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂))
            (L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j'))
-- Init.Data.List.Monadic
List.flatMapM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {l : List { x // p x }} {f : { x // p x } → m (List β)} {g : α → m (List β)},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.flatMapM f l = List.flatMapM g l.unattach
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetsResponse.mk.sizeOf_spec : ∀ (widgets : Array Lean.Widget.PanelWidgetInstance), sizeOf { widgets := widgets } = 1 + sizeOf widgets
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk.inj : ∀ {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.AddMonObj A} {M N : CategoryTheory.AddMod D A} {hom : M.X ⟶ N.X}
  {isAddModHom : CategoryTheory.IsAddModHom A hom} {hom_1 : M.X ⟶ N.X}
  {isAddModHom_1 : CategoryTheory.IsAddModHom A hom_1},
  { hom := hom, isAddModHom := isAddModHom } = { hom := hom_1, isAddModHom := isAddModHom_1 } → hom = hom_1
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.HasExplicitPullbacks.hasProp : ∀ {P : TopCat → Prop} [self : CompHausLike.HasExplicitPullbacks P] {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B),
  CompHausLike.HasExplicitPullback f g
-- Mathlib.Order.Minimal
Maximal.and_right : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Maximal P x → Q x → Maximal (fun x => P x ∧ Q x) x
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.isIso_of_f_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f : X ⟶ Y) [CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
-- Mathlib.Order.Filter.Basic
Filter.sets_ssubset_sets : ∀ {α : Type u} {f g : Filter α}, f.sets ⊂ g.sets ↔ g < f
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'_eq_wf : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  [LawfulMonad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {γ : Type x}
  (Pl : β → γ → ForInStep γ → Prop) (wf : Std.IteratorLoop.WellFounded α m Pl) {it : Std.IterM m β} {init : γ}
  {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b}
  (f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))),
  Std.IterM.DefaultConsumers.forIn' lift γ Pl it init P hP f =
    Std.IterM.DefaultConsumers.forIn'.wf lift γ Pl wf it init P hP f
-- Init.Data.Dyadic.Basic
Dyadic.neg_mul : ∀ (x y : Dyadic), -x * y = -(x * y)
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.import.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Function.Basic
Function.rightInverse_iff_comp : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse f g ↔ g ∘ f = id
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_const : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [inst : ENorm ε] (c : ε),
  0 < q → MeasureTheory.eLpNorm' (fun x => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instLawfulBEqPower : LawfulBEq Lean.Grind.CommRing.Power
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.comul_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] (c : CategoryTheory.WideSubcategory P)
  [inst_3 : CategoryTheory.ComonObj c.obj] [inst_4 : P.IsStableUnderComonoid c.obj],
  CategoryTheory.ComonObj.comul.hom = CategoryTheory.ComonObj.comul
-- Mathlib.NumberTheory.EulerProduct.Basic
tsum_eq_tsum_primes_of_support_subset_prime_powers : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  Summable f → Function.support f ⊆ {n | IsPrimePow n} → ∑' (n : ℕ), f n = ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Adds `DelabTermInfo` at the given position.

Either `docString?` or `mkDocString?` can be provided. The `docString?` field is a convenient
interface for `mkDocString?`.
 -/
Lean.PrettyPrinter.Delaborator.addDelabTermInfo : Lean.SubExpr.Pos →
  Lean.Syntax →
    Lean.Expr →
      optParam Bool false →
        optParam (Option Lean.DeclarationLocation) none →
          optParam (Option String) none →
            optParam (Option (Lean.PPContext → IO String)) none →
              optParam Bool true → Lean.PrettyPrinter.Delaborator.DelabM Unit
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquiv_counitIso : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C],
  (CategoryTheory.functorProdFunctorEquiv A B C).counitIso = CategoryTheory.functorProdFunctorEquivCounitIso A B C
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.reduced.inj : ∀ {val val_1 : Lean.Expr},
  Lean.Meta.ReduceMatcherResult.reduced val = Lean.Meta.ReduceMatcherResult.reduced val_1 → val = val_1
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsDominant
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F` commutes with shifts, so does `F.op`, for the shifts chosen on `Cᵒᵖ` in
`CategoryTheory.Triangulated.Opposite.Basic`.
 -/
CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] → (F : CategoryTheory.Functor C D) → [F.CommShift ℤ] → F.op.CommShift ℤ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_mod_two_pow : ∀ {a b n : ℕ}, (a ^^^ b) % 2 ^ n = a % 2 ^ n ^^^ b % 2 ^ n
-- Mathlib.Data.NNReal.Defs
Real.toNNReal.eq_1 : ∀ (r : ℝ), r.toNNReal = NNReal.mk (max r 0) ⋯
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.extra : Lean.Meta.Grind.Params → Lean.PArray Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x : αᵒᵈ}, Set.Iic (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ici x
-- Lean.Elab.Tactic.LibrarySearch
_private.Lean.Elab.Tactic.LibrarySearch.0.Lean.Elab.LibrarySearch.elabLibrarySearchConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Parser.Tactic.LibrarySearchConfig
-- Batteries.Data.List.Count
List.rightInverse_idxToSigmaCount_sigmaCountToIdx : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α},
  Function.RightInverse xs.idxToSigmaCount xs.sigmaCountToIdx
-- Mathlib.Logic.Function.Coequalizer
/-- The relation generating the equivalence relation used for defining `Function.coequalizer`.  -/
Function.Coequalizer.Rel : {α : Type u_1} → {β : Type u_2} → (α → β) → (α → β) → β → β → Prop
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.ext : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {f g : CentroidHom α}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Algebra.Group.Action.Prod
/-- Construct an `AddAction` by a product monoid from `AddAction`s by the factors.
This is not an instance to avoid diamonds for example when `α := M × N`.  -/
AddAction.prodOfVAddCommClass : (M : Type u_1) →
  (N : Type u_2) →
    (α : Type u_5) →
      [inst : AddMonoid M] →
        [inst_1 : AddMonoid N] →
          [inst_2 : AddAction M α] → [inst_3 : AddAction N α] → [VAddCommClass M N α] → AddAction (M × N) α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The converse of this is true with additional assumptions, see `epi_iff_epi_left`.  -/
CategoryTheory.CostructuredArrow.epi_of_epi_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B)
  [h : CategoryTheory.Epi f.left], CategoryTheory.Epi f
-- Init.Data.BitVec.Lemmas
BitVec.getElem_not : ∀ {w : ℕ} {x : BitVec w} {i : ℕ} (h : i < w), (~~~x)[i] = !x[i]
-- Mathlib.Order.GaloisConnection.Basic
/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois connection.  -/
gc_Ici_sInf : ∀ {α : Type u} [inst : CompleteSemilatticeInf α],
  GaloisConnection (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
-- Mathlib.Algebra.BigOperators.Associated
Prime.exists_mem_multiset_dvd : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] {p : M₀}, Prime p → ∀ {s : Multiset M₀}, p ∣ s.prod → ∃ a ∈ s, p ∣ a
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.num k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_1 k
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contDiffWithinAtProp_self_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_5 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {f : E → H'}
  {s : Set E} {x : E}, ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) I' n f s x ↔ ContDiffWithinAt 𝕜 n (↑I' ∘ f) s x
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
/-- The equivalence of categories between two fullsubcategories `P` and `Q`
of categories `C` and `D` that is induced by an equivalence `e : C ≌ D`
when `Q.inverseImage e.functor = P` and `Q` respects isomorphisms.  -/
CategoryTheory.Equivalence.congrFullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {P : CategoryTheory.ObjectProperty C} →
          {Q : CategoryTheory.ObjectProperty D} →
            (e : C ≌ D) →
              [Q.IsClosedUnderIsomorphisms] → Q.inverseImage e.functor = P → (P.FullSubcategory ≌ Q.FullSubcategory)
-- Mathlib.Topology.Algebra.Monoid
Continuous.nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M}, Continuous f → ∀ (n : ℕ), Continuous (n • f)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst.congr_simp : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1)
  [inst_5 : μ.IsAddHaarMeasure] (p p_1 : ℝ),
  p = p_1 →
    MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ p = MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ_1 p_1
-- Mathlib.Topology.Instances.Int
Int.pairwise_one_le_dist : Pairwise fun m n => 1 ≤ dist m n
-- Mathlib.Order.Category.PartOrd
PartOrd.hom_id : ∀ {X : PartOrd}, PartOrd.Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id
-- Mathlib.Analysis.Complex.CanonicalDecomposition
Complex.ECanonicalDecomp.mk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  MeromorphicOn f (Metric.closedBall 0 R) →
    AnalyticOnNhd ℂ g (Metric.closedBall 0 R) →
      (∀ u ∈ Metric.closedBall 0 R, g u ≠ 0) →
        f =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 R)]
            ((∏ᶠ (u : ℂ), Complex.canonicalFactor R u ^ (-(MeromorphicOn.divisor f (Metric.ball 0 R)) u)) *
                ∏ᶠ (v : ℂ), (fun x => x - v) ^ (MeromorphicOn.divisor f (Metric.sphere 0 R)) v) •
              g →
          Complex.ECanonicalDecomp f g R
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.unpackMantissa_packComponents : ∀ {spec : Float.Model.Format} {sign : Float.Model.UnpackedFloat.Sign} {exponent : BitVec spec.exponentBits}
  {mantissa : BitVec spec.mantissaBitsWithoutImplicit},
  Float.Model.UnpackedFloat.unpackMantissa (Float.Model.UnpackedFloat.packComponents spec sign exponent mantissa) =
    mantissa
-- Mathlib.Data.Set.Lattice
sSup_sUnion : ∀ {β : Type u_2} [inst : CompleteLattice β] (s : Set (Set β)), sSup (⋃₀ s) = ⨆ t ∈ s, sSup t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_erase : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α}
  {h' : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl a h' =
    Std.DTreeMap.Internal.Impl.Const.get t a ⋯
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.add_rpow_le_rpow_add : ∀ {p : ℝ} (a b : ENNReal), 1 ≤ p → a ^ p + b ^ p ≤ (a + b) ^ p
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.basis_repr : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)),
  (Module.Basis.exteriorPower n b).repr (exteriorPower.ιMulti_family R n (⇑b) s) = fun₀ | s => 1
-- Mathlib.GroupTheory.Frattini
frattini_le_coatom : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G}, IsCoatom K → frattini G ≤ K
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.symmIso_hom : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (SSet.Subcomplex.unionProd.symmIso S T).hom =
    SSet.Subcomplex.lift (CategoryTheory.CategoryStruct.comp (S.unionProd T).ι (β_ X Y).hom) ⋯