mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.map_injective : ∀ {R S : CommRingCat}, Function.Injective AlgebraicGeometry.Spec.map
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- Specialization of `ContinuousLinearMap.precomp_uniformConvergenceCLM` to compact
convergence.  -/
ContinuousLinearMap.precompCompactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_4} →
                      {F : Type u_5} →
                        (G : Type u_6) →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            [inst_13 : IsTopologicalAddGroup G] →
                                              [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                (E →SL[σ] F) →
                                                  CompactConvergenceCLM τ F G →L[𝕜₃] CompactConvergenceCLM ρ E G
-- Mathlib.Analysis.Analytic.Inverse
/-- The right inverse of a formal multilinear series, where the `n`-th term is defined inductively
in terms of the previous ones to make sure that `p ∘ (rightInv p i) = id`. For this, the linear
term `p₁` in `p` should be invertible. In the definition, `i` is a linear isomorphism that should
coincide with `p₁`, so that one can use its inverse in the construction. The definition does not
use that `i = p₁`, but proofs that the definition is well-behaved do.

The `n`-th term in `p ∘ q` is `∑ pₖ (q_{j₁}, ..., q_{jₖ})` over `j₁ + ... + jₖ = n`. In this
expression, `qₙ` appears only once, in `p₁ (qₙ)`. We adjust the definition of `qₙ` so that this
term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`.

These formulas only make sense when the constant term `p₀` vanishes. The definition we give is
general, but it ignores the value of `p₀`.
 -/
FormalMultilinearSeries.rightInv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                FormalMultilinearSeries 𝕜 E F → (E ≃L[𝕜] F) → E → FormalMultilinearSeries 𝕜 F E
-- Mathlib.Geometry.Manifold.Instances.Real
modelWithCornersEuclideanHalfSpace_toFun : ∀ (n : ℕ) [inst : NeZero n], ↑(modelWithCornersEuclideanHalfSpace n) = Subtype.val
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- When `A : IndexSet Δ` and `θ : Δ → Δ'` is a morphism in `SimplexCategoryᵒᵖ`,
an element in `IndexSet Δ'` can be defined by using the epi-mono factorisation
of `θ.unop ≫ A.e`.  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet.pull : {Δ : SimplexCategoryᵒᵖ} →
  CategoryTheory.SimplicialObject.Splitting.IndexSet Δ →
    {Δ' : SimplexCategoryᵒᵖ} → (Δ ⟶ Δ') → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ'
-- Mathlib.Geometry.Manifold.ChartedSpace
instTopologicalSpaceModelPi : {ι : Type u_5} → {Hi : ι → Type u_6} → [(i : ι) → TopologicalSpace (Hi i)] → TopologicalSpace (ModelPi Hi)
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Interpret a `Homeomorph` as a `PartialHomeomorph` by restricting it
to a set `s` in the domain and to `t` in the codomain.  -/
Homeomorph.toPartialHomeomorphOfImageEq : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (e : X ≃ₜ Y) → (s : Set X) → (t : Set Y) → ⇑e '' s = t → PartialHomeomorph X Y
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Hom.injective : ∀ {X Y : PartOrdEmb} (f : X ⟶ Y), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instMulAction : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → MulAction α (LowerSet α)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_sumSwap : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'}, HasMFDerivAt% Sum.swap p (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.coe_toContinuousMap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), ⇑F.toContinuousMap = ⇑F
-- Aesop.Stats.File
Aesop.StatsFileRecord.ofStats : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.Elab.MonadParentDecl m] →
        [MonadLiftT Lean.CoreM m] → Lean.Syntax → Bool → Aesop.Stats → m Aesop.StatsFileRecord
-- Init.Core
PSum.inl.injEq : ∀ {α : Sort u} {β : Sort v} (val val_1 : α), (PSum.inl val = PSum.inl val_1) = (val = val_1)
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The identity partial equiv  -/
PartialEquiv.refl : (α : Type u_5) → PartialEquiv α α
-- Lean.Parser.Types
Lean.Parser.ParserContext.toParserContextCore : Lean.Parser.ParserContext → Lean.Parser.ParserContextCore
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_mul : ∀ {a b : UInt8}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
/-- If `G, H` are subgroups of `Γ` which acts on `α`, and `G ∩ H` has finite index in `G`,
then `G` acts properly discontinuously if `H` does.  -/
ProperlyDiscontinuousSMul.ofFiniteRelIndex : ∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : MulAction Γ α]
  [ContinuousConstSMul Γ α] (G H : Subgroup Γ) [hH : ProperlyDiscontinuousSMul (↥H) α] [H.IsFiniteRelIndex G],
  ProperlyDiscontinuousSMul (↥G) α
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for homogeneous power on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalOPow : Mathlib.Meta.NormNum.NormNumExt
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueCast? k (List.filter (fun p => !l₂.contains p.fst) l₁) = none
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_eq_cert.eq_1 : ∀ (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_eq_cert lhs rhs lhs' rhs' = (lhs.sub rhs).toPoly_k.beq' (lhs'.sub rhs').toPoly_k
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_inf_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N),
  Subgroup.map f (H ⊓ K) ≤ Subgroup.map f H ⊓ Subgroup.map f K
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.sepBy1NoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Order.LeftRightNhds
/-- **Alias** of `countable_setOfPred_isolated_right`.

---

The set of points which are isolated on the right is countable when the space is
second-countable.  -/
countable_setOf_isolated_right : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | nhdsWithin x (Set.Ioi x) = ⊥}.Countable
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_pos : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → 0 < a.toReal
-- Mathlib.Data.NNReal.Defs
NNReal.coe_min : ∀ (x y : NNReal), ↑(min x y) = min ↑x ↑y
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.inrCLM_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (m : M), (TrivSqZeroExt.inrCLM R M) m = TrivSqZeroExt.inr m
-- Mathlib.Topology.UniformSpace.Defs
Filter.HasBasis.uniformContinuousOn_iff : ∀ {α : Type ua} {β : Type ub} {ι : Sort u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι' : Sort u_2}
  {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s →
    ∀ {q : ι' → Prop} {t : ι' → Set (β × β)},
      (uniformity β).HasBasis q t →
        ∀ {f : α → β} {S : Set α},
          UniformContinuousOn f S ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.ofVar.eq_1 : ∀ (x : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Mon.ofVar x = Lean.Grind.CommRing.Mon.mult { x := x, k := 1 } Lean.Grind.CommRing.Mon.unit
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in after the position
`pos`. If there is no match `none` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.startPos.find? Char.isWhitespace).map (·.get!) == some ' '`

* `("tea".toSlice.pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none`
 -/
String.Slice.Pos.find? : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {s : String.Slice} → s.Pos → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → Option s.Pos
-- Std.Data.TreeMap.Basic
/-- Partitions a tree map into two tree maps based on a predicate.  -/
Std.TreeMap.partition : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → (α → β → Bool) → Std.TreeMap α β cmp → Std.TreeMap α β cmp × Std.TreeMap α β cmp
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceL!.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (ls : ℕ) (lk : α) (lv : β lk)
  (ll lr : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)),
  (match Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr => h_2 ls lk lv ll lr) =
    h_2 ls lk lv ll lr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {k k' : α} {f : β → β},
  m.WF → (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.comp_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) (a : A),
  (f.comp g) a = f (g a)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? pref.length r.lower).get ⋯
-- Mathlib.Algebra.Quandle
/-- An abelian rack is one for which the mediality axiom holds.
 -/
Rack.IsAbelian : (R : Type u_2) → [Rack R] → Prop
-- Mathlib.Computability.Encoding
Computability.decode_encodeNat : ∀ (n : ℕ), Computability.decodeNat (Computability.encodeNat n) = n
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The equivalence `Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c`.  -/
CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c) ≌
            HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c
-- Mathlib.Analysis.Complex.Harmonic.MeanValue
/-- The Mean Value Property of harmonic functions: If f : ℂ → F is harmonic in a neighborhood of a
closed disc of radius R and center c, then the circle average circleAverage f c R equals
f c.
 -/
InnerProductSpace.HarmonicOnNhd.circleAverage_eq : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c |R|) → Real.circleAverage f c R = f c
-- Mathlib.Order.Minimal
OrderEmbedding.image_setOfPred_minimal : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β},
  ⇑f '' {x | Minimal (fun x => x ∈ s) x} = {x | Minimal (fun x => x ∈ ⇑f '' s) x}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      W.negAddY P Q =
        ((P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) *
              (W.addX P Q * (P 2 * Q 2) ^ 2 - P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) +
            P 1 * Q 2 ^ 3 * WeierstrassCurve.Jacobian.addZ P Q ^ 3) /
          (P 2 * Q 2) ^ 3
-- Std.Sat.AIG.Basic
/-- The AIG that we are in.
 -/
Std.Sat.AIG.Entrypoint.aig : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG.Entrypoint α → Std.Sat.AIG α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k k' : α}, t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.filter f t)[k]? = Option.filter (f k') t[k]?
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.coe_mk : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target),
  ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ } = ↑e
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
/-- A helper definition to show that the forgetful functor `forget C : Mon C ⥤ C` creates limits:
given a limit cone `c` of `F ⋙ forget C`, we can lift it to a limit cone of `F`.
 -/
CategoryTheory.Mon.limitConeLiftsToLimit : {J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) →
            (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) →
              (hc : CategoryTheory.Limits.IsLimit c) → CategoryTheory.LiftsToLimit F (CategoryTheory.Mon.forget C) c hc
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindRing.toIsNoetherian : ∀ {A : Type u_2} {inst : CommRing A} [self : IsDedekindRing A], IsNoetherian A A
-- Mathlib.Data.ZMod.QuotientGroup
AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddGroup α] (a : α) [inst_1 : AddAction α β] (b : β)
  (n : ZMod (Function.minimalPeriod (fun x => a +ᵥ x) b)),
  (AddAction.zmultiplesQuotientStabilizerEquiv a b).symm n = n.cast • ↑⟨a, ⋯⟩
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x : αᵒᵈ}, Set.Iio (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ioi x
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {Y : D},
  CategoryTheory.IsIso (h.unit.app (R.obj Y))
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.surjective_of_comp_eq_id : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ →ₛₗ[σ'] M),
  g ∘ₛₗ f = LinearMap.id → Function.Surjective ⇑g
-- Init.Data.BitVec.Lemmas
BitVec.toNat_zero_length : ∀ (x : BitVec 0), x.toNat = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.instNormalOne : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G : C} [inst_2 : CategoryTheory.GrpObj G], CategoryTheory.IsMonHom.Normal CategoryTheory.MonObj.one
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C)
  {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (a_1 : Quot CategoryTheory.FreeBicategory.Rel),
  (CategoryTheory.FreeBicategory.lift F).map₂ a_1 = Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯ a_1
-- Lean.Server.Completion.CompletionCollectors
/-- Checks whether the type of `info.type` returns one of the type names in `typeNameSet`, for dot ident notation completion.
The process mimics the dotted identifier notation elaboration procedure at `Lean.Elab.App`.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.isDotIdCompletionMethod : Lean.Server.Completion.NameSetModPrivate✝ → Lean.ConstantInfo → Lean.MetaM Bool
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_map : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} [inst : DecidableEq o] [inst_1 : Zero α]
  [inst_2 : Zero β] (M : o → Matrix m n α) (f : α → β),
  f 0 = 0 → (Matrix.blockDiagonal M).map f = Matrix.blockDiagonal fun k => (M k).map f