mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_eq : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).unitIso =
    AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF
-- Batteries.Data.List.Matcher
/-- List stream that keeps count of items read.  -/
List.instStreamProdNat_batteries : (α : Type u_1) → Std.Stream (List α × ℕ) α
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piFinTwo_symm_apply : ∀ (R : Type u) [inst : Semiring R] (M : Fin 2 → Type v) [inst_1 : (i : Fin 2) → AddCommMonoid (M i)]
  [inst_2 : (i : Fin 2) → Module R (M i)],
  ⇑(LinearEquiv.piFinTwo R M).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- If `F : C ⥤ D` is a triangulated functor from a triangulated category, then `D`
is also triangulated if tuples of composable arrows in `D` can be lifted to `C`.  -/
CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Limits.HasZeroObject D] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : CategoryTheory.Preadditive D] [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [inst_12 : F.CommShift ℤ]
  [F.IsTriangulated] [(F.mapComposableArrows 2).EssSurj] [CategoryTheory.IsTriangulated C],
  CategoryTheory.IsTriangulated D
-- Batteries.Data.List.Basic
List.sections_eq_nil_of_isEmpty : ∀ {α : Type u_1} {L : List (List α)}, L.any List.isEmpty = true → L.sections = []
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- 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.ContinuousAlternatingMap.vectorPrebundle : (𝕜 : Type u_1) →
  (ι : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : Fintype ι] →
        {B : Type u_3} →
          [inst_2 : TopologicalSpace B] →
            (F₁ : Type u_4) →
              [inst_3 : NormedAddCommGroup F₁] →
                [inst_4 : NormedSpace 𝕜 F₁] →
                  (E₁ : B → Type u_5) →
                    [inst_5 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_6 : (x : B) → Module 𝕜 (E₁ x)] →
                        [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          [inst_8 : (x : B) → TopologicalSpace (E₁ x)] →
                            [inst_9 : FiberBundle F₁ E₁] →
                              [VectorBundle 𝕜 F₁ E₁] →
                                (F₂ : Type u_6) →
                                  [inst_11 : NormedAddCommGroup F₂] →
                                    [inst_12 : NormedSpace 𝕜 F₂] →
                                      (E₂ : B → Type u_7) →
                                        [inst_13 : (x : B) → AddCommGroup (E₂ x)] →
                                          [inst_14 : (x : B) → Module 𝕜 (E₂ x)] →
                                            [inst_15 : TopologicalSpace (Bundle.TotalSpace 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)] →
                                                        VectorPrebundle 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂) fun x =>
                                                          E₁ x [⋀^ι]→L[𝕜] E₂ x
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (obj : Type u₂)
  (category : autoParam (CategoryTheory.Category.{v₂, u₂} obj) CategoryTheory.BasedCategory.category._autoParam)
  (p : CategoryTheory.Functor obj 𝒮) (obj_1 : Type u₂)
  (category_1 : autoParam (CategoryTheory.Category.{v₂, u₂} obj_1) CategoryTheory.BasedCategory.category._autoParam)
  (p_1 : CategoryTheory.Functor obj_1 𝒮),
  ({ obj := obj, category := category, p := p } = { obj := obj_1, category := category_1, p := p_1 }) =
    (obj = obj_1 ∧ category ≍ category_1 ∧ p ≍ p_1)
-- Mathlib.Algebra.Group.Subgroup.Order
Subgroup.isCoatom_map : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (f : G ≃* ↥H) {K : Subgroup G},
  IsCoatom (Subgroup.map (↑f) K) ↔ IsCoatom K
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.simpa : Lean.ParserDescr
-- Batteries.Tactic.Alias
/-- Set the alias info for a new declaration  -/
Batteries.Tactic.Alias.setAliasInfo : {m : Type → Type} → [Lean.MonadEnv m] → Batteries.Tactic.Alias.AliasInfo → Lean.Name → m Unit
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_functor : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U),
  (TopCat.Presheaf.generateEquivalenceOpensLe U hY).functor = TopCat.Presheaf.generateEquivalenceOpensLe_functor' U
-- Aesop.Rule
Aesop.defaultNormPenalty : ℤ
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.le_llp_iff_le_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T T' : CategoryTheory.MorphismProperty C),
  T ≤ T'.llp ↔ T' ≤ T.rlp
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_2 t (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.brecOn.go t F_1 F_2).2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
one_le_cfc_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) one_le_cfc_iff._auto_1 →
    autoParam (p a) one_le_cfc_iff._auto_3 → (1 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 1 ≤ f x)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) {X Y : CategoryTheory.MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).functor.map f).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.end_repr_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (x : M →ₗ[R] M),
  b.end.repr x = (Matrix.stdBasis R ι ι).repr ((LinearMap.toMatrix b b) x)
-- Mathlib.Data.Sym.Basic
Sym.instSubsingleton : ∀ {α : Type u_1} [Subsingleton α] (n : ℕ), Subsingleton (Sym α n)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The left-translation shift is continuous.  -/
SymbolicDynamics.FullShift.continuous_shift : ∀ {A : Type u_1} {G : Type u_2} [inst : AddMonoid G] [inst_1 : TopologicalSpace A] (g : G),
  Continuous (SymbolicDynamics.FullShift.shift g)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Apply a linear map on the output of a bilinear form.  -/
LinearMap.compBilinForm : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {R' : Type u_7} →
            [inst_3 : CommSemiring R'] →
              [inst_4 : Algebra R' R] →
                [inst_5 : Module R' M] →
                  [IsScalarTower R' R M] → (R →ₗ[R'] R') → LinearMap.BilinForm R M → LinearMap.BilinForm R' M
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_first : ∀ {α : Type u_1} {p : α → Bool} {xs : List α},
  (∀ x ∈ xs, p x = false) →
    ∀ (sep : α), p sep = true → ∀ (as : List α), List.splitOnP p (xs ++ sep :: as) = xs :: List.splitOnP p as
-- Mathlib.Tactic.GCongr.Core
/-- Try to construct the `GCongrLemma` for a lemma with hypotheses `hyps` and
conclusion `target`.  -/
Mathlib.Tactic.GCongr.makeGCongrLemma : Array Lean.Expr → Lean.Expr → Lean.Name → ℕ → Bool → Bool → Lean.MetaM Mathlib.Tactic.GCongr.GCongrLemma
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If the additive action of a countable group `G` admits an invariant measure `μ`
with a fundamental domain `s`, then every null-measurable set `t` of measure strictly greater than
`μ s` contains two points `x y` such that `g +ᵥ x = y` for some `g ≠ 0`.  -/
MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.NullMeasurableSet t μ → μ s < μ t → ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 0 ∧ g +ᵥ x = y
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasurableEmbedding.integrableAtFilter_iff_comap : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {l : Filter α} [inst_2 : MeasurableSpace β] {e : α → β},
  MeasurableEmbedding e →
    ∀ {f : β → ε} {μ : MeasureTheory.Measure β},
      MeasureTheory.IntegrableAtFilter f (Filter.map e l) μ ↔
        MeasureTheory.IntegrableAtFilter (f ∘ e) l (MeasureTheory.Measure.comap e μ)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : { x // x.Compatible }),
  ↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible.symm x) =
    CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ ↑x
-- Mathlib.Algebra.Order.Field.Basic
inv_pow_lt_inv_pow_of_lt : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 < a → ∀ {m n : ℕ}, m < n → (a ^ n)⁻¹ < (a ^ m)⁻¹
-- Mathlib.CategoryTheory.Galois.EssSurj
/-- If `X` is a finite, discrete `Aut F`-set with continuous `Aut F`-action, then
there exists `A : C` such that `F.obj A ≅ X` as `Aut F`-sets.
 -/
CategoryTheory.PreGaloisCategory.exists_lift_of_continuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (X : Action FintypeCat (CategoryTheory.Aut F)) [inst_3 : TopologicalSpace X.V.obj] [DiscreteTopology X.V.obj]
  [ContinuousSMul (CategoryTheory.Aut F) X.V.obj],
  ∃ A, Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅ X)
-- Mathlib.Order.Preorder.Chain
IsMaxChain.top_mem : ∀ {α : Type u_1} {s : Set α} [inst : LE α] [inst_1 : OrderTop α], IsMaxChain (fun x1 x2 => x1 ≤ x2) s → ⊤ ∈ s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.ofHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.AddMonObj A] [inst_3 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsAddMonHom f], (CategoryTheory.AddMon.ofHom f).hom = f
-- Lean.Meta.Basic
/-- Configuration for projection reduction. See `whnfCore`.
 -/
Lean.Meta.ProjReductionKind : Type
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.closure_isThreeCycles_eq_top : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Subgroup.closure {g | (↑g).IsThreeCycle} = ⊤
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.copy_eq : ∀ {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] (S : LieSubmodule R L M) (s : Set M) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- A graph is `k`-edge-connected if any two vertices are `k`-edge-reachable.  -/
SimpleGraph.IsEdgeConnected : {V : Type u_1} → SimpleGraph V → ℕ → Prop
-- Lean.Log
/-- Return `true` if errors have been logged.  -/
Lean.MonadLog.hasErrors : {m : Type → Type} → [self : Lean.MonadLog m] → m Bool
-- Mathlib.Analysis.Analytic.Order
/-- The order multiplies by `n` when taking an analytic function to its `n`th power.  -/
analyticOrderNatAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ → ∀ (n : ℕ), analyticOrderNatAt (f ^ n) z₀ = n • analyticOrderNatAt f z₀
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift.equiv_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7)
  (N : Type u_8) (P₂ : Type u_17) [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M)
  (n : N), (((TensorProduct.lift.equiv σ₁₂ M N P₂).symm f) m) n = f (m ⊗ₜ[R] n)
-- Mathlib.Topology.MetricSpace.Closeds
Metric.lipschitz_infDist : ∀ {α : Type u_1} [inst : MetricSpace α], LipschitzWith 2 fun p => Metric.infDist p.1 ↑p.2
-- Mathlib.Order.SymmDiff
compl_symmDiff_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), symmDiff aᶜ bᶜ = symmDiff a b
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  (s.exsphere signs).center = s.excenter signs
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitizationAlgEquiv_apply : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] (R : Type u_3) [inst_5 : CommSemiring R]
  [inst_6 : Algebra R 𝕜] [inst_7 : DistribMulAction R A] [inst_8 : IsScalarTower R 𝕜 A]
  (a : WithLp 1 (Unitization 𝕜 A)), (WithLp.unitizationAlgEquiv R) a = a.ofLp
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, Set.Icc ⊥ a = Set.Iic a
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, ¬Disjoint ↑I ↑J ↔ (↑I ∩ ↑J).Nonempty
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- This can be made a local instance in order to get `⊥`
in `Cardinal.aleph0.ord.ToType`.  -/
Cardinal.orderBotAleph0OrdToType : OrderBot Cardinal.aleph0.ord.ToType
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.isNoetherian_iff : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.IsNoetherian X ↔ AlgebraicGeometry.IsLocallyNoetherian X ∧ CompactSpace ↥X
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.precomp_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {J' : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J'] (G : CategoryTheory.Functor J' J),
  (c.precomp G).pt = c.pt
-- Mathlib.Topology.QuasiSeparated
T2Space.to_quasiSeparatedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], QuasiSeparatedSpace α
-- Init.Data.List.Basic
List.drop_nil : ∀ {α : Type u} {i : ℕ}, List.drop i [] = []
-- Std.Sat.AIG.If
_private.Std.Sat.AIG.If.0.Std.Sat.AIG.RefVec.ite.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : Std.Sat.AIG.RefVec.IfInput aig w → Sort u_1) →
            (input : Std.Sat.AIG.RefVec.IfInput aig w) →
              ((discr : aig.Ref) → (lhs rhs : aig.RefVec w) → motive { discr := discr, lhs := lhs, rhs := rhs }) →
                motive input
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.archimedean_of_mk_eq_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  (∀ (a : M), a ≠ 0 → ∀ (b : M), b ≠ 0 → ArchimedeanClass.mk a = ArchimedeanClass.mk b) → Archimedean M
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear isometry preserves the property of being orthonormal.  -/
LinearIsometry.orthonormal_comp_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : ι → E}
  (f : E →ₗᵢ[𝕜] E'), Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v
-- Mathlib.Condensed.Discrete.Basic
Condensed.discrete_map : ∀ (C : Type w) [inst : CategoryTheory.Category.{u + 1, w} C]
  [inst_1 : CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] {X Y : C} (f : X ⟶ Y),
  (Condensed.discrete C).map f =
    (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).map
      ((CategoryTheory.Functor.const CompHausᵒᵖ).map f)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero : ∀ {z : ℂ}, z.re < 0 → z.im = 0 → Filter.Tendsto Complex.arg (nhdsWithin z {z | z.im < 0}) (nhds (-Real.pi))
-- Mathlib.Data.Finset.Density
Finset.dens_univ : ∀ {α : Type u_2} [inst : Fintype α] [Nonempty α], Finset.univ.dens = 1
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.intCoe_int : ∀ (f : ArithmeticFunction ℤ), ↑f = f
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.map_add : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i))
  (x y : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p),
  Submodule.quotientPi_aux.toFun p (x + y) = Submodule.quotientPi_aux.toFun p x + Submodule.quotientPi_aux.toFun p y
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial_apply_self : ∀ (p : NNReal) (h : p ≤ 1) (n : ℕ), (PMF.binomial p h n) (Fin.last n) = ↑p ^ n
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_eq_lintegral : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ]
  (f : α → ENNReal), ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToAction F).PreservesMonomorphisms
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Lagrange's **Mean Value Theorem**, `deriv` version.  -/
exists_deriv_eq_slope' : ∀ (f : ℝ → ℝ) {a b : ℝ},
  a < b → ContinuousOn f (Set.Icc a b) → DifferentiableOn ℝ f (Set.Ioo a b) → ∃ c ∈ Set.Ioo a b, deriv f c = slope f a b
-- Mathlib.Topology.Spectral.Hom
IsSpectralMap.continuous : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsSpectralMap f → Continuous f
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p] (x : L) (n : ℕ) (y : K),
  i y = x ^ p ^ n → (PerfectRing.lift i j p) x = (iterateFrobeniusEquiv M p n).symm (j y)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Icc_succ_left_eq_Ioc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a : α},
  ¬IsMax a → ∀ (b : α), Finset.Icc (Order.succ a) b = Finset.Ioc a b
-- Mathlib.Analysis.SpecialFunctions.Log.Base
/-- The real logarithm base b is continuous as a function from nonzero reals.  -/
Real.continuous_logb : ∀ {b : ℝ}, Continuous fun x => Real.logb b ↑x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalRing : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalRing A] → [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → NonUnitalRing ↥S
-- Mathlib.Tactic.Ring.Basic
/-- Constructs the expression corresponding to `.const n`.
(The `.const` constructor does not check that the expression is correct.)
 -/
Mathlib.Tactic.Ring.ExProd.mkNat : {u : Lean.Level} → {α : Q(Type u)} → (sα : Q(CommSemiring «$α»)) → ℕ → (e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd sα e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {instOrd : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α fun x => Unit} {l : List α} (h : t₁.WF),
  (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t₁ l ⋯)).Equiv
    (List.foldl (fun acc a => Std.DTreeMap.Internal.Impl.insertIfNew! a () acc) t₁ l)