mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.hom_inv_whiskerRight_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) (k : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.hom h) k)
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.inv h) k) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) k)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α}, (Std.TreeMap.map f t)[k]? = Option.map (f k) t[k]?
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
          h))
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `shrinkCoyoneda` is compatible with `uliftFunctor`.  -/
CategoryTheory.shrinkCoyonedaUliftFunctorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.LocallySmall.{max w w', v, u} C] →
        CategoryTheory.shrinkCoyoneda.{w, v, u}.comp
            ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj
              CategoryTheory.uliftFunctor.{w', w}) ≅
          CategoryTheory.shrinkCoyoneda.{max w w', v, u}
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  Topology.IsQuotientMap f →
    ∀ [inst_2 : AddGroup E] [IsTopologicalAddGroup E] (G : AddSubgroup E),
      IsDiscrete ↑G → (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ + -e₁ ∈ G) → IsAddQuotientCoveringMap f ↥G
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeCommRing : ∀ (α : Type u_1), Infinite (FreeCommRing α)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_sup : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] {s t : ClosedSubmodule R N}
  {x : N}, x ∈ s ⊔ t ↔ x ∈ closure (↑s ⊔ ↑t).carrier
-- Init.Data.Float.Float
/-- Computes the sine of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`sin`.
 -/
Float.sin : Float → Float
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.δ_one_toSSetObjI : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) SSet.stdSimplex.toSSetObjI =
  SSet.const (TopCat.toSSetObj₀Equiv.symm 0)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj φ.Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (φ.map L hL) (CategoryTheory.CategoryStruct.comp (L.map φ.s) h) =
    CategoryTheory.CategoryStruct.comp (L.map φ.f) h
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be uniformly approximated by functions which are uniformly continuous on a
set is uniformly continuous on this set.  -/
uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  (∀ u ∈ uniformity β, ∃ F, UniformContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) → UniformContinuousOn f s
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.comp_of_map : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε},
  MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) → AEMeasurable f μ → MeasureTheory.MemLp (g ∘ f) p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.eqToHom_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {j j' : J} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.Sigma.ι f j') =
    CategoryTheory.Limits.Sigma.ι f j
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_max_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.cthickening (max 0 δ) E = Metric.cthickening δ E
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.findLeadingSpacesSize.findNextLine : {s : String} → s.Pos → ℕ → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Composition of graph isomorphisms.  -/
SimpleGraph.Iso.comp : {V : Type u_1} →
  {W : Type u_2} →
    {X : Type u_3} → {G : SimpleGraph V} → {G' : SimpleGraph W} → {G'' : SimpleGraph X} → G' ≃g G'' → G ≃g G' → G ≃g G''
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {S : Submonoid R} {f : M →ₗ[R] M'},
  (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)) →
    (∀ (y : M'), ∃ x, x.2 • y = f x.1) → (∀ {x₁ x₂ : M}, f x₁ = f x₂ → ∃ c, c • x₁ = c • x₂) → IsLocalizedModule S f
-- Std.Async.Basic
/-- Sequences two computations, allowing the second to depend on the value computed by the first.
 -/
Std.Async.MaybeTask.bind : {α β : Type} →
  Std.Async.MaybeTask α →
    (α → Std.Async.MaybeTask β) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.MaybeTask β
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The arrow `(G →₀ A) --d₁₀--> A` is isomorphic to the differential
`(inhomogeneousChains A).d 1 0` of the complex of inhomogeneous chains of `A`.  -/
groupHomology.d₁₀ArrowIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        CategoryTheory.Arrow.mk ((groupHomology.inhomogeneousChains A).d 1 0) ≅
          CategoryTheory.Arrow.mk (groupHomology.d₁₀ A)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mkLinearMap_apply : ∀ {R : Type u} [inst : CommSemiring R] (S : Submonoid R) (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (m : M), (LocalizedModule.mkLinearMap S M) m = LocalizedModule.mk m 1
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_eq_card_nsmul : ∀ {α : Type u_3} [inst : AddMonoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise AddCommute) (m : α),
  (∀ x ∈ s, x = m) → s.noncommSum comm = s.card • m
-- Mathlib.Control.Monad.Cont
instLawfulMonadContStateT : ∀ {m : Type u → Type v} {σ : Type u} [inst : Monad m] [inst_1 : MonadCont m] [LawfulMonadCont m],
  LawfulMonadCont (StateT σ m)
-- Init.Data.SInt.Lemmas
ISize.ofIntClamp_bitVecToInt : ∀ (n : BitVec System.Platform.numBits), ISize.ofIntClamp n.toInt = ISize.ofBitVec n
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformly.hasSumUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  SummableUniformly f → HasSumUniformly f fun x => ∑' (i : ι), f i x
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeqSet.eq_1 : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p : α → (ι → β) → Prop),
  aeSeqSet hf p =
    (MeasureTheory.toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ)ᶜ
-- Mathlib.Data.Matrix.Reflection
/-- `dotProduct` with better defeq for `Fin`  -/
Matrix.dotProductᵣ : {α : Type u_1} → [Mul α] → [Add α] → [Zero α] → {m : ℕ} → (Fin m → α) → (Fin m → α) → α
-- Mathlib.Algebra.Order.Monoid.Units
Units.compare_val : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Ord α] (a b : αˣ), compare ↑a ↑b = compare a b
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.RightAdjoint.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {left : a ⟶ b} {right : b ⟶ a}
  {adj : CategoryTheory.Bicategory.Adjunction left right} {right_1 : b ⟶ a}
  {adj_1 : CategoryTheory.Bicategory.Adjunction left right_1},
  { right := right, adj := adj } = { right := right_1, adj := adj_1 } → right = right_1 ∧ adj ≍ adj_1
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- The category of open sets contained in some element of the cover.
 -/
TopCat.Presheaf.SheafCondition.OpensLeCover : {X : TopCat} → {ι : Type u_2} → (ι → TopologicalSpace.Opens ↑X) → Type w
-- Mathlib.Geometry.Manifold.Algebra.Monoid
smoothLeftMul_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G' : Type u_8}
  [inst_4 : Monoid G'] [inst_5 : TopologicalSpace G'] [inst_6 : ChartedSpace H G'] [inst_7 : ContMDiffMul I (↑⊤) G']
  (g' : G'), (smoothLeftMul I g') 1 = g'
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.mem_adjoint_domain_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F)
  [inst_5 : CompleteSpace E] (y : F), y ∈ T.adjoint.domain ↔ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `antilipschitzWith_inv_iff`. -/
AntilipschitzWith.of_inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E},
  AntilipschitzWith K f⁻¹ → AntilipschitzWith K f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex : ∀ (K : Type u_1) [inst : Field K] (x : K) (w : { w // w.IsComplex }),
  ((NumberField.mixedEmbedding K) x).2 w = (↑w).embedding x
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- Given two functors `F₁` and `F₂` from a category `J` to a `V`-enriched
ordinary category `C`, this is the diagram `Jᵒᵖ ⥤ J ⥤ V` whose end shall be
the `V`-morphisms in `J ⥤ V` from `F₁` to `F₂`.  -/
CategoryTheory.Enriched.FunctorCategory.diagram : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [CategoryTheory.EnrichedOrdinaryCategory V C] →
                CategoryTheory.Functor J C →
                  CategoryTheory.Functor J C → CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J V)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (∀ a ∈ m, l.contains a = false) → (m.insertManyIfNewUnit l).size = m.size + l.length
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).m = c.m
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.succ_mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo a : α}, Std.PRange.succ a ∈ (Std.PRange.succ lo)...* ↔ a ∈ lo...*
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_inj : ∀ {M : Type u_2} [inst : AddZeroClass M] {S T : AddSubmonoid M}, S.op = T.op ↔ S = T
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalInterior_union_fundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  MeasureTheory.fundamentalInterior G s ∪ MeasureTheory.fundamentalFrontier G s = s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderiv_ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → fderiv ℂ (fun x => Complex.cos (f x)) x = -Complex.sin (f x) • fderiv ℂ f x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (Std.ExtDHashMap.ofList l).get! k' = cast ⋯ v
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- If `G` acts freely on `X`, `X` is equivalent
to the product of the quotient of `X` by `G` and `G`.
See `AddAction.selfEquivOrbitsQuotientProd` with `φ = Quotient.out`.  -/
AddAction.selfEquivOrbitsQuotientProd' : {G : Type u} →
  {X : Type v} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        {φ : Quotient (AddAction.orbitRel G X) → X} →
          Function.LeftInverse Quotient.mk'' φ →
            (∀ (b : X), AddAction.stabilizer G b = ⊥) → X ≃ Quotient (AddAction.orbitRel G X) × G
-- Lean.Parser.Term
Lean.Parser.Term.throwNamedErrorMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
/-- The `MeasurableSpace` of sets which are measurable with respect to a given σ-algebra `m`
on `α`, modulo a given σ-filter `l` on `α`.  -/
eventuallyMeasurableSpace : {α : Type u_1} → MeasurableSpace α → (l : Filter α) → [CountableInterFilter l] → MeasurableSpace α
-- Mathlib.Algebra.Tropical.Basic
Tropical.injective_trop : ∀ {R : Type u}, Function.Injective Tropical.trop
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.eval_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ) (f : AdicCompletion I M), (AdicCompletion.eval I M n) f = ↑f n
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.property : ∀ {𝕜 : 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}
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), P f h.domChart h.codChart
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- If the image under the norm is zero, then the argument is zero.  -/
NonarchAddGroupNorm.eq_zero_of_map_eq_zero' : ∀ {G : Type u_6} [inst : AddGroup G] (self : NonarchAddGroupNorm G) (x : G), self.toFun x = 0 → x = 0
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_take_le : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} {i : ℕ} (h : List.take i xs ≠ []), List.maxIdxOn f (List.take i xs) h ≤ List.maxIdxOn f xs ⋯
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- A (random) lift of the complex embedding `φ : k →+* ℂ` to an extension `K` of `k`.
 -/
NumberField.ComplexEmbedding.lift : (K : Type u_1) →
  [inst : Field K] →
    {k : Type u_2} → [inst_1 : Field k] → [inst_2 : Algebra k K] → [Algebra.IsAlgebraic k K] → (k →+* ℂ) → K →+* ℂ
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsMap_mk : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {f : α → β} (hf : Continuous f)
  (x : α), hf.connectedComponentsMap (ConnectedComponents.mk x) = ConnectedComponents.mk (f x)
-- Mathlib.CategoryTheory.Square
/-- Flipping commutative squares is an auto-equivalence.  -/
CategoryTheory.Square.flipEquivalence : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C ≌ CategoryTheory.Square C
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.Flat g],
  AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.RepresentationTheory.Intertwining
/-- The natural intertwining map `σ.tprod ρ → τ.tprod ρ` induced by `f : σ → τ`.  -/
Representation.IntertwiningMap.rTensor : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : CommSemiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          (ρ : Representation A G V) →
                            {σ : Representation A G W} →
                              {τ : Representation A G U} → σ.IntertwiningMap τ → (σ.tprod ρ).IntertwiningMap (τ.tprod ρ)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.compFunctor_obj : ∀ {J : Type u_1} [inst : LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) (x : (i ⟶ j) × (j ⟶ k)),
  (i.compFunctor j k).obj x = CategoryTheory.CategoryStruct.comp x.1 x.2
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint64.sizeOf_spec : ∀ (val : UInt64), sizeOf (Lean.Compiler.LCNF.LitValue.uint64 val) = 1 + sizeOf val
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.prod_slash : ∀ {ι : Type u_1} {k : ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι},
  SlashAction.map (k * ↑s.card) g (∏ i ∈ s, f i) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑s.card - 1) • ∏ i ∈ s, SlashAction.map k g (f i)
-- Mathlib.Logic.Equiv.Defs
Equiv.apply_eq_iff_eq : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α}, f x = f y ↔ x = y
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Multiset.bell_cons_mul_count : ∀ (m : Multiset ℕ) {a : ℕ}, a ≠ 0 → (a ::ₘ m).bell * Multiset.count a (a ::ₘ m) = (m.sum + a).choose a * m.bell
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_inv : ∀ {α : Type u_1} [inst : Inv α] (a : Colex α), ofColex a⁻¹ = (ofColex a)⁻¹
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ClosedComplemented.exists_isTopCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M}, p.ClosedComplemented → ∃ q, Submodule.IsTopCompl p q
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocMod hp a (b + m • p) = toIocMod hp a b
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.ext_iff : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s t : HahnSeries.SummableFamily Γ R α}, s = t ↔ ∀ (a : α), s a = t a
-- Mathlib.Topology.LocallyFinite
LocallyFinite.closure : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → LocallyFinite fun i => closure (f i)
-- Mathlib.Topology.Closure
frontier_subset_iff_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, frontier s ⊆ s ↔ IsClosed s
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addMonoid : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddMonoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffAdd I' n G] → AddMonoid (ContMDiffMap I I' N G n)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.lowerBound?_exists : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t → ((∃ x, RBTree.RBNode.lowerBound? cut t = some x) ↔ ∃ x ∈ t, cut x ≠ Ordering.lt)
-- Init.Data.String.Basic
String.Slice.rawEndPos_sliceTo : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceTo pos).rawEndPos = pos.offset
-- Mathlib.Data.Set.Basic
Set.mem_dite_empty_right : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : p → Set α) (x : α),
  (x ∈ if h : p then t h else ∅) ↔ ∃ (h : p), x ∈ t h
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Normalize a compatible `intro`-like tactic to the arguments of an equivalent `intro`.  -/
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.introMergeArgs? : Lean.TSyntax `tactic → Option (Array Lean.Term)