mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.gcdCoeffs.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → ℤ → Sort u_1) (k' : ℤ) (v : Int.Internal.Linear.Var)
  (p : Int.Internal.Linear.Poly) (k : ℤ) (h_1 : (k k_1 : ℤ) → motive (Int.Internal.Linear.Poly.num k) k_1)
  (h_2 :
    (k' : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → (k : ℤ) → motive (Int.Internal.Linear.Poly.add k' v p) k),
  (match Int.Internal.Linear.Poly.add k' v p, k with
    | Int.Internal.Linear.Poly.num k, k_1 => h_1 k k_1
    | Int.Internal.Linear.Poly.add k' v p, k => h_2 k' v p k) =
    h_2 k' v p k
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- The entropy of an entourage `U`, defined as the exponential rate of growth of the size of the
largest `(U, n)`-dynamical net of `F`. Takes values in the space of extended real numbers
`[-∞,+∞]`. This version uses a `limsup`, and is chosen as the default definition.  -/
Dynamics.netEntropyEntourage : {X : Type u_1} → (X → X) → Set X → SetRel X X → EReal
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.destruct_apply_eq_unfold : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (h : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op)
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  (op ms).destruct =
    Option.map
      (fun x =>
        match x with
        | (exp, coef, op') => (exp, coef, ↑op' ms.tail))
      (h.unfold ms.head)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
noZeroDivisors_iff_forall_mem_nonZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀], NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → x ∈ nonZeroDivisors M₀
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_biUnion_le : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} {T : Set ι},
  Countable ↑T → μ.restrict (⋃ i ∈ T, s i) ≤ MeasureTheory.Measure.sum fun i => μ.restrict (s ↑i)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra K E] [inst_5 : Algebra K F] [inst_6 : IsScalarTower K F E],
  IntermediateField.restrictScalars K ⊤ = ⊤
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_inj : ∀ {n : ℕ} {c₁ c₂ : Composition n}, c₁.reverse = c₂.reverse ↔ c₁ = c₂
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.Nonempty.div_zero : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α] {s : Finset α}, s.Nonempty → s / 0 = 0
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G'] [inst_6 : NormedSpace ℝ G'] {T : Set α → G' →L[ℝ] G''}
  {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ {f : ↥(α →₁ₛ[μ] G')}, 0 ≤ f → 0 ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) f
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.abs_left_iff : ∀ {R : Type u} [inst : CommRing R] [inst_1 : LinearOrder R] [AddLeftMono R] (x y : R), IsCoprime |x| y ↔ IsCoprime x y
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_of_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → (∀ y ∈ insert x s, g y = f y) → ContinuousWithinAt g s x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_sub_nnrealPart_neg : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ),
  f.nnrealPart.toReal - (-f).nnrealPart.toReal = f
-- Aesop.BaseM
Aesop.BaseM.instMonadBacktrackSavedState : Lean.MonadBacktrack Lean.Meta.SavedState Aesop.BaseM
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.mk.inj : ∀ {levelParams : Array Lean.Name} {proof : Lean.Expr} {symbols : List Lean.HeadIndex} {origin : Lean.Meta.Grind.Origin}
  {levelParams_1 : Array Lean.Name} {proof_1 : Lean.Expr} {symbols_1 : List Lean.HeadIndex}
  {origin_1 : Lean.Meta.Grind.Origin},
  { levelParams := levelParams, proof := proof, symbols := symbols, origin := origin } =
      { levelParams := levelParams_1, proof := proof_1, symbols := symbols_1, origin := origin_1 } →
    levelParams = levelParams_1 ∧ proof = proof_1 ∧ symbols = symbols_1 ∧ origin = origin_1
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxiHasSize_eq : Int8.instRxiHasSize = HasModel.instRxiHasSize✝
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.trajFun.congr_simp : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ κ_1 : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) (e_κ : κ = κ_1)
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (x₀ x₀_1 : (i : ↥(Finset.Iic a)) → X ↑i),
  x₀ = x₀_1 → ProbabilityTheory.Kernel.trajFun κ a x₀ = ProbabilityTheory.Kernel.trajFun κ_1 a x₀_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.getThenInsertIfNew? k v).1 = t[k]?
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.fold.visit : {α : Type} → (Lean.Name → α → Lean.MetaM α) → Lean.Expr → α → Lean.Expr.FoldRelevantConstantsImpl.FoldM✝ α
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lieSpan.eq_1 : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (s : Set L),
  LieSubalgebra.lieSpan R L s = sInf {N | s ⊆ ↑N}
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.comp_reflectsCofilteredLimits : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
-- Init.Data.BitVec.Bitblast
/-- Recursively extract one bit at a time and extend it to width `w`  -/
BitVec.extractAndExtendAux : {w : ℕ} → (k len : ℕ) → BitVec w → BitVec (k * len) → k ≤ w → BitVec (w * len)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
and `B ⟶ X` is an arrow of `S`. This is the object `B`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.middle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} → {S : J.Cover X} → {T : (I : S.Arrow) → J.Cover I.Y} → (S.bind T).Arrow → C
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k).getKey? k = none
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {weight : Type v} {weightIsAddCommGroup : AddCommGroup weight}
  {weightIsModule : Module R weight} {coweight : Type v} {coweightIsAddCommGroup : AddCommGroup coweight}
  {coweightIsModule : Module R coweight} {index : Type v} {pairing : RootPairing index R weight coweight}
  {weight_1 : Type v} {weightIsAddCommGroup_1 : AddCommGroup weight_1} {weightIsModule_1 : Module R weight_1}
  {coweight_1 : Type v} {coweightIsAddCommGroup_1 : AddCommGroup coweight_1} {coweightIsModule_1 : Module R coweight_1}
  {index_1 : Type v} {pairing_1 : RootPairing index_1 R weight_1 coweight_1},
  { weight := weight, weightIsAddCommGroup := weightIsAddCommGroup, weightIsModule := weightIsModule,
        coweight := coweight, coweightIsAddCommGroup := coweightIsAddCommGroup, coweightIsModule := coweightIsModule,
        index := index, pairing := pairing } =
      { weight := weight_1, weightIsAddCommGroup := weightIsAddCommGroup_1, weightIsModule := weightIsModule_1,
        coweight := coweight_1, coweightIsAddCommGroup := coweightIsAddCommGroup_1,
        coweightIsModule := coweightIsModule_1, index := index_1, pairing := pairing_1 } →
    weight = weight_1 ∧
      weightIsAddCommGroup ≍ weightIsAddCommGroup_1 ∧
        weightIsModule ≍ weightIsModule_1 ∧
          coweight = coweight_1 ∧
            coweightIsAddCommGroup ≍ coweightIsAddCommGroup_1 ∧
              coweightIsModule ≍ coweightIsModule_1 ∧ index = index_1 ∧ pairing ≍ pairing_1
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix.mk.injEq : ∀ {n m : ℕ} (data data_1 : Array (Array ℚ)), ({ data := data } = { data := data_1 }) = (data = data_1)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.oddCommuteEquiv_symm_apply : ∀ {n : ℕ} (hn : Odd n) (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n),
  (DihedralGroup.oddCommuteEquiv hn).symm x =
    match x with
    | Sum.inl i => ⟨(DihedralGroup.sr i, DihedralGroup.r 0), ⋯⟩
    | Sum.inr (Sum.inl j) => ⟨(DihedralGroup.r 0, DihedralGroup.sr j), ⋯⟩
    | Sum.inr (Sum.inr (Sum.inl k)) =>
      ⟨(DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), ⋯⟩
    | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(DihedralGroup.r i, DihedralGroup.r j), ⋯⟩
-- Mathlib.Control.Traversable.Equiv
/-- The function `Equiv.traverse` transfers a traversable functor
instance across the equivalences `eqv`.  -/
Equiv.traversable : {t t' : Type u → Type u} → ((α : Type u) → t α ≃ t' α) → [Traversable t] → Traversable t'
-- Mathlib.Computability.Primrec.Basic
primrecRel_iff_primrec_decide : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {R : α → β → Prop}
  [inst_2 : DecidableRel R], PrimrecRel R ↔ Primrec₂ fun a b => decide (R a b)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a `CommRing` is a `CommRing`.  -/
Subring.toCommRing : {R : Type u_1} → [inst : CommRing R] → (s : Subring R) → CommRing ↥s
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- Eta-expanded form of `AbsolutelyContinuousOnInterval.mul`

---

If `f` and `g` are absolutely continuous on `uIcc a b`, then `f * g` is absolutely continuous
on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.fun_mul : ∀ {a b : ℝ} {f g : ℝ → ℝ},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (fun i => f i * g i) a b
-- Mathlib.Topology.Category.TopCat.Opens
IsOpenMap.functor.congr_simp : ∀ {X Y : TopCat} {f f_1 : X ⟶ Y} (e_f : f = f_1) (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)),
  hf.functor = ⋯.functor
-- Init.Data.List.Monadic
List.idRun_forIn'_yield_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : (a : α) → a ∈ l → β → Id β) (init : β),
  (forIn' l init fun a m b => ForInStep.yield <$> f a m b).run =
    List.foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => (f a h b).run)
      init l.attach
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given `R`-module X and `S`-module Y and a map `g : (extendScalars f).obj X ⟶ Y`, i.e. `S`-linear
map `S ⨂ X → Y`, there is a `X ⟶ (restrictScalars f).obj Y`, i.e. `R`-linear map `X ⟶ Y` by
`x ↦ g (1 ⊗ x)`.
 -/
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          {X : ModuleCat R} →
            {Y : ModuleCat S} → ((ModuleCat.extendScalars f).obj X ⟶ Y) → (X ⟶ (ModuleCat.restrictScalars f).obj Y)
-- Aesop.RuleTac.Apply
Aesop.RuleTac.applyExpr' : Lean.MVarId →
  Lean.Expr → Lean.Term → Option Aesop.Substitution → Lean.Meta.TransparencyMode → Aesop.BaseM Aesop.RuleApplication
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Variant of `get?_map` that holds without `LawfulEqOrd`.  -/
Std.DTreeMap.Internal.Impl.Const.get?_map' : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.map f t) k =
    Option.pmap (fun v h' => f (t.getKey k h') v) (Std.DTreeMap.Internal.Impl.Const.get? t k) ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey! k = default
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_univ : ∀ (F : Type u_3) (E : Type u_4) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IntermediateField.adjoin F Set.univ = ⊤
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball.eq_1 : ∀ {β : Type ub} (x : β) (V : Set (β × β)), UniformSpace.ball x V = Prod.mk x ⁻¹' V
-- Init.Data.UInt.Lemmas
UInt8.lt_iff_toBitVec_lt : ∀ {a b : UInt8}, a < b ↔ a.toBitVec < b.toBitVec
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddAction : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Small.{v, u_2} α] → [inst_1 : AddMonoid M] → [AddAction M α] → AddAction M (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instFaithfulFunctor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], (CategoryTheory.Preadditive.RightFreyd.functor V).Faithful
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_intMin : ∀ {i : ℕ} (w : ℕ), (BitVec.intMin w).getLsbD i = decide (i + 1 = w)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_himp_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R → Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R)
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.eq_1 : ∀ (p : ℕ) (q : ℚ), padicNorm p q = if q = 0 then 0 else ↑p ^ (-padicValRat p q)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.singleton : ∀ {α : Type u} {a : α × Bool}, FreeGroup.IsReduced [a]
-- Lean.Meta.CoeAttr
/-- The basic coercion `↑x`, see `CoeT.coe`  -/
Lean.Meta.CoeFnType.coe : Lean.Meta.CoeFnType
-- Mathlib.LinearAlgebra.Matrix.Symmetric
/-- The diagonal matrix `diagonal v` is symmetric.  -/
Matrix.isSymm_diagonal : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : Zero α] (v : n → α), (Matrix.diagonal v).IsSymm
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Rcc.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Rcc.HasRcoIntersection α] → Std.Rcc α → Std.Rco α → Std.Rco α
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup_base_case : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  f.ClearInsertInductionMotive ⋯ (f.insertRupUnits units).1.rupUnits 0 (f.insertRupUnits units).1.assignments
-- Init.Data.List.Erase
List.erase_ne_nil_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α} {a : α}, xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_smul_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R) {u v : R},
  IsUnit u → IsUnit v → W'.add (u • P) (v • Q) ≈ W'.add P Q
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀ {h' : k' ∈ Std.DTreeMap.Const.insertMany t l},
            Std.DTreeMap.Const.get (Std.DTreeMap.Const.insertMany t l) k' h' = v
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.abs_sinh : ∀ (x : ℝ), |Real.sinh x| = Real.sinh |x|
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPCOfShape.of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C],
  (∀ (J : ι → Type w) [inst_2 : (i : ι) → CategoryTheory.SmallCategory (J i)]
      [∀ (i : ι), CategoryTheory.IsFiltered (J i)] (F : (i : ι) → CategoryTheory.Functor (J i) C)
      [inst_4 : ∀ (i : ι), CategoryTheory.Limits.HasColimit (F i)],
      ∃ (x : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)),
        CategoryTheory.IsIso (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)) →
    CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_trans : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (e₁ : M ≃+ N)
  (e₂ : N ≃+ P), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.ofUpper_inj : ∀ {α : Type u_1} {a b : Topology.WithUpper α}, Topology.WithUpper.ofUpper a = Topology.WithUpper.ofUpper b ↔ a = b
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldl.eq_2 : ∀ {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (x : σ) (v : α) (r : RBTree.RBNode α) (tail : RBTree.RBNode.Stream α),
  RBTree.RBNode.Stream.foldl f x (RBTree.RBNode.Stream.cons v r tail) =
    RBTree.RBNode.Stream.foldl f (RBTree.RBNode.foldl f (f x v) r) tail
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.instPreorder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] → [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → Preorder (α →Co β)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.isCompact_iff_exists : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens}, IsCompact ↑U ↔ ∃ R f, Set.range ⇑f = ↑U
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.whiskerLeft_η_addCommutator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G CategoryTheory.AddMonObj.zero)
      (CategoryTheory.AddGrpObj.addCommutator G) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj G (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
      CategoryTheory.AddMonObj.zero
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.uniformContinuous_symm : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), UniformContinuous ⇑h.symm
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  {X Y : CategoryTheory.SimplicialObject A} (f : X ⟶ Y) {Z : ChainComplex A ℕ}
  (h : AlgebraicTopology.NormalizedMooreComplex.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.map f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.map f) h)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.continuousOn : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj),
  ContinuousOn (↑e') e'.source
-- Std.Sync.Broadcast
/-- Returns true if the buffer is at full capacity.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.isFull : {α : Type} → Std.AtomicT (Std.Bounded.State✝ α) BaseIO Bool
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_left_right : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime x (y + x * z)
-- Std.Http.Data.Chunk
/-- Converts the trailer headers to an array of key-value pairs.
 -/
Std.Http.Trailer.toArray : Std.Http.Trailer → Array (Std.Http.Header.Name × Std.Http.Header.Value)
-- Mathlib.Data.Nat.Factorial.BigOperators
Nat.factorial_eq_prod_range_add_one : ∀ (n : ℕ), n.factorial = ∏ i ∈ Finset.range n, (i + 1)
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT_readyForRatAdd : ∀ (cnf : Std.Sat.CNF ℕ), (Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT cnf).ReadyForRatAdd
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_eq_mk : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.MemLp (⇑f) p μ),
  ↑↑(f.toLp hf) = MeasureTheory.AEEqFun.mk ⇑f ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.Equiv t₂ → t₁.minKey! = t₂.minKey!
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.loogleTermImpl : Lean.Elab.Term.TermElab
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies the expression `Zero.zero`, returning `0`.  -/
Mathlib.Meta.NormNum.evalZero : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Matrix.iSup_eigenspace_toLin_diagonal_eq_top : ∀ {R : Type u_1} {n : Type u_2} {M : Type u_3} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (d : n → R) (b : Module.Basis n R M),
  ⨆ μ, Module.End.eigenspace ((Matrix.toLin b b) (Matrix.diagonal d)) μ = ⊤
-- Mathlib.Algebra.Group.Ext
RightCancelMonoid.toMonoid_injective : ∀ {M : Type u}, Function.Injective (@RightCancelMonoid.toMonoid M)
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on a metric sphere in a real normed space  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromSphere : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_inverse_map : ∀ {X Y : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)} (f : X ⟶ Y),
  CategoryTheory.typeEquiv.inverse.map f = f.hom.app (Opposite.op PUnit.{u + 1})
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_left_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.i = CategoryTheory.CategoryStruct.comp h.left.i e.hom.τ₂