mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
IsCovariantDerivativeOn.torsion_apply : ∀ {𝕜 : 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] [inst_6 : IsManifold I 2 M] [inst_7 : CompleteSpace E]
  {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [inst_8 : CompleteSpace 𝕜]
  [inst_9 : FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) {x : M} {X : (x : M) → TangentSpace I x},
  MDiffAt (T% X) x →
    ∀ {Y : (x : M) → TangentSpace I x},
      MDiffAt (T% Y) x →
        ((hcov.torsion x) (X x)) (Y x) = (cov Y x) (X x) - (cov X x) (Y x) - VectorField.mlieBracket I X Y x
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  (DerivedCategory.triangleOfSES hS).obj₃ = DerivedCategory.Q.obj S.X₃
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.lift_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f k h) (CategoryTheory.Limits.kernel.ι f) = k
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (next' : α)
  (h_1 : (next'_1 : α) → some next' = some next'_1 → motive (some next'_1)) (h_2 : some next' = none → motive none),
  (match hs : some next' with
    | some next'_1 => h_1 next'_1 hs
    | none => h_2 hs) =
    h_1 next' ⋯
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Convenience congruence lemma stating in a dependent setting that, if the arguments to a formal
multilinear series are equal, then the values are also equal.  -/
FormalMultilinearSeries.congr : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {m n : ℕ} {v : Fin m → E} {w : Fin n → E},
  m = n → (∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩) → (p m) v = (p n) w
-- Mathlib.Data.Fintype.EquivFin
/-- Two `Fintype`s with the same cardinality are (noncomputably) in bijection.

See `Fintype.truncEquivOfCardEq` for the computable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq` for
the specialization to `Fin`.
 -/
Fintype.equivOfCardEq : {α : Type u_1} → {β : Type u_2} → [inst : Fintype α] → [inst_1 : Fintype β] → Fintype.card α = Fintype.card β → α ≃ β
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.abs_moebius : ∀ {n : ℕ}, |ArithmeticFunction.moebius n| = if Squarefree n then 1 else 0
-- Mathlib.LinearAlgebra.Prod
/-- `Prod.map` of two linear maps.  -/
LinearMap.prodMap : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        {M₄ : Type z} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommMonoid M₄] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module R M₄] → (M →ₗ[R] M₃) → (M₂ →ₗ[R] M₄) → M × M₂ →ₗ[R] M₃ × M₄
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso_inv_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] (X_1 : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso f).inv.app X_1).right =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout X_1.hom f)
-- Mathlib.Algebra.Group.Hom.Defs
/-- Any type satisfying `ZeroHomClass` can be cast into `ZeroHom` via
`ZeroHomClass.toZeroHom`.  -/
instCoeTCZeroHomOfZeroHomClass : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : Zero M] → [inst_1 : Zero N] → [inst_2 : FunLike F M N] → [ZeroHomClass F M N] → CoeTC F (ZeroHom M N)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.applyAssignment : Array Lean.Expr → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit
-- Mathlib.Data.Set.Card.Arithmetic
Set.exists_union_disjoint_ncard_eq_of_even : ∀ {α : Type u_1} {s : Set α}, Even s.ncard → ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard
-- Init.Data.Range.Polymorphic.PRange
/-- `a<...*` is the range of elements greater than `a`. See also `Std.Roi`.  -/
Std.«term_<...*» : Lean.TrailingParserDescr
-- Init.Tactics
/-- If true (default: false), then when preprocessing, removes irrelevant variables and reverts the local context.
A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
or if it is a proposition that refers to a relevant variable.  -/
Lean.Parser.Tactic.DecideConfig.revert : Lean.Parser.Tactic.DecideConfig → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.nat_mul_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {f : ℤ → M},
  Multipliable f → Multipliable fun n => f ↑n * f (-(↑n + 1))
-- Mathlib.MeasureTheory.Group.Arithmetic
MulOpposite.instMeasurableSpace.eq_1 : ∀ {α : Type u_2} [h : MeasurableSpace α], MulOpposite.instMeasurableSpace = MeasurableSpace.map MulOpposite.op h
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_symm_comm : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  {α : R₁ ⟶ R₂} {β : R₂ ⟶ R₁},
  CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.id R₁ →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₁).symm β)
        ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) =
      CategoryTheory.CategoryStruct.id L₁
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.Context.mk.inj : ∀ {config : Lean.Meta.Simp.Config} {userConfig : Lean.Options} {zetaDeltaSet initUsedZetaDelta : Lean.FVarIdSet}
  {metaConfig indexConfig : Lean.Meta.ConfigWithKey} {maxDischargeDepth : UInt32}
  {simpTheorems : Lean.Meta.SimpTheoremsArray} {congrTheorems : Lean.Meta.SimpCongrTheorems}
  {parent? : Option Lean.Expr} {dischargeDepth : UInt32} {lctxInitIndices : ℕ} {inDSimp : Bool}
  {config_1 : Lean.Meta.Simp.Config} {userConfig_1 : Lean.Options} {zetaDeltaSet_1 initUsedZetaDelta_1 : Lean.FVarIdSet}
  {metaConfig_1 indexConfig_1 : Lean.Meta.ConfigWithKey} {maxDischargeDepth_1 : UInt32}
  {simpTheorems_1 : Lean.Meta.SimpTheoremsArray} {congrTheorems_1 : Lean.Meta.SimpCongrTheorems}
  {parent?_1 : Option Lean.Expr} {dischargeDepth_1 : UInt32} {lctxInitIndices_1 : ℕ} {inDSimp_1 : Bool},
  { config := config, userConfig := userConfig, zetaDeltaSet := zetaDeltaSet, initUsedZetaDelta := initUsedZetaDelta,
        metaConfig := metaConfig, indexConfig := indexConfig, maxDischargeDepth := maxDischargeDepth,
        simpTheorems := simpTheorems, congrTheorems := congrTheorems, parent? := parent?,
        dischargeDepth := dischargeDepth, lctxInitIndices := lctxInitIndices, inDSimp := inDSimp } =
      { config := config_1, userConfig := userConfig_1, zetaDeltaSet := zetaDeltaSet_1,
        initUsedZetaDelta := initUsedZetaDelta_1, metaConfig := metaConfig_1, indexConfig := indexConfig_1,
        maxDischargeDepth := maxDischargeDepth_1, simpTheorems := simpTheorems_1, congrTheorems := congrTheorems_1,
        parent? := parent?_1, dischargeDepth := dischargeDepth_1, lctxInitIndices := lctxInitIndices_1,
        inDSimp := inDSimp_1 } →
    config = config_1 ∧
      userConfig = userConfig_1 ∧
        zetaDeltaSet = zetaDeltaSet_1 ∧
          initUsedZetaDelta = initUsedZetaDelta_1 ∧
            metaConfig = metaConfig_1 ∧
              indexConfig = indexConfig_1 ∧
                maxDischargeDepth = maxDischargeDepth_1 ∧
                  simpTheorems = simpTheorems_1 ∧
                    congrTheorems = congrTheorems_1 ∧
                      parent? = parent?_1 ∧
                        dischargeDepth = dischargeDepth_1 ∧ lctxInitIndices = lctxInitIndices_1 ∧ inDSimp = inDSimp_1
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓRes_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] (F : CategoryTheory.Sheaf J A) {V U : Cᵒᵖ} (f : U ⟶ V),
  CategoryTheory.CategoryStruct.comp (F.ΓRes U) (F.obj.map f) = F.ΓRes V
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.isUniformInducing_toContinuousMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal},
  IsUniformInducing fun α => ODE.FunSpace.toContinuousMap α
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionHomologyIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i i_1 : ι) (e_i : i = i_1) (j k k_1 : ι)
  (e_k : k = k_1) (hi : c.prev j = i) (hk : c.next j = k) {i' i'_1 : ι'} (e_i' : i' = i'_1) {j' k' k'_1 : ι'}
  (e_k' : k' = k'_1) (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'' = K.restrictionHomologyIso e i_1 j k_1 ⋯ ⋯ ⋯ hj' ⋯ ⋯ ⋯
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- A function is `C^n` within a set at a point, for `n : ℕ` or `n = ω`,
if and only if it is `C^n` on a neighborhood of this point.  -/
contMDiffWithinAt_iff_contMDiffOn_nhds : ∀ {𝕜 : 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'} {s : Set M} {x : M}
  {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  n ≠ ↑⊤ → (ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ nhdsWithin x (insert x s), ContMDiffOn I I' n f u)
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`.  -/
closure_Ioi : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α)
  [NoMaxOrder α], closure (Set.Ioi a) = Set.Ici a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeEndWhile_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, (s.takeEndWhile pat).takeEndWhile pat = s.takeEndWhile pat
-- Aesop.Tree.Data.ForwardRuleMatches
/-- `O(n)` Number of matches in `ms`.  -/
Aesop.ForwardRuleMatches.size : Aesop.ForwardRuleMatches → ℕ
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wMk'.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f : (P.B a).Arrow (α ::: P.W α)),
  P.wMk' ⟨a, f⟩ = P.wMk a (TypeVec.dropFun f) (TypeVec.lastFun f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} {k k' : α} {fallback : β} (h : t.WF),
  t.getKey? k = some k' →
    Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k fallback =
      (Option.filter (fun x => f k' x) (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The push-forward of a finite measure by a function between measurable spaces.  -/
MeasureTheory.FiniteMeasure.map : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] → MeasureTheory.FiniteMeasure Ω → (Ω → Ω') → MeasureTheory.FiniteMeasure Ω'
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_const_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε'] {c : ε'},
  ‖c‖ₑ ≠ ⊤ → ∀ [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.MemLp (fun x => c) p μ
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_atBot_eq : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] {f : α → β},
  Filter.map f Filter.atBot = ⨅ a, Filter.principal (f '' {a' | a' ≤ a})
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_id_f_map_epi : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) [CategoryTheory.Epi φ]
  (i : ℕ), CategoryTheory.Epi ((groupHomology.chainsMap (MonoidHom.id G) φ).f i)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.of.sizeOf_spec : ∀ (carrier : Type u) [commSemiring : CommSemiring carrier],
  sizeOf (CommSemiRingCat.of carrier) = 1 + sizeOf carrier + sizeOf commSemiring
-- Init.Prelude
Nat.modCoreGo_lt : ∀ {fuel y : ℕ} (hy : 0 < y) (x : ℕ) (hfuel : x < fuel), Nat.modCore.go y hy fuel x hfuel < y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_dropLast_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → p.dropLast.support ++ [v] = p.support
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), ψ.op.φQ = ψ.φK.op
-- Init.Data.Array.Lemmas
Array.getElem_append : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} (h : i < (xs ++ ys).size),
  (xs ++ ys)[i] = if h' : i < xs.size then xs[i] else ys[i - xs.size]
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} {fallback : β a},
  ∅.getD a fallback = fallback
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitBinder.parenthesizer : optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_eqToHom_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] {R' : 𝒮} (h : R' = R),
  p.IsHomLift (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) φ
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.toBitVec_minValueSealed_eq_intMinSealed : Int32.minValueSealed✝.toBitVec = BitVec.Signed.intMinSealed✝ 32
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_eq_true_of_lt_skipPrefixWhile_bool : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile p), p (pos.get ⋯) = true
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.instCoeHeadCarrierObjMonCatToFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} →
      (S : CategoryTheory.SubmonoidFunctor M) → {U : C} → CoeHead ↑(S.toFunctor.obj U) ↑(M.obj U)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l →
        ∀
          {h' :
            (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity
                      l)).contains
                k' =
              true},
          (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity
                    l)).getKey
              k' h' =
            k
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalUnopUnop_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.unopUnop C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_one : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R], MvPowerSeries.expand 1 ⋯ = AlgHom.id R (MvPowerSeries σ R)
-- Mathlib.CategoryTheory.Bicategory.Free
/-- A prefunctor from a quiver `B` to a bicategory `C` can be lifted to a pseudofunctor from
`free_bicategory B` to `C`.
 -/
CategoryTheory.FreeBicategory.lift : {B : Type u₁} →
  [inst : Quiver B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → B ⥤q C → CategoryTheory.Pseudofunctor (CategoryTheory.FreeBicategory B) C
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYoneda_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (X_1 : Cᵒᵖ),
  (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).obj X_1 = ULift.{w, v₁} (Opposite.unop X_1 ⟶ X)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_eq_zero`.  -/
hammingDist_eq_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  hammingDist x y = 0 ↔ x = y
-- Mathlib.Order.Hom.Basic
OrderHom.pi_coe : ∀ {α : Type u_2} [inst : Preorder α] {ι : Type u_6} {π : ι → Type u_7} [inst_1 : (i : ι) → Preorder (π i)]
  (f : (i : ι) → α →o π i) (x : α) (i : ι), (OrderHom.pi f) x i = (f i) x
-- Init.Data.UInt.Bitwise
UInt64.or_comm : ∀ (a b : UInt64), a ||| b = b ||| a
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- The natural isomorphism encoding `comp_const`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.compIso : {𝒮 : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) →
      (S : 𝒮) →
        (CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).comp
            (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F) ≅
          (CategoryTheory.Functor.const ↑(F.obj { as := Opposite.op S })).obj S
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant] {f : C(G, ℝ)},
  HasCompactSupport ⇑f ∧ 0 ≤ f ∧ f 1 ≠ 0 → ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
-- Init.Data.List.Nat.Modify
List.getElem?_modifyHead : ∀ {α : Type u_1} {l : List α} {f : α → α} {i : ℕ},
  (List.modifyHead f l)[i]? = if i = 0 then Option.map f l[i]? else l[i]?
-- Mathlib.Data.Real.Basic
Real.instLT : LT ℝ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_sub_div : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (d - x / c) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x
-- Lean.Elab.MutualInductive
/-- Auxiliary function for `inferResultingUniverse`. Applies `accLevel` to the given constructor parameter.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.accLevelAtCtor : Lean.Expr → Lean.Level → ℕ → Array Lean.LMVarId → StateT Lean.Elab.Command.AccLevelState✝ Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- When all four morphisms in a square are left adjoints, the mates operation can be iterated:
```
         l₁                  r₁                  r₁
      a --→ b             a ←-- b             a ←-- b
   f₁ ↓  ↗  ↓  f₂      f₁ ↓  ↘  ↓ f₂       u₁ ↑  ↙  ↑ u₂
      c --→ d             c ←-- d             c ←-- d
         l₂                  r₂                  r₂
```
In this case the iterated mate equals the conjugate of the original 2-morphism and is thus an
isomorphism if and only if the original 2-morphism is. This explains why some Beck-Chevalley
2-morphisms are isomorphisms.
 -/
CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f₁ : a ⟶ c} {u₁ : c ⟶ a} {f₂ : b ⟶ d} {u₂ : d ⟶ b}
  {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (adj₃ : CategoryTheory.Bicategory.Adjunction f₁ u₁)
  (adj₄ : CategoryTheory.Bicategory.Adjunction f₂ u₂)
  (α : CategoryTheory.CategoryStruct.comp f₁ l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ f₂),
  (CategoryTheory.Bicategory.mateEquiv adj₄ adj₃) ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α) =
    (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.subsingleton_iff : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R}, Subsingleton (R ⧸ I) ↔ I = ⊤
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.tendsto_coe_atImInfty : Filter.Tendsto UpperHalfPlane.coe UpperHalfPlane.atImInfty (Filter.comap Complex.im Filter.atTop)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.δ.hcongr_8 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (inst_1 : CategoryTheory.Preadditive C) (inst'_1 : CategoryTheory.Preadditive C'),
          inst_1 ≍ inst'_1 →
            ∀ (F : CochainComplex C ℤ) (F' : CochainComplex C' ℤ),
              F ≍ F' →
                ∀ (G : CochainComplex C ℤ) (G' : CochainComplex C' ℤ),
                  G ≍ G' →
                    ∀ (n n' : ℤ),
                      n = n' →
                        ∀ (m m' : ℤ),
                          m = m' →
                            ∀ (z : CochainComplex.HomComplex.Cochain F G n)
                              (z' : CochainComplex.HomComplex.Cochain F' G' n'),
                              z ≍ z' → CochainComplex.HomComplex.δ n m z ≍ CochainComplex.HomComplex.δ n' m' z'