mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub_flip : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α}, a - b ≤ b - a ↔ a ≤ b
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_obj_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G)
  (a : F.Grothendieck), ((CategoryTheory.Pseudofunctor.Grothendieck.map α).obj a).base = a.base
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp}, x ∈ t.toList ↔ x ∈ ↑t
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars.congr_simp : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M]
  (V V_1 : Submodule R M), V = V_1 → Submodule.restrictScalars S V = Submodule.restrictScalars S V_1
-- Mathlib.Data.Set.Card
/-- **Alias** of the reverse direction of `Set.encard_eq_top_iff`. -/
Set.encard_eq_top : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.encard = ⊤
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionLlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.llp.IsStableUnderTransfiniteComposition
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) [inst_2 : Inhabited (β a)]
  (l l_1 : List ((a : α) × β a)), l = l_1 → Std.Internal.List.getValueCast! a l = Std.Internal.List.getValueCast! a l_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagNode.proof : Lean.Meta.Grind.EMatchDiagNode → Lean.Expr
-- Mathlib.Analysis.Convex.Quasiconvex
Monotone.quasiconcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → QuasiconcaveOn 𝕜 Set.univ f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.CommSq.cocone_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} (s : CategoryTheory.CommSq f g h i), s.cocone.inr = i
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_dec : ∀ {p : String.Pos.Raw}, p.dec.byteIdx = p.byteIdx - 1
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_add_bdiv' : ∀ (x : ℤ) (m : ℕ), x.bmod m + x.bdiv m * ↑m = x
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- Construct a pseudofunctor from an oplax functor whose `mapId` and `mapComp` are isomorphisms.  -/
CategoryTheory.Pseudofunctor.mkOfOplax' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) →
          [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] →
            [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] →
              CategoryTheory.Pseudofunctor B C
-- Mathlib.Data.Seq.Defs
Stream'.Seq.corec_cons : ∀ {α : Type u} {β : Type v} {f : β → Option (α × β)} {b : β} {x : α} {s : β},
  f b = some (x, s) → Stream'.Seq.corec f b = Stream'.Seq.cons x (Stream'.Seq.corec f s)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Occasionally useful for rewriting in the backwards direction.  -/
CategoryTheory.MorphismProperty.Under.forget_comp_forget_map : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T)
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Under.forget P Q X).comp (CategoryTheory.Under.forget X)).map f = f.right
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.gc : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], GaloisConnection (NonUnitalStarAlgebra.adjoin R) SetLike.coe
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instAdditivePushforward : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (AlgebraicGeometry.Scheme.Modules.pushforward f).Additive
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  HomologicalComplex.singleObjHomologySelfIso c j A =
    (((HomologicalComplex.single C c j).obj A).isoHomologyπ (c.prev j) j ⋯ ⋯).symm ≪≫
      HomologicalComplex.singleObjCyclesSelfIso c j A
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.fderivCLM_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  (f : TestFunction Ω F n), ⇑((TestFunction.fderivCLM 𝕜 n k) f) = if k + 1 ≤ n then fderiv ℝ ⇑f else 0
-- Mathlib.Algebra.Module.Torsion.Basic
Module.instQuotientIdealSubmoduleHSMulTop : {R : Type u_1} →
  (M : Type u_2) →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (I : Ideal R) → [inst_3 : I.IsTwoSided] → Module (R ⧸ I) (M ⧸ I • ⊤)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    Lean.Grind.Linarith.Expr.denote ctx lhs = Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p = 0
-- Mathlib.RingTheory.IsTensorProduct
/-- If `N` is the base change of `M` to `S` and `O` the base change of `M` to `T`, then
`O` is the base change of `N` to `T`.  -/
IsBaseChange.of_comp : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [inst_9 : CommSemiring T]
  [inst_10 : Algebra R T] [inst_11 : Algebra S T] [IsScalarTower R S T] [inst_13 : AddCommMonoid O]
  [inst_14 : Module R O] [inst_15 : Module S O] [inst_16 : Module T O] [inst_17 : IsScalarTower S T O]
  [inst_18 : IsScalarTower R S O] [inst_19 : IsScalarTower R T O] {f : M →ₗ[R] N},
  IsBaseChange S f → ∀ {h : N →ₗ[S] O}, IsBaseChange T (↑R h ∘ₗ f) → IsBaseChange T h
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.symm_reindexAddEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [inst : Add R] (eₘ : m ≃ m')
  (eₙ : n ≃ n'), (Matrix.reindexAddEquiv R eₘ eₙ).symm = Matrix.reindexAddEquiv R eₘ.symm eₙ.symm
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The component 1-morphisms of a lax transformation.  -/
CategoryTheory.Lax.LaxTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → CategoryTheory.Lax.LaxTrans F G → (a : B) → F.obj a ⟶ G.obj a
-- Lean.Server.References
Lean.Server.DirectImports.mk.injEq : ∀ (ordered : Array Lean.Server.ModuleImport) (index : Lean.Server.ModuleImportIndex)
  (ordered_1 : Array Lean.Server.ModuleImport) (index_1 : Lean.Server.ModuleImportIndex),
  ({ ordered := ordered, index := index } = { ordered := ordered_1, index := index_1 }) =
    (ordered = ordered_1 ∧ index = index_1)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_biUnion_le : ∀ {ι α : Type u} (A : ι → Set α) (s : Set ι), Cardinal.mk ↑(⋃ x ∈ s, A x) ≤ Cardinal.mk ↑s * ⨆ x, Cardinal.mk ↑(A ↑x)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedNotification.default : {α : Type u} → [Inhabited α] → Lean.JsonRpc.Notification α
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.mk.injEq : ∀ (depth : ℕ) (commonFVarIds : Array Lean.FVarId) (goals : Array (Lean.MVarId × Array Lean.FVarId)) (depth_1 : ℕ)
  (commonFVarIds_1 : Array Lean.FVarId) (goals_1 : Array (Lean.MVarId × Array Lean.FVarId)),
  ({ depth := depth, commonFVarIds := commonFVarIds, goals := goals } =
      { depth := depth_1, commonFVarIds := commonFVarIds_1, goals := goals_1 }) =
    (depth = depth_1 ∧ commonFVarIds = commonFVarIds_1 ∧ goals = goals_1)
-- Mathlib.Order.Atoms
OrderIso.isAtomic_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] (f : α ≃o β), IsAtomic α ↔ IsAtomic β
-- Std.Data.ExtHashSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtHashSet.get? : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → α → Option α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.flip : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C},
  sq.IsPushout → sq.flip.IsPushout
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_inj : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} {f g : ι k →₀ M},
  f.embSigma = g.embSigma ↔ f = g
-- Std.Internal.Parsec.Basic
/-- Represents an error that can occur during parsing.
 -/
Std.Internal.Parsec.Error : Type
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- A choice of charts witnessing the local property `P` of `f` at `x`.  -/
Manifold.LiftSourceTargetPropertyAt.localPresentationAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              {P :
                                                  (M → N) →
                                                    OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} →
                                                Manifold.LiftSourceTargetPropertyAt I J n f x P →
                                                  Manifold.LocalPresentationAt I J n f x P
-- Mathlib.Topology.Inseparable
Filter.HasBasis.specializes_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set X},
  (nhds y).HasBasis p s → (x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i)
-- Aesop.Forward.Match.Types
Aesop.CompleteMatch.mk : Array Aesop.Match → Aesop.CompleteMatch
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A variant of `LeftHomotopy.compLeft` useful for dealing with homotopy equivalences.  -/
CategoryTheory.Arrow.LeftHomotopy.compLeftId : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f : v ⟶ v} →
          CategoryTheory.Arrow.LeftHomotopy f (CategoryTheory.CategoryStruct.id v) →
            (g : u ⟶ v) → CategoryTheory.Arrow.LeftHomotopy (CategoryTheory.CategoryStruct.comp g f) g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.ofList l cmp)[k]! = default
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M}, Continuous f → Continuous g → Continuous (f * g)
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.ι₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            (CategoryTheory.NonemptyParallelPairPresentationAux.F₁ f g P₁ P₂).comp CategoryTheory.yoneda ⟶
              (CategoryTheory.Functor.const (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂)).obj A
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap'_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] (h₁ : S₁.HomologyData)
  (h₂ : S₂.HomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂)
-- Std.Time.Duration
Std.Time.Duration.instLT : LT Std.Time.Duration
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.eq_1 : ∀ (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}),
  Ordinal.IsPrincipal op o = ∀ ⦃a b : Ordinal.{u_1}⦄, a < o → b < o → op a b < o
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `get_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.get_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α}
  {h : k ∈ Std.ExtDTreeMap.filterMap f t},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.filterMap f t) k h = (f k (Std.ExtDTreeMap.Const.get t k ⋯)).get ⋯
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.hadamard_self : ∀ {α : Type u_1} {V : Type u_2} [inst : MulZeroOneClass α] {A : Matrix V V α}, A.IsAdjMatrix → A.hadamard A = A
-- Mathlib.Data.Matrix.Block
/-- Extract a block from the diagonal of a block diagonal matrix.

This is the block form of `Matrix.diag`, and the left-inverse of `Matrix.blockDiagonal'`.  -/
Matrix.blockDiag' : {o : Type u_4} →
  {m' : o → Type u_7} →
    {n' : o → Type u_8} →
      {α : Type u_12} → Matrix ((i : o) × m' i) ((i : o) × n' i) α → (k : o) → Matrix (m' k) (n' k) α
-- Mathlib.Topology.Neighborhoods
frequently_frequently_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop},
  (∃ᶠ (x' : X) in nhds x, ∃ᶠ (x'' : X) in nhds x', p x'') ↔ ∃ᶠ (x : X) in nhds x, p x
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.subordinateOrthonormalBasis.congr_simp : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : RCLike 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) {inst_5 : DecidableEq ι} [inst_6 : DecidableEq ι] {V V_1 : ι → Submodule 𝕜 E}
  (e_V : V = V_1) (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
  DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV' = DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯
-- Mathlib.Probability.Distributions.Beta
/-- Measure defined by the beta distribution.  -/
ProbabilityTheory.betaMeasure : ℝ → ℝ → MeasureTheory.Measure ℝ
-- Mathlib.Topology.VectorBundle.Basic
VectorBundle.mk : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (trivialization_linear' :
    ∀ (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e],
      Bundle.Trivialization.IsLinear R e),
  (∀ (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : MemTrivializationAtlas e]
      [inst_10 : MemTrivializationAtlas e'],
      ContinuousOn (fun b => ↑(Bundle.Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)) →
    VectorBundle R F E
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonAssocSemiring : {R : Type u_1} → [NonAssocSemiring R] → NonAssocSemiring Rᵒᵈ
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.instProductive : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [Std.Iterators.Productive α m] {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)},
  Std.Iterators.Productive (Std.Iterators.Types.TakeWhile α m β P) m
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinearEquivRight'OfInv_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1)
  (hM'M : M' * M = 1) (a : m → R) (a_1 : n),
  (Matrix.toLinearEquivRight'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLinearMapRight' M) a a_1
-- Mathlib.Logic.Function.Basic
Function.Injective.hasLeftInverse : ∀ {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β}, Function.Injective f → Function.HasLeftInverse f
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Beck's comonadicity theorem. If `F` has a right adjoint and creates equalizers of `F`-cosplit pairs,
then it is comonadic.
This is the converse of `createsFSplitEqualizersOfComonadic`.
 -/
CategoryTheory.Comonad.comonadicOfCreatesFSplitEqualizers : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) → [CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair F] → CategoryTheory.ComonadicLeftAdjoint F
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.intCast_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : IntCast β] (n : ℤ)
  (x : α), ↑n x = ↑n
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_smul_eq : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R},
  IsUnit r → ∀ (x : M), R ∙ r • x = R ∙ x
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceOperator_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_4 : CompleteSpace E],
  MeasureTheory.MemLp id 2 μ → ∀ (x : E), (ProbabilityTheory.covarianceOperator μ) x = ∫ (y : E), inner ℝ x y • y ∂μ
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}, P ≤ CategoryTheory.MorphismProperty.sourceLocalClosure K P
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryGED t₁ k fallback = Std.DTreeMap.Const.getEntryGED t₂ k fallback
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.Subcomplex.mk''_I : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) [h : Topology.CWComplex C] (E : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [inst_1 : Topology.CWComplex E]
  (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ),
  (Topology.CWComplex.Subcomplex.mk'' C E I union).I n = I n
-- Lean.Util.Diff
/-- Invariant: the count is non-zero iff there is a saved index  -/
Lean.Diff.Histogram.Entry.leftWF : ∀ {α : Type u} {lsize rsize : ℕ} (self : Lean.Diff.Histogram.Entry α lsize rsize),
  self.leftCount = 0 ↔ self.leftIndex = none
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.split'.match_1.eq_1 : ∀ (motive : ONote × ℕ → Sort u_1) (a' : ONote) (m : ℕ) (h_1 : (a' : ONote) → (m : ℕ) → motive (a', m)),
  (match (a', m) with
    | (a', m) => h_1 a' m) =
    h_1 a' m
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.symm_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.symm.counitIso = e.unitIso.symm
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ n₁_1 : ℤ) (e_n₁ : n₁ = n₁_1)
  (hn₁ : n₀ + 1 = n₁), X.cyclesIsoH f n₀ n₁ hn₁ = X.cyclesIsoH f n₀ n₁_1 ⋯
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.mem_addUnits_of_val_mem_neg_val_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M}, ↑x ∈ S → ↑(-x) ∈ S → x ∈ S.addUnits
-- Mathlib.Data.Real.Basic
Real.mk_mul : ∀ {f g : CauSeq ℚ abs}, Real.mk (f * g) = Real.mk f * Real.mk g
-- Lean.Elab.Term.TermElabM
/-- Locates expressions that have level metavariables, calling `f` with the level metavariables exposed.
Gives entire applications to `f`.
 -/
Lean.Elab.Term.forEachExprWithExposedLevelMVars : Lean.Expr → (Lean.Expr → Lean.Elab.TermElabM Unit) → Lean.Elab.TermElabM Unit
-- Init.Data.Array.Lemmas
Array.foldlM_congr : ∀ {β : Type u_1} {α : Type u_2} {start start' stop stop' : ℕ} {m : Type u_1 → Type u_3} [inst : Monad m]
  {f g : β → α → m β} {b : β} {xs xs' : Array α},
  xs = xs' →
    (∀ (x : β) (y : α), f x y = g x y) →
      start = start' → stop = stop' → Array.foldlM f b xs start stop = Array.foldlM g b xs' start' stop'
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivWithinAt c c' s x → ∀ (d : 𝕜'), HasDerivWithinAt (fun x => c x / d) (c' / d) s x
-- Mathlib.Order.Lattice.Nat
Nat.iSup_of_not_bddAbove : ∀ {ι : Sort u_1} {f : ι → ℕ}, ¬BddAbove (Set.range f) → ⨆ i, f i = 0
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instPreservesFiniteLimitsEtaleOverForget : ∀ (X : AlgebraicGeometry.Scheme), CategoryTheory.Limits.PreservesFiniteLimits (AlgebraicGeometry.Scheme.Etale.forget X)