mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_counit_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (U : CategoryTheory.Over Y),
  ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.inv).counit.app U).left =
    CategoryTheory.CategoryStruct.id U.left
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_powerset_sdiff_elem : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∈ s →
      ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
        (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapLeft_prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  (γ : Type u_5) {x : MeasurableSpace γ},
  (ProbabilityTheory.Kernel.prodMkRight γ κ).swapLeft = ProbabilityTheory.Kernel.prodMkLeft γ κ
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.bound_of_isBigO_nat_atTop : ∀ {E : Type u_3} {E'' : Type u_9} [inst : Norm E] [inst_1 : NormedAddCommGroup E''] {f : ℕ → E} {g'' : ℕ → E''},
  f =O[Filter.atTop] g'' → ∃ C > 0, ∀ ⦃x : ℕ⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- If `f` is a closed immersion with affine target, the source is affine and
the induced map on global sections is surjective.  -/
AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.IsAffine X ∧
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Mathlib.Data.Finsupp.Defs
Finsupp.mem_support_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α →₀ M} {a : α}, a ∈ f.support ↔ f a ≠ 0
-- Init.Data.Ord.Basic
Ordering.isLT_gt : Ordering.gt.isLT = false
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.rightInverse_rightInverse : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} (h : f.HasRightInverse), Function.RightInverse ⇑h.rightInverse ⇑f
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.trans_isBigO : ∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f g₁ : α → β} {g₂ : α → β₂}, Asymptotics.IsEquivalent l f g₁ → g₁ =O[l] g₂ → f =O[l] g₂
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_sup_eq_top : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ}, I ⊔ J = ⊤ → I ^ n ⊔ J = ⊤
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.norm_setToL1_le_mul_norm : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  0 ≤ C → ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), ‖(MeasureTheory.L1.setToL1 hT) f‖ ≤ C * ‖f‖
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitFlipIsoCompColim_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K),
  (CategoryTheory.Limits.colimitFlipIsoCompColim F).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (app a) (G.map f) ⟶
                      CategoryTheory.CategoryStruct.comp (F.map f) (app b)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (naturality f)
                        (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η))
                        (naturality g))
                  CategoryTheory.Oplax.LaxTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a))
                          (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a)) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
                            (CategoryTheory.Bicategory.leftUnitor (app a)).inv))
                    CategoryTheory.Oplax.LaxTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g))
                            (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                                    (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv)))))
                      CategoryTheory.Oplax.LaxTrans.naturality_comp._autoParam →
                    CategoryTheory.Oplax.LaxTrans F G
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommRingCat.FilteredColimits.nontrivial : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  [CategoryTheory.IsFilteredOrEmpty J] [∀ (i : J), Nontrivial ↑(F.obj i)] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c), Nontrivial ↑c.pt
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_generate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (R : CategoryTheory.Presieve Y),
  (CategoryTheory.Sieve.overEquiv Y) (CategoryTheory.Sieve.generate R) =
    CategoryTheory.Sieve.generate (CategoryTheory.Presieve.functorPushforward (CategoryTheory.Over.forget X) R)
-- Mathlib.Data.List.Sublists
List.revzip.eq_1 : ∀ {α : Type u_1} (l : List α), l.revzip = l.zip l.reverse
-- Mathlib.Topology.NhdsWithin
nhdsWithin_restrict' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} (s : Set α) {t : Set α},
  t ∈ nhds a → nhdsWithin a s = nhdsWithin a (s ∩ t)
-- Mathlib.Control.Monad.Cont
MonadCont.Label.mk.sizeOf_spec : ∀ {α : Type w} {m : Type u → Type v} {β : Type u} [inst : SizeOf α] [inst_1 : (a : Type u) → SizeOf (m a)]
  [inst_2 : SizeOf β] (apply : α → m β), sizeOf { apply := apply } = 1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
NNDist.mk : {α : Type u_3} → (α → α → NNReal) → NNDist α
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropWhile_eq_dropWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.dropWhile pat = s.toSlice.dropWhile pat
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_inj : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
  G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Combining all `HahnEmbedding.Seed.coeff` as
a partial linear map from `HahnEmbedding.Seed.baseDomain` to `HahnSeries`.  -/
HahnEmbedding.Seed.baseEmbedding : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              HahnEmbedding.Seed K M R → M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.left_notMem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → x ∉ s
-- Mathlib.Order.Ideal
Order.Ideal.top_mem_iff_eq_top : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderTop P] {I : Order.Ideal P}, ⊤ ∈ I ↔ I = ⊤
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
/-- the canonical `MorphComponents` whose associated morphism is the identity
(see `F_id`) thanks to `decomposition_Q n (n+1)`  -/
AlgebraicTopology.DoldKan.MorphComponents.id : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      (X : CategoryTheory.SimplicialObject C) →
        (n : ℕ) → AlgebraicTopology.DoldKan.MorphComponents X n (X.obj (Opposite.op { len := n + 1 }))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_zero`. -/
ContinuousLinearMap.coe_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂], ↑0 = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toLaxFunctor : CategoryTheory.LaxFunctor B C)
  (map_id :
    autoParam
      (∀ (X : B),
        toLaxFunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toLaxFunctor.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam)
  (mapId_eq_eqToHom :
    autoParam (∀ (X : B), toLaxFunctor.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam),
  sizeOf { toLaxFunctor := toLaxFunctor, map_id := map_id, mapId_eq_eqToHom := mapId_eq_eqToHom } =
    1 + sizeOf toLaxFunctor
-- Mathlib.Order.Filter.Partial
/-- Generic "limit of a partial function" predicate. `PTendsto' r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `p`-preimage of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to partial functions.  -/
Filter.PTendsto' : {α : Type u} → {β : Type v} → (α →. β) → Filter α → Filter β → Prop
-- Mathlib.RingTheory.Bialgebra.Quotient
/-- The bialgebra structure on `A ⧸ I` when `I` is a biideal.  -/
Bialgebra.Quotient.instQuotientIdeal : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Bialgebra R A] →
          (I : Ideal A) → [inst_3 : I.IsTwoSided] → [(Submodule.restrictScalars R I).IsCoideal] → Bialgebra R (A ⧸ I)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.reverse.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.reverse = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Data.List.Pairwise
List.pairwise_replicate_of_refl : ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {n : ℕ} [Std.Refl R], List.Pairwise R (List.replicate n a)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} →
      {p₁ p₂ : R ⟶ X} →
        CategoryTheory.ReflexiveRelation p₁ p₂ →
          (s : R ⟶ R) →
            autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂)
                CategoryTheory.SymmetricRelation.symmetry₁._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁)
                  CategoryTheory.SymmetricRelation.symmetry₂._autoParam →
                (c : CategoryTheory.Limits.PullbackCone p₂ p₁) →
                  CategoryTheory.Limits.IsLimit c →
                    (t : c.pt ⟶ R) →
                      autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
                          CategoryTheory.TransitiveRelation.transitivity₁._autoParam →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
                            CategoryTheory.TransitiveRelation.transitivity₂._autoParam →
                          CategoryTheory.EquivalenceRelation p₁ p₂
-- Mathlib.Algebra.Module.PointwisePi
vadd_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : AddGroup K] [inst_1 : (i : ι) → AddAction K (R i)] (r : K)
  (S : Set ι) (t : (i : ι) → Set (R i)), r +ᵥ S.pi t = S.pi (r +ᵥ t)
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.toComposition.eq_1 : ∀ {n : ℕ} (c : CompositionAsSet n), c.toComposition = { blocks := c.blocks, blocks_pos := ⋯, blocks_sum := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.unitOfList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {hd : α} {tl : List α},
  Std.ExtDHashMap.Const.unitOfList (hd :: tl) = Std.ExtDHashMap.Const.insertManyIfNewUnit (∅.insertIfNew hd ()) tl
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_le_iff_le_comap : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubsemiring R}
  {t : NonUnitalSubsemiring S}, NonUnitalSubsemiring.map f s ≤ t ↔ s ≤ NonUnitalSubsemiring.comap f t
-- Mathlib.Topology.MetricSpace.Completion
Isometry.completion_map : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → Isometry (UniformSpace.Completion.map f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_eq_false_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = true → t.isEmpty = false
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.attachLift.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} [inst : MonadAttach m] (x : m α),
  Std.Iterators.PostconditionT.attachLift x = { Property := MonadAttach.CanReturn x, operation := MonadAttach.attach x }
-- Mathlib.Order.SupClosed
/-- The semilattice generated by a finite set is finite.  -/
Set.Finite.supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, s.Finite → (supClosure s).Finite
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).obj X).hom = X.left.hom
-- Mathlib.Topology.Separation.Regular
/-- `ConnectedComponents X` is Hausdorff when `X` is Hausdorff and compact  -/
ConnectedComponents.t2 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X], T2Space (ConnectedComponents X)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv_eq.match_1.splitter : (motive : Bool → Bool → Sort u_1) →
  (x x_1 : Bool) →
    (Unit → motive false false) →
      (Unit → motive false true) → (Unit → motive true false) → (Unit → motive true true) → motive x x_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive false) (h_2 : Unit → motive true),
  (match false with
    | false => h_1 ()
    | true => h_2 ()) =
    h_1 ()
-- Init.Data.SInt.Lemmas
Int32.instIsLinearOrder : Std.IsLinearOrder Int32
-- Mathlib.Algebra.Category.FGModuleCat.Basic
LinearMap.comp_id_fgModuleCat : ∀ {R : Type u_1} [inst : Ring R] {G : FGModuleCat R} {H : Type v} [inst_1 : AddCommGroup H] [inst_2 : Module R H]
  (f : ↑G →ₗ[R] H), f ∘ₗ ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id G).hom = f
-- Mathlib.Topology.VectorBundle.Hom
/-- The continuous `σ`-semilinear maps between two topological vector bundles form a
`VectorPrebundle` (this is an auxiliary construction for the
`VectorBundle` instance, in which the pretrivializations are collated but no topology
on the total space is yet provided).  -/
Bundle.ContinuousLinearMap.vectorPrebundle : {𝕜₁ : Type u_1} →
  [inst : NontriviallyNormedField 𝕜₁] →
    {𝕜₂ : Type u_2} →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {B : Type u_3} →
            (F₁ : Type u_4) →
              [inst_2 : NormedAddCommGroup F₁] →
                [inst_3 : NormedSpace 𝕜₁ F₁] →
                  (E₁ : B → Type u_5) →
                    [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)] →
                        [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          (F₂ : Type u_6) →
                            [inst_7 : NormedAddCommGroup F₂] →
                              [inst_8 : NormedSpace 𝕜₂ F₂] →
                                (E₂ : B → Type u_7) →
                                  [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                    [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] →
                                      [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                        [inst_12 : TopologicalSpace B] →
                                          [inst_13 : (x : B) → TopologicalSpace (E₁ x)] →
                                            [inst_14 : FiberBundle F₁ E₁] →
                                              [VectorBundle 𝕜₁ F₁ E₁] →
                                                [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                  [inst_17 : FiberBundle F₂ E₂] →
                                                    [VectorBundle 𝕜₂ F₂ E₂] →
                                                      [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                        [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] →
                                                          [inst_21 : RingHomIsometric σ] →
                                                            VectorPrebundle 𝕜₂ (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : AddMonoid A] [inst_1 : GroupWithZero G₀] [inst_2 : DistribMulAction G₀ A]
  {S T : AddSubmonoid A} {a : G₀}, a ≠ 0 → (a • S ≤ a • T ↔ S ≤ T)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] [inst : Inhabited α],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t = true → t.getKey! k = k
-- Mathlib.Algebra.Order.Field.Basic
mul_self_inj_of_nonneg : ∀ {α : Type u_4} [inst : CommRing α] [NoZeroDivisors α] [inst_2 : PartialOrder α] [IsStrictOrderedRing α] {a b : α},
  0 ≤ a → 0 ≤ b → (a * a = b * b ↔ a = b)
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Pred.0.String.Slice.Pattern.Model.split.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (pos : s.Pos) → none = some pos → motive (some pos))
  (h_2 : none = none → motive none),
  (match hd : none with
    | some pos => h_1 pos hd
    | none => h_2 hd) =
    h_2 ⋯
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.copy_eq : ∀ {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (neg : α) (hi : neg = ↑(-u)),
  u.copy val hv neg hi = u
-- Mathlib.Algebra.Lie.Ideal
/-- Transfer the `LieAlgebra` instance from the coercion `LieIdeal → LieSubalgebra`.  -/
LieIdeal.lieAlgebra : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → LieAlgebra R ↥I
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.mem_resolventSet_of_norm_lt_mul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {k : 𝕜}, ‖a‖ * ‖1‖ < ‖k‖ → k ∈ resolventSet 𝕜 a
-- Batteries.Control.LawfulMonadState
/-- Class for well behaved state monads, extending the base `MonadState` type.
Requires that `modifyGet` is equal to the same definition with only `get` and `set`,
that `get` is idempotent if the result isn't used, and that `get` after `set` returns
exactly the value that was previously `set`.  -/
LawfulMonadStateOf : (σ : semiOutParam (Type u_1)) → (m : Type u_1 → Type u_2) → [Monad m] → [MonadStateOf σ m] → Prop
-- Mathlib.Data.Seq.Computation
Computation.of_think_terminates : ∀ {α : Type u} {s : Computation α}, s.think.Terminates → s.Terminates
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_zero : Real.arctan 0 = 0
-- Mathlib.CategoryTheory.Join.Basic
/-- The canonical inclusion from D to `C ⋆ D`.
Terms of the form `(inclRight C D).map f` should be treated as primitive when working with joins
and one should avoid trying to reduce them. For this reason, there is no `inclRight_map` simp
lemma.  -/
CategoryTheory.Join.inclRight : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D (CategoryTheory.Join C D)
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_bernoulli : ∀ {p : NNReal} (h : p ≤ 1), (PMF.bernoulli p h).support = {b | bif b then p ≠ 0 else p ≠ 1}