mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_apply : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)]
  (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι), (LinearMap.pi f) c i = (f i) c
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiable_num : ∀ (g : GL (Fin 2) ℝ), MDiff fun τ => UpperHalfPlane.num g ↑τ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.insert k v).get? k = some v
-- Init.Data.SInt.Lemmas
ISize.ofNat_int32ToNatClampNeg : ∀ (x : Int32), 0 ≤ x → ISize.ofNat x.toNatClampNeg = x.toISize
-- Init.MetaTypes
/-- Ignore stuck typeclass synthesis while elaborating the term. Default: `false`.  -/
Lean.Meta.Command.ReduceConfig.ignoreStuckTC : Lean.Meta.Command.ReduceConfig → Bool
-- Mathlib.Data.Fintype.BigOperators
/-- Product over a sigma type equals the repeated product, curried version.
This version is useful to rewrite from right to left.  -/
Fintype.prod_sigma' : ∀ {ι : Type u_9} {α : ι → Type u_7} {M : Type u_8} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)]
  [inst_2 : CommMonoid M] (f : (i : ι) → α i → M), ∏ x, f x.fst x.snd = ∏ x, ∏ y, f x y
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.hδ'₂ : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
  f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op))
      (SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result : Type
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- Let `N` be a localization of an `R`-module `M` at `p`.
This is the localization of an `R`-submodule of `M` viewed as an `R`-submodule of `N`.  -/
Submodule.localized₀ : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (p : Submonoid R) → (f : M →ₗ[R] N) → [IsLocalizedModule p f] → Submodule R M → Submodule R N
-- Mathlib.Order.CompleteBooleanAlgebra
iInf_sup_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (f : ι → α) (a : α), (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃Functor_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  {X Y : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} (f : X ⟶ Y) (X_1 : C₁)
  (Y_1 : C₃) (Z : C₂),
  (((CategoryTheory.Functor.flip₂₃Functor.map f).app X_1).app Y_1).app Z = ((f.app X_1).app Z).app Y_1
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.instInhabitedGenerators : (B : Type v) → [Inhabited B] → Inhabited (CartanMatrix.Generators B)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.MapsTo.sub : ∀ {α : Type u_2} {β : Type u_3} [inst : Sub β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  Set.MapsTo f₁ A B₁ → Set.MapsTo f₂ A B₂ → Set.MapsTo (f₁ - f₂) A (B₁ - B₂)
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- A path in the tree gives a hom, by composition.  -/
IsFreeGroupoid.SpanningTree.homOfPath : {G : Type u} →
  [inst : CategoryTheory.Groupoid G] →
    [inst_1 : IsFreeGroupoid G] →
      (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) →
        [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] →
          {a : G} →
            Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a →
              (IsFreeGroupoid.SpanningTree.root'✝ T ⟶ a)
-- Mathlib.Topology.Constructions.SumProd
isClosedMap_sum : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X ⊕ Y → Z},
  IsClosedMap f ↔ (IsClosedMap fun a => f (Sum.inl a)) ∧ IsClosedMap fun b => f (Sum.inr b)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.toByteArray_eq_right : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → t₂.toByteArray = s.copy.toByteArray.extract p.offset.byteIdx s.copy.toByteArray.size
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Right homotopy classes of maps between bifibrant objects identify
to morphisms in the homotopy category `BifibrantObject.HoCat`.  -/
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        [inst_2 : HomotopicalAlgebra.IsCofibrant X] →
          [inst_3 : HomotopicalAlgebra.IsCofibrant Y] →
            [inst_4 : HomotopicalAlgebra.IsFibrant X] →
              [inst_5 : HomotopicalAlgebra.IsFibrant Y] →
                HomotopicalAlgebra.RightHomotopyClass X Y ≃
                  (HomotopicalAlgebra.BifibrantObject.toHoCat.obj (HomotopicalAlgebra.BifibrantObject.mk X) ⟶
                    HomotopicalAlgebra.BifibrantObject.toHoCat.obj (HomotopicalAlgebra.BifibrantObject.mk Y))
-- Mathlib.Data.ENNReal.Basic
ENNReal.instCommSemiring : CommSemiring ENNReal
-- Mathlib.Algebra.Group.Finsupp
/-- The support of a sum is the union of the supports when the supports are disjoint.

In the case where the coefficients satisfy `CanonicallyOrderedAdd`, there is also
`Finsupp.support_add_eq_union`, which holds without any disjointness assumption.  -/
Finsupp.support_add_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {g₁ g₂ : ι →₀ M} [inst_1 : DecidableEq ι],
  Disjoint g₁.support g₂.support → (g₁ + g₂).support = g₁.support ∪ g₂.support
-- Mathlib.Topology.Algebra.Group.Basic
DenseRange.topologicalClosure_map_addSubgroup : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : AddGroup H] [inst_4 : TopologicalSpace H] [inst_5 : IsTopologicalAddGroup H] {f : G →+ H},
  Continuous ⇑f →
    DenseRange ⇑f → ∀ {s : AddSubgroup G}, s.topologicalClosure = ⊤ → (AddSubgroup.map f s).topologicalClosure = ⊤
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.sum.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)] {e : Q(«$α»)} (x : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e),
  sizeOf (Mathlib.Tactic.Ring.Common.ExBase.sum x) = 1 + sizeOf e + sizeOf x
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_iCycles_odd_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [inst_3 : CategoryTheory.CategoryWithHomology C] {j : ℕ},
  c.Rel (c.prev j) j →
    c.Rel j (c.next j) →
      Odd j →
        ∀ {Z : C} (h : A ⟶ Z),
          CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j)
              (CategoryTheory.CategoryStruct.comp ψ h) =
            CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.fromGlued_injective : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), Function.Injective ⇑(AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰)
-- Lean.Data.SMap
Lean.SMap.insert : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → α → β → Lean.SMap α β
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.pushouts_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f),
  (CategoryTheory.MorphismProperty.coproducts.{w, v, u} (CategoryTheory.MorphismProperty.ofHoms g)).pushouts f
-- Mathlib.Algebra.DualNumber
DualNumber.algHom_ext_iff : ∀ {R : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {f g : DualNumber R →ₐ[R] A}, f = g ↔ f DualNumber.eps = g DualNumber.eps
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Create a `RefinedDiscrTree` consisting of all entries generated by `act`
from imported constants; `addConstToPreDiscrTree` calls this helper.
This uses parallel computation.
 -/
Lean.Meta.RefinedDiscrTree.createImportedDiscrTree : {α : Type} →
  Lean.NameGenerator →
    Lean.Environment →
      (Lean.Name →
          Lean.ConstantInfo →
            Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
        ℕ → ℕ → Lean.CoreM (Lean.Meta.RefinedDiscrTree α)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If `n` has only one element, the determinant of an `n` by `n` matrix is just that element.
Although `Unique` implies `DecidableEq` and `Fintype`, the instances might
not be syntactically equal. Thus, we need to fill in the args explicitly.  -/
Matrix.det_unique : ∀ {R : Type v} [inst : CommRing R] {n : Type u_3} [inst_1 : Unique n] [inst_2 : DecidableEq n] [inst_3 : Fintype n]
  (A : Matrix n n R), A.det = A default default
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- Galois insertion between `adjoin` and `coe`.  -/
Algebra.gi : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → GaloisInsertion (Algebra.adjoin R) SetLike.coe
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A subtraction-free formula for the rank of a set in the dual matroid.  -/
Matroid.eRk_dual_add_eRank : ∀ {α : Type u_1} (M : Matroid α) (X : Set α),
  autoParam (X ⊆ M.E) Matroid.eRk_dual_add_eRank._auto_1 → M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.IsComplete.out' : ∀ {α : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : μ.IsComplete] (s : Set α),
  μ s = 0 → MeasurableSet s
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_of_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → Set.uIoo a b = Set.Ioo b a
-- Mathlib.Order.Minimal
minimal_iff_minimal_of_imp_of_forall : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : PartialOrder α],
  (∀ ⦃x : α⦄, Q x → P x) → (∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y) → (Minimal P x ↔ Minimal Q x)
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 404 status code.
 -/
Std.Http.Response.notFound : Std.Http.Response.Builder
-- Mathlib.LinearAlgebra.Matrix.Symmetric
/-- A matrix `A : Matrix n n α` is "symmetric" if `Aᵀ = A`.  -/
Matrix.IsSymm : {α : Type u_1} → {n : Type u_3} → Matrix n n α → Prop
-- Std.Time.Date.Unit.Year
Std.Time.Year.instReprEra : Repr Std.Time.Year.Era
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toRange_app_val : ∀ {X Y : SSet} (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (x : X.obj Δ),
  ↑((CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.toRange f).app Δ)) x) =
    (CategoryTheory.ConcreteCategory.hom (f.app Δ)) x
-- Std.Http.Protocol.H1.Event
/-- The body should be closed.
 -/
Std.Http.Protocol.H1.Event.closeBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.cancel_right : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : DecidableEq ι] [inst_8 : AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B}
  {𝒞 : ι → Submodule R C} [inst_9 : GradedAlgebra 𝒜] [inst_10 : GradedAlgebra ℬ] [inst_11 : GradedAlgebra 𝒞]
  {g₁ g₂ : ℬ →ₐᵍ[R] 𝒞} {f : 𝒜 →ₐᵍ[R] ℬ}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.even_card : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [inst : Fintype ↑M.verts],
  M.IsMatching → Even M.verts.toFinset.card
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
isOpenMap_iff_lowerHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsOpenMap f ↔ LowerHemicontinuous fun x => f ⁻¹' {x}
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.neg.injEq : ∀ (a a_1 : Lean.Grind.CommRing.Expr), (a.neg = a_1.neg) = (a = a_1)
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.resultType : Lean.IR.Decl → Lean.IR.IRType
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.smul_mem_mono : ∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {s : Set E} [inst_3 : NormedRing 𝕝] [inst_4 : Module 𝕜 𝕝] [NormSMulClass 𝕜 𝕝]
  [inst_6 : SMulWithZero 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {a : 𝕜} {x : E} [SMulCommClass 𝕝 𝕜 E],
  Balanced 𝕝 s → ∀ {b : 𝕝}, a • x ∈ s → ‖b‖ ≤ ‖a‖ → b • x ∈ s
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_indicator : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) {t : Finset ι} (f : (i : ι) → i ∈ s → α)
  [inst_1 : DecidableEq ι],
  (Finsupp.indicator t fun i x => (Finsupp.indicator s f) i) = Finsupp.indicator (s ∩ t) fun i hi => f i ⋯
-- Std.Http.Data.Status
Std.Http.Status.notExtended.sizeOf_spec : sizeOf Std.Http.Status.notExtended = 1
-- Mathlib.Algebra.Polynomial.Div
Polynomial.finiteMultiplicity_X_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (a : R), p ≠ 0 → FiniteMultiplicity (Polynomial.X - Polynomial.C a) p
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.coe_finsuppSum : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Zero β] (c : AddCon M) (h : ι → β → M)
  (f : ι →₀ β), ↑(f.sum h) = f.sum fun i b => ↑(h i b)
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  (x : HahnSeries Γ V) (f : PowerSeries R),
  HahnSeries.SummableFamily.powerSeriesFamily x f =
    HahnSeries.SummableFamily.smulFamily (fun n => (PowerSeries.coeff n) f) (HahnSeries.SummableFamily.powers x)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Batteries.Data.List.Count
List.idxToSigmaCount_sigmaCountToIdx : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs : List α} {xc : (x : α) × Fin (List.count x xs)},
  xs.idxToSigmaCount (xs.sigmaCountToIdx xc) = xc
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point within a set.  -/
Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e]
  (f : M → Bundle.TotalSpace F E) {s : Set M} {x₀ : M},
  f x₀ ∈ e.source → (MDiffAt[s] f x₀ ↔ (MDiffAt[s] fun x => (f x).proj) x₀ ∧ (MDiffAt[s] fun x => (↑e (f x)).2) x₀)