mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insert : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced),
  l.Ordered →
    (Std.DTreeMap.Internal.Impl.insert k v l hlb).impl.toListModel.Perm
      (Std.Internal.List.insertEntry k v l.toListModel)
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult : Type
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.concat.eq_def : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon),
  m₁.concat m₂ =
    match m₁ with
    | Lean.Grind.CommRing.Mon.unit => m₂
    | Lean.Grind.CommRing.Mon.mult pw m₁ => Lean.Grind.CommRing.Mon.mult pw (m₁.concat m₂)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- If `v'` is a quasi-inverse of `v` and `w` is a quasi-inverse of `v ∘ₗ u`, then
`w ∘ₗ v` is a quasi-inverse of `u`.  -/
LinearMap.IsQuasiInverse.of_comp_right : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {v' : V₃ →ₗ[K] V₂} {w : V₃ →ₗ[K] V},
  v'.IsQuasiInverse v → w.IsQuasiInverse (v ∘ₗ u) → (w ∘ₗ v).IsQuasiInverse u
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMkEvalHorizontalCompMonoidalM : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.SetTheory.Ordinal.Notation
/-- Given an ordinal, returns:

* `inl none` for `0`
* `inl (some a)` for `a + 1`
* `inr f` for a limit ordinal `a`, where `f i` is a sequence converging to `a`  -/
ONote.fundamentalSequence : ONote → Option ONote ⊕ (ℕ → ONote)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffAt.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f g : M → G} {x₀ : M},
  ContMDiffAt I' I n f x₀ → ContMDiffAt I' I n g x₀ → ContMDiffAt I' I n (fun x => f x / g x) x₀
-- Mathlib.Lean.Name
/-- This should be exactly the same as `toStringWithToken.maybePseudoSyntax`.  -/
_private.Mathlib.Lean.Name.0.Lean.Name.willRoundTrip.maybePseudoSyntax : Lean.Name → Bool
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.inv_eq : ∀ (p q r : ENNReal) [p.HolderTriple q r], r⁻¹ = p⁻¹ + q⁻¹
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.map_le_one : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → ∀ (x : O), v ((algebraMap O R) x) ≤ 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.eval_ult : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinPred.ult.eval = BitVec.ult
-- Mathlib.Order.Heyting.Hom
instCoeTCHeytingHomOfHeytingHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : HeytingAlgebra α] → [inst_2 : HeytingAlgebra β] → [HeytingHomClass F α β] → CoeTC F (HeytingHom α β)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 0th object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
to `A` as a `k`-module.  -/
groupCohomology.cochainsIso₀ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → (groupCohomology.inhomogeneousCochains A).X 0 ≅ ModuleCat.of k ↑A
-- Lean.Language.Basic
/-- Creates a snapshot task from the syntax processed by the task and a `BaseIO` action.  -/
Lean.Language.SnapshotTask.ofIO : {α : Type} →
  (stx? : Option Lean.Syntax) →
    Option IO.CancelToken →
      optParam Lean.Language.SnapshotTask.ReportingRange (Lean.Language.SnapshotTask.defaultReportingRange stx?) →
        BaseIO α → BaseIO (Lean.Language.SnapshotTask α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (I₀ : Type w) → (X : I₀ → C) → ((i : I₀) → X i ⟶ S) → CategoryTheory.PreZeroHypercover S
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (AlgebraicGeometry.PresheafedSpace.forget C)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toLinearMap₁₂_inj : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G),
  ContinuousLinearMap.toLinearMap₁₂ L₁ = ContinuousLinearMap.toLinearMap₁₂ L₂ ↔ L₁ = L₂
-- Mathlib.CategoryTheory.Action
/-- Given `G` acting on `X`, a functor from the corresponding action groupoid to a group `H`
can be curried to a group homomorphism `G →* (X → H) ⋊ G`.  -/
CategoryTheory.ActionCategory.curry : {X : Type u} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {H : Type u_3} →
          [inst_2 : Group H] →
            CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H) →
              G →* (X → H) ⋊[mulAutArrow] G
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.prependNode.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (z : Lean.PersistentHashMap.Zipper α β)
  (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  Lean.PersistentHashMap.Zipper.prependNode (Lean.PersistentHashMap.Node.entries es) z =
    Lean.PersistentHashMap.Zipper.consEntries es.toSubarray z
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℕ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.natCast n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.intCast n => h_2 n
    | Lean.Grind.CommRing.Expr.natCast n => h_3 n
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | x => h_5 x) =
    h_3 n
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_signExtend : ∀ {w : ℕ} {x : BitVec w} {v i : ℕ},
  (BitVec.signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformity_eq : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ V ∈ uniformity β, Filter.principal (UniformOnFun.gen 𝔖 s V)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasForget₂ContinuousLinearMapIdCarrierModuleCatLinearMap : (R : Type u) →
  [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.HasForget₂ (TopModuleCat R) (ModuleCat R)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEquiv_isBasis_iff : ∀ {α : Type u_3} {β : Type u_4} {M : Matroid α} (f : α ≃ β) {I X : Set β},
  (M.mapEquiv f).IsBasis I X ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_left : ∀ {α : Type u_2} {s t : Finset α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
-- Init.Data.List.Attach
List.pmap_ne_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) {xs : List α} (H : ∀ a ∈ xs, P a),
  List.pmap f xs H ≠ [] ↔ xs ≠ []
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_add₃_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b c : E}, ‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsSFiniteKernelSectLOfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel (κ.sectL b)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] {f g : A →⋆ₙₐ[R] B}, f = g ↔ ∀ (x : A), f x = g x
-- Init.Data.Float.Model.Float32
/-- Returns `true` if the float represents a real number, i.e., it is neither infinite nor `NaN`.
 -/
Float32.Model.isFinite : Float32.Model → Bool
-- Init.Data.Rat.Basic
/-- The floor of a rational number `a` is the largest integer less than or equal to `a`.  -/
Rat.floor : ℚ → ℤ
-- Mathlib.NumberTheory.NumberField.AdeleRing
/-- `𝔸ᶠ[K]` is notation for `IsDedekindDomain.FiniteAdeleRing (𝓞 K) K`.  -/
NumberField.AdeleRing.«term𝔸ᶠ[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.LieEquiv.ofCoboundary_toFun : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c c' : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : LieModule.Cohomology.oneCochain R L M)
  (h : ↑c' = ↑c + (LieModule.Cohomology.d₁₂ R L M) x) (y : LieAlgebra.ofTwoCocycle c),
  (LieAlgebra.LieEquiv.ofCoboundary c c' x h) y =
    (LieAlgebra.ofProd c')
      (((LieAlgebra.ofProd c).symm y).1, ((LieAlgebra.ofProd c).symm y).2 - x ((LieAlgebra.ofProd c).symm y).1)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instSubsingleton : ∀ {M : Type u_1} [Subsingleton M], Subsingleton (ArchimedeanOrder M)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z)
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.divMod_zero_left : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I J : FractionalIdeal (nonZeroDivisors R) K},
  I.divMod 0 J = 0
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_injective : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i),
  Function.Injective ⇑(DirectSum.lmap f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)
-- Mathlib.Data.Set.Restrict
Set.codRestrict.congr_simp : ∀ {α : Type u_1} {ι : Sort u_5} (f f_1 : ι → α) (e_f : f = f_1) (s : Set α) (h : ∀ (x : ι), f x ∈ s) (a a_1 : ι),
  a = a_1 → Set.codRestrict f s h a = Set.codRestrict f_1 s ⋯ a_1
-- Mathlib.Algebra.GCDMonoid.Basic
isUnit_gcd_one_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α), IsUnit (gcd a 1)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.singletonSubgraph_le_iff : ∀ {V : Type u} {G : SimpleGraph V} (v : V) (H : G.Subgraph), G.singletonSubgraph v ≤ H ↔ v ∈ H.verts
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.fourierInv_apply_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  (f : SchwartzMap V E),
  FourierTransformInv.fourierInv f =
    (SchwartzMap.compCLMOfContinuousLinearEquiv ℂ ↑(LinearIsometryEquiv.neg ℝ)) (FourierTransform.fourier f)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.true_intro_simp : ∀ {σs : List (Type u)} {Q : Std.Do.SPred σs}, Q ⊢ₛ ⌜True⌝ ↔ True
-- Mathlib.Order.BourbakiWitt
instSetLikeNonemptyChain : {α : Type u_4} → [inst : LE α] → SetLike (NonemptyChain α) α
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.union_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t u : Set X},
  SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.instCategorySubterminals : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Category.{v₁, u₁} (CategoryTheory.Subterminals C)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.unramifiedPlacesOver.eq_1 : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.unramifiedPlacesOver L v = {w | w.LiesOver v ∧ NumberField.InfinitePlace.IsUnramified K w}
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
/-- **The Schröder-Bernstein Theorem**:
Given injections `α → β` and `β → α`, we can get a bijection `α → β`.  -/
Function.Embedding.schroeder_bernstein : ∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
  Function.Injective f → Function.Injective g → ∃ h, Function.Bijective h
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.antitone_lower : ∀ {ι : Type u_1}, Antitone fun I => I.lower
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_3.eq_2 : ∀ (s : String.Slice)
  (motive :
    Std.IterStep (Std.IterM Id (String.Slice.Pattern.SearchStep s)) (String.Slice.Pattern.SearchStep s) → Sort u_1)
  (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
      (out : String.Slice.Pattern.SearchStep s) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) → motive (Std.IterStep.skip it'))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Init.Data.List.Lemmas
List.last_eq_of_concat_eq : ∀ {α : Type u_1} {a b : α} {l₁ l₂ : List α}, l₁.concat a = l₂.concat b → a = b
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.implicitFunction_apply_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (x : E) in nhds φ.pt, φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_mul : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)] (i : I) (x y : f i),
  Pi.mulSingle i (x * y) = Pi.mulSingle i x * Pi.mulSingle i y
-- Batteries.Data.Array.Merge
/-- Auxiliary definition for `mergeUnsortedDedup`.  -/
Array.mergeUnsortedDedup.go : {α : Type u_1} → [eq : BEq α] → Array α → Array α → Array α
-- Init.Data.UInt.Lemmas
UInt16.lt_one_iff : ∀ {a : UInt16}, a < 1 ↔ a = 0
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.mwd.sizeOf_spec : ∀ (month : Std.Time.Month.Ordinal) (week : Std.Time.Week.Aligned.Ordinal) (day : Std.Time.Weekday.Ordinal),
  sizeOf (Std.Time.TimeZone.TransitionSpec.mwd month week day) = 1 + sizeOf month + sizeOf week + sizeOf day
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_zero : ∀ (n : ℤ), n >>> 0 = n
-- Aesop.RuleTac.Basic
Aesop.RuleTacOutput.applications : Aesop.RuleTacOutput → Array Aesop.RuleApplication
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- By `infer_instance` for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.finite_locoalization : ∀ {S : Type u_2} [inst : CommRing S] (q : Ideal S) [inst_1 : q.IsPrime] {K : Type u_4} [inst_2 : Field K]
  [inst_3 : Algebra K S] [Algebra.WeaklyQuasiFiniteAt K q], Module.Finite K (Localization.AtPrime q)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmop_hom_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ), (β_ X Y).hom.unmop = (β_ Y.unmop X.unmop).hom
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
  (a : A ⟶ (CategoryTheory.Monad.comparison adj).obj B),
  (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B).symm a =
    (((adj.homEquiv A.A B).symm.subtypeEquiv ⋯).trans
        (CategoryTheory.Limits.Cofork.IsColimit.homIso
            (CategoryTheory.Limits.colimit.isColimit
              (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))))
            B).symm)
      ({ toFun := fun f => ⟨f.f, ⋯⟩, invFun := fun g => { f := ↑g, h := ⋯ }, left_inv := ⋯, right_inv := ⋯ } a)
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_surjective : ∀ {α : Type u_1}, Function.Surjective ⇑SymAlg.sym
-- Mathlib.Tactic.Linter.TextBased
/-- Possible results of comparing an `ErrorContext` to an `existing` entry:
most often, they are different --- if the existing entry covers the new exception,
depending on the error, we prefer the new or the existing entry.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ComparisonResult : Type
-- Mathlib.Data.Multiset.Interval
Multiset.Icc_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Finset.Icc s t =
    Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.Icc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))
-- Init.Sym.Simp.SimprocDSL
Lean.Parser.Category.sym_discharger : Lean.Parser.Category
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_mk : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : Subalgebra R A)
  (h : ∀ {a : A}, a ∈ S.carrier → star a ∈ S.carrier), ↑{ toSubalgebra := S, star_mem' := h } = ↑S
-- Mathlib.Lean.Elab.InfoTree
/-- Traverses an `InfoTree` to collect `TryThisInfo` suggestions.  -/
Lean.Elab.collectTryThisSuggestions.go : Array Lean.Meta.Tactic.TryThis.Suggestion → Lean.Elab.InfoTree → Array Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Monotone.mul_const : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [MulPosMono M₀], Monotone f → 0 ≤ a → Monotone fun x => f x * a
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey : Hashable Lean.Elab.Tactic.Grind.DSimpCacheKey
-- Mathlib.Algebra.Module.Lattice
/-- A finitely-generated `R`-submodule of `V` of rank at least the `K`-rank of `V`
is a lattice.  -/
Submodule.IsLattice.of_rank_le : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module K V] [inst_5 : Module R V] [inst_6 : IsScalarTower R K V] [IsDomain R]
  [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V},
  M.FG → Module.rank K V ≤ Module.rank R ↥M → Submodule.IsLattice K M
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.addAndCompileNonRec : Lean.LocalContext × Lean.LocalInstances →
  (preDef : Lean.Elab.PreDefinition) →
    optParam (List Lean.Name) [preDef.declName] → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_def : ∀ {o : ONote} {x : Option ONote ⊕ (ℕ → ONote)} (e : o.fundamentalSequence = x),
  o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i => a.fastGrowing^[i] i
    | Sum.inr f, x => fun i => (f i).fastGrowing i
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.coeff_toLaurent : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  (Polynomial.toLaurent f).coeff = Finsupp.mapDomain (⇑Nat.castEmbedding) f.toFinsupp.coeff
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.PlausibleStep.skip : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {it' : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it') →
    Std.Iterators.Types.Drop.PlausibleStep it (Std.IterStep.skip (Std.IterM.drop it.internalState.remaining it'))
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.pi_norm_sq : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] (x : WithCStarModule A ((i : ι) → E i)),
  ‖x‖ ^ 2 = ‖∑ i, inner A (x i) (x i)‖
-- Mathlib.Data.Multiset.Count
Multiset.countP_pos : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α}, 0 < Multiset.countP p s ↔ ∃ a ∈ s, p a
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inlₗ.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.inlₗ α β =
    { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderMonoidHom.inl α β)).toFun, map_one' := ⋯, map_mul' := ⋯,
      monotone' := ⋯ }
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp P.p.f f.f.f = CategoryTheory.CategoryStruct.comp f.f.f Q.p.f