mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.mono : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  {l : Filter ι} {f : ι → α → E} {g : α → E} {v : Filter ι},
  v ≤ l → MeasureTheory.TendstoInMeasure μ f l g → MeasureTheory.TendstoInMeasure μ f v g
-- Mathlib.Algebra.GradedMonoid
/-- `(*) : A 0 → A 0 → A 0` is the value provided in `GradedMonoid.GMul.mul`, composed with
an `Eq.rec` to turn `A (0 + 0)` into `A 0`.
 -/
GradedMonoid.GradeZero.mul : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddZeroClass ι] → [GradedMonoid.GMul A] → Mul (A 0)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentRegistrationOptions.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentRegistrationOptions
-- Mathlib.Analysis.Fourier.Notation
/-- The Fourier transform as a linear map.  -/
FourierTransform.fourierₗ : (R : Type u_2) →
  (E : Type u_3) →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransform E F] → [FourierAdd E F] → [FourierSMul R E F] → E →ₗ[R] F
-- Init.Data.Fin.Lemmas
Fin.le_rfl : ∀ {n : ℕ} {a : Fin n}, a ≤ a
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Alias** of `ZetaAsymptotics.termSum_one`. -/
ZetaAsymptotics.term_sum_one : ∀ (N : ℕ), ZetaAsymptotics.termSum 1 N = Real.log (↑N + 1) - ↑(harmonic (N + 1)) + 1
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintEmpty : Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Order.SupIndep
/-- If both the index type and the lattice have decidable equality,
then the `SupIndep` predicate is decidable.

TODO: speedup the definition and drop the `[DecidableEq ι]` assumption
by iterating over the pairs `(a, t)` such that `s = Finset.cons a t _`
using something like `List.eraseIdx`
or by generating both `f i` and `(s.erase i).sup f` in one loop over `s`.
Yet another possible optimization is to precompute partial suprema of `f`
over the inits and tails of the list representing `s`,
store them in 2 `Array`s,
then compute each `sup` in 1 operation.  -/
Finset.instDecidableSupIndepOfDecidableEq : {α : Type u_1} →
  {ι : Type u_3} →
    [inst : Lattice α] →
      [inst_1 : OrderBot α] →
        {s : Finset ι} → {f : ι → α} → [DecidableEq ι] → [DecidableEq α] → Decidable (s.SupIndep f)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_set : ∀ {arr : Array Batteries.UFNode} {x : ℕ} {v : Batteries.UFNode} {i : ℕ} {h : x < arr.size},
  Batteries.UnionFind.parentD (arr.set x v h) i = if x = i then v.parent else Batteries.UnionFind.parentD arr i
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.le_tsub_of_add_le_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable a → a + b ≤ c → b ≤ c - a
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsNontrivial.exists_lt_one : ∀ {K : Type u_7} [inst : DivisionRing K] {Γ₀ : Type u_8} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  {v : Valuation K Γ₀} [hv : v.IsNontrivial], ∃ x, x ≠ 0 ∧ v x < 1
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**, combined form.

Let $M$ be a module over a commutative ring $R$. The following are equivalent:
* $M$ is flat.
* For all ideals $I \subseteq R$, the map $I \otimes M \to M$ is injective.
* Every $\sum_i f_i \otimes x_i$ that vanishes in $R \otimes M$ vanishes trivially.
* Every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
* For all finite free modules $R^l$, all elements $f \in R^l$, and all linear maps
  $x \colon R^l \to M$ such that $x(f) = 0$, there exist a finite free module $R^k$ and
  linear maps $a \colon R^l \to R^k$ and $y \colon R^k \to M$ such
  that $x = y \circ a$ and $a(f) = 0$.
 -/
Module.Flat.tfae_equational_criterion : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  [Module.Flat R M, ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I)),
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → TensorProduct.VanishesTrivially R f x,
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → Module.IsTrivialRelation f x,
      ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0].TFAE
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.isCentralScalar : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] [inst_1 : SMul αᵐᵒᵖ β] [IsCentralScalar α β],
  IsCentralScalar α (Set β)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∈ t → (cmp t.min! k).isLE = true
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toSubsemigroup_injective : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], Function.Injective NonUnitalSubring.toSubsemigroup
-- Mathlib.Data.Set.Finite.Lemmas
/-- Induction up to a finite set `S`.  -/
Set.Finite.induction_to : ∀ {α : Type u} {C : Set α → Prop} {S : Set α},
  S.Finite → ∀ S0 ⊆ S, C S0 → (∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) → C S
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(η ◫ ηs) ◫ θ`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompAuxCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.WhiskerRight →
      Mathlib.Tactic.BicategoryLike.HorizontalComp →
        Mathlib.Tactic.BicategoryLike.HorizontalComp →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Order.Category.Semilat
/-- `OrderDual` as a functor.  -/
SemilatInfCat.dual : CategoryTheory.Functor SemilatInfCat SemilatSupCat
-- Init.Data.Order.Factories
/-- Returns a `LawfulOrderMin α` instance given certain properties.

This lemma derives a `LawfulOrderMin α` instance from two properties involving `LE α` and `Min α`
instances.

The produced instance entails `LawfulOrderInf α` and `MinEqOr α`.
 -/
Std.LawfulOrderMin.of_le_min_iff : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α],
  autoParam (∀ (a b c : α), a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c) Std.LawfulOrderMin.of_le_min_iff._auto_1 →
    autoParam (∀ (a b : α), a ⊓ b = a ∨ a ⊓ b = b) Std.LawfulOrderMin.of_le_min_iff._auto_3 → Std.LawfulOrderMin α
-- Mathlib.CategoryTheory.Equivalence
/-- Equivalence of categories is symmetric.  -/
CategoryTheory.Equivalence.symm : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → (D ≌ C)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv_eq.match_1.eq_4 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_4 ()
-- Mathlib.Topology.Sets.Compacts
/-- See Note [custom simps projection].  -/
TopologicalSpace.PositiveCompacts.Simps.coe : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.PositiveCompacts α → Set α
-- Init.Data.List.Impl
List.findRev?.eq_1 : ∀ {α : Type u} (p : α → Bool), List.findRev? p [] = none
-- Init.Data.BitVec.Bitblast
BitVec.uppcRec.congr_simp : ∀ {w : ℕ} (x x_1 : BitVec w), x = x_1 → ∀ (s s_1 : ℕ) (e_s : s = s_1) (hs : s < w), x.uppcRec s hs = x_1.uppcRec s_1 ⋯
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_lt_nonempty : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  0 < N → {n | MeasureTheory.upperCrossingTime a b f N n ω < N}.Nonempty
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Let `M, N` be `R`-modules, `m ≤ M` and `n ≤ N` be an `R`-submodules. Then we have a linear
isomorphism between tensor products of the quotients and the quotient of the tensor product:
`(M ⧸ m) ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N ⊔ M ⊗ n)`.
 -/
TensorProduct.quotientTensorQuotientEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                (m : Submodule R M) →
                  (n : Submodule R N) →
                    TensorProduct R (M ⧸ m) (N ⧸ n) ≃ₗ[R]
                      TensorProduct R M N ⧸
                        (TensorProduct.map m.subtype LinearMap.id).range ⊔
                          (TensorProduct.map LinearMap.id n.subtype).range
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.exists_mul_eq_mul_mul_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), ∃ n, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_rhs_prefix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Lean.Data.Lsp.Extra
/-- `$/lean/rpc/call` client->server request.

A request to execute a procedure bound for RPC.
If an incorrect session ID is present, the server errors with `RpcNeedsReconnect`.

Extends `TextDocumentPositionParams` because in Lean,
symbols exist in the context of a position within a source file
(e.g., `foo` is defined below but not above `def foo`).
We use the position to resolve the set of defined constants,
registered RPC methods, etc.

Both the request and the response may contain `RpcEncodable` data.
It is serialized following the `RpcWireFormat`.
 -/
Lean.Lsp.RpcCallParams : Type
-- Batteries.Data.UInt
UInt32.toNat_max : ∀ (x y : UInt32), (x ⊔ y).toNat = max x.toNat y.toNat
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Dual of `Monotone.covariant_of_const'`  -/
Antitone.covariant_of_const' : ∀ {N : Type u_2} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N}
  [CovariantClass N N (Function.swap μ) fun x1 x2 => x1 ≤ x2], Antitone f → ∀ (m : N), Antitone fun x => f (μ x m)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {he : t ≠ ∅} {km : α}, t.minKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Order.WithBot
WithTop.denselyOrdered : ∀ {α : Type u_1} [inst : LT α] [DenselyOrdered α] [NoMaxOrder α], DenselyOrdered (WithTop α)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F],
  CategoryTheory.Limits.PreservesLimits F.op
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : ChainComplex C ℕ),
  (AlgebraicTopology.DoldKan.N₂.map (CategoryTheory.Idempotents.DoldKan.isoΓ₀.hom.app X)).f =
    AlgebraicTopology.DoldKan.PInfty
-- Lean.Meta.Tactic.NormCast
/-- `addMove decl` adds `decl` as a `move` lemma to be used by `norm_cast`.  -/
Lean.Meta.NormCast.addMove : Lean.Name → optParam Lean.AttributeKind Lean.AttributeKind.global → optParam ℕ 1000 → Lean.MetaM Unit
-- Mathlib.Topology.ShrinkingLemma
/-- Each set from the partially refined family is open.  -/
ShrinkingLemma.PartialRefinement.isOpen : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (self : ShrinkingLemma.PartialRefinement u s p) (i : ι), IsOpen (self.toFun i)
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_zipWith : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  [D : DecidableEq α] {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N},
  (Finsupp.zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
-- Mathlib.Data.Finset.Disjoint
/-- **Alias** of the forward direction of `Finset.disjoint_right`. -/
Disjoint.notMem_of_mem_right_finset : ∀ {α : Type u_2} {s t : Finset α}, Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.RefVec.get.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ}
  (motive : aig.RefVec len → Sort u_1) (refs : Vector Std.Sat.AIG.Fanin len)
  (hrefs : ∀ {i : ℕ} (h : i < len), refs[i].gate < aig.decls.size)
  (h_1 :
    (refs : Vector Std.Sat.AIG.Fanin len) →
      (hrefs : ∀ {i : ℕ} (h : i < len), refs[i].gate < aig.decls.size) → motive { refs := refs, hrefs := hrefs }),
  (match { refs := refs, hrefs := hrefs } with
    | { refs := refs, hrefs := hrefs } => h_1 refs hrefs) =
    h_1 refs hrefs
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage.name : Lean.Doc.ElabImage✝ → Lean.StrLit
-- Init.System.IO
/-- Writes the contents of the string to the stream, followed by a newline.
 -/
IO.FS.Stream.putStrLn : IO.FS.Stream → String → IO Unit
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.edist_comm : ∀ {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x y : α), edist x y = edist y x
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformSpace_comap_restrict_sUnion : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (𝔖 : Set (Set ι)),
  UniformSpace.comap (⋃₀ 𝔖).domRestrict (Pi.uniformSpace fun i => α ↑i) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.domRestrict (Pi.uniformSpace fun i => α ↑i)
-- Lean.Elab.App
/-- Returns the expected type to use for the argument for the current parameter.
Only valid if `fTypeIsForall` has returned `true`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getArgExpectedType : Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.upperBounds_l_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (s : Set α), upperBounds (l '' s) = u ⁻¹' upperBounds s
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Y Y' Z : C}
  [inst_2 : CategoryTheory.ExactPairing Y Y'] (f : Y ⟶ Z),
  (CategoryTheory.tensorRightHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y Y' Z).symm
      (CategoryTheory.CategoryStruct.comp (η_ Y Y') (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = false ↔ ∃ a, a ∈ m)
-- Mathlib.Algebra.BigOperators.Fin
Fin.natAdd.eq_1 : ∀ {m : ℕ} (n : ℕ) (i : Fin m), Fin.natAdd n i = ⟨n + ↑i, ⋯⟩
-- Mathlib.Analysis.Convex.Body
ConvexBody.instPartialOrder : {V : Type u_1} →
  [inst : TopologicalSpace V] → [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → PartialOrder (ConvexBody V)
-- Mathlib.Algebra.DirectSum.Ring
_private.Mathlib.Algebra.DirectSum.Ring.0.DirectSum.one_mul : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (x : DirectSum ι fun i => A i), 1 * x = x
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.liftToPathCategory_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G)
  {X Y : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)} (f : X ⟶ Y),
  (CategoryTheory.Localization.Construction.liftToPathCategory G hG).map f =
    CategoryTheory.composePath
      ({ obj := fun X => G.obj X.obj,
            map := fun {X Y} a =>
              Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }.mapPath
        f)
-- Std.Http.Protocol.H1.Config
/-- Maximum length of chunk extension name (default: 256 bytes).
 -/
Std.Http.Protocol.H1.Config.maxChunkExtNameLength : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_comp_proj : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (i : n),
  CoalgebraStruct.comul ∘ₗ LinearMap.proj i =
    TensorProduct.map (LinearMap.proj i) (LinearMap.proj i) ∘ₗ CoalgebraStruct.comul
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zpow.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : One α] [inst_2 : Mul α] [inst_3 : Inv α],
  Finset.zpow = { pow := fun s n => zpowRec npowRec n s }
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence follows from preserved non-negative distance. Backward direction of
`congruent_iff_nndist_eq`.  -/
Congruent.of_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], (∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.nsmul_subset : ∀ {M : Type u_3} [inst : AddMonoid M] {s : Set M} {S : AddSubmonoid M} {n : ℕ}, s ⊆ ↑S → n • s ⊆ ↑S
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descFOne.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.InjectiveResolution.descFOne f I J =
    ⋯.descToInjective
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descFZero f I J) (I.cocomplex.d 0 1)) ⋯
-- Init.Data.List.Find
List.find?_cons_eq_some : ∀ {α : Type u_1} {a : α} {xs : List α} {p : α → Bool} {b : α},
  List.find? p (a :: xs) = some b ↔ p a = true ∧ a = b ∨ (!p a) = true ∧ List.find? p xs = some b
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateDecImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu →
    Lean.FVarId → ℕ → Bool → Bool → Option ℕ → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Init.WF
Prod.RProd : {α : Type u} → {β : Type v} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- An element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`
if and only if `x` is equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries
`(a, m)` of `p`.
 -/
PiTensorProduct.mem_lifts_iff : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x : PiTensorProduct R fun i => s i) (p : FreeAddMonoid (R × ((i : ι) → s i))),
  p ∈ x.lifts ↔ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr)
  (hfoo : aig.decls.size ≤ (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls.size),
  (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast hfoo
-- Mathlib.GroupTheory.Subgroup.Saturated
AddSubmonoid.NSMulSaturated.eq_1 : ∀ {G : Type u_1} [inst : AddMonoid G] (H : AddSubmonoid G),
  H.NSMulSaturated = ∀ ⦃n : ℕ⦄ ⦃g : G⦄, n • g ∈ H → n = 0 ∨ g ∈ H
-- Init.Data.Vector.Lemmas
Vector.getElem_set_self : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (hi : i < n), (xs.set i x hi)[i] = x
-- Init.Data.Option.Lemmas
Option.pfilter_guard : ∀ {α : Type u_1} {a : α} {p : α → Bool} {q : (a' : α) → Option.guard p a = some a' → Bool},
  (Option.guard p a).pfilter q = if ∃ (h : p a = true), q a ⋯ = true then some a else none
-- Std.Time.Date.PlainDate
/-- Checks if the `PlainDate` is in a leap year.
 -/
Std.Time.PlainDate.inLeapYear : Std.Time.PlainDate → Bool
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The set we are interested in (prime numbers in the residue class `a`) is the same as the support
of `ArithmeticFunction.vonMangoldt.residueClass` restricted to primes (and divided by `n`;
this is how this result is used later).  -/
ArithmeticFunction.vonMangoldt.support_residueClass_prime_div : ∀ {q : ℕ} (a : ZMod q),
  (Function.support fun n => (if Nat.Prime n then ArithmeticFunction.vonMangoldt.residueClass a n else 0) / ↑n) =
    {p | Nat.Prime p ∧ ↑p = a}
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instTypeNameBodyInfo : TypeName Lean.Elab.Term.BodyInfo
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh.eq_1 : ∀ (x : ℝ), Real.sinh x = (Complex.sinh ↑x).re
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Given `iter₁ : Φ.Iteration j₁` and `iter₂ : Φ.Iteration j₂`, with `j₁ ≤ j₂`,
if `k₁ ≤ k₂` are elements such that `k₁ ≤ j₁` and `k₂ ≤ k₂`, then this
is the canonical map `iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {Φ : CategoryTheory.SmallObject.SuccStruct C} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] →
                [inst_5 : WellFoundedLT J] →
                  {j₁ j₂ : J} →
                    (iter₁ : Φ.Iteration j₁) →
                      (iter₂ : Φ.Iteration j₂) →
                        {k₁ k₂ : J} →
                          k₁ ≤ k₂ →
                            (h₁ : k₁ ≤ j₁) → (h₂ : k₂ ≤ j₂) → j₁ ≤ j₂ → (iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- A monad equipped with the ability to construct `NormalExpr` terms.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalExpr : (Type → Type) → Type
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_one : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (p : ENNReal),
  (Matrix.toLpLin p p) 1 = LinearMap.id
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] (M : Matrix m n α), M.conjTranspose.transpose = M.map star
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : MeasureTheory.ComplexMeasure α}
  [c.HaveLebesgueDecomposition μ], c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c