mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.Exception
/-- A generalisation of `fail_if_success` to an arbitrary `MonadError`.
 -/
successIfFail : {α : Type} → {M : Type → Type} → [Lean.MonadError M] → [Monad M] → M α → M Lean.Exception
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_uIcc : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.map (finCongr h).toEmbedding (Finset.uIcc i j) = Finset.uIcc (Fin.cast h i) (Fin.cast h j)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans F G) {a b c : B} {a' : C} (f : a ⟶ b)
  (g : b ⟶ c) (h : G.obj c ⟶ a') {Z : F.obj a ⟶ a'}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (η.app a)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h))
          h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom
          h)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c))
              h).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f)
              (CategoryTheory.Bicategory.whiskerRight (η.naturality g) h))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g))
                  h).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight
                  (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (G.map g)) h)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight
                      (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h)
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.Bicategory.associator (η.app a)
                          (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom
                      h_1))))))))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_succ_succ : ∀ {m n : ℤ}, ((m + 1)...n + 1).toList = List.map (fun x => x + 1) (m...n).toList
-- Mathlib.Algebra.Group.Defs
DivInvMonoid.toZPow : {G : Type u} → [self : DivInvMonoid G] → ZPow G
-- Mathlib.CategoryTheory.Types.Basic
/-- Any equivalence between types in the same universe gives
a categorical isomorphism between those types.
 -/
Equiv.toIso : {X Y : Type u} → X ≃ Y → (X ≅ Y)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.toString_extract : ∀ {b e : String.Pos.Raw} {s : Substring.Raw},
  s.Valid →
    { str := s.toString, startPos := b, stopPos := e }.Valid →
      (s.extract b e).toString = String.Pos.Raw.extract s.toString b e
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_comap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B), ↑(Subalgebra.comap f S) = ⇑f ⁻¹' ↑S
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_self_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, s ⊆ t → s /ₛ s ⊆ t /ₛ t
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.rightUnitor_hom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.f =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.fst).hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path includes the data of `n + 1` 0-simplices in `X`.  -/
SSet.Truncated.Path.vertex : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} →
    {m : ℕ} → X.Path m → Fin (m + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := ⋯ })
-- Mathlib.Order.Heyting.Basic
sdiff_le_iff' : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ c ⊔ b
-- Mathlib.GroupTheory.CosetCover
/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
Then at least one subgroup `H i` has finite index in `G`.  -/
Subgroup.exists_finiteIndex_of_leftCoset_cover : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ → ∃ k ∈ s, (H k).FiniteIndex
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.instHasLiftingPropertyInr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Y} {s : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout s f] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [CategoryTheory.HasLiftingProperty s p],
  CategoryTheory.HasLiftingProperty (CategoryTheory.Limits.pushout.inr s f) p
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c),
  CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.obj K =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNatClamp_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMapIso'_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  (CategoryTheory.ShortComplex.homologyMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.homologyMap' e.hom h₁ h₂
-- Mathlib.Algebra.Order.Field.Power
zpow_two_pos_of_ne_zero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α}, a ≠ 0 → 0 < a ^ 2
-- Mathlib.RingTheory.Polynomial.Pochhammer
Nat.cast_choose_eq_ascPochhammer_div : ∀ (K : Type u_1) [inst : DivisionSemiring K] [CharZero K] (a b : ℕ),
  ↑(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b.factorial
-- Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
HomotopyCategory.composableArrowsFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1}
  (φ : X ⟶ Y),
  (HomotopyCategory.composableArrowsFunctor C).map φ =
    CochainComplex.mappingCone.map
      (X.map' 0 1 HomotopyCategory.composableArrowsFunctor._proof_1 HomotopyCategory.composableArrowsFunctor._proof_2)
      (Y.map' 0 1 HomotopyCategory.composableArrowsFunctor._proof_1 HomotopyCategory.composableArrowsFunctor._proof_2)
      (φ.app 0) (φ.app 1) ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.interSmallerFn.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l sofar : List ((a : α) × β a)) (k : α),
  Std.Internal.List.interSmallerFn l sofar k =
    match Std.Internal.List.getEntry? k l with
    | some kv' => Std.Internal.List.insertEntry kv'.fst kv'.snd sofar
    | none => sofar
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofProfinite.eq_1 : ∀ (G : Profinite) [inst : AddGroup ↑G.toTop] [inst_1 : IsTopologicalAddGroup ↑G.toTop],
  ProfiniteAddGrp.ofProfinite G = ProfiniteAddGrp.of ↑G.toTop
-- Mathlib.Data.Set.Image
Set.forall_subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : Set β → Prop}, (∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_apply_mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (x : FreeAddMonoid (M ⊕ N)),
  (AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.mk x) = (FreeAddMonoid.lift (Sum.elim ⇑f ⇑g)) x
-- Mathlib.Topology.LocallyClosed
isLocallyClosed_iff_isOpen_coborder : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsLocallyClosed s ↔ IsOpen (coborder s)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Topology.IsClosedEmbedding.map_tsum : ∀ {ι : Type u_4} {α : Type u_5} {α' : Type u_6} {G : Type u_7} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid α']
  [inst_2 : TopologicalSpace α] [inst_3 : TopologicalSpace α'] [T2Space α'] (f : ι → α) {L : SummationFilter ι} {g : G}
  [inst_5 : FunLike G α α'] [AddMonoidHomClass G α α'],
  Topology.IsClosedEmbedding ⇑g → g (∑'[L] (i : ι), f i) = ∑'[L] (i : ι), g (f i)
-- Mathlib.Order.Interval.Set.Basic
Set.subsingleton_Icc_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → (Set.Icc a b).Subsingleton
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mk : {R : Type u} →
  {M : Type v} →
    [inst : SMul R M] → (carrier : Set M) → (∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier) → SubMulAction R M
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldlM.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (n : ℕ) (f : α → Fin n → m α) (x : α) (i : ℕ),
  Fin.foldlM.loop✝ n f x i =
    if h : i < n then do
      let x ← f x ⟨i, h⟩
      Fin.foldlM.loop✝ n f x (i + 1)
    else pure x
-- Mathlib.Data.Matrix.Mul
Matrix.neg_mul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n]
  (M : Matrix m n α) (N : Matrix n o α), -M * N = -(M * N)
-- Mathlib.Algebra.GradedMonoid
/-- `GCommMonoid` implies a `CommMonoid (GradedMonoid A)`, although this is only used as an
instance locally to define notation in `gmonoid` and similar typeclasses.  -/
GradedMonoid.GCommMonoid.toCommMonoid : {ι : Type u_1} →
  (A : ι → Type u_2) → [inst : AddCommMonoid ι] → [GradedMonoid.GCommMonoid A] → CommMonoid (GradedMonoid A)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.component.of : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i j : ι) (b : M j),
  (DirectSum.component R ι M i) ((DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Module.Basis.continuous_coe_repr : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [inst : NontriviallyNormedField R] [CompleteSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M] [inst_6 : Module R M]
  [ContinuousSMul R M] (B : Module.Basis ι R M), Continuous fun m => ⇑(B.repr m)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.whiskering`.

---

Whiskering on the left by `E : K ⥤ J` gives a functor from `Cone F` to `Cone (E ⋙ F)`.
 -/
CategoryTheory.Limits.Cones.whiskering : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (E : CategoryTheory.Functor K J) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (E.comp F))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k a fallback : α}, (t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Mathlib.Order.Atoms
IsAtomic.exists_atom : ∀ (α : Type u_2) [inst : PartialOrder α] [inst_1 : OrderBot α] [Nontrivial α] [IsAtomic α], ∃ a, IsAtom a
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanIso_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanIso 0 A B f ↔ Set.BijOn f A B
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [CategoryTheory.Abelian C],
  CategoryTheory.IsSeparator G →
    ∀ {X : C} (A : CategoryTheory.Subobject X),
      A ≠ ⊤ →
        ∃ A', ∃ (h : A < A'), (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).pushouts (A.ofLE A' ⋯)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_functor_obj_hom : ∀ {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] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
/-- A functor `G : C ⥤ D` is locally faithful w.r.t. a topology on `D` if for every `f₁ f₂ : U ⟶ V`
whose images in `D` are equal, the set of `G.map gᵢ : G.obj Wᵢ ⟶ G.obj U` such that
`gᵢ ≫ f₁ = gᵢ ≫ f₂` is a coverage of the topology on `D`.
 -/
CategoryTheory.Functor.IsLocallyFaithful : {C : Type uC} →
  [inst : CategoryTheory.Category.{vC, uC} C] →
    {D : Type uD} →
      [inst_1 : CategoryTheory.Category.{vD, uD} D] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → Prop
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (a : α) (as : List α) (acc : Array α)
  (h_1 : (x : Array α) → motive [] x) (h_2 : (a : α) → (as : List α) → (acc : Array α) → motive (a :: as) acc),
  (match a :: as, acc with
    | [], x => h_1 x
    | a :: as, acc => h_2 a as acc) =
    h_2 a as acc
-- Mathlib.Analysis.SpecificLimits.Normed
/-- The **alternating series test** for antitone sequences.  -/
Antitone.tendsto_alternating_series_of_tendsto_zero : ∀ {f : ℕ → ℝ},
  Antitone f →
    Filter.Tendsto f Filter.atTop (nhds 0) →
      ∃ l, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.instSupSet : SupSet ℝ
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.subset_of_diffUnion_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), ∀ t ∈ ↑(hC.disjointOfDiffUnion hs hI), t ⊆ s \ ⋃₀ ↑I
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrix.congr_simp : ∀ (n : Type u_1) {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (R : Type u_2)
  [inst_3 : CommRing R] (m m_1 : R), m = m_1 → FixedDetMatrix n R m = FixedDetMatrix n R m_1
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root_coroot_eq_pairing : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  (P.toLinearMap (P.root i)) (P.coroot j) = P.pairing i j
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
MulEquiv.toContinuousMulEquiv.eq_1 : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s),
  e.toContinuousMulEquiv he =
    { toFun := ⇑e, invFun := ⇑e.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_abs : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a : M),
  ArchimedeanClass.mk |a| = ArchimedeanClass.mk a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z),
  I.map (CategoryTheory.CategoryStruct.comp f g) = (I.map f).map g
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.toPartialEquiv : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → {proj : Z → B} → Bundle.Pretrivialization F proj → PartialEquiv Z (B × F)
-- Init.Data.Vector.Find
Vector.findSome?_map : ∀ {β : Type u_1} {γ : Type u_2} {n : ℕ} {α : Type u_3} {p : γ → Option α} {f : β → γ} {xs : Vector β n},
  Vector.findSome? p (Vector.map f xs) = Vector.findSome? (p ∘ f) xs
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_5 : Std.Roi.Sliceable ByteArray ℕ ByteSlice
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_1 : ∀ {a0 a1 : ℤ} {t : List ℤ}, (Lean.Omega.LinearCombo.coordinate 1).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1
-- Std.Time.Duration
Std.Time.Duration.instCoeOffset_3 : Coe Std.Time.Hour.Offset Std.Time.Duration
-- Mathlib.RingTheory.Perfection
/-- **Alias** of `Perfection.submonoid`.

---

`Perfection M p` as a submonoid of `ℕ → M`.  -/
Monoid.perfection : (M : Type u_1) → [inst : CommMonoid M] → ℕ → Submonoid (ℕ → M)
-- Lean.Elab.Command
Lean.Elab.Command.lintersRef : IO.Ref (Array Lean.Linter)
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_apply_single : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {c : RingCon R} {i j : n} {x y : R}, (RingCon.matrix n c) (Matrix.single i j x) (Matrix.single i j y) ↔ c x y
-- Init.Core
/-- Auxiliary type used to compile `do` notation. It is an optimization of
either `DoResultPRBC α PEmpty σ` or `DoResultPRBC PEmpty α σ` to remove the
impossible case, used when either `pure` or `return` is never used.
 -/
DoResultSBC : Type u → Type u → Type u
-- Mathlib.Data.Int.Fib.Basic
Int.fib_eq_zero : ∀ {n : ℤ}, Int.fib n = 0 ↔ n = 0
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- The predicate corresponding to a base set of the filter defined by an
`IntegrationParams`. It says that

* if `l.bHenstock`, then `π` is a Henstock prepartition, i.e. each tag belongs to the corresponding
  closed box;
* `π` is subordinate to `r`;
* if `l.bDistortion`, then the distortion of each box in `π` is less than or equal to `c`;
* if `l.bDistortion`, then there exists a prepartition `π'` with distortion `≤ c` that covers
  exactly `I \ π.iUnion`.

The last condition is automatically verified for partitions, and is used in the proof of the
Sacks-Henstock inequality to compare two prepartitions covering the same part of the box.

It is also automatically satisfied for any `c > 1`, see TODO section of the module docstring for
details.  -/
BoxIntegral.IntegrationParams.MemBaseSet : {ι : Type u_1} →
  [Fintype ι] →
    BoxIntegral.IntegrationParams →
      (I : BoxIntegral.Box ι) → NNReal → ((ι → ℝ) → ↑(Set.Ioi 0)) → BoxIntegral.TaggedPrepartition I → Prop
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_succ_zero : ∀ (n : ℕ), n.succ.stirlingFirst 0 = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `sum_apply`. -/
SchwartzMap.sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.Data.Multiset.Bind
Multiset.card_product : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β), (s ×ˢ t).card = s.card * t.card
-- Mathlib.Data.Set.Prod
Set.graphOn_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (f : α → β) (g : β → γ),
  Set.graphOn (g ∘ f) s = (fun x => (x.1, g x.2)) '' Set.graphOn f s
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.Slice.Pos.prevn.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedHeader.default : Std.Time.TimeZone.TZif.Header
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.map_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {M : Type u_1} [inst : L.Structure M]
  [inst_1 : L'.Structure M] [ϕ.IsExpansionOn M] {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
-- Mathlib.Data.Stream.Init
Stream'.append_stream_head_tail : ∀ {α : Type u} (s : Stream' α), [s.head] ++ₛ s.tail = s
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coeMonoidHom_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  (self : { x // x ∈ Set.Ioc 0 1 }), Set.Ioc.coeMonoidHom self = ↑self
-- Mathlib.Order.WellFoundedSet
Finset.isPWO_bUnion : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (s : Finset ι) {f : ι → Set α},
  (⋃ i ∈ s, f i).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.jacobianOfHasCoeffs.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀], P.jacobianOfHasCoeffs R₀ = (P.ofHasCoeffs R₀).jacobiMatrix.det
-- Mathlib.RepresentationTheory.Basic
Representation.norm_ofMulDistribMulAction_eq : ∀ {G M : Type} [inst : Group G] [inst_1 : Fintype G] [inst_2 : CommGroup M] [inst_3 : MulDistribMulAction G M]
  (x : Additive M), Additive.toMul ((Representation.ofMulDistribMulAction G M).norm x) = ∏ g, g • Additive.toMul x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKey? k = none
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.map_id : ∀ {V₁ : Type u_3} [inst : SeminormedAddCommGroup V₁] {W₁ : Type u_6} [inst_1 : SeminormedAddCommGroup W₁]
  {f₁ g₁ : NormedAddGroupHom V₁ W₁},
  NormedAddGroupHom.Equalizer.map (NormedAddGroupHom.id V₁) (NormedAddGroupHom.id W₁) ⋯ ⋯ =
    NormedAddGroupHom.id ↥(f₁.equalizer g₁)