mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iio.injEq : ∀ (n n_1 : Lean.Term), (BigOperators.FinsetResult.Iio✝ n = BigOperators.FinsetResult.Iio✝ n_1) = (n = n_1)
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioo_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (b₁ b₂ : β),
  Finset.Ioo (Sum.inrₗ b₁) (Sum.inrₗ b₂) =
    Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioo b₁ b₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_surjective : ∀ {n : ℕ}, Function.Surjective SSet.stdSimplex.objMk₁
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV1.mk.injEq : ∀ (header : Std.Time.TimeZone.TZif.Header) (transitionTimes : Array ℤ) (transitionIndices : Array UInt8)
  (localTimeTypes : Array Std.Time.TimeZone.TZif.LocalTimeType) (abbreviations : Array String)
  (leapSeconds : Array Std.Time.TimeZone.TZif.LeapSecond) (stdWallIndicators utLocalIndicators : Array Bool)
  (header_1 : Std.Time.TimeZone.TZif.Header) (transitionTimes_1 : Array ℤ) (transitionIndices_1 : Array UInt8)
  (localTimeTypes_1 : Array Std.Time.TimeZone.TZif.LocalTimeType) (abbreviations_1 : Array String)
  (leapSeconds_1 : Array Std.Time.TimeZone.TZif.LeapSecond) (stdWallIndicators_1 utLocalIndicators_1 : Array Bool),
  ({ header := header, transitionTimes := transitionTimes, transitionIndices := transitionIndices,
        localTimeTypes := localTimeTypes, abbreviations := abbreviations, leapSeconds := leapSeconds,
        stdWallIndicators := stdWallIndicators, utLocalIndicators := utLocalIndicators } =
      { header := header_1, transitionTimes := transitionTimes_1, transitionIndices := transitionIndices_1,
        localTimeTypes := localTimeTypes_1, abbreviations := abbreviations_1, leapSeconds := leapSeconds_1,
        stdWallIndicators := stdWallIndicators_1, utLocalIndicators := utLocalIndicators_1 }) =
    (header = header_1 ∧
      transitionTimes = transitionTimes_1 ∧
        transitionIndices = transitionIndices_1 ∧
          localTimeTypes = localTimeTypes_1 ∧
            abbreviations = abbreviations_1 ∧
              leapSeconds = leapSeconds_1 ∧
                stdWallIndicators = stdWallIndicators_1 ∧ utLocalIndicators = utLocalIndicators_1)
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Additive (Multiplicative G)` is just `G`.  -/
AddEquiv.additiveMultiplicative : (G : Type u_2) → [inst : AddZeroClass G] → Additive (Multiplicative G) ≃+ G
-- Init.Core
iff_true_right : ∀ {a b : Prop}, a → ((b ↔ a) ↔ b)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_hom_id_left_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T}
  (h : g.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.hom) h) =
    h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Init.Grind.ToInt
/-- The embedding into the integers takes modulo to modulo (without needing to wrap into the range interval).
 -/
Lean.Grind.ToInt.Mod : (α : Type u) → [Mod α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_prodMk : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {s : Set M} {x : M} {f : M → M'} {g : M → M''},
  MDiffAt[s] f x →
    MDiffAt[s] g x → UniqueMDiffAt[s] x → (mfderiv[s] fun x => (f x, g x)) x = (mfderiv[s] f x).prod (mfderiv[s] g x)
-- Mathlib.Data.List.AList
AList.keys_empty : ∀ {α : Type u} {β : α → Type v}, ∅.keys = []
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.extendUpdatedVarsAux.update : Lean.Elab.Term.Do.VarSet → Lean.Elab.Term.Do.Code → Lean.Elab.TermElabM Lean.Elab.Term.Do.Code
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_zero_iff : ∀ {V : Type u} {G : SimpleGraph V}, G.Colorable 0 ↔ IsEmpty V
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.elabFunBindersAux : Array Lean.Syntax → ℕ → Lean.Elab.Term.FunBinders.State → Lean.Elab.TermElabM Lean.Elab.Term.FunBinders.State
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a meromorphic function `f` at `z₀` is finite iff `f` can locally be
written as `f z = (z - z₀) ^ order • g z`, where `g` is analytic and does not
vanish at `z₀`.
 -/
meromorphicOrderAt_ne_top_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  MeromorphicAt f z₀ →
    (meromorphicOrderAt f z₀ ≠ ⊤ ↔
      ∃ g,
        AnalyticAt 𝕜 g z₀ ∧
          g z₀ ≠ 0 ∧ f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun z => (z - z₀) ^ (meromorphicOrderAt f z₀).untop₀ • g z)
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instSDiff : {α : Type u} → {cmp : α → α → Ordering} → SDiff (Std.TreeSet.Raw α cmp)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₂₃_comp_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G × G → ↑A),
  (CategoryTheory.ConcreteCategory.hom
        (CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) 2 3))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₃ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.d₂₃ A)) x)
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_self : ∀ {a : ℤ} (b : ℤ), 0 ≤ a → a / b ≤ a
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.le_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsSemitopologicalRing R] (s : Subring R),
  s ≤ s.topologicalClosure
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSubtypePathLength : {V : Type u} →
  (G : SimpleGraph V) →
    [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype { p // p.IsPath ∧ p.length = n }
-- Init.Data.Nat.Lemmas
Nat.log2_zero : Nat.log2 0 = 0
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMotivesNonConst : Lean.Options → Bool
-- Std.Time.Date.PlainDate
/-- The month component of the date. It is represented as an `Ordinal` type from `Month`.  -/
Std.Time.PlainDate.month : Std.Time.PlainDate → Std.Time.Month.Ordinal
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the inverse direction of the isomorphism
`PreservesColimit₂.isoObjCoconePointsOfIsColimit` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone K₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cocone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsColimit c₃) (j : J₁ × J₂) {Z : C} (h : (G.obj c₁.pt).obj c₂.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c₃.ι.app j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv h) =
    CategoryTheory.CategoryStruct.comp ((G.map (c₁.ι.app j.1)).app (K₂.obj j.2))
      (CategoryTheory.CategoryStruct.comp ((G.obj c₁.pt).map (c₂.ι.app j.2)) h)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_embedding : ∀ {α β : Type u} (f : α ↪ β) (s : Set α), Cardinal.mk ↑(⇑f '' s) = Cardinal.mk ↑s
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.le_expGrowthInf_iff : ∀ {u : ℕ → ENNReal} {a : EReal}, a ≤ ExpGrowth.expGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in Filter.atTop, (b * ↑n).exp ≤ u n
-- Std.Internal.UV.Loop
/-- Block a SIGPROF signal when polling for new events. It's commonly used for unnecessary wakeups
when using a sampling profiler.
 -/
Std.Internal.UV.Loop.Options.blockSigProfSignal : Std.Internal.UV.Loop.Options → Bool
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.inr_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsLimit t.toCone),
  t.inr = CategoryTheory.Limits.BinaryFan.IsLimit.lift ht 0 (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Probability.Moments.Basic
/-- The moment-generating function is monotone in the random variable for `t ≥ 0`.  -/
ProbabilityTheory.mgf_mono_of_nonneg : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ},
  X ≤ᵐ[μ] Y →
    0 ≤ t →
      MeasureTheory.Integrable (fun ω => Real.exp (t * Y ω)) μ →
        ProbabilityTheory.mgf X μ t ≤ ProbabilityTheory.mgf Y μ t
-- Mathlib.Data.List.AList
AList.mk : {α : Type u} → {β : α → Type v} → (entries : List (Sigma β)) → entries.NodupKeys → AList β
-- Mathlib.Tactic.Ring.Common
/-- Exponentiates two polynomials `va, vb`.

* `a ^ 0 = 1`
* `a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂`
 -/
Mathlib.Tactic.Ring.Common.evalPow : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a : Q(«$α»)} →
              {b : Q(ℕ)} →
                Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                  Mathlib.Tactic.Ring.Common.ExSumNat b →
                    Lean.MetaM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» ^ «$b»))
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_sub : ∀ {R : Type u} {a b : R} [inst : Ring R], Polynomial.C (a - b) = Polynomial.C a - Polynomial.C b
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (match Lean.Grind.CommRing.Poly.add k m p with
    | Lean.Grind.CommRing.Poly.num k => h_1 k
    | Lean.Grind.CommRing.Poly.add k m p => h_2 k m p) =
    h_2 k m p
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairEquiv_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D'),
  (CategoryTheory.Join.mapPairEquiv e e').functor = CategoryTheory.Join.mapPair e.functor e'.functor
-- Mathlib.Data.Multiset.Replicate
Multiset.count_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α) (n : ℕ),
  Multiset.count a (Multiset.replicate n b) = if b = a then n else 0
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.linearMapEquiv_symm_apply : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N), h.linearMapEquiv.symm s = h.desc s
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
/-- Inductive construction of homotopies from `P q` to `𝟙 _`  -/
AlgebraicTopology.DoldKan.homotopyPToId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (X : CategoryTheory.SimplicialObject C) →
        (q : ℕ) →
          Homotopy (AlgebraicTopology.DoldKan.P q)
            (CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X))
-- Std.Internal.Parsec.String
_private.Std.Internal.Parsec.String.0.Std.Internal.Parsec.String.digitsCore.go : {s : String} → s.Pos → ℕ → ℕ × s.Pos
-- Mathlib.CategoryTheory.Types.Basic
equivIsoIso_hom : ∀ {X Y : Type u}, equivIsoIso.hom = TypeCat.ofHom fun e => e.toIso
-- Mathlib.Combinatorics.Graph.Basic
Graph.Compatible.isLink_congr : ∀ {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β},
  e ∈ G.edgeSet → e ∈ H.edgeSet → G.Compatible H → ∀ {x y : α}, G.IsLink e x y ↔ H.IsLink e x y
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- **Alias** of `Subgroup.smul_algebraMap`. -/
smul_eq_self : ∀ {G : Type u_1} (B : Type u_3) [inst : Group G] [inst_1 : Semiring B] [inst_2 : MulSemiringAction G B] {C : Type u_4}
  [inst_3 : CommSemiring C] [inst_4 : Algebra C B] {H : Subgroup G} [SMulCommClass (↥H) C B] {g : G},
  g ∈ H → ∀ (x : C), g • (algebraMap C B) x = (algebraMap C B) x
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_add_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y z : E), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G)
  (a : F.CoGrothendieck), ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).obj a).base = a.base
-- Mathlib.Data.Matrix.Block
Matrix.dotProduct_block : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_12} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : Mul α]
  [inst_3 : AddCommMonoid α] (v w : m ⊕ n → α), v ⬝ᵥ w = v ∘ Sum.inl ⬝ᵥ w ∘ Sum.inl + v ∘ Sum.inr ⬝ᵥ w ∘ Sum.inr
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.lower.sizeOf_spec : sizeOf Lean.FuzzyMatching.CharType.lower = 1
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.withDensity_rnDeriv_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ.MutuallySingular ν
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.meas_inter : ∀ {α : Type u_1} {Ω : Type u_2} {γ : Type u_6} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_10} [mβ : MeasurableSpace β]
  [mγ : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ},
  ProbabilityTheory.Kernel.IndepFun f g κ μ →
    ∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
instLEMultiplicative : {α : Type u_1} → [LE α] → LE (Multiplicative α)
-- Mathlib.Order.ModularLattice
sup_lt_sup_of_lt_of_inf_le_inf : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, y < x → x ⊓ z ≤ y ⊓ z → y ⊔ z < x ⊔ z
-- Mathlib.Data.Nat.SuccPred
Nat.instSuccAddOrder : SuccAddOrder ℕ
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the left.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
      (self.mapComp f' g)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.homEquiv_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A.Hom B),
  Rep.homEquiv f = f.hom
-- Init.Data.SInt.Lemmas
Int16.toInt.eq_1 : ∀ (i : Int16), i.toInt = i.toBitVec.toInt
-- Mathlib.Algebra.Category.Grp.Abelian
/-- The category of abelian groups is abelian.  -/
AddCommGrpCat.instAbelian : CategoryTheory.Abelian AddCommGrpCat
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?_append_eq_some : ∀ {b : ByteArray} {i : ℕ} {c : Char},
  b.utf8DecodeChar? i = some c → ∀ (b' : ByteArray), (b ++ b').utf8DecodeChar? i = some c
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- There is a unique morphism from any object `X` to the zero object.  -/
CategoryTheory.Limits.HasZeroObject.uniqueFrom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → (X : C) → Unique (X ⟶ 0)
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.takeLongest.sizeOf_spec : sizeOf Lean.Parser.OrElseOnAntiquotBehavior.takeLongest = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → (m.insertMany l).getKey! k' = k
-- Lean.Expr
/-- Returns the "body" of a nested lambda expression, like in `Expr.getForallBody`.
The number of skipped lambdas is given by `Expr.getNumHeadLambdas`.
 -/
Lean.Expr.getLambdaBody : Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.Group.Arithmetic
AddUnits.measurableVAdd : ∀ {M : Type u_4} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : AddMonoid M] [inst_2 : AddAction M β]
  [inst_3 : MeasurableSpace M] [MeasurableVAdd M β], MeasurableVAdd (AddUnits M) β
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α),
  ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.nondegenerate_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] (M : Matrix m n R), M.Nondegenerate ↔ M.SeparatingLeft ∧ M.SeparatingRight
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m (Option γ)} (it : Std.IterM Id β),
  (Std.IterM.filterMapWithPostcondition f it).toList = List.filterMapM (fun x => (f x).run) it.toList.run
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.mk.inj : ∀ {triggerCharacters? allCommitCharacters? : Option (Array String)} {resolveProvider : Bool}
  {triggerCharacters?_1 allCommitCharacters?_1 : Option (Array String)} {resolveProvider_1 : Bool},
  { triggerCharacters? := triggerCharacters?, allCommitCharacters? := allCommitCharacters?,
        resolveProvider := resolveProvider } =
      { triggerCharacters? := triggerCharacters?_1, allCommitCharacters? := allCommitCharacters?_1,
        resolveProvider := resolveProvider_1 } →
    triggerCharacters? = triggerCharacters?_1 ∧
      allCommitCharacters? = allCommitCharacters?_1 ∧ resolveProvider = resolveProvider_1
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.toNatTrans : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} →
          CategoryTheory.BasedNatTrans F G → CategoryTheory.NatTrans F.toFunctor G.toFunctor
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.isBoundedAtImInfty_iff : ∀ {α : Type u_1} [inst : Norm α] {f : UpperHalfPlane → α},
  UpperHalfPlane.IsBoundedAtImInfty f ↔ ∃ M A, ∀ (z : UpperHalfPlane), A ≤ z.im → ‖f z‖ ≤ M
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₁.getKey k ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.fst_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst G H).hom.hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst G.X H.X
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.ULiftCoyoneda.instFaithfulOppositeFunctorTypeUliftCoyoneda : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.Faithful
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : C ⥤ D`, this is `F.partialRightAdjoint` on objects: it sends
`X : D` such that `F.rightAdjointObjIsDefined X` holds to an object of `C`
which represents the functor `F.op ⋙ yoneda.obj X.obj`.  -/
CategoryTheory.Functor.partialRightAdjointObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → F.PartialRightAdjointSource → C
-- Mathlib.Data.Finset.Sym
Finset.sym_filterNe_mem : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ} {m : Sym α n} (a : α),
  m ∈ s.sym n → (Sym.filterNe a m).snd ∈ (s.erase a).sym (n - ↑(Sym.filterNe a m).fst)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_derivWithin_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairingIn_pairingIn_mem_set_of_length_eq_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) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] {i j : ι} [IsDomain R] {B : P.InvariantForm},
  (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) →
    i ≠ j → P.root i ≠ -P.root j → (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1)}
-- Lean.Parser.Command
/-- Skip input until the next whitespace character or delimiter (used for error recovery for certain
tokens, especially names that occur in signatures)  -/
_private.Lean.Parser.Command.0.Lean.Parser.Command.skipUntilWsOrDelim : Lean.Parser.Parser