mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.PostCond
Std.Do.PostShape.brecOn.eq : ∀ {motive : Std.Do.PostShape → Sort u_1} (t : Std.Do.PostShape)
  (F_1 : (t : Std.Do.PostShape) → Std.Do.PostShape.below t → motive t),
  Std.Do.PostShape.brecOn t F_1 = F_1 t (Std.Do.PostShape.brecOn.go t F_1).2
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Estimate for `log⁺` of a product. See `Real.posLog_mul` for a variant with
only two factors.  -/
Real.posLog_prod : ∀ {α : Type u_1} (s : Finset α) (f : α → ℝ), (∏ t ∈ s, f t).posLog ≤ ∑ t ∈ s, (f t).posLog
-- Mathlib.Algebra.Polynomial.Inductions
/-- A property holds for all polynomials of non-zero `natDegree` with coefficients in a
semiring `R` if it holds for
* `p + a`, with `a ∈ R`, `p ∈ R[X]`,
* `p + q`, with `p, q ∈ R[X]`,
* monomials with nonzero coefficient and non-zero exponent,

with appropriate restrictions on each term.

Note that multiplication is "hidden" in the assumption on monomials, so there is no explicit
multiplication in the statement.
See `degree_pos_induction_on` for a similar statement involving more explicit multiplications.
 -/
Polynomial.natDegree_ne_zero_induction_on : ∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Prop} {f : Polynomial R},
  f.natDegree ≠ 0 →
    (∀ {a : R} {p : Polynomial R}, M p → M (Polynomial.C a + p)) →
      (∀ {p q : Polynomial R}, M p → M q → M (p + q)) →
        (∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((Polynomial.monomial n) a)) → M f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Cumulative number of steps performed by the model search.
The model search is interrupted when this counter reaches the `liaSteps`
configuration threshold, and the solver becomes incomplete.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.steps : Lean.Meta.Grind.Arith.Cutsat.State → ℕ
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.epi_iff_epi_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasPushouts A]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G]
  {Y Z : CategoryTheory.CostructuredArrow G X} (f : Y ⟶ Z), CategoryTheory.Epi f ↔ CategoryTheory.Epi f.left
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.mk.sizeOf_spec : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  [inst_4 : SizeOf G] [inst_5 : SizeOf H] (toAddEquiv : G ≃+ H)
  (continuous_toFun : autoParam (Continuous toAddEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toAddEquiv.invFun) Homeomorph.continuous_invFun._autoParam),
  sizeOf { toAddEquiv := toAddEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    1 + sizeOf toAddEquiv + sizeOf continuous_toFun + sizeOf continuous_invFun
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The span of a union of an indexed family of sets is the sup of their spans.  -/
AffineSubspace.span_iUnion : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_5} (s : ι → Set P), affineSpan k (⋃ i, s i) = ⨆ i, affineSpan k (s i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Complex.cos`.  -/
Complex.hasSum_cos : ∀ (z : ℂ), HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n).factorial) (Complex.cos z)
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddLocalization.Away.addEquivOfQuotient.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {N : Type u_2} [inst_1 : AddCommMonoid N] (x : M)
  (f : AddSubmonoid.LocalizationMap.AwayMap x N),
  AddLocalization.Away.addEquivOfQuotient x f = AddLocalization.addEquivOfQuotient f
-- Mathlib.Probability.CondVar
/-- Conditional variance of a real-valued random variable. It is defined as `0` if any one of the
following conditions is true:
- `m` is not a sub-σ-algebra of `m₀`,
- `volume` is not σ-finite with respect to `m`,
- `X - 𝔼[X | m]` is not square-integrable.  -/
ProbabilityTheory.«termVar[_|_]» : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformlyOn.mul₀_of_isBoundedUnder : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {s : Set X} {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (f y) 0) →
        (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (g y) 0) →
          TendstoLocallyUniformlyOn (F * G) (f * g) l s
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.badVertices.congr_simp : ∀ {α : Type u_1} (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G_1.Adj] (ε ε_1 : ℝ),
      ε = ε_1 →
        ∀ (s s_1 : Finset α),
          s = s_1 →
            ∀ (t t_1 : Finset α), t = t_1 → SimpleGraph.badVertices✝ G ε s t = SimpleGraph.badVertices✝ G_1 ε_1 s_1 t_1
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instAddCommGroup : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → AddCommGroup (QuadraticMap R M N)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_max_of_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a : R} [PosMulMono R] (b c : R),
  0 ≤ a → a * max b c = max (a * b) (a * c)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α} {b : β}, (t.insert a b).getKey! a = a
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.comp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra F} (f : V₀ ⟶ V₁) (g : V₁ ⟶ V₂),
  (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] (a : α),
  (κ.compProd η) a = (κ a).compProd (η.sectR a)
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_primeFactors_card_subset : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G],
  p ≠ 0 → (IsPGroup p G ↔ (Nat.card G).primeFactors ⊆ p.primeFactors)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.mul_subset_mul`.  -/
Set.list_prod_subset_list_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : List ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → (List.map f₁ t).prod ⊆ (List.map f₂ t).prod
-- Mathlib.Algebra.Torsor.Basic
Set.Nonempty.zero_mem_vsub_self : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {s : Set P}, s.Nonempty → 0 ∈ s -ᵥ s
-- Mathlib.Analysis.Normed.Group.Defs
/-- An enormed monoid is an additive monoid endowed with a continuous enorm,
which is positive definite: in other words, this is an `ESeminormedAddMonoid` with a positive
definiteness condition added.  -/
ENormedAddMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Init.Data.Option.Lemmas
Option.join_max : ∀ {α : Type u_1} [inst : Max α] {o o' : Option (Option α)}, (o ⊔ o').join = o.join ⊔ o'.join
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxiLawfulHasSize : ∀ {n : ℕ}, Std.Rxi.LawfulHasSize (BitVec n)
-- Init.Data.UInt.Lemmas
UInt64.ofFin_uint16ToFin : ∀ (n : UInt16), UInt64.ofFin (Fin.castLE UInt16.toFin_toUInt64._proof_1 n.toFin) = n.toUInt64
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_of_not_isNonloop : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isLoop_of_not_isNonloop._auto_1 → ¬M.IsNonloop e → M.IsLoop e
-- Init.Omega.Coeffs
/-- Shim for `IntList.combo`.  -/
Lean.Omega.Coeffs.combo : ℤ → Lean.Omega.Coeffs → ℤ → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.uncurry_singleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (u : Y ⟶ X),
  (CategoryTheory.Presieve.singleton u).uncurry = {⟨Y, u⟩}
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instToJsonCancelParams : Lean.ToJson Lean.Lsp.CancelParams
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.sectionsSubgroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat),
  GrpCat.sectionsSubgroup F =
    { carrier := (F.comp (CategoryTheory.forget GrpCat)).sections, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- A reformulation of `IsCyclotomicExtension` in the case `S` is a singleton.  -/
IsCyclotomicExtension.iff_singleton : ∀ (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b | b ^ n = 1}
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g : G →L[𝕜] H)
  (x : TensorProduct 𝕜 E G), (TensorProduct.mapL f g) x = (TensorProduct.map ↑f ↑g) x
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_eq' : ∀ {α : Type u_1} (y : α) [inst : Fintype { x // y = x }], Fintype.card { x // y = x } = 1
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddMonoid X] [inst_1 : AddMonoid Y] (f : X →+ Y),
  AddMonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuousAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {x : E},
  ContinuousAt (↑I.symm) x
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- **Steinhaus Theorem**.

In any locally compact group `G` with an inner regular Haar measure `μ`,
for any measurable set `E` of positive measure, the set `E / E` is a neighbourhood of `1`.  -/
MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegular] (E : Set G),
  MeasurableSet E → 0 < μ E → E / E ∈ nhds 1
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ioi' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Ioi a).Nonempty → frontier (Set.Ioi a) = {a}
-- Init.Data.SInt.Bitwise
Int32.xor_self : ∀ {a : Int32}, a ^^^ a = 0
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffOn_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E], UniqueDiffOn 𝕜 ∅
-- Mathlib.Logic.Function.Basic
Function.uncurry_flip : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ),
  Function.uncurry (flip f) = Function.uncurry f ∘ Prod.swap
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} {hom : I.cocomplex ⟶ I'.cocomplex}
  {ι_f_zero_comp_hom_f_zero :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)}
  {hom_1 : I.cocomplex ⟶ I'.cocomplex}
  {ι_f_zero_comp_hom_f_zero_1 :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom_1.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)},
  { hom := hom, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero } =
      { hom := hom_1, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero_1 } →
    hom = hom_1
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.mk.sizeOf_spec : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : ⦃X Y : AlgebraicGeometry.Scheme⦄ → (x : X ⟶ Y) → SizeOf (P x)] (I₀ : Type v) (X : I₀ → CommRingCat)
  (f : (j : I₀) → AlgebraicGeometry.Spec (X j) ⟶ S) (idx : ↥S → I₀) (covers : ∀ (x : ↥S), x ∈ Set.range ⇑(f (idx x)))
  (map_prop : autoParam (∀ (j : I₀), P (f j)) AlgebraicGeometry.Scheme.AffineCover.map_prop._autoParam),
  sizeOf { I₀ := I₀, X := X, f := f, idx := idx, covers := covers, map_prop := map_prop } = 1 + sizeOf I₀
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.match_3.eq_3 : ∀ {α : Type u_1} (motive : (x : ℕ) → { l // l.length = x } → Sort u_2) (n : ℕ) (xs : { l // l.length = n + 2 })
  (h_1 : (property : [].length = 0) → motive 0 ⟨[], property⟩)
  (h_2 : (a : α) → (property : [a].length = 1) → motive 1 ⟨[a], property⟩)
  (h_3 : (n : ℕ) → (xs : { l // l.length = n + 2 }) → motive n.succ.succ xs),
  (match n.succ.succ, xs with
    | 0, ⟨[], property⟩ => h_1 property
    | 1, ⟨[a], property⟩ => h_2 a property
    | n.succ.succ, xs => h_3 n xs) =
    h_3 n xs
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom h k) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f h)
        (CategoryTheory.CategoryStruct.comp g k))
      h_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instAddMonoid.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  MonoidAlgebra.instAddMonoid =
    {
      add := fun a a_1 =>
        MonoidAlgebra.coeffEquiv.2 (MonoidAlgebra.coeffEquiv.toFun a + MonoidAlgebra.coeffEquiv.toFun a_1),
      add_assoc := ⋯, zero := MonoidAlgebra.coeffEquiv.2 0, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun a a_1 => MonoidAlgebra.coeffEquiv.2 (a • MonoidAlgebra.coeffEquiv.toFun a_1), nsmul_zero := ⋯,
      nsmul_succ := ⋯ }
-- Init.SizeOf
/-- `SizeOf` is a typeclass automatically derived for every inductive type,
which equips the type with a "size" function to `Nat`.
The default instance defines each constructor to be `1` plus the sum of the
sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the
constructor has a smaller size than the constructor itself,
and in many cases this will suffice to do the proof that a recursive function
is only called on smaller values.
If the default proof strategy fails, it is recommended to supply a custom
size measure using the `termination_by` argument on the function definition.
 -/
SizeOf : Sort u → Sort (max 1 u)
-- Init.Data.String.Basic
/-- Given a string and two valid positions within the string, obtain a slice on the string formed by
the two positions.

This happens to be equivalent to the constructor of `String.Slice`.
 -/
String.slice : (s : String) → (startInclusive endExclusive : s.Pos) → startInclusive ≤ endExclusive → String.Slice
-- Plausible.Testable
Plausible.Testable.iffTestable : {p q : Prop} → [Plausible.Testable (p ∧ q ∨ ¬p ∧ ¬q)] → Plausible.Testable (p ↔ q)
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.self_notMem_Ioi`. -/
Set.notMem_Ioi_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∉ Set.Ioi a
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ}, (Std.HashMap.Raw.emptyWithCapacity c).WF
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_add : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddZeroClass 𝕜] [inst_1 : LE α] (f g : IncidenceAlgebra 𝕜 α), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.of_normalize_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g f' : C}
  {η θ : f ≅ g}
  (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f ≅ f')
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g ≅ f'),
  CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) η ≪≫ η_g = η_f →
    CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) θ ≪≫ η_g = η_f →
      η = θ
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (h : A = B),
  (CategoryTheory.eqToHom h).hom₃ = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.Set.Pairwise.Basic
Pairwise.range_pairwise : ∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α}, Pairwise (Function.onFun r f) → (Set.range f).Pairwise r
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_false : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] (f : False → α), ⨆ (i : False), f i = ⊥
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.ker_map_le_ker_mk_comp_ghostComponent : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] (n : ℕ),
  RingHom.ker (WittVector.map (Ideal.Quotient.mk (Ideal.span {↑p}))) ≤
    RingHom.ker ((Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))).comp (WittVector.ghostComponent n))
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- **Alias** of `OrderIso.lift_cof_congr`. -/
OrderIso.lift_cof_eq : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.needStartLine.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Reader.State.needStartLine = 1
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.aeval_modByMonic_minpoly : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (p : Polynomial A) (x : B),
  (Polynomial.aeval x) (p %ₘ minpoly A x) = (Polynomial.aeval x) p
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_pow_self_iff : ∀ {n k : ℕ}, n ≠ 0 → k ≠ 0 → (n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.mkFreshExprMVarCore : Lean.Expr → Lean.MetavarKind → Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.Group.Basic
topologicalGroup_inf : ∀ {G : Type w} [inst : Group G] {t₁ t₂ : TopologicalSpace G},
  IsTopologicalGroup G → IsTopologicalGroup G → IsTopologicalGroup G
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divRight_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [IsTopologicalGroup H] [inst_3 : PartialOrder H]
  [IsOrderedMonoid H] {c a : H},
  Filter.map (fun x => x / c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a / c) (Set.Ioi (a / c))
-- Mathlib.Tactic.ToFun
/-- Generate an eta-expanded version of a lemma. Adding `@[to_fun]` to a lemma written in "point-free"
form, e.g.
```
theorem Differentiable.mul (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) :
    Differentiable 𝕜 (f * g)
```
will generate a new lemma `Differentiable.fun_mul` with conclusion
`Differentiable 𝕜 fun x => f x * g x`.

You can specify the name of the new declaration manually, as in `@[to_fun Differentiable.fun_mul]`.
If you do so, the newly generated name is namespaced to match the original declaration's name:
tagging `Foo.bar` with `to_fun baz` generates `Foo.baz`;
tagging `Foo.Bar.baz` with `Bars.baz` generates `Foo.Bars.baz`, etc.

Use the `to_fun (attr := ...)` (or `to_fun (attr := ...) new_name`) syntax
to add the same attribute to both declarations.
 -/
Mathlib.Tactic.to_fun : Lean.ParserDescr
-- Lean.Message
Lean.NamingContext.mk.sizeOf_spec : ∀ (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl),
  sizeOf { currNamespace := currNamespace, openDecls := openDecls } = 1 + sizeOf currNamespace + sizeOf openDecls
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight.mk.sizeOf_spec : ∀ (range : Lean.Lsp.Range) (kind? : Option Lean.Lsp.DocumentHighlightKind),
  sizeOf { range := range, kind? := kind? } = 1 + sizeOf range + sizeOf kind?
-- Mathlib.Analysis.Complex.Basic
/-- Linear isometry version of the canonical embedding of `ℝ` in `ℂ`.  -/
Complex.ofRealLI : ℝ →ₗᵢ[ℝ] ℂ
-- Mathlib.Tactic.Tauto
/-- Report places where `tauto` can be replaced by `grind`.  -/
tautoToGrind : Mathlib.TacticAnalysis.Config
-- Mathlib.FieldTheory.IsSepClosed
/-- **Alias** of `IsSepClosed.surjective_domRestrict_of_isSeparable`. -/
IsSepClosed.surjective_restrictDomain_of_isSeparable : ∀ {K : Type u} (L : Type v) {M : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : Field M]
  [inst_4 : Algebra K M] [IsSepClosed M] {E : Type u_1} [inst_6 : Field E] [inst_7 : Algebra K E] [inst_8 : Algebra L E]
  [inst_9 : IsScalarTower K L E] [Algebra.IsSeparable L E], Function.Surjective fun φ => AlgHom.domRestrict L φ
-- Lean.Elab.RecAppSyntax
/-- We store the syntax at recursive applications to be able to generate better error messages
when performing well-founded and structural recursion.

We additionally store the source position as an extra key, so that two recursive applications
that are structurally identical as `Syntax` but originate from different source positions
still produce distinct `MData`. Otherwise hashconsing or simplification can merge them and
attribute an error to the wrong call site (issue #13444).
 -/
Lean.mkRecAppWithSyntax : Lean.Expr → Lean.Syntax → Lean.Expr
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.str : (self : PartOrdEmb) → PartialOrder ↑self
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.add_zero : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.add a (Lean.Grind.Ring.OfSemiring.natCast 0) = a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_inter_eq_size_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size