mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instBooleanAlgebra : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → BooleanAlgebra (L.DefinableSet A α)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_eq_padic_norm : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ_[p]} (hq : ‖q‖ ≤ 1), ‖⟨q, hq⟩‖ = ‖q‖
-- Mathlib.Logic.Embedding.Basic
Equiv.coe_toEmbedding : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), ⇑f.toEmbedding = ⇑f
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  Disjoint (NumberField.InfinitePlace.ramifiedPlacesOver L v) (NumberField.InfinitePlace.unramifiedPlacesOver L v)
-- Mathlib.Algebra.CharP.Defs
ringExpChar.eq_iff : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R] {q : ℕ}, ringExpChar R = q ↔ ExpChar R q
-- Mathlib.Topology.CompactOpen
/-- Definition of `ContinuousMap.compactOpen`.  -/
ContinuousMap.compactOpen_eq : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ContinuousMap.compactOpen =
    TopologicalSpace.generateFrom (Set.image2 (fun K U => {f | Set.MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen t})
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem.below : {α : Type u_1} →
  {S : Set (Set α)} → {motive : (a : Set α) → generatePiSystem S a → Prop} → {a : Set α} → generatePiSystem S a → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {carrier : Set α} {isCompact' : IsCompact carrier} {carrier_1 : Set α}
  {isCompact'_1 : IsCompact carrier_1},
  { carrier := carrier, isCompact' := isCompact' } = { carrier := carrier_1, isCompact' := isCompact'_1 } →
    carrier = carrier_1
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.match_1.splitter : {α : Type u_1} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [inst_2 : DecidableLT α] →
        {n : Type u_1 → Type u_3} →
          (γ : Type u_1) →
            (Pl : α → γ → ForInStep γ → Prop) →
              (motive :
                  (it : Std.IterM Id α) →
                    ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2) →
                (it : Std.IterM Id α) →
                  (f : (b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
                    ((next upperBound : α) →
                        (f :
                            (b : α) →
                              {
                                      internalState :=
                                        { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput
                                  b →
                                (c : γ) → n (Subtype (Pl b c))) →
                          motive { internalState := { next := some next, upperBound := upperBound } } f) →
                      ((upperBound : α) →
                          (f :
                              (b : α) →
                                {
                                        internalState :=
                                          { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput
                                    b →
                                  (c : γ) → n (Subtype (Pl b c))) →
                            motive { internalState := { next := none, upperBound := upperBound } } f) →
                        motive it f
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.map_symm_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) (w : W), (SimpleGraph.Iso.map f G).symm w = f.symm w
-- Mathlib.Topology.Connected.Clopen
/-- A clopen set is the union of its connected components.  -/
IsClopen.biUnion_connectedComponent_eq : ∀ {α : Type u} [inst : TopologicalSpace α] {Z : Set α}, IsClopen Z → ⋃ x ∈ Z, connectedComponent x = Z
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E` and `K` are isomorphic as `F`-algebras, then `perfectClosure F E` and
`perfectClosure F K` are also isomorphic as `F`-algebras.  -/
perfectClosure.algEquivOfAlgEquiv : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type w} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(perfectClosure F E) ≃ₐ[F] ↥(perfectClosure F K)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_sum : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S), (E.sum F).presieve₀ = E.presieve₀ ⊔ F.presieve₀
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- An operator is a symmetric projection if and only if it is an orthogonal projection.  -/
LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {p : E →ₗ[𝕜] E}, p.IsSymmetricProjection ↔ ∃ (x : p.range.HasOrthogonalProjection), p = ↑p.range.starProjection
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instSetLikeFinset : (ι : Type u_1) → SetLike (PreAbstractSimplicialComplex ι) (Finset ι)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) {x : X},
  ↑(e.trans e') x = ↑e' (↑e x)
-- Mathlib.Topology.Order.LiminfLimsup
exists_seq_tendsto_limsInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [FirstCountableTopology α] {f : Filter α} [f.NeBot] [f.IsCountablyGenerated],
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f) exists_seq_tendsto_limsInf._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) exists_seq_tendsto_limsInf._auto_3 →
      ∃ x, Filter.Tendsto x Filter.atTop (nhds f.limsInf) ∧ Filter.Tendsto x Filter.atTop f
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.neg_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) {x : α}, (-f) x = -f x
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.Raw.keysIter.eq_1 : ∀ {α : Type u} {β : α → Type u} (m : Std.DHashMap.Raw α β), m.keysIter = Std.Iter.map (fun e => e.fst) m.iter
-- Mathlib.Algebra.MvPolynomial.Cardinal
MvPolynomial.cardinalMk_eq_lift : ∀ {σ : Type u} {R : Type v} [inst : CommSemiring R] [IsEmpty σ],
  Cardinal.mk (MvPolynomial σ R) = Cardinal.lift.{u, v} (Cardinal.mk R)
-- Mathlib.GroupTheory.PGroup
/-- If `gcd(p,n) = 1`, then the `n`th power map is a bijection.  -/
IsPGroup.powEquiv : {p : ℕ} → {G : Type u_1} → [inst : Group G] → IsPGroup p G → {n : ℕ} → p.Coprime n → G ≃ G
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx?_eq_map : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {i : ℕ},
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t i = Option.map (fun x => (x.fst, x.snd)) (t.entryAtIdx? i)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.liftOn₂_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (Localization.r S) (a, b) (a', b') → (Localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d')
  (a c : M) (b d : ↥S), (Localization.mk a b).liftOn₂ (Localization.mk c d) f H = f a b c d
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (toIsComplex : S.IsComplex),
  (∀ (i : ℕ) (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.Exact._auto_1),
      (S.sc toIsComplex i hi).Exact) →
    S.Exact
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.one_pow : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ), 1 ^ n = 1
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The diagram we will take the colimit of to define local cohomology, corresponding to the
directed system determined by the functor `I`  -/
localCohomology.diagram : {R : Type u} →
  [inst : CommRing R] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        CategoryTheory.Functor D (Ideal R) →
          ℕ → CategoryTheory.Functor Dᵒᵖ (CategoryTheory.Functor (ModuleCat R) (ModuleCat R))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_iUnion_toMeasurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_8} [Countable ι] (s : ι → Set α),
  μ (⋃ i, MeasureTheory.toMeasurable μ (s i)) = μ (⋃ i, s i)
-- Mathlib.Order.Directed
IsMax.isTop : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [IsDirectedOrder α], IsMax a → IsTop a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α}, (Std.DTreeMap.Internal.Impl.erase! k t).get? a = if compare k a = Ordering.eq then none else t.get? a
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toAddGroup : AddGroup E] →
      [toPseudoMetricSpace : PseudoMetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖-x + y‖) SeminormedAddGroup.dist_eq._autoParam → SeminormedAddGroup E
-- Mathlib.Data.Sym.Sym2
Sym2.mem_fromRel_comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (sym : Std.Symm r) (f : α → β) (z : Sym2 α),
  z ∈ Sym2.fromRel ⋯ ↔ Sym2.map f z ∈ Sym2.fromRel sym
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.le : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H.IsInducedSubgraph G → H.IsSubgraph G
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConcaveOn.condExp_map_le_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConcaveOn ℝ Set.univ φ →
    UpperSemicontinuous φ →
      MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.lintegral_coe_le_coe_iff_integral_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal},
  MeasureTheory.Integrable (fun x => ↑(f x)) μ → ∀ {b : NNReal}, ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b ↔ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b
-- Mathlib.LinearAlgebra.Prod
LinearMap.graph_eq_ker_coprod : ∀ {R : Type u} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommGroup M₃] [inst_2 : AddCommGroup M₄]
  [inst_3 : Module R M₃] [inst_4 : Module R M₄] (g : M₃ →ₗ[R] M₄), g.graph = ((-g).coprod LinearMap.id).ker
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coneOfDiagramTerminal_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C)
  [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] (x : J),
  (CategoryTheory.Limits.coneOfDiagramTerminal hX F).π.app x = CategoryTheory.inv (F.map (hX.from x))
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.top_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], ⊤.toNonUnitalSubalgebra = ⊤
-- Mathlib.Data.Fintype.Card
Fintype.instNeZeroNatCardOfNonempty : ∀ {α : Type u_1} [inst : Fintype α] [Nonempty α], NeZero (Fintype.card α)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'.d_comp_d_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j k : ι) {Z : C} (h : HomologicalComplex.truncGE'.X K e k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'.d K e i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'.d K e j k) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.sInf_toSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set (Subsemiring R)), (sInf s).toSubmonoid = ⨅ t ∈ s, t.toSubmonoid
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_subsingleton : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [Subsingleton R] {f : MvPolynomial σ R},
  m.degree f = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_back?_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.max? = t.toArray.back?
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.ae_enorm_le_bound : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ENNReal},
  (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a) →
    (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F' n a) Filter.atTop (nhds (f' a))) → ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instSMulCommClassAEEqFun_1 : ∀ {M : Type u_3} {N : Type u_1} {α : Type u_4} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] [inst_5 : SMul N β] [inst_6 : ContinuousConstSMul N β],
  SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.Data.Rel
SetRel.comp_subset_comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S₁ S₂ : SetRel β γ}, S₁ ⊆ S₂ → R.comp S₁ ⊆ R.comp S₂
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eq_one : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R},
  f.support.card = 1 ↔ ∃ k x, ∃ (_ : x ≠ 0), f = Polynomial.C x * Polynomial.X ^ k
-- Mathlib.Algebra.Group.Defs
zsmul_eq_smul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (n : ℤ) (x : G), ZSMul.zsmul n x = n • x
-- Init.Data.String.Basic
String.Pos.copy_toSlice_eq_cast : ∀ {s : String} (p : s.Pos), p.toSlice.copy = p.cast ⋯
-- Std.Http.Data.Headers.Name
/-- Standard Content-Length header name
 -/
Std.Http.Header.Name.contentLength : Std.Http.Header.Name
-- Mathlib.Order.SuccPred.Limit
WithBot.isPredLimit_iff : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMinOrder α] {x : WithBot α},
  Order.IsPredLimit x ↔ x = ⊥ ∨ ∃ y, x = ↑y ∧ Order.IsPredLimit y
-- Mathlib.Algebra.Order.Group.Indicator
Function.support_max : ∀ {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : LinearOrder M] (f g : α → M),
  (Function.support fun x => max (f x) (g x)) ⊆ Function.support f ∪ Function.support g
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernel.instIsCondKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ], κ.IsCondKernel κ.condKernel
-- Std.Http.Data.Headers.Basic
Std.Http.Header.TransferEncoding.mk.inj : ∀ {codings : Array String} {isValid : Std.Http.Header.TransferEncoding.Validate codings = true}
  {codings_1 : Array String} {isValid_1 : Std.Http.Header.TransferEncoding.Validate codings_1 = true},
  { codings := codings, isValid := isValid } = { codings := codings_1, isValid := isValid_1 } → codings = codings_1
-- Mathlib.Data.Finsupp.Single
Finsupp.update_erase_eq_update : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M),
  (Finsupp.erase a f).update a b = f.update a b
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_const_le' : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedGroup E] (a : E), ‖fun x => a‖ ≤ ‖a‖
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k k' : α} {f : β → β},
      Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.Const.modify k f t) =
        Std.DTreeMap.Internal.Impl.contains k' t
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldr.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : (a : α) → β a → δ → δ) (init : δ)
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.foldr f init t =
    (Std.DTreeMap.Internal.Impl.foldrM (fun x1 x2 x3 => pure (f x1 x2 x3)) init t).run
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.mk : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, s.copy = t₁ ++ t₂ → p.offset = t₁.rawEndPos → p.Splits t₁ t₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), ψ.unop.φH = ψ.φH.unop
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.instIterator.eq_1 : ∀ {α : Type u_1} {β : Type u_2},
  Lean.PersistentHashMap.instIterator =
    { IsPlausibleStep := fun it step => step = Lean.PersistentHashMap.Zipper.step it,
      step := fun it => pure (Std.Shrink.deflate ⟨Lean.PersistentHashMap.Zipper.step it, ⋯⟩) }
-- Mathlib.Data.Holor
/-- Left associator for `HolorIndex`  -/
HolorIndex.assocLeft : {ds₁ ds₂ ds₃ : List ℕ} → HolorIndex (ds₁ ++ (ds₂ ++ ds₃)) → HolorIndex (ds₁ ++ ds₂ ++ ds₃)
-- Mathlib.Order.Monotone.Monovary
StrictAntiOn.trans_antivaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : PartialOrder ι], StrictAntiOn f s → AntivaryOn g f s → MonotoneOn g s
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findFinIdx?.go.match_1.splitter : {α : Type u_1} →
  (l : List α) →
    (motive : (x : List α) → (x_1 : ℕ) → x.length + x_1 = l.length → Sort u_2) →
      (x : List α) →
        (x_1 : ℕ) →
          (x_2 : x.length + x_1 = l.length) →
            ((x : ℕ) → (x_3 : [].length + x = l.length) → motive [] x x_3) →
              ((a : α) → (l_1 : List α) → (i : ℕ) → (h : (a :: l_1).length + i = l.length) → motive (a :: l_1) i h) →
                motive x x_1 x_2
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.tendsto_extend_comp_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {α : Type u_8} {l : Filter α} {g : α → M},
  (∀ᶠ (z : α) in l, g z ∈ f.source) →
    ∀ {y : M},
      y ∈ f.source → (Filter.Tendsto (↑(f.extend I) ∘ g) l (nhds (↑(f.extend I) y)) ↔ Filter.Tendsto g l (nhds y))
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_mem_haarProduct : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.haar.chaar K₀ ∈ MeasureTheory.Measure.haar.haarProduct ↑K₀
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperLinearSet.singleton : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : M), IsProperLinearSet {a}
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Coercion of an `AddHom` into a function is itself an `AddHom`.

See also `AddHom.eval`.  -/
AddHom.coeFn : (α : Type u_5) → (β : Type u_6) → [inst : Add α] → [inst_1 : AddCommSemigroup β] → (α →ₙ+ β) →ₙ+ α → β
-- Init.Prelude
/-- Replaces the current value of the mutable state with a new one.
 -/
MonadStateOf.set : {σ : semiOutParam (Type u)} → {m : Type u → Type v} → [self : MonadStateOf σ m] → σ → m PUnit.{u + 1}
-- Mathlib.Data.Set.Subsingleton
Set.univ_set_eq_singleton_empty_iff : ∀ {α : Type u}, Set.univ = {∅} ↔ IsEmpty α
-- Mathlib.Order.Rel.GaloisConnection
/-- `leftFixedPoints` is the set of elements `J : Set α` satisfying `rightDual (leftDual J) = J`.  -/
SetRel.leftFixedPoints : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set (Set α)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (carrier : Type v) [commRing : CommRing carrier]
  [algebra : Algebra R carrier],
  sizeOf { carrier := carrier, commRing := commRing, algebra := algebra } =
    1 + sizeOf carrier + sizeOf commRing + sizeOf algebra
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.mk : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} [inst : FunLike F UpperHalfPlane ℂ]
  [toSlashInvariantFormClass : SlashInvariantFormClass F Γ k],
  (∀ (f : F), MDiff ⇑f) → (∀ (f : F) {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt (⇑f) k) → ModularFormClass F Γ k
-- LeanSearchClient.Basic
leansearchclient.useragent : Lean.Option String
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_subtype : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), ⇑s.subtype = Subtype.val
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.toEquiv_addRight : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  (MeasurableEquiv.addRight g).toEquiv = Equiv.addRight g
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_smul_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (c : ℝ),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) →
    ∀ (f : α → E), MeasureTheory.setToFun μ T' hT' f = c • MeasureTheory.setToFun μ T hT f
-- Lean.Parser.Term
/-- Implementation of the `show_term` term elaborator.
 -/
Lean.Parser.Term.showTermElabImpl : Lean.Parser.Parser
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Print a premise using HTML.  -/
Mathlib.Tactic.ClickSuggestions.Premise.toHtml : Mathlib.Tactic.ClickSuggestions.Premise → Lean.MetaM ProofWidgets.Html
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instBot.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instBot = { bot := { toTopologicalSpace := ⊥, toIsTopologicalAddGroup := ⋯ } }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km : α} (hc : Std.DTreeMap.Internal.Impl.contains k t = true),
  t.maxKey?.get ⋯ = km → (compare k km).isLE = true