mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafFunctor_map : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] {X_1 Y : C} (f : X_1 ⟶ Y),
  (skyscraperPresheafFunctor p₀).map f = SkyscraperPresheafFunctor.map' p₀ f
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isLocal_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Sort u_1} (W : ι → CategoryTheory.MorphismProperty C),
  (⨆ i, W i).isLocal = ⨅ i, (W i).isLocal
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0),
  CochainComplex.HomComplex.Cocycle.ofHom z.homOf = z
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.eq_4 : ∀ (fuel_2 : ℕ) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit =
    Ordering.lt
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.Internal.List.alterKey_cons_perm.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} {k : α} (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Order.Atoms
/-- A complemented modular coatomic lattice is strongly atomic.
Not an instance to prevent loops.  -/
ComplementedLattice.isStronglyCoatomic' : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α]
  [h : IsCoatomic α], IsStronglyAtomic α
-- Mathlib.LinearAlgebra.Complex.Module
realPart_ofReal : ∀ (r : ℝ), ↑(realPart ↑r) = ↑r
-- Mathlib.Data.Finsupp.MonomialOrder
/-- Given a monomial order with bot, notation for the corresponding order relation on
`WithBot (σ →₀ ℕ)`  -/
MonomialOrder.«term_≼'[_]_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comapₗ.eq_1 : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier),
  AlgebraicGeometry.StructureSheaf.comapₗ f U V hUV =
    { toFun := fun s => ⟨AlgebraicGeometry.StructureSheaf.comapFun f U V hUV ↑s, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_aleph0_iff_fintype : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Nonempty (Fintype α)
-- Mathlib.Data.Finset.Insert
/-- `{a} : Finset a` is the set `{a}` containing `a` and nothing else.

This differs from `insert a ∅` in that it does not require a `DecidableEq` instance for `α`.
 -/
Finset.instSingleton : {α : Type u_1} → Singleton α (Finset α)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inl_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inl X Y) CategoryTheory.Limits.prod.snd = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β], MeasureTheory.FinStronglyMeasurable f μ → MeasureTheory.AEFinStronglyMeasurable f μ
-- Init.SimpLemmas
Bool.beq_to_eq : ∀ (a b : Bool), ((a == b) = true) = (a = b)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_div_comm : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, a < b / c ↔ c < b / a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_apply_mul' : ∀ {p t x : ℝ}, p ∈ Set.Ioo 0 1 → 0 ≤ t → 0 ≤ x → p.rpowIntegrand₀₁ (x * t) x * x = p.rpowIntegrand₀₁ t 1 * x ^ p
-- Mathlib.Topology.MetricSpace.Isometry
/-- `IsometryClass F α β` states that `F` is a type of isometries.  -/
IsometryClass : (F : Type u_3) →
  (α : outParam (Type u_4)) →
    (β : outParam (Type u_5)) → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → [FunLike F α β] → Prop
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_const : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] [Nonempty ι] (a : E),
  ‖fun _i => a‖₊ = ‖a‖₊
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hom_ofHom : ∀ {X Y : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : Fintype X] [inst_3 : DistribLattice Y]
  [inst_4 : BoundedOrder Y] [inst_5 : Fintype Y] (f : BoundedLatticeHom X Y),
  FinBddDistLat.Hom.hom (FinBddDistLat.ofHom f) = f
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveElabDescr : Inhabited Lean.Elab.Command.InductiveElabDescr
-- Init.System.ST
EST.Out.ok.inj : ∀ {ε σ α : Type} {a : α} {a_1 : Void σ} {a_2 : α} {a_3 : Void σ},
  EST.Out.ok a a_1 = EST.Out.ok a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_natCast_mul_add : ∀ {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 : ℕ), toIocMod hp a (↑m * p + b) = toIocMod hp a b
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ (k : α), m₁.Equiv m₂ → (m₁.insert k).Equiv (m₂.insert k)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_natCast : iSup Nat.cast = Ordinal.omega0
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.tendsto_zero : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] {a : σ → S},
  MvPowerSeries.HasEval a → Filter.Tendsto a Filter.cofinite (nhds 0)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_2 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i j : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.pair i j, CategoryTheory.Pairwise.pair i j,
      CategoryTheory.Pairwise.Hom.id_pair i j with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_2 i j
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.readCommonMCtx? : Aesop.EqualUpToIdsM (Option Lean.MetavarContext)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.funLike : (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) → (k : outParam ℤ) → FunLike (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.image_coe_ball : ∀ (z : UpperHalfPlane) (r : ℝ), UpperHalfPlane.coe '' Metric.ball z r = Metric.ball (↑(z.center r)) (z.im * Real.sinh r)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bornology α] [inst_1 : Bornology β] [inst_2 : Bornology γ]
  (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Data.Set.Function
Set.mapsTo_univ_iff_range_subset : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Set.MapsTo f Set.univ t ↔ Set.range f ⊆ t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.continuous_cos : Continuous Real.Angle.cos
-- Mathlib.RingTheory.Idempotents
AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst : ∀ (R : Type u_1) [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {e f : S}
  (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hef₁ : e + f = 1) (hef₂ : e * f = 0) (a : S),
  ((AlgEquiv.prodQuotientOfIsIdempotentElem R he hf hef₁ hef₂) a).1 = (Ideal.Quotient.mk (Ideal.span {e})) a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedAlt : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Alt a)
-- Lean.Expr
Lean.Expr.const.sizeOf_spec : ∀ (declName : Lean.Name) (us : List Lean.Level), sizeOf (Lean.Expr.const declName us) = 1 + sizeOf declName + sizeOf us
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The inverse functor of equivalence of localized categories given by `Localization.uniq` is
compatible with the localization functors.  -/
CategoryTheory.Localization.compUniqInverse : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L₁.IsLocalization W'] →
                    [inst_4 : L₂.IsLocalization W'] → L₂.comp (CategoryTheory.Localization.uniq L₁ L₂ W').inverse ≅ L₁
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] {Z_1 : C} (h : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g)
      h
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The free product of the collection of `R`-algebras `A i`,
as a quotient of `PowerAlgebra R A`  -/
LinearAlgebra.FreeProduct.asPowers : {I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) → [inst_1 : (i : I) → Semiring (A i)] → [(i : I) → Algebra R (A i)] → Type (max (max u v) w)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfcHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A)
  (f : C(↑(spectrum 𝕜 a), 𝕜)) (ha : autoParam (p a) norm_cfcHom._auto_1), ‖(cfcHom ⋯) f‖ = ‖f‖
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The arrow `A --d₀₁--> Fun(G, A)` is isomorphic to the differential
`(inhomogeneousCochains A).d 0 1` of the complex of inhomogeneous cochains of `A`.  -/
groupCohomology.dArrowIso₀₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        CategoryTheory.Arrow.mk ((groupCohomology.inhomogeneousCochains A).d 0 1) ≅
          CategoryTheory.Arrow.mk (groupCohomology.d₀₁ A)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.mk.sizeOf_spec : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : SizeOf E] (toFun : ℝ → E → ℝ)
  (mem_Icc : ∀ (R : ℝ) (x : E), toFun R x ∈ Set.Icc 0 1) (symmetric : ∀ (R : ℝ) (x : E), toFun R (-x) = toFun R x)
  (smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry toFun) (Set.Ioi 1 ×ˢ Set.univ))
  (eq_one : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → toFun R x = 1)
  (support : ∀ (R : ℝ), 1 < R → Function.support (toFun R) = Metric.ball 0 R),
  sizeOf
      { toFun := toFun, mem_Icc := mem_Icc, symmetric := symmetric, smooth := smooth, eq_one := eq_one,
        support := support } =
    1
-- Mathlib.Algebra.Tropical.Basic
Tropical.mulRightMono : ∀ {R : Type u} [inst : LE R] [inst_1 : Add R] [AddRightMono R], MulRightMono (Tropical R)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.id_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (S : CategoryTheory.SimplicialObject.Split C) (n : ℕ),
  (CategoryTheory.CategoryStruct.id S).f n = CategoryTheory.CategoryStruct.id (S.s.N n)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- `e : Edge x y` is a composition of `Edge.id x` with `e`.  -/
SSet.Truncated.Edge.CompStruct.idComp : {X : SSet.Truncated 2} →
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    (e : SSet.Truncated.Edge x y) → (SSet.Truncated.Edge.id x).CompStruct e e
-- Mathlib.Order.RelClasses
/-- Set notation form of `not_lt_of_ge` -/
not_ssubset_of_superset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊂ a
-- Mathlib.Topology.Algebra.Group.Basic
/-- An additive monoid homomorphism (a bundled morphism of a type that implements
`AddMonoidHomClass`) from an additive topological group to an additive topological monoid is
continuous provided that it is continuous at zero.

This version assumes that `f x → 0` as `x → 0`,
saving a rewrite of `f 0 = 0` compared to `continuous_of_continuousAt_zero` in some cases.
See also `uniformContinuous_of_continuousAt_zero`.  -/
continuous_of_tendsto_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {M : Type u_1}
  {hom : Type u_2} [inst_3 : AddZeroClass M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [inst_6 : FunLike hom G M]
  [AddMonoidHomClass hom G M] (f : hom), Filter.Tendsto (⇑f) (nhds 0) (nhds 0) → Continuous ⇑f
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.iterate : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → ∀ (m : ℕ), Function.IsPeriodicPt f^[m] n x
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A measure `μ` on the additive quotient of `α` by `G` satisfying
`AddQuotientMeasureEqMeasurePreimage` and having finite covolume is a finite measure.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [hasFun : MeasureTheory.HasAddFundamentalDomain G α ν],
  MeasureTheory.addCovolume G α ν ≠ ⊤ → MeasureTheory.IsFiniteMeasure μ
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.toList_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.iter.toList = s.toList
-- Init.SimpLemmas
_private.Init.SimpLemmas.0.Lean.Arrow.eq_1 : ∀ (α : Sort u) (β : Sort v), Lean.Arrow α β = (α → β)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.contains_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m₁.Equiv m₂ → m₁.contains k = m₂.contains k
-- Init.Core
Std.LawfulRightIdentity.toRightIdentity : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → α} {o : outParam β} [self : Std.LawfulRightIdentity op o],
  Std.RightIdentity op o
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.prependMap.induct_unfolding : ∀ {α : Type u} {β : α → Type v}
  (motive :
    Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Std.DTreeMap.Internal.Zipper α β → Prop),
  (∀ (it : Std.DTreeMap.Internal.Zipper α β), motive Std.DTreeMap.Internal.Impl.leaf it it) →
    (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β),
        motive l (Std.DTreeMap.Internal.Zipper.cons k v r it)
            (Std.DTreeMap.Internal.Zipper.prependMap l (Std.DTreeMap.Internal.Zipper.cons k v r it)) →
          motive (Std.DTreeMap.Internal.Impl.inner size k v l r) it
            (Std.DTreeMap.Internal.Zipper.prependMap l (Std.DTreeMap.Internal.Zipper.cons k v r it))) →
      ∀ (a : Std.DTreeMap.Internal.Impl α β) (a_1 : Std.DTreeMap.Internal.Zipper α β),
        motive a a_1 (Std.DTreeMap.Internal.Zipper.prependMap a a_1)
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_comp_sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 (fun x => f (x - b)) a ↔ DifferentiableAt 𝕜 f (a - b)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ}, (μ.bind ⇑κ).bind ⇑η = μ.bind ⇑(η.comp κ)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The range of a surjective ring homomorphism is the whole of the codomain.  -/
RingHom.rangeS_top_of_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  Function.Surjective ⇑f → f.rangeS = ⊤
-- Mathlib.Order.Concept
Concept.isLowerSet_extent_le : ∀ {α : Type u_6} [inst : Preorder α] (c : Concept α α fun x1 x2 => x1 ≤ x2), IsLowerSet c.extent
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.uniformity_eq_aux : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A], uniformity (Unitization 𝕜 A) = uniformity (Unitization 𝕜 A)
-- Mathlib.Algebra.Order.Group.Synonym
isAddLeftRegular_toColex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddLeftRegular (toColex a) ↔ IsAddLeftRegular a
-- Lean.Syntax
Lean.instBEqSourceInfo_lean.beq : Lean.SourceInfo → Lean.SourceInfo → Bool
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices.  -/
SimpleGraph.completeGraph : (V : Type u) → SimpleGraph V
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : D),
  CategoryTheory.inv (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z) =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.inv f) z
-- Mathlib.Order.Hom.Lattice
SupHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β],
  SupHom.dual =
    { toFun := fun f => { toFun := ⇑f, map_inf' := ⋯ }, invFun := fun f => { toFun := ⇑f, map_sup' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Order.Hom.Basic
SubmultiplicativeHomClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Mul α] [inst_1 : Mul β] [inst_2 : LE β]
  [inst_3 : FunLike F α β], (∀ (f : F) (a b : α), f (a * b) ≤ f a * f b) → SubmultiplicativeHomClass F α β
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
mem_posTangentConeAt_of_frequently_mem : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {x y : E},
  (∃ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), x + t • y ∈ s) → y ∈ posTangentConeAt s x
-- Aesop.Percent
Aesop.Percent.instLT : LT Aesop.Percent
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α} {k fallback : α},
  k ∈ t → (t.insertManyIfNewUnit l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.instSupSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α],
  WithTop.instSupSet =
    {
      sSup := fun S =>
        if ⊤ ∈ S then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' S) then ↑(sSup ((fun a => ↑a) ⁻¹' S)) else ⊤ }
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf_iff_le_normalizer : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → ((H.subgroupOf K).Normal ↔ K ≤ Subgroup.normalizer ↑H)
-- Mathlib.NumberTheory.MulChar.Basic
/-- The equivalence between multiplicative characters and homomorphisms of unit groups.  -/
MulChar.equivToUnitHom : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → MulChar R R' ≃ (Rˣ →* R'ˣ)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inl_comp_pushoutObjIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D)
  {Z : C} (h : CategoryTheory.Limits.pushout (f.app d) (g.app d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pushout.inl f g).app d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutObjIso f g d).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (f.app d) (g.app d)) h
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GCommSemiring.toGSemiring : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddCommMonoid ι} →
      {inst_1 : (i : ι) → AddCommMonoid (A i)} → [self : DirectSum.GCommSemiring A] → DirectSum.GSemiring A
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.one_mem_toNonUnitalSubring : ∀ {R : Type u} [inst : NonAssocRing R] (S : Subring R), 1 ∈ S.toNonUnitalSubring
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_add_right_of_ge : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atBot → (∀ (x : α), g x ≤ C) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.property_index : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s)
  (ht : t ∈ l), p ↑(h.index t ht)
-- Mathlib.Order.Bounds.Basic
IsLeast.orderBot.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α} (h : IsLeast s a), h.orderBot = { bot := ⟨a, ⋯⟩, bot_le := ⋯ }
-- Init.PropLemmas
forall_eq : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∀ (a : α), a = a' → p a) ↔ p a'