mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List ((a : α) × β a) → Sort u_3) →
      (x : List ((a : α) × β a)) →
        (Unit → motive []) → ((k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)) → motive x
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousAt_iInf_rng : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_7} [tX : TopologicalSpace X] {u : κ → UniformSpace α'}
  {F : ι → X → α'} {x₀ : X}, EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀
-- Std.Time.Duration
Std.Time.Duration.instDecidableLe : {x y : Std.Time.Duration} → Decidable (x ≤ y)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- If `F i → f` in `L1`, then `∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ]`.  -/
MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1' : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} (f : X → E),
  MeasureTheory.AEStronglyMeasurable f μ.variation →
    ∀ {F_1 : ι → X → E} {l : Filter ι},
      (∀ᶠ (i : ι) in l, μ.Integrable (F_1 i)) →
        Filter.Tendsto (fun i => MeasureTheory.eLpNorm (F_1 i - f) 1 μ.variation) l (nhds 0) →
          ∀ (s : Set X),
            Filter.Tendsto (fun i => ∫ᵛ (x : X) in s, F_1 i x ∂[B; μ]) l (nhds ∫ᵛ (x : X) in s, f x ∂[B; μ])
-- Lean.ToExpr
Lean.instToExprUInt8 : Lean.ToExpr UInt8
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C) {x y : B} (f : x ⟶ y),
  F.toStrictlyUnitaryLaxFunctor.map f = F.map f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minEntry?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.minEntry? = t₂.minEntry?
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.comp.match_1.eq_2 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2)
  (x : CategoryTheory.WithInitial C) (_X : C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithInitial.of _X) (CategoryTheory.WithInitial.of _Y) (CategoryTheory.WithInitial.of _Z))
  (h_2 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive CategoryTheory.WithInitial.star x (CategoryTheory.WithInitial.of _X))
  (h_3 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive x (CategoryTheory.WithInitial.of _X) CategoryTheory.WithInitial.star)
  (h_4 :
    (_Y : C) →
      (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of _Y) CategoryTheory.WithInitial.star x)
  (h_5 : Unit → motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X with
    | CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X => h_2 x _X
    | x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star => h_3 x _X
    | CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x => h_4 _Y x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star => h_5 ()) =
    h_2 x _X
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_neg : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ),
  ProbabilityTheory.condVar m (-X) μ =ᵐ[μ] ProbabilityTheory.condVar m X μ
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.mk : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  Set.BijOn f A B →
    (∀ ⦃s t : Multiset α⦄,
        (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
          (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
            s.card = n → t.card = n → ((Multiset.map f s).sum = (Multiset.map f t).sum ↔ s.sum = t.sum)) →
      IsAddFreimanIso n A B f
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActions.mk.inj : ∀ {onAnyCmd : Array Lean.CodeAction.CommandCodeAction} {onCmd : Lean.NameMap (Array Lean.CodeAction.CommandCodeAction)}
  {onAnyCmd_1 : Array Lean.CodeAction.CommandCodeAction}
  {onCmd_1 : Lean.NameMap (Array Lean.CodeAction.CommandCodeAction)},
  { onAnyCmd := onAnyCmd, onCmd := onCmd } = { onAnyCmd := onAnyCmd_1, onCmd := onCmd_1 } →
    onAnyCmd = onAnyCmd_1 ∧ onCmd = onCmd_1
-- Init.Data.SInt.Lemmas
ISize.toInt16_mul : ∀ (a b : ISize), (a * b).toInt16 = a.toInt16 * b.toInt16
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- If `S` is a Mayer-Vietoris square, and `P` is a presheaf
which satisfies the sheaf condition with respect to `S`, then
elements of `P` over `S.X₂` and `S.X₃` can be glued if the
coincide over `S.X₁`.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.glue : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        {S : J.MayerVietorisSquare} →
          {P : CategoryTheory.Functor Cᵒᵖ (Type v')} →
            S.SheafCondition P →
              (u : P.obj (Opposite.op S.X₂)) →
                (v : P.obj (Opposite.op S.X₃)) →
                  (CategoryTheory.ConcreteCategory.hom (P.map S.f₁₂.op)) u =
                      (CategoryTheory.ConcreteCategory.hom (P.map S.f₁₃.op)) v →
                    P.obj (Opposite.op S.X₄)
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_comap_eq_of_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [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₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R₂ M₂},
  p ≤ f.range → Submodule.map f (Submodule.comap f p) = p
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rcc_eq_add : ∀ {m n i fallback : ℕ}, i < n + 1 - m → (m...=n).toList.getD i fallback = m + i
-- Mathlib.Data.List.Fold
/-- **Alias** of `List.foldl_cons_eq_apply_foldl`. -/
List.foldl_eq_of_comm' : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v],
  List.foldl v b (a :: l) = v (List.foldl v b l) a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l).getD k' fallback = v
-- Init.Data.Int.Compare
Int.compare_eq_lt : ∀ {a b : ℤ}, compare a b = Ordering.lt ↔ a < b
-- Init.Data.Fin.Lemmas
Fin.dite_val : ∀ {n : ℕ} {c : Prop} [inst : Decidable c] {x y : Fin n}, ↑(if c then x else y) = if c then ↑x else ↑y
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n a n' : ℤ) (hn' : n + a = n') (γ : CochainComplex.HomComplex.Cocycle K L n),
  (CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv n a n' hn') γ = γ.leftShift a n' hn'
-- Mathlib.Logic.Encodable.Basic
ULower.down_eq_down : ∀ {α : Type u_1} [inst : Encodable α] {a b : α}, ULower.down a = ULower.down b ↔ a = b
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {inst_1 : DecidableEq (Associates α)}
  [inst_2 : DecidableEq (Associates α)] {inst_3 : (p : Associates α) → Decidable (Irreducible p)}
  [inst_4 : (p : Associates α) → Decidable (Irreducible p)] (p p_1 : Associates α),
  p = p_1 → ∀ (a a_1 : Associates.FactorSet α), a = a_1 → p.count a = p_1.count a_1
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
AEMeasurable.re : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {m : MeasurableSpace α} {f : α → 𝕜} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => RCLike.re (f x)) μ
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.natCast_natAbs : ∀ (n : ℤ), ↑n.natAbs = |n|
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.const.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Lp.const p μ = MeasureTheory.Lp.const p μ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.sum_finsupport' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s),
  ∀ x₀ ∈ s, ∀ {I_1 : Finset ι}, ρ.finsupport x₀ ⊆ I_1 → ∑ i ∈ I_1, (ρ i) x₀ = 1
-- Mathlib.Data.Set.Disjoint
Set.disjoint_of_subset_left : ∀ {α : Type u} {s t u : Set α}, s ⊆ u → Disjoint u t → Disjoint s t
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.zero_vadd : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : AddMonoid M] [inst_3 : AddAction M X] [ContinuousVAdd M X] {f : α → M} {g : α → X} {l : Filter α} {a : X},
  Filter.Tendsto f l (nhds 0) → Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x +ᵥ g x) l (nhds a)
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.Model.isLongestMatch_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} {pos : s.Pos}
  {pos' : t.Pos},
  s = t →
    pos.offset = pos'.offset →
      String.Slice.Pattern.Model.IsLongestMatch pat pos → String.Slice.Pattern.Model.IsLongestMatch pat pos'
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.instCCPO : {α : Sort u} → {b : α} → Lean.Order.CCPO (Lean.Order.FlatOrder b)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceDiv : Lean.Meta.Simp.DSimproc
-- Init.Data.Option.Lemmas
Option.ite_none_left_eq_some : ∀ {β : Type u_1} {a : β} {p : Prop} {x : Decidable p} {b : Option β}, (if p then none else b) = some a ↔ ¬p ∧ b = some a
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm : ∀ {S' : Type u_4} [inst : SeminormedAddGroup S'], IsNonarchimedean norm → IsUltrametricDist S'
-- Mathlib.Data.Fin.Tuple.Sort
/-- `graphEquiv₁ f` is the natural equivalence between `Fin n` and `graph f`,
mapping `i` to `(f i, i)`.  -/
Tuple.graphEquiv₁ : {n : ℕ} → {α : Type u_1} → [inst : LinearOrder α] → (f : Fin n → α) → Fin n ≃ ↥(Tuple.graph f)
-- Mathlib.Analysis.LConvolution
/-- Scoped notation for the multiplicative convolution of functions with respect to a measure `μ`.
 -/
MeasureTheory.«term_⋆ₘₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measurableSet_fiber' : ∀ {α : Type u} [inst : MeasurableSpace α] {β : Type v} (self : MeasureTheory.SimpleFunc α β) (x : β),
  MeasurableSet (self.toFun ⁻¹' {x})
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isHamiltonianCycle_rotate`. -/
SimpleGraph.Walk.IsHamiltonianCycle.of_rotate : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a v : α} {p : G.Walk a a} (hv : v ∈ p.support),
  (p.rotate v hv).IsHamiltonianCycle → p.IsHamiltonianCycle
-- Init.Data.Slice.Notation
Std.Rio.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Rio β → γ) → Std.Rio.Sliceable α β γ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C),
  groupHomology.mapCycles₁ (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ) (groupHomology.mapCycles₁ g ψ)
-- Mathlib.Algebra.GroupWithZero.Defs
mul_left_cancel₀ : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [IsLeftCancelMulZero M₀] {a b c : M₀},
  a ≠ 0 → a * b = a * c → b = c
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk_coe_of_dist_eq : ∀ {α : Type u_5} {β : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (f : α →ᵈ β)
  (h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y), Dilation.mkOfDistEq (⇑f) h = f
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.lsmul_flip_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E), (ContinuousLinearMap.lsmul 𝕜 𝕜).flip x = ContinuousLinearMap.toSpanSingleton 𝕜 x
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_lt_one : ∀ (x : ℝ), x.sigmoid < 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Adjunction.mapMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [inst_6 : a.IsMonoidal],
  a.mapMon =
    {
      unit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapMonIdIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapMonNatTrans a.unit)
            CategoryTheory.Functor.mapMonCompIso.hom),
      counit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapMonCompIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapMonNatTrans a.counit)
            CategoryTheory.Functor.mapMonIdIso.hom),
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Order.KrullDimension
Order.krullDim_nonpos_iff_forall_isMin : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α ≤ 0 ↔ ∀ (x : α), IsMin x
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small.h : ∀ {α : Type v} [self : Std.Internal.Small α], Nonempty (Std.Internal.ComputableSmall α)
-- Mathlib.Algebra.Notation.Support
Function.support_eq_preimage : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] (f : ι → M), Function.support f = f ⁻¹' {0}ᶜ
-- Init.Data.SInt.Lemmas
Int32.toBitVec_toUInt32 : ∀ (x : Int32), x.toUInt32.toBitVec = x.toBitVec
-- Init.Data.UInt.Lemmas
UInt8.toNat_lt : ∀ (n : UInt8), n.toNat < 2 ^ 8
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_maxD_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp k (t.maxD fallback)).isLE = true
-- Lean.Parser.Syntax
Lean.Parser.Command.macro : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (fallback : (a : α) × β a) (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : (a : α) × β a) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1,
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Init.Data.SInt.Bitwise
Bool.toInt64.eq_1 : ∀ (b : Bool), b.toInt64 = if b = true then 1 else 0
-- Mathlib.Data.List.OffDiag
List.map_prodMap_offDiag : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α), List.map (Prod.map f f) l.offDiag = (List.map f l).offDiag
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_of_notMem_support : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, a ∉ f.support → Finsupp.erase a f = f
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x) (x : Lean.Grind.CommRing.Var),
  a = Lean.Grind.CommRing.Expr.var x →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | x => h_3 x) ≍
      h_2 x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_smul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) {S : Type u_4} [inst : CommRing R]
  [inst_1 : SMulZeroClass S R] (s : S), (s • a).im = s • a.im
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Equiv.Perm.sum_comp : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → M),
  {a | σ a ≠ a} ⊆ ↑s → ∑ x ∈ s, f (σ x) = ∑ x ∈ s, f x
-- Mathlib.NumberTheory.SmoothNumbers
/-- We establish the bijection from `ℕ × smoothNumbers p` to `smoothNumbers (p+1)`
given by `(e, n) ↦ p^e * n` when `p` is a prime. See `Nat.smoothNumbers_succ` for
when `p` is not prime.  -/
Nat.equivProdNatSmoothNumbers : {p : ℕ} → Nat.Prime p → ℕ × ↑p.smoothNumbers ≃ ↑(p + 1).smoothNumbers
-- Mathlib.Data.List.TFAE
List.tfae_cons_of_mem : ∀ {a b : Prop} {l : List Prop}, b ∈ l → ((a :: l).TFAE ↔ (a ↔ b) ∧ l.TFAE)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : LawfulBEq α] {a : α},
  Std.DHashMap.Const.get? m a = m.get? a
-- Mathlib.Order.Filter.Defs
/-- `f.IsBounded r`: the filter `f` is eventually bounded w.r.t. the relation `r`,
i.e. eventually, it is bounded by some uniform bound.
`r` will be usually instantiated with `(· ≤ ·)` or `(· ≥ ·)`.  -/
Filter.IsBounded : {α : Type u_1} → (α → α → Prop) → Filter α → Prop
-- Mathlib.CategoryTheory.Iso
CategoryTheory.isIso_comp_left_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g) ↔ CategoryTheory.IsIso g
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.coe_id : ∀ {V : Type u_1} {G : SimpleGraph V}, ⇑SimpleGraph.Hom.id = id
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.createLimitsOfSizeMapCompForget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        CategoryTheory.CreatesLimitsOfSize.{w, w', v, v, max u v, u}
          ((CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X))
-- Mathlib.Data.Set.Image
Set.preimage_image_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' f '' Set.univ = Set.univ
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.isRepresentation.toEnd_surjective : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤),
  Function.Surjective ⇑(Matrix.isRepresentation.toEnd R b hb)
-- Mathlib.Data.Set.FiniteExhaustion
/-- The underlying sequence of a `FiniteExhaustion`.  -/
Set.FiniteExhaustion.toFun : {α : Type u_1} → {s : Set α} → s.FiniteExhaustion → ℕ → Set α
-- Mathlib.Data.Sym.Sym2
Sym2.toRel_mono_iff : ∀ {α : Type u_1} (s₁ s₂ : Set (Sym2 α)), Sym2.ToRel s₁ ≤ Sym2.ToRel s₂ ↔ s₁ ⊆ s₂