mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- Let `L : C ⥤ D` be a localization functor for `W`, if an extension `E`
of `F : C ⥤ H` along `L` is such that the natural transformation
`E.hom : F ⟶ L ⋙ E.right` is an isomorphism, then `E` is a pointwise
left Kan extension.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  (E : L.LeftExtension F) →
                    [CategoryTheory.IsIso (CategoryTheory.StructuredArrow.hom E)] →
                      [L.IsLocalization W] → E.IsPointwiseLeftKanExtension
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.coe_add`. -/
AddAut.coe_mul : ∀ (M : Type u_2) [inst : Add M] (e₁ e₂ : AddAut M), ⇑(e₁ + e₂) = ⇑e₁ ∘ ⇑e₂
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.is_left_invariant_addIndex : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {K : Set G},
  IsCompact K →
    ∀ (g : G) {V : Set G},
      (interior V).Nonempty →
        MeasureTheory.Measure.haar.addIndex ((fun h => g + h) '' K) V = MeasureTheory.Measure.haar.addIndex K V
-- Init.Data.UInt.Lemmas
UInt64.toNat_sub : ∀ (a b : UInt64), (a - b).toNat = (2 ^ 64 - b.toNat + a.toNat) % 2 ^ 64
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.ext : ∀ {R : Type u_1} [inst : NonAssocRing R] {p q : MulRingNorm R}, (∀ (x : R), p x = q x) → p = q
-- Init.Data.SInt.Basic
/-- Bitwise left shift for 64-bit signed integers. Usually accessed via the `<<<` operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.shiftLeft : Int64 → Int64 → Int64
-- Lean.Widget.UserWidget
Lean.Widget.instFromJsonUserWidgetDefinition : Lean.FromJson Lean.Widget.UserWidgetDefinition
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The additive monoid homomorphism from a given additive monoid in the diagram to the
colimit additive monoid.  -/
AddMonCat.FilteredColimits.coconeMorphism : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] → (j : J) → F.obj j ⟶ AddMonCat.FilteredColimits.colimit F
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.funLeft_injective_of_surjective : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} (f : m → n), Function.Surjective f → Function.Injective ⇑(LinearMap.funLeft R M f)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instSDiffOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → SDiff (Std.ExtTreeSet α cmp)
-- Mathlib.Analysis.Complex.Conformal
isConformalMap_complex_linear : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedSpace ℂ E] {map : ℂ →L[ℂ] E},
  map ≠ 0 → IsConformalMap (ContinuousLinearMap.restrictScalars ℝ map)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The second factor of `p` in the universal factorization ring of `p`.  -/
Polynomial.UniversalFactorizationRing.factor₂ : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Polynomial.MonicDegreeEq (Polynomial.UniversalFactorizationRing m k hn p) k
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.vadd_def : ∀ {M' : Type u_1} {α : Type u_2} [inst : AddZeroClass M'] [inst_1 : VAdd M' α] {S : AddSubmonoid M'} (g : ↥S) (a : α),
  g +ᵥ a = ↑g +ᵥ a
-- Lean.ResolveName
Lean.reservedNamePredicatesExt : Lean.EnvExtension (Array (Lean.Environment → Lean.Name → Bool))
-- Mathlib.Tactic.Translate.ToDual
/-- We need to fix a few abbreviations after applying `nameDict`, i.e. replacing `ZeroLE` by `Nonneg`.
This dictionary contains these fixes.
The input should contain entries that is in `lowerCamelCase` (e.g. `ltzero`; the initial sequence
of capital letters should be lower-cased) and the output should be in `UpperCamelCase`
(e.g. `LTZero`).
When applying the dictionary, we lower-case the output if the input was also given in lower-case.
 -/
Mathlib.Tactic.ToDual.abbreviationDict : Std.HashMap String String
-- Aesop.Script.SpecificTactics
Aesop.straightLineExtS : Lean.MVarId → Aesop.ScriptM Aesop.ExtResult
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Filter.Tendsto.logb : ∀ {α : Type u_1} {b : ℝ} {f : α → ℝ} {l : Filter α} {x : ℝ},
  Filter.Tendsto f l (nhds x) → x ≠ 0 → Filter.Tendsto (fun y => Real.logb b (f y)) l (nhds (Real.logb b x))
-- Mathlib.Data.Nat.Prime.Defs
Nat.dvd_prime_two_le : ∀ {p m : ℕ}, Nat.Prime p → 2 ≤ m → (m ∣ p ↔ m = p)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.diff m₂).getKey! k = if m₂.contains k = true then default else m₁.getKey! k
-- Mathlib.Order.Irreducible
/-- A sup-prime element is a non-bottom element which isn't less than the supremum of anything
smaller.  -/
SupPrime : {α : Type u_2} → [SemilatticeSup α] → α → Prop
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.eq_2 : ∀ {α : Type u_1} (motive : RegularExpression α → α → Sort u_2) (x : α) (h_1 : (x : α) → motive RegularExpression.zero x)
  (h_2 : (x : α) → motive RegularExpression.epsilon x) (h_3 : (a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂)
  (h_4 : (P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a)
  (h_5 : (P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a)
  (h_6 : (P : RegularExpression α) → (a : α) → motive P.star a),
  (match RegularExpression.epsilon, x with
    | RegularExpression.zero, x => h_1 x
    | RegularExpression.epsilon, x => h_2 x
    | RegularExpression.char a₁, a₂ => h_3 a₁ a₂
    | P.plus Q, a => h_4 P Q a
    | P.comp Q, a => h_5 P Q a
    | P.star, a => h_6 P a) =
    h_2 x
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (toModuleCat : ModuleCat R) (instCoalgebra : Coalgebra R ↑toModuleCat)
  (toModuleCat_1 : ModuleCat R) (instCoalgebra_1 : Coalgebra R ↑toModuleCat_1),
  ({ toModuleCat := toModuleCat, instCoalgebra := instCoalgebra } =
      { toModuleCat := toModuleCat_1, instCoalgebra := instCoalgebra_1 }) =
    (toModuleCat = toModuleCat_1 ∧ instCoalgebra ≍ instCoalgebra_1)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_sum_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ι : Type u_3} [inst : Countable ι] {κ : ι → ProbabilityTheory.Kernel α β}
  [h : ∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i)],
  μ.compProd (ProbabilityTheory.Kernel.sum κ) = MeasureTheory.Measure.sum fun i => μ.compProd (κ i)
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X),
  R.EffectiveEpimorphic ↔ ∀ (Y : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj Y) R
-- Init.Data.Int.DivMod.Lemmas
Int.neg_emod : ∀ {a b : ℤ}, -a % b = if b ∣ a then 0 else ↑b.natAbs - a % b
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) →
          (x : Turing.TM2.Stmt Γ Λ σ) →
            (x_1 : σ) →
              (x_2 : (k : K) → List (Γ k)) →
                ((k : K) →
                    (f : σ → Γ k) →
                      (q : Turing.TM2.Stmt Γ Λ σ) →
                        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S) →
                  ((k : K) →
                      (f : σ → Option (Γ k) → σ) →
                        (q : Turing.TM2.Stmt Γ Λ σ) →
                          (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S) →
                    ((k : K) →
                        (f : σ → Option (Γ k) → σ) →
                          (q : Turing.TM2.Stmt Γ Λ σ) →
                            (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S) →
                      ((a : σ → σ) →
                          (q : Turing.TM2.Stmt Γ Λ σ) →
                            (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S) →
                        ((f : σ → Bool) →
                            (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
                              (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S) →
                          ((f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S) →
                            ((v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S) → motive x x_1 x_2
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternatingEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  ExteriorAlgebra.liftAlternatingEquiv a = ExteriorAlgebra.liftAlternating a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.opCospan_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingCospanᵒᵖ),
  (CategoryTheory.Limits.opCospan f g).inv.app X_1 =
    (match Opposite.unop X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op Z)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Y)).hom
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ),
  (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- The simplicial nerve of a simplicial category `C` is defined as the simplicial set whose
`n`-simplices are given by the set of simplicial functors from the simplicial thickening of
the linear order `Fin (n + 1)` to `C`
 -/
CategoryTheory.SimplicialNerve : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.SimplicialCategory C] → SSet
-- Init.Grind.Interactive
Lean.Parser.Tactic.grindErase : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.II.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), h.II = Set.range h.type₂
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Monotone.const_mul_of_nonpos : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R],
  Monotone f → a ≤ 0 → Antitone fun x => a * f x
-- Init.Data.Nat.Lcm
Nat.lcm_eq_left_iff_dvd : ∀ {m n : ℕ}, m.lcm n = m ↔ n ∣ m
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedCommMonoid.toUniqueAddUnits.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α],
  CanonicallyOrderedCommMonoid.toUniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }
-- Mathlib.Algebra.Group.Defs
AddCommMagma.to_isCommutative : ∀ {G : Type u_1} [inst : AddCommMagma G], IsAddCommutative G
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dot_nil_right : ∀ {xs : Lean.Omega.Coeffs}, xs.dot [] = 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_natCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ), (↑n).re = ↑n
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.of.injEq : ∀ (carrier : Type u) [semiring : Semiring carrier] (carrier_1 : Type u) (semiring_1 : Semiring carrier_1),
  (SemiRingCat.of carrier = SemiRingCat.of carrier_1) = (carrier = carrier_1 ∧ semiring ≍ semiring_1)
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- The sum of a finite power series `p` admits `p` as a power series.  -/
FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}, (∀ (m : ℕ), n ≤ m → p m = 0) → HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_stoppedProcess_apply : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] {ω : Ω},
  σ ω ≠ ⊤ →
    MeasureTheory.stoppedValue (MeasureTheory.stoppedProcess u τ) σ ω =
      MeasureTheory.stoppedValue u (fun ω => min (σ ω) (τ ω)) ω
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The natural isomorphism witnessing the pseudo-functoriality of `Grothendieck.map`.  -/
CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      (α : F ⟶ G) →
        (β : G ⟶ H) →
          CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Pseudofunctor.Grothendieck.map α).comp (CategoryTheory.Pseudofunctor.Grothendieck.map β)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.ofNat_one : ↑1 = 1
-- Init.Data.List.Basic
List.or_nil : [].or = false
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} {ε : Type u_9}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] [inst_2 : NormedAddCommGroup 𝕜] [inst_3 : SMul 𝕜 ε]
  [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜) {f : α → ε},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (c • f) μ
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
RCLike.measurable_im : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], Measurable ⇑RCLike.im
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.isBridge_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.IsBridge s(u, v) ↔ ¬(G.deleteEdges {s(u, v)}).Reachable u v
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_le_unop_iff : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S₁ S₂ : Subsemiring Rᵐᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_surjective_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α →* β},
  Function.Surjective ⇑(WithZero.map' f) ↔ Function.Surjective ⇑f
-- ProofWidgets.Data.Html
ProofWidgets.Html.ofComponent : {Props : Type} →
  [Lean.Server.RpcEncodable Props] → ProofWidgets.Component Props → Props → Array ProofWidgets.Html → ProofWidgets.Html
-- Mathlib.Data.ENat.Basic
/-- Specialization of `WithTop.map` to `ENat`.
 -/
ENat.map : {α : Type u_1} → (ℕ → α) → ℕ∞ → WithTop α
-- Lean.DocString.Parser
/-- Formatter for `withoutVersoSyntax`—formats according to the underlying formatter.
 -/
Lean.Doc.Parser.withoutVersoSyntax.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF → (Std.DTreeMap.Raw.filterMap f t).get? k = (t.get? k).bind (f k)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A morphism `f` satisfies `[Fibration f]` if it belongs to `fibrations C`.  -/
HomotopicalAlgebra.Fibration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → [HomotopicalAlgebra.CategoryWithFibrations C] → Prop
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Fin.accumulate_rec : ∀ {i n m : ℕ} (hin : i < n) (him : i + 1 < m) (t : Fin n → ℕ),
  (Fin.accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (Fin.accumulate n m) t ⟨i + 1, him⟩
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- [P. Berthelot and A. Ogus, *Notes on crystalline cohomology* (Lemma 3.6)][BerthelotOgus-1978]  -/
DividedPowers.span_isSubDPIdeal_iff : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {S : Set A},
  S ⊆ ↑I → (hI.IsSubDPIdeal (Ideal.span S) ↔ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Real.stronglyMeasurable_sinc : MeasureTheory.StronglyMeasurable Real.sinc
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.nhds_one_hasBasis : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G), (nhds 1).HasBasis (fun V => V ∈ B) id
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.mem_unitsFstOne : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {x : (Unitization R A)ˣ},
  x ∈ Unitization.unitsFstOne R A ↔ (↑x).toProd.1 = 1
-- Mathlib.Data.Matrix.Mul
Matrix.diagonal_mul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] (d : m → α) (M : Matrix m n α) (i : m) (j : n), (Matrix.diagonal d * M) i j = d i * M i j
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIntCast : {R : Type u_1} → [inst : TopologicalSpace R] → [IntCast R] → IntCast (SeparationQuotient R)
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.instSemilatticeSupSubtypeFG : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → SemilatticeSup { P // P.FG }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.minKey?.isSome = true
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**. Let `f : E → F` be a complex analytic function
on an open ball with center `c`.
If `f` sends this ball to a closed ball with center `f c` and the same radius,
then for any `z` in the former ball we have `dist (f z) (f c) ≤ dist z c`.
 -/
Complex.dist_le_dist_of_mapsTo_ball : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R : ℝ} {f : E → F} {c z : E},
  DifferentiableOn ℂ f (Metric.ball c R) →
    Set.MapsTo f (Metric.ball c R) (Metric.closedBall (f c) R) → z ∈ Metric.ball c R → dist (f z) (f c) ≤ dist z c
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- To prove a property on morphisms of a path category, it suffices to prove it for the identity
and prove that the property is preserved under composition on the right with length 1 paths.  -/
CategoryTheory.Paths.induction : ∀ {V : Type u₁} [inst : Quiver V] (P : {a b : CategoryTheory.Paths V} → (a ⟶ b) → Prop),
  (∀ {v : V}, P (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of V).obj v))) →
    (∀ {u v w : V} (p : (CategoryTheory.Paths.of V).obj u ⟶ (CategoryTheory.Paths.of V).obj v) (q : v ⟶ w),
        P p → P (CategoryTheory.CategoryStruct.comp p ((CategoryTheory.Paths.of V).map q))) →
      ∀ {a b : CategoryTheory.Paths V} (f : a ⟶ b), P f
-- Mathlib.Algebra.Category.Grp.Injective
AddCommGrpCat.injective_as_module_iff : ∀ (A : Type u) [inst : AddCommGroup A],
  CategoryTheory.Injective (ModuleCat.of ℤ A) ↔ CategoryTheory.Injective (AddCommGrpCat.of A)
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.encodePosNum.match_1.eq_2 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit0 with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_2 n
-- Mathlib.ModelTheory.Substructures
/-- See Note [custom simps projection]  -/
FirstOrder.Language.Substructure.Simps.coe : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → L.Substructure M → Set M
-- Mathlib.Data.Finset.Disjoint
/-- `disjUnion s t h` is the set such that `a ∈ disjUnion s t h` iff `a ∈ s` or `a ∈ t`.
It is the same as `s ∪ t`, but it does not require decidable equality on the type. The hypothesis
ensures that the sets are disjoint.  -/
Finset.disjUnion : {α : Type u_2} → (s t : Finset α) → Disjoint s t → Finset α
-- Mathlib.Algebra.WithConv
WithConv.symm_congrLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] (f : A ≃ₗ[R] B),
  (WithConv.congrLinearEquiv f).symm = WithConv.congrLinearEquiv f.symm
-- Mathlib.Order.CompletePartialOrder
DirectedOn.sSup_le : ∀ {α : Type u_2} [inst : CompletePartialOrder α] {d : Set α} {a : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) d → (∀ b ∈ d, b ≤ a) → sSup d ≤ a
-- Mathlib.Logic.Relation
Std.Symm.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [Std.Symm r] (f : α → β), Std.Symm (Function.onFun r f)
-- Lean.LocalContext
/-- Creates the expression `fun x₁ .. xₙ => b` for free variables `xs = #[x₁, .., xₙ]`,
suitably abstracting `b` and the types for each of the `xᵢ`.  -/
Lean.LocalContext.mkLambda : Lean.LocalContext → Array Lean.Expr → Lean.Expr → optParam Bool true → optParam Bool false → Lean.Expr
-- Mathlib.Topology.UniformSpace.Equiv
/-- `α × β` is uniformly isomorphic to `β × α`.  -/
UniformEquiv.prodComm : (α : Type u) → (β : Type u_1) → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α × β ≃ᵤ β × α
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcherApp : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Expr → m Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.contains a = false → t.getKey! a = default
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_singleton' : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (a : ι), {a}.sum = fun f => f a
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongrAlg.congr_simp : ∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e e_1 : G ≃* H}
  (e_e : e = e_1) (he : ∀ (a : G) (x : A), a • x = e a • x),
  SkewMonoidAlgebra.domCongrAlg k A he = SkewMonoidAlgebra.domCongrAlg k A ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_source : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), (e.lift_openEmbedding hf).source = f '' e.source