mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a linearly ordered type `ι` and `I : MultispanIndex (.prod ι) C`,
this is the isomorphism of functors between
`WalkingMultispan.inclusionOfLinearOrder ι ⋙ I.multispan`
and `I.toLinearOrder.multispan`.  -/
CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) →
        [inst_1 : LinearOrder ι] →
          (CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder ι).comp I.multispan ≅ I.toLinearOrder.multispan
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α],
  MulAction.orbitRel.Quotient G α = Quotient (MulAction.orbitRel G α)
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.instLatticeOfTopologicalLattice : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Lattice β] → [TopologicalLattice β] → Lattice C(α, β)
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.cardinal_eq_two_pow_rank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Cardinal.aleph0 ≤ Module.rank F E → Cardinal.mk (Field.Emb F E) = 2 ^ Module.rank F E
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by multiplication.  -/
ContinuousMonoidHom.mul : (E : Type u_6) → [inst : CommMonoid E] → [inst_1 : TopologicalSpace E] → [ContinuousMul E] → E × E →ₜ* E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_ne_zero_iff : ∀ {θ : Real.Angle}, 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
-- Mathlib.FieldTheory.AxGrothendieck
FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime : ∀ {ι : Type u_1} {α : Type u_2} [inst : Finite α] [inst_1 : Finite ι] {p : ℕ},
  Nat.Prime p →
    ∀ (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)),
      FirstOrder.Language.Theory.ACF p ⊨ᵇ FirstOrder.genericPolyMapSurjOnOfInjOn φ mons
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.extendScalars_Ring : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), P.extendScalars.Ring = P.Ring
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter_eq_filterMap : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Bool},
  Std.DTreeMap.Internal.Impl.filter f t h =
    Std.DTreeMap.Internal.Impl.filterMap (fun k v => if f k v = true then some v else none) t h
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.vComp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans F G)
  (θ : CategoryTheory.Lax.StrongTrans G H) (a : B), (η.vComp θ).app a = (η.toLax.vComp θ.toLax).app a
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {l : Filter α} {c : F''}, c ≠ 0 → ((f'' =o[l] fun _x => c) ↔ Filter.Tendsto f'' l (nhds 0))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {v : β k}, (m.insert k v).get? k = some v
-- Mathlib.Data.Set.Subsingleton
/-- **Alias** of the reverse direction of `Set.not_nontrivial_iff`. -/
Set.Subsingleton.not_nontrivial : ∀ {α : Type u} {s : Set α}, s.Subsingleton → ¬s.Nontrivial
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_inj : ∀ {α : Type u} [inst : AddMonoid α] {a b : AddUnits α}, ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
      [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
      [inst_4 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory A FC]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [J.WEqualsLocallyBijective (Type w)] [CategoryTheory.HasSheafify J (Type w)] {X Y : CategoryTheory.Functor Cᵒᵖ A}
      (f : X ⟶ Y),
      (∀ (Φ : P.FullSubcategory),
          Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
        CategoryTheory.Presheaf.IsLocallySurjective J f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.getArity : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → ℕ
-- Init.Data.BitVec.Bootstrap
BitVec.getLsbD_of_ge : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), w ≤ i → x.getLsbD i = false
-- Std.Data.HashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.HashMap.Raw.WF.out : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}, m.WF → m.inner.WF
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelUp'.eq_1 : ∀ (α : Type u_1) [inst : AddRightCancelSemigroup α] [inst_1 : DecidableEq α] (a x x_1 : α),
  ComplexShape.instDecidableRelRelUp' α a x x_1 = id inferInstance
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.coe_congrOrderIso_apply : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N]
  (e : MulArchimedeanClass M ≃o MulArchimedeanClass N) (a : FiniteMulArchimedeanClass M),
  ↑((FiniteMulArchimedeanClass.congrOrderIso e) a) = e ↑a
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : 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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      h_1
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.instName : Lean.Elab.Deriving.Context → Lean.Name
-- Init.Data.Nat.Basic
/-- A case analysis principle for `Nat` that uses the notations `0` for `Nat.zero` and `n + 1` for
`Nat.succ`.

It is otherwise identical to the default recursor `Nat.casesOn`. It is used as the default `Nat`
case analysis principle for `Nat` by the `cases` tactic.
 -/
Nat.casesAuxOn : {motive : ℕ → Sort u} → (t : ℕ) → motive 0 → ((n : ℕ) → motive (n + 1)) → motive t
-- Mathlib.Data.ENat.Basic
ENat.natCast_lt_succ : ∀ {n : ℕ}, ↑n < ↑n + 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.alter.match_3.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.eq = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.eq = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.eq with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_3 ⋯
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_two : Nat.fermatNumber 2 = 17
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Get all potential rewrite lemmas from the current file. Exclude lemmas from modules
in the `librarySearch.excludedModules` option.  -/
Mathlib.Tactic.LibraryRewrite.getModuleCandidates : Lean.Expr → Lean.MetaM (Array (Array Mathlib.Tactic.LibraryRewrite.RewriteLemma))
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_Icc_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Icc a b)) (Filter.principal (Set.Icc a b))
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₁.congr_simp : ∀ (w w_1 : UInt8) (e_w : w = w_1)
  (h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done),
  ByteArray.utf8DecodeChar?.assemble₁ w h = ByteArray.utf8DecodeChar?.assemble₁ w_1 ⋯
-- Init.Data.Char.Ordinal
/-- The size of the `Char` type.  -/
Char.numCodePoints : ℕ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CFC.conjugate_rpow_neg_one_half : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : A),
  autoParam (IsStrictlyPositive a) CFC.conjugate_rpow_neg_one_half._auto_1 → a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_norm_le_norm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖-a + b‖
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α),
  (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n
-- Init.Data.Range.Polymorphic.SInt
ISize.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite ISize
-- Mathlib.Logic.Equiv.Set
Equiv.Set.image.congr_simp : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Function.Injective f),
  Equiv.Set.image f s H = Equiv.Set.image f s H
-- Mathlib.Data.Seq.Computation
/-- Alternate definition of `LiftRel` over relations between `Computation`s  -/
Computation.LiftRelAux : {α : Type u} →
  {β : Type v} → (α → β → Prop) → (Computation α → Computation β → Prop) → α ⊕ Computation α → β ⊕ Computation β → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.maxKey? = some km → (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.const_add` -/
InnerProductSpace.HarmonicContOnCl.fun_const_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl (fun i => c + f i) s
-- Mathlib.Algebra.Group.Action.Hom
AddAction.IsPretransitive.of_compHom : ∀ {M : Type u_4} {N : Type u_5} {α : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddAction N α]
  (f : M →+ N) [h : AddAction.IsPretransitive M α], AddAction.IsPretransitive N α
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- The Yoneda lemma yields a natural transformation `yonedaCollectionPresheaf A F ⟶ A`.  -/
CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) →
        CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F ⟶ A
-- Mathlib.NumberTheory.Height.Basic
_private.Mathlib.NumberTheory.Height.Basic.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {x : ι → K},
  x ≠ 0 → Function.HasFiniteMulSupport fun v => ⨆ i, ↑v (x i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_of_gt_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    ∀ (x : S.obj (Opposite.op { len := n + 1 })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.succ))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j.castSucc)) x) =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i)) x)
-- Mathlib.Data.List.GetD
List.getD_eq_get : ∀ {α : Type u} (l : List α) (d : α) (i : Fin l.length), l.getD (↑i) d = l.get i
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (F : CategoryTheory.Sheaf J (Type v))
  (sq : CategoryTheory.Square C),
  (sq.op.map
        ((CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v))).op.comp
          (CategoryTheory.yoneda.obj F))).IsPullback ↔
    (sq.op.map F.obj).IsPullback
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.isProbabilityMeasure : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module ℝ E],
  ProbabilityTheory.IsGaussianProcess X P → MeasureTheory.IsProbabilityMeasure P
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variables to divisibility constraints. Recall that we keep the divisibility constraint in solved form.
Thus, we have at most one divisibility per variable.  -/
Lean.Meta.Grind.Arith.Cutsat.State.dvds : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)
-- Init.Prelude
MonadEvalT.mk : {m : Type u → Type v} → {n : Type u → Type w} → ({α : Type u} → m α → n α) → MonadEvalT m n
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_two_iff' : ∀ {α : Type u_1} (x : α), Nat.card α = 2 ↔ ∃! y, y ≠ x
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinder.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : ↥s) → α ↑i)),
  MeasureTheory.cylinder s S = s.restrict ⁻¹' S
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.root_ne_neg_of_ne : ∀ {ι : 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)
  [Nontrivial R] {i j : ι}, i ∈ b.support → j ∈ b.support → i ≠ j → P.root i ≠ -P.root j
-- Std.Data.DTreeMap.Internal.Operations
/-- The key.  -/
Std.DTreeMap.Internal.Impl.View.k : {α : Type u} → {β : α → Type v} → {size : ℕ} → Std.DTreeMap.Internal.Impl.View α β size → α
-- Mathlib.Order.Filter.Subsingleton
Filter.Subsingleton.map : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α}, l.Subsingleton → ∀ (f : α → β), (Filter.map f l).Subsingleton
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.eq_left : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → p.Splits t₃ t₄ → t₁ = t₃
-- Mathlib.Analysis.Convex.Between
wbtw_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Wbtw R x y z ↔ Wbtw R z y x
-- Lean.Parser.Syntax
Lean.Parser.Command.macroTail.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.DocString.Types
Lean.Doc.instReprListItem : {α : Type u_1} → [Repr α] → Repr (Lean.Doc.ListItem α)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_neg : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), ∀ U ∈ p.basisSets, ∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U
-- Lean.Elab.DocString
Lean.Doc.instReprSuggestionMode.repr : Lean.Doc.SuggestionMode → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.basis_repr_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (l : ι →₀ R),
  h.basis.repr.symm l = Module.DualBases.lc e l
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- The derivative of `star ∘ f ∘ conj` is `star ∘ deriv f ∘ conj`.  -/
deriv_star_conj : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] [NormedStarGroup 𝕜]
  {f : 𝕜 → F}, deriv (star ∘ f ∘ ⇑(starRingEnd 𝕜)) = star ∘ deriv f ∘ ⇑(starRingEnd 𝕜)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isBigO_logb_const_mul_log_atTop : ∀ {b : ℝ} (c : ℝ), (fun x => Real.logb b (c * x)) =O[Filter.atTop] Real.log
-- Init.Data.List.Lemmas
List.not_any_eq_all_not : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, (!l.any p) = l.all fun a => !p a
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_Icc : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.image (Fin.castLE h) (Finset.Icc a b) = Finset.Icc (Fin.castLE h a) (Fin.castLE h b)
-- Lean.Data.KVMap
Lean.instReprDataValue.repr : Lean.DataValue → ℕ → Std.Format
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.mk : {α : Type} →
  Std.Queue (IO.Promise Bool) →
    Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α) →
      (capacity : ℕ) →
        Vector (IO.Ref (Option α)) capacity →
          ℕ →
            (sendIdx : ℕ) →
              sendIdx < capacity → (recvIdx : ℕ) → recvIdx < capacity → Bool → Std.CloseableChannel.Bounded.State✝ α
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.instAway : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R), Algebra.IsStandardOpenImmersion R (Localization.Away r)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_comm : ∀ (z w : UpperHalfPlane), dist z w = dist w z
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.proj_apply : ∀ (p : ENNReal) {𝕜 : Type u_1} {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)] (i : ι) (x : PiLp p β),
  (PiLp.proj p β i) x = x.ofLp i
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.familyOfBFamily.eq_1 : ∀ {α : Type u_1} (o : Ordinal.{u_3}) (f : (a : Ordinal.{u_3}) → a < o → α),
  o.familyOfBFamily f = Ordinal.familyOfBFamily' (fun x1 x2 => x1 < x2) ⋯ f
-- Init.Data.UInt.Bitwise
USize.shiftRight_xor : ∀ {a b c : USize}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_eq_pow_card : ∀ {α : Type u_3} [inst : Monoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (m : α),
  (∀ x ∈ s, x = m) → s.noncommProd comm = m ^ s.card
-- Init.Data.Int.Gcd
Int.lcm_eq_right : ∀ {b a : ℤ}, 0 ≤ b → a ∣ b → ↑(a.lcm b) = b
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.startsWithVar : Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Bool
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.const : Lean.Name → ℕ → Lean.Meta.LazyDiscrTree.Key
-- Init.Coe
/-- `↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
typeclasses to resolve a suitable conversion function. You can often leave the
`↑` off entirely, since coercion is triggered implicitly whenever there is a
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
between e.g. `↑x + ↑y` and `↑(x + y)`.
 -/
coeNotation : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_add_succ_right_eq_append : ∀ {m n : ℕ}, (m...m + n + 1).toList = (m...m + n).toList ++ [m + n]
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Let `K / k / A⟮X⟯ / A[X]` be a tower. If `K / k / A[X]` is a scalar tower
then so is `K / k / A⟮X⟯`.  -/
RatFunc.instIsScalarTowerOfPolynomial_1 : ∀ (A : Type u_1) (k : Type u_2) (K : Type u_3) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Field k]
  [inst_3 : Field K] [inst_4 : Algebra (Polynomial A) k] [inst_5 : Algebra (Polynomial A) K] [inst_6 : SMul k K]
  [inst_7 : FaithfulSMul (Polynomial A) k] [inst_8 : FaithfulSMul (Polynomial A) K] [IsScalarTower (Polynomial A) k K],
  IsScalarTower (RatFunc A) k K
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientMulEquivOfEq_mk : ∀ {G : Type u} [inst : Group G] {M N : Subgroup G} [inst_1 : M.Normal] [inst_2 : N.Normal] (h : M = N) (x : G),
  (QuotientGroup.quotientMulEquivOfEq h) ↑x = ↑x
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LeftPreLieAlgebra.instLieAdmissibleAlgebra : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : LeftPreLieRing L] → [LeftPreLieAlgebra R L] → LieAdmissibleAlgebra R L
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.toSSetObj₁Equiv_apply_one : ∀ {X : TopCat} (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := 1 })),
  (CategoryTheory.ConcreteCategory.hom (TopCat.toSSetObj₁Equiv s)) 1 =
    TopCat.toSSetObj₀Equiv
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) 0)) s)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instIsScalarTower' : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] {S : NonUnitalSubalgebra R A} [inst_3 : Semiring R'] [inst_4 : SMul R' R] [inst_5 : Module R' A]
  [inst_6 : IsScalarTower R' R A], IsScalarTower R' R ↥S
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.isTrueCond : Lean.Expr → Bool
-- Mathlib.Analysis.MeanInequalities
Real.summable_mul_of_Lp_Lq_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q : ℝ},
  p.HolderConjugate q →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) → (Summable fun i => f i ^ p) → (Summable fun i => g i ^ q) → Summable fun i => f i * g i
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.locallyFinite_tsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s),
  LocallyFinite fun i => tsupport ⇑(f i)
-- Mathlib.Algebra.Group.Prod
AddEquiv.coe_prodComm_symm : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N], ⇑AddEquiv.prodComm.symm = Prod.swap