mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Match
/-- Creating a mapping containing `b ↦ e'` where `patternWithRef e' = some (stx, b)`,
and `e'` is a subterm of `e`.

This is a helper function for `whnfPreservingPatternRef`.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.mkPatternRefMap : Lean.Expr → Lean.ExprMap Lean.Expr
-- Mathlib.RingTheory.Algebraic.Integral
/-- **Alias** of `IsFractionRing.finrank_eq`. -/
Algebra.IsAlgebraic.finrank_of_isFractionRing : ∀ (A : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [inst : CommRing A] [inst_1 : CommRing K]
  [inst_2 : CommRing B] [inst_3 : CommRing L] [inst_4 : Algebra A B] [inst_5 : Module K L] [inst_6 : Algebra A K]
  [inst_7 : Algebra B L] [inst_8 : Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K]
  [IsFractionRing B L], Module.finrank K L = Module.finrank A B
-- Batteries.Data.List.Basic
List.inits.eq_1 : ∀ {α : Type u_1}, [].inits = [[]]
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.coe_intCast : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ),
  ↑↑n = ↑n
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangePushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.pushouts.IsStableUnderCobaseChange
-- Init.Data.UInt.Bitwise
UInt8.right_le_or : ∀ {a b : UInt8}, b ≤ a ||| b
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.isCompact_symm_image_closedBall : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E],
  IsCompact (↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- Cohomology classes identify to morphisms in the homotopy category.  -/
CochainComplex.HomComplex.CohomologyClass.homAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.CohomologyClass K L n ≃+
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `ofReal_norm'`. -/
ofReal_norm_eq_enorm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_eq : ∀ {α : Type u_1} {xs : Subarray α}, Std.Slice.toList xs = (xs.array.extract xs.start xs.stop).toList
-- Mathlib.LinearAlgebra.InvariantBasisNumber
strongRankCondition_iff : ∀ (R : Type u) [inst : Semiring R],
  StrongRankCondition R ↔ ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Injective ⇑f → n ≤ m
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLED_eq_getD_getEntryLE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} {fallback : (a : α) × β a},
  Std.DTreeMap.Internal.Impl.getEntryLED k t fallback = (Std.DTreeMap.Internal.Impl.getEntryLE? k t).getD fallback
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.lt_three : ∀ {p q r : ℕ+}, p ≤ q → q ≤ r → 1 < ADEInequality.sumInv {p, q, r} → p < 3
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- The (contravariant) functoriality of weighted limits with respect to the weight.  -/
CategoryTheory.Functor.weightedLimFlipObjMap : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {W W' : CategoryTheory.Functor J (Type w)} →
          (W ⟶ W') →
            (F : CategoryTheory.Functor J C) →
              [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] →
                [inst_3 : CategoryTheory.Limits.HasWeightedLimit W' F] → W'.weightedLimObjObj F ⟶ W.weightedLimObjObj F
-- Mathlib.MeasureTheory.Order.Group.Lattice
measurable_posPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α] [MeasurableSup α],
  Measurable posPart
-- Mathlib.Topology.Order.IsLUB
DenseRange.exists_seq_strictAnti_tendsto_of_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {β : Type u_3}
  [inst_3 : LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α},
  DenseRange f →
    Monotone f →
      x < y → ∃ u, StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioo x y) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
-- Mathlib.Order.Category.PartOrd
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe : ∀ (X : Preord) (a : ↑((Preord.dual.comp preordToPartOrd).obj X)),
  (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a =
    (OrderIso.dualAntisymmetrization ↑X).symm a
-- Mathlib.Data.Finsupp.Basic
Finsupp.mk_mem_graph_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {m : M} {f : α →₀ M}, (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_false_iff_forall_mem_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = false ↔ ∀ a' ∈ Std.Internal.List.keys l, (a == a') = false
-- Mathlib.Analysis.Analytic.Constructions
/-- `(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticWithinAt.inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {x : E} {s : Set E}, AnalyticWithinAt 𝕜 f s x → f x ≠ 0 → AnalyticWithinAt 𝕜 f⁻¹ s x
-- Mathlib.Data.PEquiv
Equiv.toPEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ≃ β) (x : α), f.toPEquiv x = some (f x)
-- Mathlib.Data.Num.Lemmas
Num.succ'_to_nat : ∀ (n : Num), ↑n.succ' = ↑n + 1
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthogonalFamily.linearIsometry_apply : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : OrthogonalFamily 𝕜 G V) (f : ↥(lp G 2)), hV.linearIsometry f = ∑' (i : ι), (V i) (↑f i)
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X}
  [μ.IsOpenPosMeasure], μ.AbsolutelyContinuous ν → ν.IsOpenPosMeasure
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The composition of the unit and the counit is equal to the identity up to unitors.  -/
CategoryTheory.Bicategory.Equivalence.left_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} (self : CategoryTheory.Bicategory.Equivalence a b),
  CategoryTheory.Bicategory.leftZigzagIso self.unit self.counit =
    CategoryTheory.Bicategory.leftUnitor self.hom ≪≫ (CategoryTheory.Bicategory.rightUnitor self.hom).symm
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup_add_one_le : ∀ {α : Type u} (f : α → Ordinal.{u}), (⨆ i, f i + 1).cof ≤ Cardinal.mk α
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorems.mk.injEq : ∀ (tree : Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem) (erased : Lean.PHashSet Lean.Name)
  (tree_1 : Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem) (erased_1 : Lean.PHashSet Lean.Name),
  ({ tree := tree, erased := erased } = { tree := tree_1, erased := erased_1 }) = (tree = tree_1 ∧ erased = erased_1)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.instModuleNNReal : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → Module NNReal (StieltjesFunction R)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.variation_WithDensity_le : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G},
  (μ.withDensity f B).variation ≤ (μ.transpose B).variation.withDensity fun x => ‖f x‖ₑ
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsAffineHom f]
  [AlgebraicGeometry.IsAffine Y], AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback f g)
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofNatClamp_of_le : ∀ {n : ℕ}, UInt64.size ≤ n → (UInt64.ofNatClamp n).toFin = ⟨UInt64.size - 1, UInt64.toFin_ofNatClamp_of_le._proof_1⟩
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited β] {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c)[a]! = default
-- Lean.Parser.Basic
/-- Parses a token and asserts the result is of the given kind.
`desc` is used in error messages as the token kind.  -/
Lean.Parser.expectTokenFn : Lean.SyntaxNodeKind → String → Lean.Parser.ParserFn
-- Mathlib.Tactic.Simps.Basic
Simps.instInhabitedProjectionData : Inhabited Simps.ProjectionData
-- Init.Data.SInt.Lemmas
Int8.toISize_ofIntLE : ∀ {n : ℤ} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt),
  (Int8.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Extension : Type
-- Mathlib.Algebra.Algebra.Basic
instFaithfulSMulIntOfCharZero : ∀ (R : Type u_3) [inst : Ring R] [CharZero R], FaithfulSMul ℤ R
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.mem_cycleType_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {n : ℕ} {σ : Equiv.Perm α},
  n ∈ σ.cycleType ↔ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n
-- Mathlib.Data.List.TFAE
/-- TFAE: The Following (propositions) Are Equivalent.

The `tfae_have` and `tfae_finish` tactics can be useful in proofs with `TFAE` goals.
 -/
List.TFAE : List Prop → Prop
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valuation.ltAddSubgroup.eq_1 : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : Γ₀ˣ), v.ltAddSubgroup γ = { carrier := {x | v x < ↑γ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Batteries.Data.Char.Basic
Char.max.eq_1 : Char.max = 1114111
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Cᵒᵖ A) {Z : A} (h : Φ.presheafFiber.obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.map f.op) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) h) =
    CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) P)
      h
-- Mathlib.CategoryTheory.Functor.Currying
/-- The currying functor, taking a functor `(C × D) ⥤ E` and producing a functor `C ⥤ (D ⥤ E)`.
 -/
CategoryTheory.Functor.curry : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor (CategoryTheory.Functor (C × D) E)
              (CategoryTheory.Functor C (CategoryTheory.Functor D E))
-- Std.Http.Protocol.H1.Error
/-- The aggregate byte size of all header fields exceeds the configured limit.
Maps to HTTP 431 Request Header Fields Too Large.
 -/
Std.Http.Protocol.H1.Error.headersTooLarge : Std.Http.Protocol.H1.Error
-- Lean.Elab.Binders
Lean.Elab.Term.elabLetTmpDecl : Lean.Elab.Term.TermElab
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubAddAction.ofStabilizer.isPretransitive_iff_of_addConj : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a b : α} {g : G},
  b = g +ᵥ a →
    (AddAction.IsPretransitive ↥(AddAction.stabilizer G a) ↥(SubAddAction.ofStabilizer G a) ↔
      AddAction.IsPretransitive ↥(AddAction.stabilizer G b) ↥(SubAddAction.ofStabilizer G b))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensRangeParams.toJson : Lean.Lsp.SemanticTokensRangeParams → Lean.Json
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_add : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (x y : MonoidAlgebra R M), MonoidAlgebra.map f (x + y) = MonoidAlgebra.map f x + MonoidAlgebra.map f y
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- `integrableExpSet X μ` is a convex subset of `ℝ` (it is an interval).  -/
ProbabilityTheory.convex_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  Convex ℝ (ProbabilityTheory.integrableExpSet X μ)
-- Mathlib.Data.ENat.BigOperators
/-- A product of finite numbers is still finite.  -/
ENat.prod_lt_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, (∀ a ∈ s, f a < ⊤) → ∏ a ∈ s, f a < ⊤
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The global ref for looking up `apply` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.appRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma))
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →+ B` and `ψ : B →+ C` define a short exact sequence of additive
topological groups, and if `ψ` is injective on an open set `U`, then the induced measure on `U` is
bounded above by `μC Set.univ * μA {1}` (possibly infinite).  -/
TopologicalAddGroup.IsSES.inducedMeasure_lt_of_injOn : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B] {U : Set B},
  IsOpen U → ∀ [DiscreteTopology A], Set.InjOn (⇑ψ) U → (H.inducedMeasure μA μC) U ≤ μC Set.univ * μA {0}
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel (α × γ) β` from a `Kernel α β` by taking the comap of the projection.  -/
ProbabilityTheory.Kernel.prodMkRight : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (γ : Type u_5) → [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel (α × γ) β
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_right_inj : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b c : α}, ↑a + b = ↑a + c ↔ b = c
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.postcomp_injective : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
  solution.postcomp f = solution.postcomp f' → f = f'
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instIsNegApplySet : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [inst_2 : IsTopologicalAddGroup M], IsNegApply (MeasureTheory.VectorMeasure α M) (Set α) M
-- Batteries.Data.Vector.Basic
/-- Auxiliary tail-recursive function for scanrM  -/
Vector.scanrM.loop : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      {n : ℕ} → [Monad m] → (α → β → m β) → Vector α n → β → (i : ℕ) → i ≤ n → Vector β (n - i) → m (Vector β (n + 1))
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- `linMulLin f g` is the bilinear form mapping `x` and `y` to `f x * g y`  -/
LinearMap.BilinForm.linMulLin : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] R) → (M →ₗ[R] R) → LinearMap.BilinForm R M
-- Lean.Parser.Syntax
Lean.Parser.precedenceParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.updateRIn_rIn : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) (r : ℝ) (hr : r ∈ Set.Ioo 0 f.rOut), (f.updateRIn r hr).rIn = r
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.unbounded.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ch : Std.CloseableChannel.Unbounded✝ α),
  sizeOf (Std.CloseableChannel.Flavors.unbounded✝ ch) = 1 + sizeOf ch
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.charFn_inj : ∀ {X : Type u_1} (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : MulZeroOneClass Y] {U V : Set X} [Nontrivial Y]
  (hU : IsClopen U) (hV : IsClopen V), LocallyConstant.charFn Y hU = LocallyConstant.charFn Y hV → U = V
-- Lean.Parser.Basic
Lean.Parser.categoryParser : Lean.Name → ℕ → Lean.Parser.Parser
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_one`. -/
Ordinal.principal_mul_one : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) 1
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.complete'' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE),
  ∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_add : ∀ {a : ℕ} (a1 : 1 < a) (m n : ℕ), Pell.yn a1 (m + n) = Pell.xn a1 m * Pell.yn a1 n + Pell.yn a1 m * Pell.xn a1 n
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn.congr_simp : ∀ {a a_1 : ℕ} (e_a : a = a_1) (a1 : 1 < a) (n n_1 : ℕ), n = n_1 → Pell.xn a1 n = Pell.xn ⋯ n_1
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.skippingBinders.loop : {α : Type} →
  ℕ →
    Array Lean.Name →
      (Array Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α) →
        ℕ → Array Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α
-- Init.System.IO
IO.FS.instBEqFileType.beq : IO.FS.FileType → IO.FS.FileType → Bool
-- Lean.Elab.Term.TermElabM
/-- Execute `x` without allowing it to postpone elaboration tasks.
That is, `tryPostpone` is a noop.  -/
Lean.Elab.Term.withoutPostponing : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_zero : ∀ {a : UInt16}, a <<< 0 = a
-- Mathlib.Data.Nat.Bits
Nat.boddDiv2.eq_1 : Nat.boddDiv2 0 = (false, 0)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.sinh : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => Real.sinh (f x)) μ
-- Mathlib.GroupTheory.Divisible
RootableBy.mk : {A : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid A] →
      [inst_1 : Pow A α] →
        [inst_2 : Zero α] →
          (root : A → α → A) →
            (∀ (a : A), root a 0 = 1) → (∀ {n : α} (a : A), n ≠ 0 → root a n ^ n = a) → RootableBy A α
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.commAlgEquiv_single_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (m : M) (n : N) (a : A),
  (AddMonoidAlgebra.commAlgEquiv R) (AddMonoidAlgebra.single m (AddMonoidAlgebra.single n a)) =
    AddMonoidAlgebra.single n (AddMonoidAlgebra.single m a)
-- Init.Data.SInt.Basic
instShiftLeftISize : ShiftLeft ISize
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tildeEquiv_inverse : ∀ {R : CommRingCat},
  AlgebraicGeometry.tildeEquiv.inverse =
    (SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf).ι.comp AlgebraicGeometry.moduleSpecΓFunctor
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.getStateImpl : {σ : Type} → [Inhabited σ] → Lean.EnvExtension σ → Array Lean.EnvExtensionState → σ
-- Mathlib.Data.Setoid.Basic
Setoid.eq_top_iff : ∀ {α : Type u_1} {s : Setoid α}, s = ⊤ ↔ ∀ (x y : α), s x y
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.coeff_killCompl : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (p : MvPowerSeries τ R) (x : σ →₀ ℕ),
  (MvPowerSeries.coeff x) ((MvPowerSeries.killCompl e) p) = (MvPowerSeries.coeff (Finsupp.embDomain e x)) p
-- Mathlib.Analysis.Complex.Poisson
/-- **Derivative of the Herglotz–Riesz kernel integral**: if `f` is circle integrable and `w` lies
inside the circle, then `w ↦ circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • f ζ) 0 R` has
derivative `circleAverage (fun ζ ↦ (2 * ζ / (ζ - w) ^ 2) • f ζ) 0 R` at `w`.
 -/
hasDerivAt_circleAverage_herglotzRieszKernel_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ},
  CircleIntegrable f 0 R →
    w ∈ Metric.ball 0 R →
      HasDerivAt (fun w => Real.circleAverage (fun ζ => herglotzRieszKernel 0 w ζ • f ζ) 0 R)
        (Real.circleAverage (fun ζ => (2 * ζ / (ζ - w) ^ 2) • f ζ) 0 R) w
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMin'.match_3.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (x : α) (r : Ordnode α)
  (h_1 : (x : α) → (r : Ordnode α) → motive Ordnode.nil x r)
  (h_2 :
    (size : ℕ) →
      (ll : Ordnode α) →
        (lx : α) → (lr : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size ll lx lr) x r),
  (match Ordnode.nil, x, r with
    | Ordnode.nil, x, r => h_1 x r
    | Ordnode.node size ll lx lr, x, r => h_2 size ll lx lr x r) =
    h_1 x r
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.monoidHomMonoidHomEquiv.congr_simp : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)],
  CommGroup.monoidHomMonoidHomEquiv G M = CommGroup.monoidHomMonoidHomEquiv G M
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.CandidateKind.prio : Lean.Server.FileWorker.SignatureHelp.CandidateKind → ℕ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Hom.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.LaxTrans.Hom η θ},
  x.as = y.as → x = y
-- Mathlib.Order.Filter.Partial
Filter.ptendsto_iff_rtendsto : ∀ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α →. β),
  Filter.PTendsto f l₁ l₂ ↔ Filter.RTendsto f.graph' l₁ l₂
-- Init.Data.Int.DivMod.Lemmas
Int.mul_lt_mul_left_of_neg : ∀ {a b c : ℤ}, a < 0 → (a * b < a * c ↔ c < b)