mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k fallback : α} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => (f x m[x]).isSome).getD fallback
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.comp : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (self : CategoryTheory.Limits.DiagramOfCones F)
  {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
  (self.map (CategoryTheory.CategoryStruct.comp f g)).hom =
    CategoryTheory.CategoryStruct.comp (self.map f).hom (self.map g).hom
-- Mathlib.Topology.Algebra.Group.Basic
Filter.inv_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, (nhdsWithin a (Set.Ioi a))⁻¹ = nhdsWithin a⁻¹ (Set.Iio a⁻¹)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) ≠ j → HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
-- Mathlib.RingTheory.NoetherNormalization
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.degreeOf_zero_t : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v : Fin (n + 1) →₀ ℕ) {a : k},
  a ≠ 0 →
    MvPolynomial.degreeOf 0 ((NoetherNormalization.T✝ f) ((MvPolynomial.monomial v) a)) =
      ∑ i, (fun i => (2 + f.totalDegree) ^ ↑i) i * v i
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Roo α → Std.DTreeMap.Internal.RooSliceData α β
-- Mathlib.FieldTheory.Separable
IntermediateField.isSeparable_tower_top : ∀ (F : Type u_1) [inst : Field F] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra F K] (M : IntermediateField F K)
  [Algebra.IsSeparable F K], Algebra.IsSeparable (↥M) K
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.hom_ofHom : ∀ {X Y : Type u} [inst : UniformSpace X] [inst_1 : UniformSpace Y] (f : { f // UniformContinuous f }),
  UniformSpaceCat.Hom.hom (UniformSpaceCat.ofHom f) = f
-- Mathlib.NumberTheory.Height.MvPolynomial
IsNonarchimedean.eval_mvPolynomial_le : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} [Finite ι] {v : AbsoluteValue K ℝ},
  IsNonarchimedean ⇑v →
    ∀ {p : MvPolynomial ι K} {N : ℕ},
      p.IsHomogeneous N →
        ∀ (x : ι → K), v ((MvPolynomial.eval x) p) ≤ (⨆ s, v (MvPolynomial.coeff (↑s) p)) * (⨆ i, v (x i)) ^ N
-- Mathlib.Analysis.Analytic.Order
/-- The order multiplies by `n` when taking an analytic function to its `n`th power.  -/
analyticOrderAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ → ∀ (n : ℕ), analyticOrderAt (f ^ n) z₀ = n • analyticOrderAt f z₀
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- **Alias** of `spectrum.hasDerivAt_resolvent_const_left`. -/
spectrum.hasDerivAt_resolvent : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {k : 𝕜}, k ∈ resolventSet 𝕜 a → HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
-- Init.Prelude
/-- Applies a function inside a functor. This is used to overload the `<$>` operator.

When mapping a constant function, use `Functor.mapConst` instead, because it may be more
efficient.


Conventions for notations in identifiers:

 * The recommended spelling of `<$>` in identifiers is `map`. -/
Functor.map : {f : Type u → Type v} → [self : Functor f] → {α β : Type u} → (α → β) → f α → f β
-- Mathlib.Order.SymmDiff
bihimp_isCommutative : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α], Std.Commutative fun x1 x2 => bihimp x1 x2
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_toFun : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : ℕ} (h : n < List.length basis),
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial basis n).toFun = basis[n]
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_zero_zero : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M], Finsupp.cons 0 0 = 0
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : k.succ = 0 → motive 0) (h_2 : (k_1 : ℕ) → k.succ = k_1.succ → motive k_1.succ),
  (match h' : k.succ with
    | 0 => h_1 h'
    | k_1.succ => h_2 k_1 h') =
    h_2 k ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.refl_target : ∀ (X : Type u_7) [inst : TopologicalSpace X], (OpenPartialHomeomorph.refl X).target = Set.univ
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ici : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a x : α}, x ∈ Finset.Ici a ↔ a ≤ x
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHSubOffset_2 : HSub Std.Time.PlainTime Std.Time.Second.Offset Std.Time.PlainTime
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_ofFn : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin n → M), (List.ofFn f).sum = ∑ i, f i
-- Lean.Elab.Tactic.ElabTerm
/-- Try to close main goal using `x target tag`, where `target` is the type of the main goal and `tag` is its user name.

If `checkNewUnassigned` is true, then throws an error if the resulting value has metavariables that were created during the execution of `x`.
If it is false, then it is the responsibility of `x` to add such metavariables to the goal list.

During the execution of `x`:
* The local context is that of the main goal.
* The goal list has the main goal removed.
* It is allowable to modify the goal list, for example with `Lean.Elab.Tactic.pushGoals`.

On failure, the main goal remains at the front of the goal list.
 -/
Lean.Elab.Tactic.closeMainGoalUsing : Lean.Name →
  (Lean.Expr → Lean.Name → Lean.Elab.Tactic.TacticM Lean.Expr) → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If `X` and `Y` forms an exact pairing in a braided category, then so does `Y` and `X`
by composing the coevaluation and evaluation morphisms with associators.  -/
CategoryTheory.BraidedCategory.exactPairing_swap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        (X Y : C) → [CategoryTheory.ExactPairing X Y] → CategoryTheory.ExactPairing Y X
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget₂AddMon_obj_X : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.RingObjCat C),
  ((CategoryTheory.RingObjCat.forget₂AddMon C).obj R).X = R.X
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.id_toLinearMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A], ↑(CoalgHom.id R A) = LinearMap.id
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_map : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {k : β → α} {l : Filter β}, f =o[Filter.map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_le_maxKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {he : t.isEmpty = false}, (cmp (t.maxKey he) ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_prod_list_of_pairwise_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {l : List (Equiv.Perm α)},
  List.Pairwise Equiv.Perm.Disjoint l → l.prod.support.card = (List.map (Finset.card ∘ Equiv.Perm.support) l).sum
-- Lean.Meta.Basic
Lean.Meta.savingCache : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.mk.injEq : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (val val_1 : X),
  ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `G` is an equivalence, then a left extension of `F` along `L` is universal iff
the corresponding left extension of `G ⋙ F` along `G ⋙ L` is.  -/
CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquiv : {C : Type u_1} →
  {C' : Type u_2} →
    {H : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (L : CategoryTheory.Functor C D) →
                  (F : CategoryTheory.Functor C H) →
                    (G : CategoryTheory.Functor C' C) →
                      [G.IsEquivalence] →
                        (e : L.LeftExtension F) →
                          CategoryTheory.StructuredArrow.IsUniversal e ≃
                            CategoryTheory.StructuredArrow.IsUniversal
                              ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj e)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.hom_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ 𝒞₂ 𝒞₃ : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.CategoryStruct.comp (𝒞₁.hom 𝒞₂) (𝒞₂.hom 𝒞₃) = 𝒞₁.hom 𝒞₃
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.isClosed : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D], IsClosed C
-- Mathlib.GroupTheory.Torsion
/-- The `p`-primary component is a `p`-group.  -/
CommGroup.primaryComponent.isPGroup : ∀ {G : Type u_1} [inst : CommGroup G] {p : ℕ}, IsPGroup p ↥(CommGroup.primaryComponent G p)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.algebraMap_posForm : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] {x y : ↥(Submodule.span S (Set.range ⇑P.root))},
  (algebraMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuousWithinAt.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α} {a : α},
  LowerSemicontinuousWithinAt f s a →
    LowerSemicontinuousWithinAt g s a → LowerSemicontinuousWithinAt (fun x => max (f x) (g x)) s a
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If a functor `F` has a limit, so does any naturally isomorphic functor.  -/
CategoryTheory.Limits.hasLimit_of_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] (α : F ≅ G), CategoryTheory.Limits.HasLimit G
-- Mathlib.Topology.Connected.PathConnected
/-- When two points are joined, choose some path from `x` to `y`.  -/
Joined.somePath : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Joined x y → Path x y
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (v : ι → E), Orthonormal 𝕜 v = ((∀ (i : ι), ‖v i‖ = 1) ∧ Pairwise fun i j => inner 𝕜 (v i) (v j) = 0)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_finset_product_right : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) → ∀ {f : α × γ → β}, ∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (a, c)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.restrictionLE_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) {k₁ k₂ : ↑(Set.Iic i)} (φ : k₁ ⟶ k₂),
  (CategoryTheory.SmallObject.restrictionLE F hi).map φ = F.map (CategoryTheory.homOfLE ⋯)
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.nth_zero : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), l.nth 0 = l.head
-- Mathlib.Analysis.Convex.Join
convexHull_insert : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E},
  s.Nonempty → (convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} ((convexHull 𝕜) s)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The `i`th cycles functor `HomologicalComplex C c ⥤ C`.  -/
HomologicalComplex.cyclesFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          ι → [CategoryTheory.CategoryWithHomology C] → CategoryTheory.Functor (HomologicalComplex C c) C
-- Lean.Language.Lean.Types
Lean.Language.Lean.instToSnapshotTreeHeaderProcessedSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.HeaderProcessedSnapshot
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.eq_1 : ∀ {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {α : Type u_8} {x : MeasurableSpace α}
  (f : α → ε) (μ : MeasureTheory.Measure α),
  MeasureTheory.Integrable f μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.HasFiniteIntegral f μ)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.Hom.toPartialMap_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (AlgebraicGeometry.Scheme.Hom.toPartialMap f).hom = CategoryTheory.CategoryStruct.comp X.topIso.hom f
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_swap : ∀ {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : AddGroupWithOne α] (i j : n),
  (Equiv.toPEquiv (Equiv.swap i j)).toMatrix =
    1 - (PEquiv.single i i).toMatrix - (PEquiv.single j j).toMatrix + (PEquiv.single i j).toMatrix +
      (PEquiv.single j i).toMatrix
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given two functors `L : C ⥤ D` and `F : C ⥤ H`, this is the category of functors
`F' : D ⥤ H` equipped with a natural transformation `L ⋙ F' ⟶ F`.  -/
CategoryTheory.Functor.RightExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            CategoryTheory.Functor C D →
              CategoryTheory.Functor C H → Type (max (max (max (max u_3 u_4) v_3) v_4) u_1 v_3)
-- Mathlib.Data.Finset.Card
Finset.card_singleton : ∀ {α : Type u_1} (a : α), {a}.card = 1
-- Mathlib.Topology.Order
/-- In the indiscrete topology no points are separable.

The corresponding `bot` lemma is handled more generally by `inseparable_iff_eq`.  -/
Inseparable.all : ∀ {α : Type u} [inst : TopologicalSpace α] [IndiscreteTopology α] (x y : α), Inseparable x y
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.add_sInter_subset : ∀ {α : Type u_2} [inst : Add α] (s : Set α) (T : Set (Set α)), s + ⋂₀ T ⊆ ⋂ t ∈ T, s + t
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.comp_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {X Y Z : CategoryTheory.Comma L R} {f : Y ⟶ X} {g : Z ⟶ Y},
  (CategoryTheory.CategoryStruct.comp g f).right = CategoryTheory.CategoryStruct.comp g.right f.right
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapLMultilinear_toFun_apply : ∀ {ι : Type u_1} [inst : Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (E' : ι → Type u_5)
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i) (a : PiTensorProduct 𝕜 fun i => E i),
  ((PiTensorProduct.mapLMultilinear 𝕜 E E') f) a =
    (PiTensorProduct.liftAux ((PiTensorProduct.tprodL 𝕜).compContinuousLinearMap f).toMultilinearMap) a
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.encode.match_1.eq_2 : ∀ (motive : Mathlib.Deriving.Encodable.S✝ → Sort u_1) (a b : Mathlib.Deriving.Encodable.S✝)
  (h_1 : (n : ℕ) → motive (Mathlib.Deriving.Encodable.S.nat✝ n))
  (h_2 : (a b : Mathlib.Deriving.Encodable.S✝) → motive (Mathlib.Deriving.Encodable.S.cons✝ a b)),
  (match Mathlib.Deriving.Encodable.S.cons✝ a b with
    | Mathlib.Deriving.Encodable.S.nat✝ n => h_1 n
    | Mathlib.Deriving.Encodable.S.cons✝ a b => h_2 a b) =
    h_2 a b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.real_toNNReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => (f x).toNNReal
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.disjoint_C_support_lim : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P),
  Disjoint c.C (Function.support c.lim)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_C_mul_T : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ) (a : R),
  a ≠ 0 → (LaurentPolynomial.C a * LaurentPolynomial.T n).degree = ↑n
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.diag_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.diag C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C × C))
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX_hom_D₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_C_of_ne_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {m : σ →₀ ℕ},
  m ≠ 0 → ∀ (a : R), MvPolynomial.coeff m (MvPolynomial.C a) = 0
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [inst_2 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (F.map f) =
    CategoryTheory.CategoryStruct.id (F.obj X)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zipWith.eq_1 : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (as : Array α) (bs : Array β),
  Array.zipWith f as bs = (as.zipWithMAux bs (fun x1 x2 => pure (f x1 x2)) 0 #[]).run
-- Batteries.Data.Fin.Coding
Fin.encodeSigma_decodeSigma : ∀ {n : ℕ} (f : Fin n → ℕ) (x : Fin (Fin.sum f)), Fin.encodeSigma f (Fin.decodeSigma f x) = x
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.X : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          CategoryTheory.coherentTopology.struct✝ F → ℕ → C
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.ofπ.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (π π_1 : Y ⟶ P) (e_π : π = π_1)
  (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π),
  CategoryTheory.Limits.Cofork.ofπ π w = CategoryTheory.Limits.Cofork.ofπ π_1 ⋯