mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.one_zsmul : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.zsmul 1 a = a
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- Given a continuous linear isomorphism between the domains,
generate a continuous linear isomorphism between the spaces of continuous alternating maps.

This is `ContinuousAlternatingMap.compContinuousLinearMap` as an equivalence,
and is the continuous version of `AlternatingMap.domLCongr`.  -/
ContinuousLinearEquiv.continuousAlternatingMapCongrLeft : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {E' : Type u_3} →
      {F : Type u_4} →
        {ι : Type u_6} →
          [inst : NormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : Module 𝕜 E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : AddCommGroup E'] →
                    [inst_5 : Module 𝕜 E'] →
                      [inst_6 : TopologicalSpace E'] →
                        [inst_7 : AddCommGroup F] →
                          [inst_8 : Module 𝕜 F] →
                            [inst_9 : TopologicalSpace F] →
                              [inst_10 : IsTopologicalAddGroup F] →
                                [inst_11 : ContinuousConstSMul 𝕜 F] →
                                  (E ≃L[𝕜] E') → E [⋀^ι]→L[𝕜] F ≃L[𝕜] E' [⋀^ι]→L[𝕜] F
-- Lean.Parser.Syntax
Lean.Parser.Command.macroRhs.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_apply_iterate : ∀ {α : Type u_1} {f : α → α} {x : α},
  x ∈ Function.periodicPts f → ∀ (n : ℕ), Function.minimalPeriod f (f^[n] x) = Function.minimalPeriod f x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeHomEquiv_freeMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I J_1 : Type u} (f : I → J_1),
  (SheafOfModules.free J_1).freeHomEquiv (SheafOfModules.freeMap f) = SheafOfModules.freeSection ∘ f
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
/-- **Alias** of `MeasureTheory.memLp_finsetSum'`. -/
MeasureTheory.memLp_finset_sum' : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : MeasureTheory.Measure α} [ContinuousAdd ε'] {ι : Type u_5}
  (s : Finset ι) {f : ι → α → ε'}, (∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) → MeasureTheory.MemLp (∑ i ∈ s, f i) p μ
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_pos : ∀ {o : Ordinal.{u_1}}, 0 < Cardinal.preAleph o ↔ 0 < o
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_iSup : ∀ {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : TopologicalSpace N] [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N]
  (f : ι → ClosedSubmodule R N), ↑(⨆ i, f i) = closure (⨆ i, ↑(f i)).carrier
-- Lean.Parser.Types
Lean.Parser.adaptCacheableContextFn : (Lean.Parser.CacheableParserContext → Lean.Parser.CacheableParserContext) → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.instRefl : ∀ {α : Type u_1} {x : MeasurableSpace α}, Std.Refl fun x1 x2 => x1.AbsolutelyContinuous x2
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 →
    ∀ (signs signs_1 : Finset (Fin (n + 1))),
      signs = signs_1 →
        ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.excenterWeightsUnnorm signs i = s_1.excenterWeightsUnnorm signs_1 i_1
-- Init.Data.Format.Instances
instToFormatOption : {α : Type u} → [Std.ToFormat α] → Std.ToFormat (Option α)
-- Batteries.Data.AssocList
/-- `O(n)`. Remove the first entry in the list with key equal to `a`.  -/
Batteries.AssocList.eraseP : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → Batteries.AssocList α β → Batteries.AssocList α β
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.any_iff : ∀ {α : Type u_1} {p : α → Bool} {t : RBTree.RBNode α},
  RBTree.RBNode.any p t = true ↔ RBTree.RBNode.Any (fun x => p x = true) t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff! m₂) k = default
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- If a group has `UniqueProds`, then it actually has `TwoUniqueProds`.
For an example of a semigroup `G` embeddable into a group that has `UniqueProds`
but not `TwoUniqueProds`, see Example 10.13 in
[J. Okniński, *Semigroup Algebras*][Okninski1991].  -/
UniqueProds.toTwoUniqueProds_of_group : ∀ {G : Type u_1} [inst : Group G] [UniqueProds G], TwoUniqueProds G
-- Mathlib.Order.Max
Subsingleton.isMin : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α] (a : α), IsMin a
-- Init.Data.SInt.Lemmas
Int16.zero_div : ∀ {a : Int16}, 0 / a = 0
-- Mathlib.Algebra.Group.Units.Defs
isUnit_one : ∀ {M : Type u_1} [inst : Monoid M], IsUnit 1
-- Mathlib.Logic.Relation
/-- `ReflTransGen r`: reflexive transitive closure of `r`  -/
Relation.ReflTransGen : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.MemLp.toLp_const : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E),
  MeasureTheory.MemLp.toLp (fun x => c) ⋯ = (MeasureTheory.Lp.const p μ) c
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.smul_inv_mem_fixedBy_iff_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α} {g : G},
  g⁻¹ • a ∈ MulAction.fixedBy α g ↔ a ∈ MulAction.fixedBy α g
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Equation (11.3.8) from Cohn's proof, viewed as an equation of polynomials with coefficients
in `K⟮X⟯`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₀_mul_Φ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ →
    RatFunc.Luroth.Q₀✝ E * Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.Luroth.Φ✝ E) =
      Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.Luroth.θ✝ E)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (n₁ n₂ : ℤ) {Z : C}
  (h : (CochainComplex.mappingCone φ).X n₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₁)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d n₁ n₂) h) =
    CategoryTheory.CategoryStruct.comp (G.d n₁ n₂)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₂) h)
-- Mathlib.Lean.Expr.Basic
/-- `isConstantApplication e` checks whether `e` is syntactically an application of the form
`(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words,
it does a syntactic check that the expression does not depend on `yₙ`.  -/
Lean.Expr.isConstantApplication : Lean.Expr → Bool
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.congr_eq_3 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) (x : Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  x = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) ≍
      h_3 ()
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `(F ⋙ forget RingCat).sections` is `u`-small, `F` has a limit.  -/
RingCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections], CategoryTheory.Limits.HasLimit F
-- Lean.Data.Options
Lean.Options.get : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Name → α → α
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsFinitelySatisfiable.eq_1 : ∀ {L : FirstOrder.Language} (T : L.Theory),
  T.IsFinitelySatisfiable = ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → FirstOrder.Language.Theory.IsSatisfiable ↑T0
-- Mathlib.Data.List.Cycle
Cycle.lists_nil : ∀ {α : Type u_1}, Cycle.nil.lists = {[]}
-- Mathlib.Analysis.BoxIntegral.Basic
/-- **Henstock-Sacks inequality**. Let `r : ℝⁿ → (0, ∞)` be a function such that for any tagged
*partition* of `I` subordinate to `r`, the integral sum of `f` over this partition differs from the
integral of `f` by at most `ε`. Then for any tagged *prepartition* `π` subordinate to `r`, the
integral sum of `f` over this prepartition differs from the integral of `f` over the part of `I`
covered by `π` by at most `ε`.

The actual statement

- uses `BoxIntegral.Integrable.convergenceR` instead of a predicate assumption on `r`;
- uses `BoxIntegral.IntegrationParams.MemBaseSet` instead of “subordinate to `r`” to
  account for additional requirements like being a Henstock partition or having a bounded
  distortion;
- takes an extra argument `π₀ : prepartition I` and an assumption `π.Union = π₀.Union` instead of
  using `π.to_prepartition`.
 -/
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
  {π : BoxIntegral.TaggedPrepartition I} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E}
  {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : NNReal} {ε : ℝ} [CompleteSpace F]
  (h : BoxIntegral.Integrable I l f vol),
  0 < ε →
    l.MemBaseSet I c (h.convergenceR ε c) π →
      ∀ {π₀ : BoxIntegral.Prepartition I},
        π.iUnion = π₀.iUnion →
          dist (BoxIntegral.integralSum f vol π) (∑ J ∈ π₀.boxes, BoxIntegral.integral J l f vol) ≤ ε
-- Init.Grind.ToInt
Lean.Grind.IntInterval.isFinite : Lean.Grind.IntInterval → Bool
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport.mk.injEq : ∀ (module : Lean.Lsp.LeanModule) (kind : Lean.Lsp.LeanImportKind) (module_1 : Lean.Lsp.LeanModule)
  (kind_1 : Lean.Lsp.LeanImportKind),
  ({ module := module, kind := kind } = { module := module_1, kind := kind_1 }) = (module = module_1 ∧ kind = kind_1)
-- Mathlib.Order.SuccPred.Basic
Order.pred_succ_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [inst_2 : SuccOrder α] (a : α),
  Order.pred (Order.succ a) ≤ a
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- If the source of a faithful functor is the opposite category of one with a subobject classifier,
the same holds -- the functor reflects isomorphisms.
 -/
CategoryTheory.HasSubobjectClassifier.reflectsIsomorphismsOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.HasSubobjectClassifier C] (D : Type u₀)
  [inst_2 : CategoryTheory.Category.{v₀, u₀} D] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Faithful], F.ReflectsIsomorphisms
-- Mathlib.Algebra.Group.PUnit
PUnit.instInv_mathlib : Inv PUnit.{u_1 + 1}
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.seq_neg : ∀ {α β : Type u} (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α), f <*> -x = -(f <*> x)
-- Init.SimpLemmas
ite_self : ∀ {α : Sort u} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = a
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
a vertex `i` with `i ≥ j` can be identified with vertex `i + 1` in the original
path.  -/
SSet.StrictSegal.spine_δ_vertex_ge : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin (n + 1)} {j : Fin (n + 2)},
  j ≤ i.castSucc →
    (X.spine n
            ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j))
              (sx.spineToSimplex f))).vertex
        i =
      f.vertex i.succ
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.le_flip_dualSubmodule : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {N₁ N₂ : Submodule R M}, N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁
-- Mathlib.Data.Finset.Image
/-- `image f s` is the forward image of `s` under `f`.  -/
Finset.image : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → (α → β) → Finset α → Finset β
-- Init.Grind.Interactive
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals.
If the tactic fails on any goal, the entire `all_goals` tactic fails.
 -/
Lean.Parser.Tactic.Grind.allGoals : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapAddGrp_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal], e.mapAddGrp.functor = e.functor.mapAddGrp
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toLinearEquiv_eq_coe : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (g : SpecialLinearGroup R V), SpecialLinearGroup.toLinearEquiv g = ↑g
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {c d : E → 𝔸'} {c' d' : E →L[𝕜] 𝔸'},
  HasFDerivWithinAt c c' s x → HasFDerivWithinAt d d' s x → HasFDerivWithinAt (c * d) (c x • d' + d x • c') s x
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex], H ≤ K → K.FiniteIndex
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃ : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ}
  (s :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp
        ((SimplexCategory.Truncated.inclusion 2).op.comp X)))
  (x : s.pt) (φ : { len := 1 } ⟶ { len := n }),
  (CategoryTheory.ConcreteCategory.hom (X.map φ.op)) (SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x) =
    (CategoryTheory.ConcreteCategory.hom
        (s.π.app
          (SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ φ
            SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁._proof_1)))
      x
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_add_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] {p q : MvPolynomial σ R},
  (p + q).degrees ≤ p.degrees ⊔ q.degrees
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_surjective_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Injective ⇑f → Function.Surjective (Submodule.comap f)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMin.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (hr : t.Balanced),
  Std.DTreeMap.Internal.Impl.insertMin k v t hr =
    match t, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr =>
      { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, size_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr =>
      match Std.DTreeMap.Internal.Impl.insertMin k v l' ⋯ with
      | { impl := l'', balanced_impl := hl''₁, size_impl := hl''₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceL k' v' l'' r' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.Algebra.Module.Basic
Set.indicator_smul_const : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (s : Set α)
  (r : α → R) (m : M), (s.indicator fun x => r x • m) = fun x => s.indicator r x • m
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A generalisation of `LinearMap.id` that constructs the identity function
as a `σ`-semilinear map for any ring homomorphism `σ` which we know is the identity.  -/
LinearMap.id' : {R : Type u_1} →
  {M : Type u_8} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {σ : R →+* R} → [RingHomId σ] → M →ₛₗ[σ] M
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.trans_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E),
  (e.trans f).unitIso =
    e.unitIso ≪≫
      CategoryTheory.Functor.isoWhiskerRight
          (e.functor.rightUnitor.symm ≪≫
            e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm)
          e.inverse ≪≫
        (e.functor.comp f.functor).associator f.inverse e.inverse
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.node.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  sizeOf (RBTree.RBNode.node c l v r) = 1 + sizeOf c + sizeOf l + sizeOf v + sizeOf r
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.natCast_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddMonoidWithOne (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)]
  [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (n : ℕ) (i : ι), ↑n = ⟦⟨i, ↑n⟩⟧
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The unit group of a valuation subring, as a subgroup of `Kˣ`.  -/
ValuationSubring.unitGroup : {K : Type u} → [inst : Field K] → ValuationSubring K → Subgroup Kˣ
-- Std.Async.Basic
/-- Converts `Task` to `Async`.
 -/
Std.Async.Async.ofTask : {α : Type} → Task α → Std.Async.Async α
-- Mathlib.Algebra.Lie.Subalgebra
LieEquiv.lieSubalgebraMap_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (L₁'' : LieSubalgebra R L₁) (e : L₁ ≃ₗ⁅R⁆ L₂) (x : ↥L₁''),
  ↑((LieEquiv.lieSubalgebraMap L₁'' e) x) = e ↑x
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Given bases of two modules `M₁` and `M₂` over a commutative ring `R`, we get a linear
equivalence between linear maps `M₁ →ₗ M₂` and matrices over `R` indexed by the bases.  -/
LinearMap.toMatrix : {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [Fintype n] →
          [Finite m] →
            [DecidableEq n] →
              {M₁ : Type u_5} →
                {M₂ : Type u_6} →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] →
                          Module.Basis n R M₁ → Module.Basis m R M₂ → (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R
-- Mathlib.Data.List.MinMax
List.mem_argmax_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {m : α} [inst_1 : DecidableEq α],
  m ∈ List.argmax f l ↔ m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → List.idxOf m l ≤ List.idxOf a l
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.id : ∀ (X : Type u_1) [inst : TopologicalSpace X], Topology.IsCoinducing id
-- Init.Data.Vector.Lemmas
Vector.replace_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Array α} (h : xs.size = n) {a b : α},
  (Vector.mk xs h).replace a b = Vector.mk (xs.replace a b) ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (context : Lean.Lsp.ReferenceContext),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams, context := context } =
    1 + sizeOf toTextDocumentPositionParams + sizeOf context
-- Mathlib.CategoryTheory.Products.Basic
/-- The functor swapping the factors of a Cartesian product of categories, `C × D ⥤ D × C`.  -/
CategoryTheory.Prod.swap : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C × D) (D × C)
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_induction : ∀ {R : Type u_4} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {motive : (N : Submodule R M) → N.FG → Prop},
  (∀ (x : M), motive (R ∙ x) ⋯) →
    (∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯) →
      ∀ (N : Submodule R M) (hN : N.FG), motive N hN
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_neg_left`. -/
Asymptotics.IsBigO.neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, f' =O[l] g → (fun x => -f' x) =O[l] g
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_toRingHom : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ), ⇑↑f = ⇑f