mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousOn
/-- A function is continuous at a point `x` if `x` is isolated.  -/
continuousAt_of_not_accPt_top : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  ¬AccPt x ⊤ → ContinuousAt f x
-- Std.Internal.UV.System
/-- Information about the OS.
 -/
Std.Internal.UV.System.UnameInfo : Type
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.condition_assoc : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C))
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {i j : J} (f : i ⟶ j) {Z : C}
  (h : (F.obj (Opposite.op i)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F i)
      (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F j)
      (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
iteratedFDeriv_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : F → G} {x : E} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n g (f x) →
    ContDiffAt 𝕜 n f x →
      ∀ {i : ℕ}, ↑i ≤ n → iteratedFDeriv 𝕜 i (g ∘ f) x = (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i
-- Init.Data.Float.Float
/-- Constructs a `Float` from a `Float.Model`.  -/
Float.ofModel : Float.Model → Float
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreFunctor_map_app_iso_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : CategoryTheory.Core (CategoryTheory.Functor C D)} (η : X ⟶ Y) (X_1 : CategoryTheory.Core C),
  (((CategoryTheory.coreFunctor C D).map η).app X_1).iso.hom = η.iso.hom.app X_1.of
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_injective : ∀ {α : Type u_1}, Function.Injective ⇑SymAlg.unsym
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsIntegralClosureInt : ∀ {K : Type u_1} [inst : Field K], IsIntegralClosure (NumberField.RingOfIntegers K) ℤ K
-- Mathlib.Logic.Embedding.Basic
/-- The embedding of `α` into the sum `α ⊕ β`.  -/
Function.Embedding.inl : {α : Type u_1} → {β : Type u_2} → α ↪ α ⊕ β
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K],
  (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_comap_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N),
  Subgroup.map f (Subgroup.comap f H) ≤ H
-- Mathlib.RingTheory.Jacobson.Ring
isJacobsonRing_quotient : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [IsJacobsonRing R], IsJacobsonRing (R ⧸ I)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_of_le_of_one_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, b ≤ c → 1 ≤ a → b ≤ c * a
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
/-- Given `motive : α → β → γ → Prop`, construct a proof of
`admissible (fun f => ∀ x y r, f x y = r → motive x y r)`
 -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.mkOptionAdm : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Basic
Semigroup.to_isAssociative : ∀ {α : Type u_1} [inst : Semigroup α], Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_I₀ : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X).I₀ = X.AffineZariskiSite
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- An element of the fundamental group, constructed from an arrow in the fundamental groupoid.  -/
FundamentalGroup.fromArrow : {X : Type u_1} → [inst : TopologicalSpace X] → {x : X} → ({ as := x } ⟶ { as := x }) → FundamentalGroup X x
-- Mathlib.Order.Interval.Multiset
Multiset.card_Ico_eq_card_Icc_sub_one : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Multiset.Ico a b).card = (Multiset.Icc a b).card - 1
-- Init.Meta.Defs
Lean.origin : String
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.mem_iInf : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} {S : ι → AddSubmonoid M} {x : M},
  x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Init.Grind.Interactive
/-- Show case-split candidates.  -/
Lean.Parser.Tactic.Grind.showCases : Lean.ParserDescr
-- Lean.Data.JsonRpc
/-- Error code indicating that a server received a notification or
request before the server has received the `initialize` request.  -/
Lean.JsonRpc.ErrorCode.serverNotInitialized : Lean.JsonRpc.ErrorCode
-- Mathlib.Algebra.Lie.IdealOperations
/-- Given a Lie module `M` over a Lie algebra `L`, the set of Lie ideals of `L` acts on the set
of submodules of `M`.  -/
LieSubmodule.hasBracket : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] → [inst_5 : LieAlgebra R L] → Bracket (LieIdeal R L) (LieSubmodule R L M)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toAddEquiv_linearEquiv : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  (WithLp.linearEquiv p K V).toAddEquiv = WithLp.addEquiv p V
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_tsub_cancel_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b : α}, AddLECancellable (b - a) → a ≤ b → b - (b - a) = a
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight'.eq_1 : ∀ {n m : ℕ} (a : BitVec n) (s : BitVec m), a.sshiftRight' s = a.sshiftRight s.toNat
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion_comp : ∀ {X : AlgebraicGeometry.Scheme} {I J K : X.IdealSheafData} (h₁ : I ≤ J) (h₂ : J ≤ K),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h₂)
      (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h₁) =
    AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- When an instance of `[HasDerivedCategory.{w'} C]` is available, this is the bijection
between `Ext.{w} X Y n` and a type of morphisms in the derived category.  -/
CategoryTheory.Abelian.Ext.homEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          [inst_3 : HasDerivedCategory C] →
            {n : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃
                CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X)
                  ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.mergeWith!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (mergeFn : α → β → β → β) (t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.mergeWith! mergeFn t₁ t₂ =
    Std.DTreeMap.Internal.Impl.foldl
      (fun t a b₂ =>
        Std.DTreeMap.Internal.Impl.Const.alter! a
          (fun x =>
            match x with
            | none => some b₂
            | some b₁ => some (mergeFn a b₁ b₂))
          t)
      t₁ t₂
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_sdiff_Ioc_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → Finset.Icc a b \ Finset.Ioc a b = {a}
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : M),
  (AlgebraicGeometry.StructureSheaf.toOpenₗ R M U) f = AlgebraicGeometry.StructureSheaf.const f 1 U ⋯
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst.instIsZeroOrProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.IsZeroOrProbabilityMeasure ρ],
  MeasureTheory.IsZeroOrProbabilityMeasure ρ.fst
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_one : Real.negMulLog 1 = 0
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.zero_smul_nonneg : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {g : Filter β},
  g.NeBot → 0 ≤ 0 • g
-- Mathlib.Analysis.Convex.Quasiconvex
quasilinearOn_iff_mem_uIcc : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasilinearOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ Set.uIcc (f x) (f y)
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Ico : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b r : K},
  0 < r → r • Set.Ico a b = Set.Ico (r * a) (r * b)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Construct a lax prefunctor from a map on objects, and prefunctors between the corresponding
hom types.  -/
CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors : {B : Type u₁} →
  [inst : Quiver B] →
    [inst_1 : (a b : B) → Quiver (a ⟶ b)] →
      {C : Type u₂} →
        [inst_2 : Quiver C] →
          [inst_3 : (a b : C) → Quiver (a ⟶ b)] →
            (F : B → C) → ((a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) → CategoryTheory.PrelaxFunctorStruct B C
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNNReal_natCast_add : ∀ (n : ℕ) (r : NNReal), ↑(↑n + r) = ↑n + ↑r
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.ihom_map : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X : (i : I) → C i) {Y Z : (i : I) → C i} (f : Y ⟶ Z) (i : I),
  (CategoryTheory.Pi.ihom X).map f i = (CategoryTheory.ihom (X i)).map (f i)
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.mapDomainAlgHom_apply : ∀ {G : Type u_2} [inst : Monoid G] (k : Type u_6) (A : Type u_7) [inst_1 : CommSemiring k] [inst_2 : Semiring A]
  [inst_3 : Algebra k A] {H : Type u_8} {F : Type u_9} [inst_4 : Monoid H] [inst_5 : FunLike F G H]
  [inst_6 : MonoidHomClass F G H] [inst_7 : MulSemiringAction G A] [inst_8 : MulSemiringAction H A]
  [inst_9 : SMulCommClass G k A] [inst_10 : SMulCommClass H k A] {f : F} (hf : ∀ (a : G) (x : A), a • x = f a • x)
  (a : SkewMonoidAlgebra A G),
  (SkewMonoidAlgebra.mapDomainAlgHom k A hf) a = a.sum fun a => SkewMonoidAlgebra.single (f a)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mk.sizeOf_spec : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : SizeOf K]
  [inst_4 : SizeOf L] (toSubalgebra : Subalgebra K L)
  (inv_mem' : ∀ x ∈ toSubalgebra.carrier, x⁻¹ ∈ toSubalgebra.carrier),
  sizeOf { toSubalgebra := toSubalgebra, inv_mem' := inv_mem' } = 1 + sizeOf toSubalgebra
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for division on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalDiv : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The category of factorisations of `f` as a monomorphism that is a quasi-isomorphism
in degrees `≤ n` followed by a degreewise epimorphism with an injective kernel.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → {K L : CochainComplex C ℤ} → (K ⟶ L) → ℤ → Type (max u_1 v_1)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_one_of_allZero : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  m.AllZero → Filter.Tendsto (m.toFun basis) Filter.atTop (nhds 1)
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
/-- The map `Nobeling.ι` is a closed embedding.  -/
Profinite.Nobeling.isClosedEmbedding : ∀ (S : Profinite), Topology.IsClosedEmbedding (Profinite.Nobeling.ι S)
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
_private.Mathlib.NumberTheory.TsumDivisorsAntidiagonal.0.summable_divisorsAntidiagonal_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜},
  ‖r‖ < 1 → Summable fun c => ↑(↑c.snd).2 ^ k * r ^ ((↑c.snd).1 * (↑c.snd).2)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divLeft_apply : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x b : G),
  (Homeomorph.divLeft x) b = x / b
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If a measure `μ` on the quotient `G ⧸ Γ` of a group `G` by a discrete normal subgroup `Γ` having
fundamental domain, satisfies `QuotientMeasureEqMeasurePreimage` relative to a standardized choice
of Haar measure on `G`, and assuming `μ` is finite, then `μ` is itself Haar.
TODO: Is it possible to drop the assumption that `μ` is finite?  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [LocallyCompactSpace G] [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ]
  [i : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν] [MeasureTheory.IsFiniteMeasure μ], μ.IsHaarMeasure
-- Aesop.Script.SScript
Aesop.Script.SScript.brecOn.eq : ∀ {motive : Aesop.Script.SScript → Sort u} (t : Aesop.Script.SScript)
  (F_1 : (t : Aesop.Script.SScript) → Aesop.Script.SScript.below t → motive t),
  Aesop.Script.SScript.brecOn t F_1 = F_1 t (Aesop.Script.SScript.brecOn.go t F_1).2
-- Mathlib.Topology.Subpath
Path.concat.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ} (p : Fin (n + 1) → X)
  (F : (k : Fin n) → Path (p k.castSucc) (p k.succ)),
  Path.concat p F = Fin.dfoldl n (fun i => Path (p 0) (p i)) (fun i ih => ih.trans (F i)) (Path.refl (p 0))
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initialMul_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X],
  (CategoryTheory.Limits.initialMul X).inv = CategoryTheory.Limits.initial.to ((⊥_ C) ⨯ X)
-- Init.Data.List.Pairwise
List.Pairwise.of_cons : ∀ {α : Type u_1} {a : α} {l : List α} {R : α → α → Prop}, List.Pairwise R (a :: l) → List.Pairwise R l
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mulSingle_mem_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] [inst_1 : DecidableEq ι] {I : Set ι}
  {S : (i : ι) → Submonoid (M i)} (i : ι) (x : M i), Pi.mulSingle i x ∈ Submonoid.pi I S ↔ i ∈ I → x ∈ S i
-- Mathlib.Order.SuccPred.Archimedean
StrictAnti.not_bddAbove_range_of_isSuccArchimedean : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [inst_2 : Preorder β] {f : α → β} [NoMinOrder α]
  [inst_4 : SuccOrder β] [IsSuccArchimedean β], StrictAnti f → ¬BddAbove (Set.range f)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.whiskerLeft_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))
  {M₂ M₃ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₂ ⟶ M₃) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁ f).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M₁.obj X) (f.app X)
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Iic : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α}, IsConnected (Set.Iic a)
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, then there is `S₁ : Solution` such that
`S₁.multiplicity = S'.multiplicity`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.exists_Solution_of_Solution' : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ∃ S₁, FermatLastTheoremForThreeGen.Solution.multiplicity✝ S₁ = FermatLastTheoremForThreeGen.Solution'.multiplicity✝ S'
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.CostructuredArrow.CreatesConnected.mapCone_raiseCone : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D}
  [inst_3 : CategoryTheory.IsConnected J] {B : D} {F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)}
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.CostructuredArrow.proj K B))),
  (CategoryTheory.CostructuredArrow.proj K B).mapCone (CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone c) =
    c
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_rightDistributor_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J)
  {Z : C} (h : (⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.restrictScalars_map : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  [inst_6 : SMul R R₂] [inst_7 : Module R₂ M] [inst_8 : Module R M₂] [inst_9 : IsScalarTower R R₂ M]
  [inst_10 : IsScalarTower R R₂ M₂] (f : M →ₗ[R₂] M₂) (M' : Submodule R₂ M),
  Submodule.restrictScalars R (Submodule.map f M') = Submodule.map (↑R f) (Submodule.restrictScalars R M')
-- Mathlib.Data.Finite.Sum
Finite.instSum : ∀ {α : Type u_1} {β : Type u_2} [Finite α] [Finite β], Finite (α ⊕ β)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.nsmul_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i) (i : ι),
  (b • v) i = b • v i
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hasLeftExtension_iff_of_iso₂ : ∀ {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]
  (L : CategoryTheory.Functor C D) {F F' : CategoryTheory.Functor C H} (iso₂ : F ≅ F'),
  L.HasLeftKanExtension F ↔ L.HasLeftKanExtension F'
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_apply_of_continuousOn : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R] {s : Set X}
  [inst_3 : Zero ↑s] {f : X → R} {g : ContinuousMapZero (↑s) R} {x : ↑s},
  ContinuousOn f s → f ↑0 = 0 → (ContinuousMapZero.mkD (s.domRestrict f) g) x = f ↑x
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.categoryAsType : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [CategoryTheory.FinCategory α] → CategoryTheory.SmallCategory (CategoryTheory.FinCategory.AsType α)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
/-- The map associating to two probability measures their product is a continuous map.  -/
MeasureTheory.ProbabilityMeasure.continuous_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [SecondCountableTopology α] [inst_5 : SecondCountableTopology β]
  [TopologicalSpace.PseudoMetrizableSpace α] [TopologicalSpace.PseudoMetrizableSpace β]
  [inst_8 : OpensMeasurableSpace α] [inst_9 : OpensMeasurableSpace β], Continuous fun μ => μ.1.prod μ.2
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- We have the bound `log (stirlingSeq n) - log (stirlingSeq (n+1)) ≤ 1 / (4 n ^ 2)`.  -/
Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ : ∀ (n : ℕ), Real.log (Stirling.stirlingSeq n) - Real.log (Stirling.stirlingSeq (n + 1)) ≤ 1 / (4 * ↑n ^ 2)
-- Mathlib.Topology.Constructions
ULift.isClosed_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (ULift.{v, u} X)}, IsClosed s ↔ IsClosed (ULift.up ⁻¹' s)
-- Init.Data.List.Basic
List.filterMap_cons : ∀ {α : Type u} {β : Type v} {f : α → Option β} {a : α} {l : List α},
  List.filterMap f (a :: l) =
    match f a with
    | none => List.filterMap f l
    | some b => b :: List.filterMap f l
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkAndCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (input : aig.BinaryInput)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkAndCached input).aig.decls.size},
  (aig.mkAndCached input).aig.decls[idx] = aig.decls[idx]
-- Init.Prelude
/-- Create array `#[a₁, a₂, a₃]`  -/
Array.mkArray3 : {α : Type u} → α → α → α → Array α
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_add_eq_mk_left : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a < ArchimedeanClass.mk b → ArchimedeanClass.mk (a + b) = ArchimedeanClass.mk a
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (x : CategoryTheory.LocallyDiscrete Cᵒᵖ)
  (X : CategoryTheory.Sheaf (J.over (Opposite.unop x.as)) A) (X_1 : (CategoryTheory.Over (Opposite.unop x.as))ᵒᵖ),
  (((J.pseudofunctorOver A).mapId x).hom.toNatTrans.app X).hom.app X_1 =
    X.obj.map ((CategoryTheory.Over.mapId (Opposite.unop x.as)).inv.app (Opposite.unop X_1)).op
-- Mathlib.Order.Defs.LinearOrder
lt_trichotomy : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), a < b ∨ a = b ∨ b < a
-- Mathlib.Topology.Constructions.SumProd
Topology.IsInducing.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  Topology.IsInducing f → Topology.IsInducing g → Topology.IsInducing (Prod.map f g)