mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Equiv.Defs
/-- Applying a semilinear equivalence `f` over `σ` to `r • x` equals `σ r • f x`.  -/
SemilinearEquivClass.map_smulₛₗ : ∀ {F : Type u_14} {R : outParam (Type u_15)} {S : outParam (Type u_16)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ}
  {M : outParam (Type u_17)} {M₂ : outParam (Type u_18)} {inst_4 : AddCommMonoid M} {inst_5 : AddCommMonoid M₂}
  {inst_6 : Module R M} {inst_7 : Module S M₂} {inst_8 : EquivLike F M M₂} [self : SemilinearEquivClass F σ M M₂]
  (f : F) (r : R) (x : M), f (r • x) = σ r • f x
-- Lean.Parser.Syntax
Lean.Parser.Command.notationItem : Lean.Parser.Parser
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Order.le_cof_iff`. -/
Ordinal.le_cof_type : ∀ {α : Type u} [inst : Preorder α] {c : Cardinal.{u}}, c ≤ Order.cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- `CliffordAlgebra.reverse` as an `AlgHom` to the opposite algebra  -/
CliffordAlgebra.reverseOp : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a surjection `φ : G →* H`.

For a `computable` version, see `QuotientGroup.quotientKerEquivOfRightInverse`.
 -/
QuotientGroup.quotientKerEquivOfSurjective : {G : Type u} →
  [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → Function.Surjective ⇑φ → G ⧸ φ.ker ≃* H
-- Lean.Parser.Term.Doc
_private.Lean.Parser.Term.Doc.0.Lean.Parser.Term.Doc.getRecommendedSpellingString.indentLine : String → String
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → l.minEntry? = Std.Internal.List.minEntry? l.toListModel
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toRows₁_apply : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₁) (j : n),
  A.toRows₁ i j = A (Sum.inl i) j
-- Mathlib.Data.Ordering.Basic
Ordering.compares_lt : ∀ {α : Type u_1} [inst : LT α] (a b : α), Ordering.lt.Compares a b = (a < b)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_bot : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : T1Space M], ↑⊥ = ⊥
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.dSmooth_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y] {f : X → Y},
  Diffeology.DSmooth f ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), Diffeology.IsPlot p → Diffeology.IsPlot (f ∘ p)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- Consider a real vector bundle in which each fiber is endowed with an inner product.
We say that the bundle is *Riemannian* if the inner product depends continuously on the base point.
This assumption is spelled `IsContinuousRiemannianBundle F E` where `F` is the model fiber,
and `E : B → Type*` is the bundle.  -/
IsContinuousRiemannianBundle : {B : Type u_1} →
  [inst : TopologicalSpace B] →
    (F : Type u_2) →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          (E : B → Type u_3) →
            [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
              [inst_4 : (x : B) → NormedAddCommGroup (E x)] →
                [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] →
                  [inst_6 : FiberBundle F E] → [VectorBundle ℝ F E] → Prop
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_le_iSup_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α},
  MeasurableSet s → ∫⁻ (x : α) in s, f x ∂μ ≤ (⨆ x ∈ s, f x) * μ s
-- Init.Data.Nat.Basic
Nat.le_step : ∀ {n m : ℕ}, n ≤ m → n ≤ m.succ
-- Lean.PrettyPrinter.Delaborator.Attributes
/-- Returns whether or not the given declaration has the `@[pp_nodot]` attribute.
 -/
Lean.hasPPNoDotAttribute : Lean.Environment → Lean.Name → Bool
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.eq_1 : ∀ {n : ℕ} (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder none l = none
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.πE_d_ιE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_d_ιE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_d_ιE._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.πE_d_ιE._auto_5),
  CategoryTheory.CategoryStruct.comp (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃)) =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If a `LocalizerMorphism` is a localized equivalence, then the induced functor on
the localized categories is an equivalence  -/
CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence], (Φ.localizedFunctor L₁ L₂).IsEquivalence
-- Lean.Parser.Term
Lean.Parser.Term.paren.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.comp_f_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) {Z : V} (h : C₃.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).f i) h =
    CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (g.f i) h)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLTFactor.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.convexBodyLTFactor K = NumberField.mixedEmbedding.convexBodyLTFactor K
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.commMonoidWithZero : {α : Type u_1} →
  [inst : CommSemiring α] →
    [inst_1 : PartialOrder α] →
      [ZeroLEOneClass α] → [AddLeftMono α] → [PosMulMono α] → CommMonoidWithZero { x // 0 ≤ x }
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- The actual monadic operation. Its return value is bundled together with a proof that
it satisfies `Property` and squashed so that it fits into the monad `m`.
 -/
Std.Iterators.HetT.operation : {m : Type w → Type w'} →
  {α : Type v} → (self : Std.Iterators.HetT m α) → m (Std.Internal.USquash (Subtype self.Property))
-- Mathlib.RingTheory.FreeCommRing
/-- A map `f : α → β` produces a ring homomorphism `FreeCommRing α →+* FreeCommRing β`.  -/
FreeCommRing.map : {α : Type u} → {β : Type v} → (α → β) → FreeCommRing α →+* FreeCommRing β
-- Lean.Setup
Lean.instInhabitedImport.default : Lean.Import
-- Lean.Level
Lean.Level.PP.Result.max : Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result
-- Init.Data.UInt.Basic
/-- The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt32.mod 5 2 = 1`
* `UInt32.mod 4 2 = 0`
* `UInt32.mod 4 0 = 4`
 -/
UInt32.mod : UInt32 → UInt32 → UInt32
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_single : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R),
  { toFinsupp := AddMonoidAlgebra.single n r } = (Polynomial.monomial n) r
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_essImage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [G.Faithful] [G.Full],
  G.essImage.localEpi = (CategoryTheory.MorphismProperty.epimorphisms D).inverseImage F
-- Mathlib.Data.Finset.Powerset
Finset.powerset.eq_1 : ∀ {α : Type u_1} (s : Finset α), s.powerset = { val := Multiset.pmap Finset.mk s.val.powerset ⋯, nodup := ⋯ }
-- Mathlib.Topology.Connected.PathConnected
/-- The relation "being joined by a path in `F`". Not quite an equivalence relation since it's not
reflexive for points that do not belong to `F`.  -/
JoinedIn : {X : Type u_1} → [TopologicalSpace X] → Set X → X → X → Prop
-- Mathlib.Algebra.Ring.Basic
NoZeroDivisors.to_isDomain : ∀ (α : Type u_3) [inst : Ring α] [h : Nontrivial α] [NoZeroDivisors α], IsDomain α
-- Mathlib.Data.Finset.Powerset
Finset.powerset_empty : ∀ {α : Type u_1}, ∅.powerset = {∅}
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.coe_comp : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X}
  (f' : G' ≃g G'') (f : G ≃g G'), ⇑(f'.comp f) = ⇑f' ∘ ⇑f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') →
    (∀ (k : α), t₁[k]? = t₂[k]?) → t₁.Equiv t₂
-- Mathlib.Analysis.Normed.Module.Bases
/-- The basis vectors.  -/
GeneralSchauderBasis.basis : {β : Type u_3} →
  {𝕜 : Type u_4} →
    {X : Type u_5} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup X] →
          [inst_2 : NormedSpace 𝕜 X] → {L : SummationFilter β} → GeneralSchauderBasis β 𝕜 X L → β → X
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivWithinAt.eventually_notMem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {s : Set 𝕜} {x : 𝕜},
  HasDerivWithinAt f f' s x →
    f' ≠ 0 → ∀ (t : Set F), ¬AccPt (f x) (Filter.principal t) → ∀ᶠ (z : 𝕜) in nhdsWithin x (s \ {x}), f z ∉ t
-- Mathlib.Data.Set.Basic
Set.union_empty_iff : ∀ {α : Type u} {s t : Set α}, s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
-- Mathlib.Logic.Function.Iterate
Function.iterate_pred_comp_of_pos : ∀ {α : Type u} (f : α → α) {n : ℕ}, 0 < n → f^[n.pred] ∘ f = f^[n]
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_4 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit0, b.bit0 with
    | PosNum.one, PosNum.one => h_1 ()
    | x, PosNum.one => h_2 x
    | PosNum.one, x => h_3 x
    | a.bit0, b.bit0 => h_4 a b
    | a.bit0, b.bit1 => h_5 a b
    | a.bit1, b.bit0 => h_6 a b
    | a.bit1, b.bit1 => h_7 a b) =
    h_4 a b
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.app X).inv
      (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app
        ((CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).obj X))
-- Mathlib.Topology.Algebra.UniformConvergence
instAddGroupUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup β],
  instAddGroupUniformFun =
    { toAddMonoid := instAddMonoidUniformFun, toNeg := instNegUniformFun, toSub := instSubUniformFun,
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.congr_arg : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f : M ≃+ N} {x x' : M}, x = x' → f x = f x'
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- If `K` admits an orthogonal projection, then `K` and `Kᗮ` span the whole space.  -/
Submodule.sup_orthogonal_of_hasOrthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [K.HasOrthogonalProjection], K ⊔ Kᗮ = ⊤
-- Mathlib.Analysis.Fourier.PoissonSummation
isBigO_norm_restrict_cocompact : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : C(ℝ, E)) {b : ℝ},
  0 < b →
    (⇑f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) →
      ∀ (K : TopologicalSpace.Compacts ℝ),
        (fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[Filter.cocompact ℝ] fun x =>
          |x| ^ (-b)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'_assoc : ∀ {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.MonoidalRightAction C D] {x₁ y₁ : D} {x₂ y₂ : C} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂)
  {Z : D} (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y₁ y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x₁ g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f y₂)
        h)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank_eq_zero_of_finite : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : Finite G], AddCommGroup.freeRank G = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul.eq_1 : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly), p₁.mul p₂ = Lean.Grind.CommRing.Poly.mul.go p₂ p₁ (Lean.Grind.CommRing.Poly.num 0)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the left commutative square of a morphism in `ShortComplex`  -/
CategoryTheory.ShortComplex.Hom.comm₁₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂) {Z : C} (h : S₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp S₂.f h) =
    CategoryTheory.CategoryStruct.comp S₁.f (CategoryTheory.CategoryStruct.comp self.τ₂ h)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toList_flatMap : ∀ {α α₂ β γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ Id] [inst : Std.Iterator α Id β] [inst_2 : Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β},
  (Std.Iter.flatMap f it₁).toList = (Std.Iter.map (fun b => (f b).toList) it₁).toList.flatten
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.get?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α fun x => β) (a : α),
  Std.DHashMap.Raw.Const.get? m a =
    if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.get? ⟨m, h⟩ a else none
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `IsCofinalFor.of_subset`. -/
HasSubset.Subset.iscofinalfor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCofinalFor s t
-- Lean.Setup
Lean.instInhabitedModuleSetup : Inhabited Lean.ModuleSetup
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The anti-equivalence between cosimplicial objects and simplicial objects.  -/
CategoryTheory.cosimplicialSimplicialEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (CategoryTheory.CosimplicialObject C)ᵒᵖ ≌ CategoryTheory.SimplicialObject Cᵒᵖ
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.ne_of_gt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] {a b : α}, a > b → a ≠ b
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.hasBasis_nhds_zero : ∀ (R : Type u) [inst : Ring R] (Γ₀ : Type v) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  (nhds 0).HasBasis (fun x => True) fun γ => {x | Valued.v.restrict x < ↑γ}
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
QuotientGroup.quotientMulEquivOfEq.congr_simp : ∀ {G : Type u} [inst : Group G] {M N : Subgroup G} [inst_1 : M.Normal] [inst_2 : N.Normal] (h : M = N),
  QuotientGroup.quotientMulEquivOfEq h = QuotientGroup.quotientMulEquivOfEq h
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_top_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.IsComplement' ⊤ ↔ H = ⊥
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_toLinearMap : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂), ⇑↑e = ⇑e
-- Mathlib.Tactic.Lift
/-- An element of `α` that satisfies `cond` belongs to the range of `coe`.  -/
CanLift.prf : ∀ {α : Sort u_1} {β : Sort u_2} {coe : outParam (β → α)} {cond : outParam (α → Prop)} [self : CanLift α β coe cond]
  (x : α), cond x → ∃ y, coe y = x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtHashSet.ofList l).get? k' = some k
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The natural transformation `π₂ ⟶ π₃` induced by `S.g` for all `S : ShortComplex C`.  -/
CategoryTheory.ShortComplex.π₂Toπ₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.ShortComplex.π₂ ⟶ CategoryTheory.ShortComplex.π₃
-- Mathlib.Algebra.Quaternion
Quaternion.star_mul_self : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), star a * a = ↑(Quaternion.normSq a)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.sInter : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)},
  s.Countable → (∀ t ∈ s, MeasurableSet t) → MeasurableSet (⋂₀ s)
-- Batteries.Data.Array.Scan
Array.scanlM_reverse : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → m β}
  {as : Array α}, Array.scanlM f init as.reverse = Array.reverse <$> Array.scanrM (flip f) init as
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hasForgetToGroup.eq_1 : CommGrpCat.hasForgetToGroup =
  {
    forget₂ :=
      { obj := fun X => GrpCat.of ↑X, map := fun {X Y} f => GrpCat.ofHom (CommGrpCat.Hom.hom f),
        map_id := CommGrpCat.hasForgetToGroup._proof_1, map_comp := @CommGrpCat.hasForgetToGroup._proof_2 },
    forget_comp := CommGrpCat.hasForgetToGroup._proof_4 }
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f),
  HomotopicalAlgebra.WeakEquivalence h.p
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_add_single_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m₁ m₂ m₁' m₂' : M},
  r₁ ≠ 0 →
    r₂ ≠ 0 →
      (AddMonoidAlgebra.single m₁ r₁ + AddMonoidAlgebra.single m₂ r₂ =
          AddMonoidAlgebra.single m₁' r₁ + AddMonoidAlgebra.single m₂' r₂ ↔
        m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = m₂')
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizerOfOrbitRel.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a b : α}
  (h : (AddAction.orbitRel G α) a b),
  AddAction.stabilizerEquivStabilizerOfOrbitRel h = (AddAction.stabilizerEquivStabilizer ⋯).symm
-- Mathlib.Data.Matrix.Basic
Matrix.transposeRingEquiv_symm_apply : ∀ (m : Type u_2) (α : Type u_11) [inst : AddCommMonoid α] [inst_1 : CommMagma α] [inst_2 : Fintype m]
  (a : (Matrix m m α)ᵐᵒᵖ), (Matrix.transposeRingEquiv m α).symm a = (MulOpposite.unop a).transpose
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Deconstruct an `x : WithZero α` to the underlying value in `α`, given a proof that `x ≠ 0`.  -/
WithZero.unzero : {α : Type u} → {x : WithZero α} → x ≠ 0 → α
-- Mathlib.Probability.Process.Predictable
_private.Mathlib.Probability.Process.Predictable.0.MeasureTheory.IsStronglyPredictable.of_measurable_add_one.match_1_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The image of a morphism in `ModuleCat R` is just the bundling of `LinearMap.range f`  -/
ModuleCat.image : {R : Type u} → [inst : Ring R] → {G H : ModuleCat R} → (G ⟶ H) → ModuleCat R
-- Init.Data.UInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toUInt16 : Bool → UInt16
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RoiSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_apply_coe_coe_symm_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {F : Type u_1} [inst_5 : EquivLike F A₁ A₂]
  [inst_6 : AlgEquivClass F R A₁ A₂] (f : F) (x : A₂), f ((↑f).symm x) = x
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.associatorInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Z : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          [inst_3 : Mathlib.Tactic.Coherence.LiftObj Y] →
            [inst_4 : Mathlib.Tactic.Coherence.LiftObj Z] →
              Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
-- Mathlib.Algebra.Order.Group.MinMax
max_sub_sub_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  max (a - c) (b - c) = max a b - c