mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.instCommGroupWithZeroValueGroup₀ : {A : Type u_1} →
  {B : Type u_2} →
    [inst : MonoidWithZero A] → [inst_1 : CommGroupWithZero B] → (f : A →*₀ B) → CommGroupWithZero f.ValueGroup₀
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.div_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedDivisionRing 𝕜]
  {f : α → 𝕜}, MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => f x / c) μ
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_mk : ∀ {α : Type u} [inst : Monoid α] (x y : α) (h₁ : x * y = 1) (h₂ : y * x = 1),
  { val := x, inv := y, val_inv := h₁, inv_val := h₂ }⁻¹ = { val := y, inv := x, val_inv := h₂, inv_val := h₁ }
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAtFilter.tendsto_nhds : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F},
  L ≤ nhds x → HasGradientAtFilter f f' x L → Filter.Tendsto f L (nhds (f x))
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instNonAssocSemiring : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → NonAssocSemiring (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [∀ (i : ι), SMulCommClass R (A i) (A i)] →
              [∀ (i : ι), IsScalarTower R (A i) (A i)] → NonAssocSemiring (PiTensorProduct R fun i => A i)
-- Mathlib.Order.Filter.Map
Filter.mem_kernMap_iff_compl : ∀ {α : Type u_1} {β : Type u_2} {m : α → β} {f : Filter α} {s : Set β},
  s ∈ Filter.kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.subcategoryAcyclic C).IsTriangulated
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Away from a codiscrete subset of `𝕜`, the logarithmic derivative of the `n`-th power of a
meromorphic function is `n` times the logarithmic derivative.
 -/
Meromorphic.logDeriv_zpow_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'},
  Meromorphic f → ∀ (n : ℤ), logDeriv (f ^ n) =ᶠ[Filter.codiscrete 𝕜] n • logDeriv f
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.phase? : Aesop.Frontend.RuleConfig → Option Aesop.PhaseName
-- Mathlib.Order.JordanHolder
CompositionSeries.injective : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X), Function.Injective s.toFun
-- Mathlib.Algebra.Notation.Support
/-- The multiplicative support of a function that is everywhere non-one is the whole space.  -/
Function.mulSupport_eq_univ : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M}, (∀ (x : ι), f x ≠ 1) → Function.mulSupport f = Set.univ
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.forIn : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (α → δ → m (ForInStep δ)) → δ → Std.TreeSet.Raw α cmp → m δ
-- Mathlib.Algebra.FiniteSupport.Defs
/-- The function `f` has finite support.  -/
Function.HasFiniteSupport : {α : Type u_1} → {M : Type u_2} → [Zero M] → (α → M) → Prop
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fintypeEdgeSetInf : {V : Type u} →
  (G₁ G₂ : SimpleGraph V) → [DecidableEq V] → [Fintype ↑G₁.edgeSet] → [Fintype ↑G₂.edgeSet] → Fintype ↑(G₁ ⊓ G₂).edgeSet
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.not_continuousAt_log_log_neg_one : ¬ContinuousAt (fun x => Real.log (Real.log x)) (-1)
-- Init.Control.Lawful.Instances
OptionT.run_throw : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {e : PUnit.{u_3 + 1}} [inst : Monad m], (throw e).run = pure none
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.instIsNontrivial : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [v.IsRankOneDiscrete], v.IsNontrivial
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {ι : Sort u_3} (f : ι → ↥L),
  ↑(iInf f) = ⨅ i, ↑(f i)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
isIdempotentElem_iff_spectrum_subset : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : Field R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  p a → (IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1})
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_of_tendsto₀' : ∀ (f : CircleDeg1Lift) {τ' : ℝ},
  Filter.Tendsto (fun n => (⇑f)^[n + 1] 0 / (↑n + 1)) Filter.atTop (nhds τ') → f.translationNumber = τ'
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.selbergTerms_pos : ∀ {s : BoundingSieve} {l : ℕ}, l ∣ s.prodPrimes → 0 < BoundingSieve.selbergTerms l
-- Mathlib.Analysis.Calculus.Deriv.Mul
ContinuousLinearMap.deriv_of_bilinear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {G : Type u_1}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜 → E} {v : 𝕜 → F},
  (x ∈ tsupport v → DifferentiableAt 𝕜 u x) →
    (x ∈ tsupport u → DifferentiableAt 𝕜 v x) →
      deriv (fun y => (B (u y)) (v y)) x = (B (u x)) (deriv v x) + (B (deriv u x)) (v x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The inclusion `R ⟶ (X.chainComplex R).X n` of the summand
corresponding to a `n`-simplex `x : X _⦋n⦌`.  -/
SSet.ιChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → {R : C} → {n : ℕ} → X.obj (Opposite.op { len := n }) → (R ⟶ (X.chainComplex R).X n)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If the inner product of two vectors is equal to the product of their norms (i.e.,
`⟪x, y⟫ = ‖x‖ * ‖y‖`), then the two vectors are nonnegative real multiples of each other. One form
of the equality case for Cauchy-Schwarz.
Compare `norm_inner_eq_norm_iff`, which takes the weaker hypothesis `abs ⟪x, y⟫ = ‖x‖ * ‖y‖`.  -/
inner_eq_norm_mul_iff_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  inner ℝ x y = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_eval : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix n n (Polynomial R)) (r : R) (i j : n),
  Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) i j = Polynomial.eval r (M i j)
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
/-- **Integration by parts for Fréchet derivatives**
Version with a general bilinear form `B`.
If `B f g` is integrable, as well as `B f' g` and `B f g'` where `f'` and `g'` are derivatives
of `f` and `g` in a given direction `v`, then `∫ B f g' = - ∫ B f' g`.  -/
integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : MeasurableSpace E] {μ : MeasureTheory.Measure E}
  [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {f : E → F} {f' : E → E →L[ℝ] F} {g : E → G}
  {g' : E → E →L[ℝ] G} {v : E} {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B ((f' x) v)) (g x)) μ →
    MeasureTheory.Integrable (fun x => (B (f x)) ((g' x) v)) μ →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ →
        (∀ x ∈ tsupport g, HasFDerivAt f (f' x) x) →
          (∀ x ∈ tsupport f, HasFDerivAt g (g' x) x) →
            ∫ (x : E), (B (f x)) ((g' x) v) ∂μ = -∫ (x : E), (B ((f' x) v)) (g x) ∂μ
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This isomorphism says that hom-sets in the category `Over A` for a presheaf `A` where the domain
is of the form `(CostructuredArrow.toOver yoneda A).obj X` can instead be interpreted as
hom-sets in the category `(CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` where the domain is of the
form `yoneda.obj X` after adjusting the codomain accordingly. This is desirable because in the
latter case the Yoneda lemma can be applied.  -/
CategoryTheory.CostructuredArrow.toOverCompYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (T : CategoryTheory.Over A) →
        (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp (CategoryTheory.yoneda.obj T) ≅
          CategoryTheory.yoneda.op.comp
            (CategoryTheory.yoneda.obj ((CategoryTheory.overEquivPresheafCostructuredArrow A).functor.obj T))
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS'.visitApp : Array Lean.Expr → (e f arg : Lean.Expr) → ℕ → e = f.app arg → Lean.Meta.Sym.M✝ Lean.Expr
-- Mathlib.LinearAlgebra.StdBasis
Pi.basisFun_equivFun : ∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η],
  (Pi.basisFun R η).equivFun = LinearEquiv.refl R (η → R)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
cthickening_cthickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 ≤ ε → 0 ≤ δ → ∀ (s : Set E), Metric.cthickening ε (Metric.cthickening δ s) = Metric.cthickening (ε + δ) s
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Derives.refl : ∀ {T : Type u_1} {g : ContextFreeGrammar T} (w : List (Symbol T g.NT)), g.Derives w w
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Isomorphic graphs are trees together.  -/
SimpleGraph.Iso.isTree_iff : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G'), G.IsTree ↔ G'.IsTree
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.homologyMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C] (n : ℕ),
  SSet.homologyMap (CategoryTheory.CategoryStruct.id X) R n = CategoryTheory.CategoryStruct.id (X.homology R n)
-- Std.Time.Date.Unit.Month
/-- `Ordinal` represents a bounded value for months, which ranges between 1 and 12.
 -/
Std.Time.Month.Ordinal : Type
-- Mathlib.Topology.Bornology.Basic
/-- The `Set.univ` is bounded.  -/
BoundedSpace.bounded_univ : ∀ {α : Type u_4} {inst : Bornology α} [self : BoundedSpace α], Bornology.IsBounded Set.univ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- For a group with zero, `PosMulReflectLT G₀` implies `PosMulStrictMono G₀`.  -/
PosMulReflectLT.toPosMulStrictMono : ∀ (G₀ : Type u_3) [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀], PosMulStrictMono G₀
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- If `lhs` and `rhs` are semiring expressions that have been adapted as ring ones.
The respective semiring reified expressions are stored here.
 -/
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.ofSemiring? : Lean.Meta.Grind.Arith.CommRing.DiseqCnstr →
  Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr)
-- Mathlib.Data.Num.Bitwise
instDecidableEqNzsNum.decEq : (x x_1 : NzsNum) → Decidable (x = x_1)
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.mk.inj : ∀ {numGoals nameLength replacementSize : ℕ} {name : String} {newGoals : Array Lean.Meta.AbstractMVarsResult}
  {numGoals_1 nameLength_1 replacementSize_1 : ℕ} {name_1 : String} {newGoals_1 : Array Lean.Meta.AbstractMVarsResult},
  { numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        newGoals := newGoals } =
      { numGoals := numGoals_1, nameLength := nameLength_1, replacementSize := replacementSize_1, name := name_1,
        newGoals := newGoals_1 } →
    numGoals = numGoals_1 ∧
      nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ newGoals = newGoals_1
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₂_eq' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    ∀ (i₁₂ : I₁₂),
      K.d₂ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- The standard additive character `ZMod N → ℂ` is primitive.  -/
ZMod.isPrimitive_stdAddChar : ∀ (N : ℕ) [inst : NeZero N], ZMod.stdAddChar.IsPrimitive
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.isBigO_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x → (fun x_1 => f x_1 - f x) =O[nhds x] fun x_1 => x_1 - x
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_div : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M]
  {s t : Set M}, s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (s / t) = sSup s / sInf t
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective₂ : ∀ {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] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  {P : CategoryTheory.Functor Cᵒᵖ A}
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] (p₁ p₂ : CategoryTheory.ToType (Φ.presheafFiber.obj P)),
  ∃ X x z₁ z₂,
    (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = p₁ ∧
      (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ = p₂
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_neg : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} [inst : Neg R] (A : Matrix n l R)
  (B : Matrix n m R) (C : Matrix o l R) (D : Matrix o m R),
  -Matrix.fromBlocks A B C D = Matrix.fromBlocks (-A) (-B) (-C) (-D)
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn'_def : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] {P : Sort u_2} (x : RatFunc K)
  (f : Polynomial K → Polynomial K → P) (H : ∀ {p q a : Polynomial K}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q),
  x.liftOn' f H = x.liftOn f ⋯
-- Init.Data.Range.Polymorphic.Char
Char.pRangeSuccMany?_eq : Std.PRange.succMany? = Char.succMany?
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp_toNat : ∀ (n : UInt32), UInt32.ofNatClamp n.toNat = n
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.differentiable_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) MeasureTheory.volume → Differentiable ℝ (FourierTransform.fourier f)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_of_eq : ∀ {α β : Type u} [Infinite α], Cardinal.mk α = Cardinal.mk β → Cardinal.mk (α ≃ β) = 2 ^ Cardinal.mk α
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_reinsertAux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] (data : { d // 0 < d.size })
  (a : α) (b : β a),
  (Std.DHashMap.Internal.toListModel ↑(Std.DHashMap.Internal.Raw₀.reinsertAux hash data a b)).Perm
    (⟨a, b⟩ :: Std.DHashMap.Internal.toListModel ↑data)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.expRecOn_zero : ∀ {M : Type u_4} {motive : WithZero (Multiplicative M) → Sort u_6} (zero : motive 0)
  (exp : (a : M) → motive (WithZero.exp a)), WithZero.expRecOn 0 zero exp = zero
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.restrict_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {s : Set α} (hm : m ≤ m0) (μ : MeasureTheory.Measure α),
  MeasurableSet s → (μ.trim hm).restrict s = (μ.restrict s).trim hm
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instCreatesFiniteLimitsTopOverForget : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [CategoryTheory.Limits.HasPullbacks T] →
          [P.IsMultiplicative] →
            [P.IsStableUnderBaseChange] →
              [P.HasOfPostcompProperty P] →
                CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.MorphismProperty.Over.forget P ⊤ X)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X}
  {c : CategoryTheory.Limits.PullbackCone f g} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)),
  (hc.pullbackConeEquivBinaryFanFunctor.lift s).left =
    hc.lift
      (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left s.fst) (CategoryTheory.Over.Hom.left s.snd)
        ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast_concat : ∀ {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj v t), (p.concat h).dropLast = p.copy ⋯ ⋯
-- Init.Data.String.Basic
String.Pos.ofToSlice_toSlice : ∀ {s : String} (pos : s.Pos), String.Pos.ofToSlice pos.toSlice = pos
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
groupCohomology.inhomogeneousCochains.d_comp_d : ∀ {k G : Type u} [inst : CommRing k] (n : ℕ) [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A n) (inhomogeneousCochains.d A (n + 1)) = 0
-- Mathlib.Order.Sublattice
/-- A sublattice of a lattice inherits a supremum.  -/
Sublattice.instSupCoe : {α : Type u_2} → [inst : Lattice α] → {L : Sublattice α} → Max ↥L
-- Mathlib.CategoryTheory.Localization.Opposite
CategoryTheory.Functor.IsLocalization.op : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W], L.op.IsLocalization W.op
-- Init.Data.Nat.Div.Basic
dite.congr_simp : ∀ {α : Sort u} (c : Prop) {h : Decidable c} [h_1 : Decidable c] (t t_1 : c → α),
  t = t_1 → ∀ (e e_1 : ¬c → α), e = e_1 → dite c t e = dite c t_1 e_1
-- Mathlib.Algebra.Group.Defs
nsmulRec.eq_1 : ∀ {M : Type u_1} [inst : Zero M] [inst_1 : Add M] (x : M), nsmulRec 0 x = 0
-- Mathlib.Order.Filter.CardinalInter
cardinal_sInter_mem : ∀ {α : Type u} {c : Cardinal.{u}} {l : Filter α} {S : Set (Set α)} [CardinalInterFilter l c],
  Cardinal.mk ↑S < c → (⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l)
-- Mathlib.ModelTheory.PartialEquiv
/-- Given an embedding, returns the corresponding partial equivalence with `⊤` as domain.  -/
FirstOrder.Language.Embedding.toPartialEquiv : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Embedding M N → L.PartialEquiv M N
-- Mathlib.Data.Seq.Parallel
/-- Parallel computation of an infinite stream of computations,
taking the first result  -/
Computation.parallel : {α : Type u} → Stream'.WSeq (Computation α) → Computation α
-- Mathlib.Topology.Order.Basic
Preorder.topology.eq_1 : ∀ (α : Type u_1) [inst : Preorder α],
  Preorder.topology α = TopologicalSpace.generateFrom {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}
-- Mathlib.Topology.Constructions.SumProd
Topology.isInducing_const_prod : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {x : X} {f : Y → Z}, (Topology.IsInducing fun x' => (x, f x')) ↔ Topology.IsInducing f
-- Mathlib.GroupTheory.Exponent
AddMonoid.exp_eq_one_iff : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G = 1 ↔ Subsingleton G
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian equals the Laplacian with respect to `Set.univ`.
 -/
InnerProductSpace.laplacianWithin_univ : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F},
  InnerProductSpace.laplacianWithin f Set.univ = Laplacian.laplacian f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.IsIso φ.τ₂ →
    CategoryTheory.Epi φ.τ₁ →
      ∀ (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
        CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_iff_isClosed_hypograph : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ},
  IsClosed s → (UpperSemicontinuousOn f s ↔ IsClosed {p | p.1 ∈ s ∧ p.2 ≤ f p.1})
-- Lean.CoreM
/-- Cache for the `CoreM` monad  -/
Lean.Core.Cache : Type
-- Mathlib.Algebra.Star.Basic
starAddEquiv_apply : ∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] (a : R), starAddEquiv a = star a
-- Mathlib.Probability.ConditionalProbability
/-- The **law of total probability** for a random variable taking finitely many values: a measure
`μ` can be expressed as a linear combination of its conditional measures `μ[|X ← x]` on fibers of a
random variable `X` valued in a fintype.  -/
ProbabilityTheory.sum_meas_smul_cond_fiber : ∀ {Ω : Type u_1} {α : Type u_3} {m : MeasurableSpace Ω} [inst : Fintype α] [inst_1 : MeasurableSpace α]
  [DiscreteMeasurableSpace α] {X : Ω → α},
  Measurable X →
    ∀ (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ], ∑ x, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}] = μ
-- Mathlib.NumberTheory.ModularForms.QExpansion
SlashInvariantFormClass.periodic_comp_ofComplex : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [SlashInvariantFormClass F Γ k], h ∈ Γ.strictPeriods → Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑h
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeLeftOp_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp),
  (CategoryTheory.Limits.coneOfCoconeLeftOp c).pt = Opposite.op c.pt