mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.DTreeMap.Raw.mergeWith : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] →
        ((a : α) → β a → β a → β a) → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_union_le_size_add_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- The **Plünnecke-Ruzsa inequality**. Subtraction version.  -/
Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (m n : ℕ), ↑(m • B - n • B).card ≤ (↑(A - B).card / ↑A.card) ^ (m + n) * ↑A.card
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKey! k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.prodMkLeft γ κ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJNe0Or1728_c₄ : ∀ {R : Type u_1} [inst : CommRing R] (j : R), (WeierstrassCurve.ofJNe0Or1728 j).c₄ = j * (j - 1728) ^ 3
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `Polynomial.Gal.restrictProd` is actually a subgroup embedding.  -/
Polynomial.Gal.restrictProd_injective : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F), Function.Injective ⇑(Polynomial.Gal.restrictProd p q)
-- Init.Control.Basic
/-- Maps a function over a functor, with parameters swapped so that the function comes last.

This function is `Functor.map` with the parameters reversed, typically used via the `<&>` operator.


Conventions for notations in identifiers:

 * The recommended spelling of `<&>` in identifiers is `mapRev`. -/
«term_<&>_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.colimit_toColimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasColimit F] (hF : ∀ (j : J), P (F.obj j)),
  (CategoryTheory.ObjectProperty.ColimitOfShape.colimit F hF).toColimitPresentation =
    CategoryTheory.Limits.ColimitPresentation.colimit F
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y z : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (e : x = y) (e' : y = z),
  AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e ≪≫ AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e' =
    AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Iio_natAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.natAdd m ⁻¹' Set.Iio (Fin.natAdd m i) = Set.Iio i
-- Mathlib.Data.Set.Sups
Set.Nonempty.sups : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α}, s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.const.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Tactic.NormNum.BigOperators
/-- The set is zero.  -/
Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero : {u : Lean.Level} →
  {α : Q(Type u)} → {s : Q(Multiset «$α»)} → Q(«$s» = 0) → Mathlib.Meta.Multiset.ProveZeroOrConsResult s
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_sum_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_3}
  {f : ι → E → F} {u : Finset ι} {n : ℕ} {x : E},
  (∀ j ∈ u, ContDiffAt 𝕜 (↑n) (f j) x) → iteratedFDeriv 𝕜 n (∑ j ∈ u, f j) x = ∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (x : N), (AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.inr x) = g x
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinderHom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (p : (CategoryTheory.PreOneHypercover.cylinder f g).I₀),
  (CategoryTheory.PreOneHypercover.cylinderHom f g).h₀ p =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯)
      (F.toPullback p.snd)
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetsResponse.mk.injEq : ∀ (widgets widgets_1 : Array Lean.Widget.PanelWidgetInstance),
  ({ widgets := widgets } = { widgets := widgets_1 }) = (widgets = widgets_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCallsParams : Type
-- Init.Data.Iterators.ToIterator
Std.ToIterator.mk : {γ : Type u} → {m : Type w → Type w'} → {α β : outParam (Type w)} → (γ → Std.IterM m β) → Std.ToIterator γ m α β
-- Mathlib.Algebra.Group.Defs
/-- A mixin for left cancellative multiplication.  -/
IsLeftCancelMul : (G : Type u) → [Mul G] → Prop
-- Init.Data.BitVec.Lemmas
/-- A bitvector is upper bounded by the number of leading zeroes.  -/
BitVec.toNat_lt_two_pow_sub_clz : ∀ {w : ℕ} {x : BitVec w}, x.toNat < 2 ^ (w - x.clz.toNat)
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_mul : ∀ (a b : BitVec 32), { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instFiniteResidueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (P : Ideal R) [inst_4 : P.IsPrime] (Q : Ideal S) [inst_5 : Q.IsPrime]
  [inst_6 : Q.LiesOver P] [inst_7 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q], Module.Finite P.ResidueField Q.ResidueField
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.hasNestedActionsToLift : Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.NatIso.pi'_inv : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {E : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} E] {F G : CategoryTheory.Functor E ((i : I) → C i)}
  (e : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ≅ G.comp (CategoryTheory.Pi.eval C i)),
  (CategoryTheory.NatIso.pi' e).inv = CategoryTheory.NatTrans.pi' fun i => (e i).inv
-- Init.Data.Array.Extract
Array.le_of_extract_eq_self : ∀ {α : Type u_1} {i j : ℕ} {as : Array α}, as.extract i j = as → as.size ≤ j
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) (i : ι) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.π i) (CategoryTheory.CategoryStruct.comp (f i) h) =
    CategoryTheory.CategoryStruct.comp s.base h
-- Mathlib.Algebra.Order.Group.PosPart
Pi.negPart_apply : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → AddGroup (α i)]
  (f : (i : ι) → α i) (i : ι), f⁻ i = (f i)⁻
-- Mathlib.Algebra.Field.Rat
NNRatCast.ofScientific_eq_ite : ∀ {K : Type u_1} [inst : NNRatCast K] (m : ℕ) (b : Bool) (d : ℕ),
  OfScientific.ofScientific m b d = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone.
It only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.PushoutCocone.isColimitAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          (t : CategoryTheory.Limits.PushoutCocone f g) →
            (desc : (s : CategoryTheory.Limits.PushoutCocone f g) → t.pt ⟶ s.pt) →
              (∀ (s : CategoryTheory.Limits.PushoutCocone f g),
                  CategoryTheory.CategoryStruct.comp t.inl (desc s) = s.inl) →
                (∀ (s : CategoryTheory.Limits.PushoutCocone f g),
                    CategoryTheory.CategoryStruct.comp t.inr (desc s) = s.inr) →
                  (∀ (s : CategoryTheory.Limits.PushoutCocone f g) (m : t.pt ⟶ s.pt),
                      (∀ (j : CategoryTheory.Limits.WalkingSpan),
                          CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) →
                        m = desc s) →
                    CategoryTheory.Limits.IsColimit t
-- Batteries.Control.Nondet.Basic
/-- Apply a function to each alternative in a `Nondet m α` .  -/
Nondet.map : {σ : Type} →
  {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α β : Type} → (α → β) → Nondet m α → Nondet m β
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousAt.div₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α] {a : α},
  ContinuousAt f a → ContinuousAt g a → g a ≠ 0 → ContinuousAt (fun x => f x / g x) a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.of_dist_le_pow : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α},
  (∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n) →
    Tactic.ComputeAsymptotics.Seq.FriendlyOperation op
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.smul_eq_C_mul : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (r : K) (x : RatFunc K), r • x = RatFunc.C r * x
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.ofSeq.eq_1 : ∀ {α : Type u}, Stream'.WSeq.ofSeq = (fun x1 x2 => x1 <$> x2) some
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instAddCommMonoid : {ι : Type u_1} → {M : Type u_3} → [inst : AddCommMonoid M] → AddCommMonoid (ι →₀ M)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.computeSize.eq_1 : ∀ {α : Type u} {β : α → Type v} (buckets : Array (Std.DHashMap.Internal.AssocList α β)),
  Std.DHashMap.Internal.computeSize buckets = Array.foldl (fun d b => d + b.length) 0 buckets
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.ne_zero : ∀ {R : Type u} [inst : CommSemiring R] [Nontrivial R] {f : Polynomial R}, f.Separable → f ≠ 0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonUnitalSemiringOfIsTopologicalSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalSemiring β] → [IsTopologicalSemiring β] → NonUnitalSemiring C(α, β)
-- Batteries.Data.List.Perm
List.Perm.idxBij.congr_simp : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs ys : List α} (h : xs.Perm ys) (a a_1 : Fin xs.length),
  a = a_1 → h.idxBij a = h.idxBij a_1
-- Mathlib.MeasureTheory.Measure.Complex
/-- The complex measures form an equivalence to the type of pairs of signed measures.  -/
MeasureTheory.ComplexMeasure.equivSignedMeasure : {α : Type u_1} →
  {m : MeasurableSpace α} →
    MeasureTheory.ComplexMeasure α ≃ MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- `f` composed with `0` is `0`  -/
CategoryTheory.Limits.HasZeroMorphisms.comp_zero : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp f 0 = 0
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn.eq_1 : ∀ {α : Type u_1} (I E : Set α), Matroid.uniqueBaseOn I E = (Matroid.freeOn I).restrict E
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.head_sub : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] (a b : Fin n.succ → α),
  Matrix.vecHead (a - b) = Matrix.vecHead a - Matrix.vecHead b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyPrepareParams.toTextDocumentPositionParams : Lean.Lsp.CallHierarchyPrepareParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.finite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {ι : Type u_1} {f : ι → M}, LinearIndependent R f → Finite ι
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.get! (t.minD fallback) = t.minD fallback
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.toAddSubmonoid_inj : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p q : Submodule R M},
  p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.lid_tmul : ∀ {R : Type u_5} {P : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid P] [inst_2 : Module R P]
  [inst_3 : Coalgebra R P] (r : R) (a : P), (Coalgebra.TensorProduct.lid R P) (r ⊗ₜ[R] a) = r • a
-- Mathlib.Order.Category.BddOrd
/-- Typecheck a `BoundedOrderHom` as a morphism in `BddOrd`.  -/
BddOrd.ofHom : {X Y : Type u} →
  [inst : PartialOrder X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : PartialOrder Y] → [inst_3 : BoundedOrder Y] → BoundedOrderHom X Y → (BddOrd.of X ⟶ BddOrd.of Y)
-- Mathlib.Analysis.Seminorm
Seminorm.instAddMonoid : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → AddMonoid (Seminorm 𝕜 E)
-- Mathlib.Topology.Algebra.ConstMulAction
Topology.IsInducing.continuousConstVAdd : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α] {N : Type u_4}
  {β : Type u_5} [inst_3 : VAdd N β] [inst_4 : TopologicalSpace β] {g : β → α},
  Topology.IsInducing g → ∀ (f : N → M), (∀ {c : N} {x : β}, g (c +ᵥ x) = f c +ᵥ g x) → ContinuousConstVAdd N β
-- Mathlib.Tactic.DeriveEncodable
/-- Assuming all of the auxiliary definitions exist, create all the `instance` commands
for the `ToExpr` instances for the (mutual) inductive type(s).  -/
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkEncodableInstanceCmds : Lean.Elab.Deriving.Context →
  Array Lean.Name → Array Lean.Name → Array Lean.Name → Lean.Elab.TermElabM (Array Lean.Command)
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.autEmbedding_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  (σ : CategoryTheory.Aut F) (X : C), (CategoryTheory.PreGaloisCategory.autEmbedding F) σ X = CategoryTheory.Iso.app σ X
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_symm_apply : ∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)),
  ↑(PartialEquiv.pi ei).symm = fun f i => ↑(ei i).symm (f i)
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.algebraMap_isLocalHom_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  (IsLocalRing.maximalIdeal R).FG → IsLocalHom (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))
-- Mathlib.Algebra.Group.Action.TypeTags
toAdd_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (a : Multiplicative α) (b : β), Multiplicative.toAdd a +ᵥ b = a • b
-- Mathlib.Algebra.FreeMonoid.UniqueProds
/-- Any `FreeMonoid` has the `TwoUniqueProds` property.  -/
FreeMonoid.instTwoUniqueProds : ∀ {κ : Type u_1}, TwoUniqueProds (FreeMonoid κ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensRangeParams.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokensRangeParams
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_mul_left : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, 0 < b → a ≤ a * b
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.map_ne_zero_iff : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M},
  e x ≠ 0 ↔ x ≠ 0
-- Mathlib.LinearAlgebra.Quotient.Pi
/-- The quotient of a direct sum is the direct sum of quotients.  -/
Submodule.quotientPi : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {Ms : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommGroup (Ms i)] →
          [inst_2 : (i : ι) → Module R (Ms i)] →
            [Fintype ι] →
              [DecidableEq ι] →
                (p : (i : ι) → Submodule R (Ms i)) →
                  (((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p) ≃ₗ[R] (i : ι) → Ms i ⧸ p i
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_2 : ∀ (k : ℕ),
  Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.zero = fun n => do
    guard (n ≤ k)
    pure 0
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_I : Complex.I.sqrt = ↑√2⁻¹ * (1 + Complex.I)
-- Batteries.Data.Fin.Lemmas
/-- **Alias** of `Fin.isNone_find?_iff`. -/
Fin.find?_isNone_iff : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.find? p).isNone = true ↔ ∀ (i : Fin n), p i = false
-- Mathlib.Order.Compare
toDual_compares_toDual : ∀ {α : Type u_1} [inst : LT α] {a b : α} {o : Ordering},
  o.Compares (OrderDual.toDual a) (OrderDual.toDual b) ↔ o.Compares b a
-- Aesop.Tree.Data
Aesop.Goal.currentGoal : Aesop.Goal → Lean.MVarId
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.lt_iff : ∀ {α : Type u} (self : Std.Packages.PreorderOfLEArgs α),
  let this := self.le;
  let this_1 := self.lt;
  ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Std.Internal.Do.WP.Frame
/-- `PreservesSup.le_frameClosure` at the `wp` layer: when `x` frames every resource `r`, landing
below `wp x Q E` suffices to land below the frame closure of `wp x · E`.  -/
Std.Internal.Do.WP.Frames.le_frameClosure : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {R : Type t}
  (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] {x : Prog},
  (∀ (r : R), Std.Internal.Do.WP.Frames op x r) →
    ∀ {Q : Value → Pred} {E : EPred} {pre : Pred},
      Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x Q E) →
        Lean.Order.PartialOrder.rel pre (Lean.Order.PreservesSup.frameClosure op (fun Q => Std.Internal.Do.wp x Q E) Q)
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.disjoint_lsingle_lsingle : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s t : Set α), Disjoint s t → Disjoint (⨆ a ∈ s, (Finsupp.lsingle a).range) (⨆ a ∈ t, (Finsupp.lsingle a).range)
-- Init.Internal.Order.Basic
Lean.Order.fun_csup_eq : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.CCPO (β x)] (c : ((x : α) → β x) → Prop)
  (hc : Lean.Order.chain c), Lean.Order.fun_csup c hc = Lean.Order.CCPO.csup hc
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instIsLeftAdjointOfComonadicLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) [CategoryTheory.ComonadicLeftAdjoint L], L.IsLeftAdjoint
-- Mathlib.LinearAlgebra.AffineSpace.Slope
/-- `slope f a c` is a linear combination of `slope f a b` and `slope f b c`. This version
explicitly provides coefficients. If `a ≠ c`, then the sum of the coefficients is `1`, so it is
actually an affine combination, see `lineMap_slope_slope_sub_div_sub`.  -/
sub_div_sub_smul_slope_add_sub_div_sub_smul_slope : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b c : k),
  ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.lift_comp_toCotangent : ∀ {R : Type u} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal S}
  {M : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0),
  Ideal.Cotangent.lift f hf ∘ₗ ↑R I.toCotangent = f
-- Init.PropLemmas
instDecidablePredComp : {α : Sort u_1} → {p : α → Prop} → {α_1 : Sort u_2} → {f : α_1 → α} → [DecidablePred p] → DecidablePred (p ∘ f)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Negation on an additive topological group, as a uniform equivalence between the
right uniformity and the left uniformity.  -/
UniformEquiv.neg : (G : Type u_1) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalAddGroup G] → G ≃ᵤ G
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
MeasureTheory.Measure.addHaarScalarFactor.congr_simp : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ'_1 : MeasureTheory.Measure G) (e_μ' : μ' = μ'_1)
  (μ μ_1 : MeasureTheory.Measure G) (e_μ : μ = μ_1) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant],
  μ'.addHaarScalarFactor μ = μ'_1.addHaarScalarFactor μ_1
-- Mathlib.Data.ENat.Basic
ENat.one_lt_top : 1 < ⊤
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying `MulHom`.  -/
Semigrp.Hom.hom' : {A B : Semigrp} → A.Hom B → ↑A →ₙ* ↑B
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoMod hp (a + ↑m * p) b = toIcoMod hp a b + ↑m * p