mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f g : M → G} {x₀ : M},
  ContMDiffAt I' I n f x₀ → ContMDiffAt I' I n g x₀ → ContMDiffAt I' I n (fun x => f x - g x) x₀
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `F ⋙ G` preserves limits of shape `J` and `G` reflects limits of shape `J`, then `F` preserves
limits of shape `J`.
 -/
CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp G)] [CategoryTheory.Limits.ReflectsLimitsOfShape J G],
  CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.LinearAlgebra.SesquilinearForm.Star
LinearMap.isSymm_iff_basis : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {B : M →ₗ⋆[R] M →ₗ[R] R} {ι : Type u_4} (b : Module.Basis ι R M),
  B.IsSymm ↔ ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
IsAddUnit.set : ∀ {α : Type u_2} [inst : AddMonoid α] {a : α}, IsAddUnit a → IsAddUnit {a}
-- Mathlib.Order.RelSeries
LTSeries.map_length : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p : LTSeries α) (f : α → β)
  (hf : StrictMono f), (p.map f hf).length = p.length
-- Mathlib.Data.Fintype.Quotient
/-- Choice-free induction principle for quotients indexed by a finite type.
See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`.  -/
Quotient.induction_on_fintype_pi : ∀ {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {C : ((i : ι) → Quotient (S i)) → Prop} (q : (i : ι) → Quotient (S i)),
  (∀ (a : (i : ι) → α i), C fun x => ⟦a x⟧) → C q
-- Mathlib.Algebra.Star.Unitary
Unitary.mapEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R ≃⋆* S), Unitary.mapEquiv f.symm = (Unitary.mapEquiv f).symm
-- Mathlib.CategoryTheory.Countable
CategoryTheory.discreteCountable : ∀ {α : Type u_1} [Countable α], Countable (CategoryTheory.Discrete α)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.iff_le_add_mul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} {K : NNReal},
  LipschitzWith K f ↔ ∀ (x y : α), f x ≤ f y + ↑K * dist x y
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitor_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.f =
    CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X.src) (CategoryTheory.CategoryStruct.id X.src)
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.of_spanFinrank_maximalIdeal_le : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) ≤ ringKrullDim R → IsRegularLocalRing R
-- Lean.Attributes
Lean.AttributeExtensionState.mk : List Lean.AttributeExtensionOLeanEntry → Std.HashMap Lean.Name Lean.AttributeImpl → Lean.AttributeExtensionState
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ext_cochain_to_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j)
  {K : CochainComplex C ℤ} {γ₁ γ₂ : CochainComplex.HomComplex.Cochain K (CochainComplex.mappingCone φ) i},
  γ₁ = γ₂ ↔
    γ₁.comp (↑(CochainComplex.mappingCone.fst φ)) hij = γ₂.comp (↑(CochainComplex.mappingCone.fst φ)) hij ∧
      γ₁.comp (CochainComplex.mappingCone.snd φ) ⋯ = γ₂.comp (CochainComplex.mappingCone.snd φ) ⋯
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.instMonoFIntP : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CategoryTheory.Mono ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p✝ f n).f n)
-- Mathlib.Topology.Order.LocalExtr
isLocalMin_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {a : α} {b : β}, IsLocalMin (fun x => b) a
-- Mathlib.Algebra.RingQuot
/-- Any `S`-algebra homomorphism `f : A →ₐ[S] B` which respects a relation `s : A → A → Prop`
factors uniquely through a morphism `RingQuot s →ₐ[S] B`.
 -/
RingQuot.liftAlgHom : (S : Type u_1) →
  [inst : CommSemiring S] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra S A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra S B] →
                {s : A → A → Prop} → { f // ∀ ⦃x y : A⦄, s x y → f x = f y } ≃ (RingQuot s →ₐ[S] B)
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.det_isUnit : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.unitaryGroup n α)), IsUnit (↑A).det
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instPartialOrder : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → PartialOrder (FractionalIdeal S P)
-- Init.Data.UInt.BasicAux
/-- Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on
overflow.

This function is overridden at runtime with an efficient implementation.
 -/
Nat.toUSize : ℕ → USize
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.instToString : ToString Aesop.UnsafeQueueEntry
-- Mathlib.GroupTheory.Torsion
CommGroup.comap_torsion_of_injective : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] {f : G →* H},
  Function.Injective ⇑f → Subgroup.comap f (CommGroup.torsion H) = CommGroup.torsion G
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`.  -/
CliffordAlgebra.ofBaseChangeAux : {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) → CliffordAlgebra Q →ₐ[R] CliffordAlgebra (QuadraticForm.baseChange A Q)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_add : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
  MeasureTheory.MemLp.toLp (f + g) ⋯ = MeasureTheory.MemLp.toLp f hf + MeasureTheory.MemLp.toLp g hg
-- Mathlib.Data.Multiset.Filter
Multiset.filter_coe : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α),
  Multiset.filter p ↑l = ↑(List.filter (fun b => decide (p b)) l)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the forward direction of `OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq`. -/
OpenPartialHomeomorph.IsImage.symm_preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddZeroClassOfContinuousAdd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddZeroClass β] → [ContinuousAdd β] → AddZeroClass (CompactlySupportedContinuousMap α β)
-- Mathlib.Order.WithBot
WithTop.instPreorder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α],
  WithTop.instPreorder =
    { toLE := WithTop.instLE, toLT := WithTop.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_add_succ_right_eq_append' : ∀ {m n : ℕ}, (m...=m + (n + 1)).toList = (m...=m + n).toList ++ [m + n + 1]
-- Mathlib.Data.Fintype.Order
/-- A finite Boolean algebra is complete and atomic.  -/
Fintype.toCompleteAtomicBooleanAlgebra : (α : Type u_2) → [Fintype α] → [BooleanAlgebra α] → CompleteAtomicBooleanAlgebra α
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.whiskering_map_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C)
  (c : SimplexCategoryᵒᵖ), (((CategoryTheory.SimplicialObject.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s),
  s.inf' ⋯ f ≤ f b
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → ∀ {h' : k' ∈ m.insertMany l}, (m.insertMany l).get k' h' = k
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
CovariantDerivative.torsion_self : ∀ {𝕜 : 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] {x : M} [inst_6 : CompleteSpace 𝕜]
  [inst_7 : CompleteSpace E] [inst_8 : FiniteDimensional 𝕜 E] [inst_9 : IsManifold I 2 M]
  (cov : CovariantDerivative I E (TangentSpace I)) (X₀ : TangentSpace I x), ((cov.torsion x) X₀) X₀ = 0
-- Mathlib.Topology.Bornology.Basic
OrderDual.isBounded_preimage_toDual : ∀ {α : Type u_2} [inst : Bornology α] {s : Set αᵒᵈ},
  Bornology.IsBounded (⇑OrderDual.toDual ⁻¹' s) ↔ Bornology.IsBounded s
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_singleton_zero : ∀ {R : Type u} [inst : NonAssocSemiring R], Subsemiring.closure {0} = ⊥
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- If `b : ι → M` and `c : κ → N` are bases then so is `fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N`.  -/
Module.Basis.tensorProduct : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_5} →
          {κ : Type u_6} →
            [inst : CommSemiring R] →
              [inst_1 : Semiring S] →
                [inst_2 : Algebra R S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : Module S M] →
                        [inst_6 : IsScalarTower R S M] →
                          [inst_7 : AddCommMonoid N] →
                            [inst_8 : Module R N] →
                              Module.Basis ι S M → Module.Basis κ R N → Module.Basis (ι × κ) S (TensorProduct R M N)
-- Mathlib.Analysis.Convex.Join
convexJoin_comm : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s t : Set E), convexJoin 𝕜 s t = convexJoin 𝕜 t s
-- Batteries.Data.List.Basic
/-- Constructs the union of two lists, by inserting the elements of `l₁` in reverse order to `l₂`.
As a result, `l₂` will always be a suffix, but only the last occurrence of each element in `l₁`
will be retained (but order will otherwise be preserved).
 -/
List.union : {α : Type u_1} → [BEq α] → List α → List α → List α
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sum_le : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {ι : Type u_7} {s : Finset ι} {f : ι → R} {g : Γ₀}, (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
contMDiffAt_mulInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G]
  [inst_7 : LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G) {g : G},
  ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun g => ⟨g, mulInvariantVectorField v g⟩) g
-- Mathlib.Topology.Order.LiminfLimsup
instBoundedGENhdsClassOrderDual : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α], BoundedGENhdsClass αᵒᵈ
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- `D` has *effectively enough objects* with respect to the functor `F` if every object has an
effective presentation.
 -/
CategoryTheory.Functor.EffectivelyEnough : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Topology.Defs.Sequences
/-- A set `s` is sequentially compact if every sequence taking values in `s` has a
converging subsequence.  -/
IsSeqCompact : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `η ▷ 𝟙 _`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightId : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.NormalExpr →
      Mathlib.Tactic.BicategoryLike.NormalExpr →
        Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.LinearAlgebra.Coevaluation
/-- This lemma corresponds to one of the coherence laws for duals in rigid categories, see
`CategoryTheory.Monoidal.Rigid`.  -/
contractLeft_assoc_coevaluation : ∀ (K : Type u) [inst : Field K] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V],
  LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ
      ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ
        LinearMap.lTensor (Module.Dual K V) (coevaluation K V) =
    ↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.ext : ∀ {K : Type u_1} [inst : Field K] {x y : NumberField.RingOfIntegers K}, ↑x = ↑y → x = y
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.IsPure.mk : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {φ : outParam Prop}, (P ⊣⊢ₛ ⌜φ⌝) → Std.Do.SPred.Tactic.IsPure P φ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor α).inv.τr = (CategoryTheory.Bicategory.leftUnitor α.r).hom
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
Submodule.closure.congr_simp : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] (s s_1 : Submodule R M),
  s = s_1 → s.closure = s_1.closure
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_add_cancel : ∀ {α : Type u} [inst : SubtractionMonoid α] {b : α}, IsAddUnit b → ∀ (a : α), a - b + b = a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.nsmul_congr : ∀ {R : Type u_1} [inst : CommSemiring R] {b b' c : R} {a a' : ℕ}, a = a' → b = b' → a' • b' = c → a • b = c
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ofAddValuation_symm_eq : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀],
  Valuation.ofAddValuation.symm = Valuation.toAddValuation
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.applyOrderedFinpartition.eq_1 : ∀ {𝕜 : 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] {n : ℕ}
  (c : OrderedFinpartition n) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (v : Fin n → E) (m : Fin c.length),
  c.applyOrderedFinpartition p v m = (p m) (v ∘ c.emb m)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk.sizeOf_spec : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : SizeOf k] [inst_5 : SizeOf V] [inst_6 : SizeOf P] (carrier : Set P)
  (smul_vsub_vadd_mem' :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier),
  sizeOf { carrier := carrier, smul_vsub_vadd_mem' := smul_vsub_vadd_mem' } = 1
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.MVarId.apply.go.match_1.splitter : (motive : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr → Sort u_1) →
  (x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr) →
    ((newMVars : Array Lean.Expr) →
        (binderInfos : Array Lean.BinderInfo) → (eType : Lean.Expr) → motive (newMVars, binderInfos, eType)) →
      motive x
-- Init.Data.BitVec.Lemmas
/-- `rotateLeft` is invariant under `mod` by the bitwidth.  -/
BitVec.rotateLeft_mod_eq_rotateLeft : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, x.rotateLeft (r % w) = x.rotateLeft r
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverNonSpace : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {fallback : α}, (t.modify k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.NumberTheory.LucasLehmer
/-- **Alias** of the reverse direction of `mersenne_pos`. -/
Mathlib.Meta.Positivity.mersenne_pos_of_pos : ∀ {p : ℕ}, 0 < p → 0 < mersenne p
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_nonneg : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i : ι}, i0 ≤ i → 0 ≤ toZ i0 i
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveTelescopeInfo.mk.inj : ∀ {haveInfo : Array Lean.Meta.HaveInfo} {bodyDeps bodyTypeDeps : Std.HashSet ℕ} {body bodyType : Lean.Expr}
  {level : Lean.Level} {haveInfo_1 : Array Lean.Meta.HaveInfo} {bodyDeps_1 bodyTypeDeps_1 : Std.HashSet ℕ}
  {body_1 bodyType_1 : Lean.Expr} {level_1 : Lean.Level},
  { haveInfo := haveInfo, bodyDeps := bodyDeps, bodyTypeDeps := bodyTypeDeps, body := body, bodyType := bodyType,
        level := level } =
      { haveInfo := haveInfo_1, bodyDeps := bodyDeps_1, bodyTypeDeps := bodyTypeDeps_1, body := body_1,
        bodyType := bodyType_1, level := level_1 } →
    haveInfo = haveInfo_1 ∧
      bodyDeps = bodyDeps_1 ∧ bodyTypeDeps = bodyTypeDeps_1 ∧ body = body_1 ∧ bodyType = bodyType_1 ∧ level = level_1
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.coeff_modOf_self_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g d : G),
  (x.modOf g).coeff (g + d) = 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.mk : Array Lean.Meta.Grind.Arith.CommRing.CommRing →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
    Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ →
      Array Lean.Meta.Grind.Arith.CommRing.CommSemiring →
        Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
          Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ →
            Array Lean.Meta.Grind.Arith.CommRing.Ring →
              Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ →
                Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
                  Array Lean.Meta.Grind.Arith.CommRing.Semiring →
                    Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ →
                      Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) → ℕ → Bool → Lean.Meta.Grind.Arith.CommRing.State
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.getD_eq_getValueD : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {fallback : β},
      Std.DHashMap.Internal.Raw₀.Const.getD m a fallback =
        Std.Internal.List.getValueD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback
-- Mathlib.Analysis.InnerProductSpace.Calculus
OpenPartialHomeomorph.contDiffOn_univUnitBall_symm : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  ContDiffOn ℝ (↑n) (↑OpenPartialHomeomorph.univUnitBall.symm) (Metric.ball 0 1)
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.hasFunCCAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Bool
-- Mathlib.Data.Countable.Defs
Equiv.countable_iff : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Countable α ↔ Countable β
-- Mathlib.Order.Lattice.Congruence
/-- An equivalence relation is a congruence relation for the lattice structure if it is compatible
with the `inf` and `sup` operations.  -/
LatticeCon : (α : Type u_2) → [Lattice α] → Type u_2
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.comm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (self : X.Hom Y) (U : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj U Y.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.f U)
      (CategoryTheory.CategoryStruct.comp (Y.snd.β U).hom h) =
    CategoryTheory.CategoryStruct.comp (X.snd.β U).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U self.f) h)
-- Init.Data.Vector.Lemmas
Vector.instDecidableExistsAndMemOfDecidablePred : {α : Type u_1} → {n : ℕ} → {xs : Vector α n} → {p : α → Prop} → [DecidablePred p] → Decidable (∃ x ∈ xs, p x)
-- Mathlib.Order.Filter.Germ.Basic
/-- Lift a predicate on `β` to `Germ l β`.  -/
Filter.Germ.LiftPred : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → (β → Prop) → l.Germ β → Prop
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- The restriction map from global sections of `F` to sections on `U`.  -/
CategoryTheory.Sheaf.ΓRes : {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) → (U : Cᵒᵖ) → (CategoryTheory.Sheaf.Γ J A).obj F ⟶ F.obj.obj U