mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffOn_symm : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e],
  ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑e.symm) e.target
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.mk' S).mapComp f g = S.mapComp f g
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the degree of `v` in `G` is at most the size of
`t`.  -/
SimpleGraph.isBipartiteWith_degree_le : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)],
  G.IsBipartiteWith ↑s ↑t → v ∈ s → G.degree v ≤ t.card
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
addConj_addCommutatorElement_right_addCommutatorElement_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G),
  b + ⁅a, ⁅-b, c⁆⁆ + -b + c + ⁅b, ⁅-c, a⁆⁆ + -c + a + ⁅c, ⁅-a, b⁆⁆ + -a = 0
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.quotientTensorEquiv_apply_tmul : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : CommRing A] [inst_6 : Algebra R A]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (I : Ideal A) (a : A) (t : T),
  (Algebra.TensorProduct.quotientTensorEquiv S T A I) ((Ideal.Quotient.mk I) a ⊗ₜ[R] t) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap A (TensorProduct R A T)) I)) (a ⊗ₜ[R] t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {fallback : β k} {f : β k → β k}, (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.instEpiFunctorWhiskerRightOfPreservesEpimorphisms : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {D : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} D] {F G : CategoryTheory.Functor K C} (f : F ⟶ G)
  [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Epi f] (H : CategoryTheory.Functor C D)
  [H.PreservesEpimorphisms], CategoryTheory.Epi (CategoryTheory.Functor.whiskerRight f H)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc : ∀ {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₄], ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertMany_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β},
  Std.DHashMap.Const.insertMany m [] = m
-- Mathlib.Topology.Sheaves.SheafOfFunctions
/-- The sheaf of not-necessarily-continuous functions on `X` with values in type family
`T : X → Type u`.
 -/
TopCat.sheafToTypes : (X : TopCat) → (↑X → Type u_1) → TopCat.Sheaf (Type (max u_2 u_1)) X
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f],
  CategoryTheory.ChosenPullbacksAlong.pullback f = CategoryTheory.Over.pullback f
-- Mathlib.Algebra.Quandle
Rack.involutory_invAct_eq_act : ∀ {R : Type u_2} [inst : Rack R], Rack.IsInvolutory R → ∀ (x y : R), Rack.invAct x y = Shelf.act x y
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.free : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {V : Type u_3}
  [inst_3 : AddCommMonoid V] [inst_4 : Module R V] {W : Type u_4} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module S W] [inst_8 : IsScalarTower R S W] {ε : V →ₗ[R] W},
  IsBaseChange S ε → ∀ [Module.Free R V], Module.Free S W
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
/-- The algebra morphism from a tensor product of a polynomial algebra
by an algebra to a polynomial algebra  -/
MvPolynomial.rTensorAlgEquiv : {R : Type u} →
  {N : Type v} →
    [inst : CommSemiring R] →
      {σ : Type u_1} →
        {S : Type u_3} →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommSemiring N] →
                [inst_4 : Algebra R N] → TensorProduct R S (MvPolynomial σ N) ≃ₐ[S] MvPolynomial σ (TensorProduct R S N)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Unicity of `lift`: a map that agrees on `R` and `h.root` agrees with `lift` everywhere.  -/
IsAdjoinRoot.eq_lift : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
  (g : S →+* T), (∀ (a : R), g ((algebraMap R S) a) = i a) → g h.root = x → g = h.lift i x hx
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} {x y : sq.LiftStruct}, x = y ↔ x.l = y.l
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The inverse Fourier transform satisfies `∫ 𝓕⁻ f • g = ∫ f • 𝓕⁻ g`, i.e., it is self-adjoint.  -/
SchwartzMap.integral_fourierInv_smul_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] [CompleteSpace F] (f : SchwartzMap V ℂ) (g : SchwartzMap V F),
  ∫ (ξ : V), (FourierTransformInv.fourierInv f) ξ • g ξ = ∫ (x : V), f x • (FourierTransformInv.fourierInv g) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.snd_eq_getValueCast_of_getEntry?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  {y : (a : α) × β a} (h : Std.Internal.List.getEntry? k l = some y),
  y.snd = cast ⋯ (Std.Internal.List.getValueCast k l ⋯)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- The family of 2-morphisms out of an absolute left Kan lift.  -/
CategoryTheory.Bicategory.LeftLift.IsAbsKan.desc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.LeftLift f g} →
            t.IsAbsKan →
              {x : B} →
                {h : x ⟶ c} →
                  (s : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp h g)) →
                    CategoryTheory.CategoryStruct.comp h t.lift ⟶ s.lift
-- Mathlib.Geometry.Diffeology.Basic
/-- **Alias** of `DiffeologicalSpace.dTopology`.

---

The D-topology of the diffeology. This is included as part of the data in order to give
control over what the D-topology is defeq to. See also note [forgetful inheritance].  -/
Diffeology.dTopology : {X : Type u_1} → [self : DiffeologicalSpace X] → TopologicalSpace X
-- Std.Async.Basic
/-- Constructs an `Task` from a `MaybeTask`.
 -/
Std.Async.MaybeTask.toTask : {α : Type} → Std.Async.MaybeTask α → Task α
-- Mathlib.Order.InitialSeg
PrincipalSeg.le_iff_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a a' : α} [inst_1 : PartialOrder α] (f : α <i β),
  f.toRelEmbedding a ≤ f.toRelEmbedding a' ↔ a ≤ a'
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_add : ∀ {α : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [inst_5 : LocallyFiniteOrder α] (f : α → M) (a b c : α),
  ∏ x ∈ Finset.Ico a b, f (c + x) = ∏ x ∈ Finset.Ico (a + c) (b + c), f x
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- A function `f` is differentiable at a point `x` within a set `s` if it admits a derivative
there (possibly non-unique).  -/
DifferentiableWithinAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [Module 𝕜 E] →
          [TopologicalSpace E] →
            {F : Type u_3} →
              [inst_4 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (E → F) → Set E → E → Prop
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.coeff.eq_1 : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ), p.coeff n = (p n) 1
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Set.initialSegIicIicOfLE.congr_simp : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (h : i ≤ j), Set.initialSegIicIicOfLE h = Set.initialSegIicIicOfLE h
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.pow : ∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → γ},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun x => f x ^ g x) μ
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey : ∀ {numVarsSucc : ℕ} (self : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ self.clause ∨ (l, false) ∉ self.clause
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
  (hg₂ : S₂.g = 0), (CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Evaluation on a particular element of the module `M` is an additive map on quadratic maps.  -/
QuadraticMap.evalAddMonoidHom : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → M → QuadraticMap R M N →+ N
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {z : M} {F' : Type u_21} [inst_6 : NormedField F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'} {p' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt% p z p' → p z ≠ 0 → HasMFDerivAt% p⁻¹ z (-(p z ^ 2)⁻¹ • p')
-- Mathlib.Order.Category.Lat
_private.Mathlib.Order.Category.Lat.0.Lat.Hom.mk : {X Y : Lat} → LatticeHom ↑X ↑Y → X.Hom Y
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestFirst.go : Array (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) → ℕ → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- When `D` is a braided monoidal category,
commutative monoid objects in `C ⥤ D` are the same thing
as functors from `C` into the commutative monoid objects of `D`.
 -/
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [inst_3 : CategoryTheory.BraidedCategory D] →
            CategoryTheory.CommMon (CategoryTheory.Functor C D) ≌ CategoryTheory.Functor C (CategoryTheory.CommMon D)
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
exists_retractionCantorSet : ∀ {X : Set (ℕ → Bool)}, IsClosed X → X.Nonempty → ∃ f, Continuous f ∧ Set.range f = X
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.continuous_toLinearMap : ∀ {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₂] (f : M₁ →SL[σ₁₂] M₂), Continuous ⇑↑f
-- Mathlib.Probability.Distributions.Fernique
StrictMono.exists_between_of_tendsto_atTop : ∀ {β : Type u_1} [inst : LinearOrder β] {t : ℕ → β},
  StrictMono t → Filter.Tendsto t Filter.atTop Filter.atTop → ∀ {x : β}, t 0 < x → ∃ n, t n < x ∧ x ≤ t (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g)
  (e : Z ⟶ X) (he : CategoryTheory.CategoryStruct.comp e f = 0) {Z_1 : C} (h_1 : CategoryTheory.Limits.kernel g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f e he)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelIsoOfEq h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g e ⋯) h_1
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instTransOrdSpan : Std.TransOrd Std.Time.Nanosecond.Span
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.compL_apply : ∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ] (f : Fₗ →L[𝕜] Gₗ) (g : E →L[𝕜] Fₗ),
  ((ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ) f) g = f ∘SL g
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.mono_left : ∀ {X : Type u_1} {R S : SetRel X X} {s : Set X}, R ⊆ S → S.IsSeparated s → R.IsSeparated s