mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.isIdempotentElem_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), IsIdempotentElem (p.projectionL q h)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve : ∀ (C D : Type u) [inst : CategoryTheory.Category.{u, u} C] [inst_1 : CategoryTheory.Category.{u, u} D],
  CategoryTheory.IsIso
    (CategoryTheory.Limits.prodComparison SSet.hoFunctor (CategoryTheory.nerve C) (CategoryTheory.nerve D))
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Sets `declName` priority to be used during E-matching pattern inference  -/
Lean.Meta.Grind.addSymbolPriorityAttr : Lean.Name → Lean.AttributeKind → ℕ → Lean.MetaM Unit
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.dvd_sum : ∀ {R : Type u_4} [inst : NonUnitalSemiring R] {s : Multiset R} {a : R}, (∀ x ∈ s, a ∣ x) → a ∣ s.sum
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- Given a precylinder `P` for `X`, two maps `f` and `g` in `X ⟶ Y` are
homotopic relative to `P` when there is a morphism `h : P.I ⟶ Y`
such that `P.i₀ ≫ h = f` and `P.i₁ ≫ h = g`.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → HomotopicalAlgebra.Precylinder X → {Y : C} → (X ⟶ Y) → (X ⟶ Y) → Type v
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a finitely supported function.  -/
Finsupp.mulHeight : {K : Type u_1} → [inst : Field K] → [Height.AdmissibleAbsValues K] → {α : Type u_4} → (α →₀ K) → ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.  -/
CategoryTheory.Limits.isSplitMono_coprod_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)],
  CategoryTheory.IsSplitMono CategoryTheory.Limits.coprod.inr
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- We say that a set is simply connected if it's a simply connected topological space
in the induced topology.  -/
IsSimplyConnected : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Differentiable.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ},
  Differentiable ℂ f → Differentiable ℂ fun x => Complex.cosh (f x)
-- Mathlib.Probability.Process.LocalProperty
MeasureTheory.IsStoppingTime.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m)
  (τ : Ω → WithTop ι), MeasureTheory.IsStoppingTime f τ = ∀ (i : ι), MeasurableSet {ω | τ ω ≤ ↑i}
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.consumeSpaces.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Init.Data.Repr
Nat.reprFast : ℕ → String
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_roc : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_roc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
    List.filter (fun e => decide ((cmp e lowerBound).isGT = true ∧ (cmp e upperBound).isLE = true)) t.toList
-- Lean.Meta.CoeAttr
Lean.Meta.instInhabitedCoeFnInfo.default : Lean.Meta.CoeFnInfo
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.keys.eq_def : ∀ {α : Type u} {β : α → Type v} (x : List ((a : α) × β a)),
  Std.Internal.List.keys x =
    match x with
    | [] => []
    | ⟨k, snd⟩ :: l => k :: Std.Internal.List.keys l
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
CategoryTheory.MorphismProperty.quotient_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  (homRel : HomRel C) [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel]
  [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] [inst_3 : W.HasQuotient homRel] {X Y : C} (f : X ⟶ Y),
  W.quotient homRel ((CategoryTheory.Quotient.functor homRel).map f) ↔ W f
-- Init.Data.Int.DivMod.Bootstrap
Int.div_def : ∀ (a b : ℤ), a / b = a.ediv b
-- Init.Data.Float.Float32
instMaxFloat32 : Max Float32
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo : Lean.Meta.ElimInfo →
  Array Lean.Elab.Tactic.ElimApp.Alt →
    Lean.Syntax →
      Option (Array Lean.Syntax) →
        Lean.Syntax →
          ℕ →
            Array Lean.FVarId →
              Array Lean.FVarId → Array (Lean.Ident × Lean.FVarId) → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.SymbolPriorities.mk : Lean.PHashMap Lean.Name ℕ → Lean.Meta.Grind.SymbolPriorities
-- Lean.Meta.PProdN
/-- Given types `t₁` and `t₂`, produces `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow)  -/
Lean.Meta.mkPProd : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.localization_localization_map_units : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (N : Submonoid S) (T : Type u_3) [inst_3 : CommSemiring T] [inst_4 : Algebra R T]
  [inst_5 : Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T]
  (y : ↥(IsLocalization.localizationLocalizationSubmodule M N)), IsUnit ((algebraMap R T) ↑y)
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.map_apply_tmul : ∀ {R : Type u_5} {A : Type u_6} {B : Type u_7} {L : Type u_8} {L' : Type u_9} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : LieRing L] [inst_6 : LieAlgebra R L]
  [inst_7 : LieRing L'] [inst_8 : LieAlgebra R L'] {f : A →ₐ[R] B} {g : L →ₗ⁅R⁆ L'} (a : A) (x : L),
  (LieAlgebra.ExtendScalars.map f g) (a ⊗ₜ[R] x) = f a ⊗ₜ[R] g x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  {f : α → β → Option γ},
  (Std.DHashMap.Const.toList (Std.DHashMap.filterMap (fun k v => f k v) m)).Perm
    (List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DHashMap.Const.toList m))
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionHom`, the bifunctorial action of morphisms in `C` and
`D` on `- ⊙ₗ -`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊙ₗₘ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.eq : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → A.conjTranspose = A
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.isClosed_setOfPred_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α], IsClosed {s | TotallyBounded s}
-- Mathlib.Data.Complex.Basic
/-- The real part of a complex number.  -/
Complex.re : ℂ → ℝ
-- Mathlib.Algebra.BigOperators.Fin
finSigmaFinEquiv.eq_2 : ∀ (m_2 : ℕ) (n_2 : Fin m_2.succ → ℕ),
  finSigmaFinEquiv =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm (Equiv.sumSigmaDistrib fun a => Fin (n_2 (finSumFinEquiv a))))
          (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n_2 (finSumFinEquiv (Sum.inr i))))))
        finSumFinEquiv)
      (finCongr ⋯)
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (n : ℕ) (x : α),
  s ∩ Multiset.replicate n x = Multiset.replicate (min (Multiset.count x s) n) x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced → ∀ {i : ℕ} {fallback : (a : α) × β a}, t.entryAtIdxD i fallback = t.toListModel.getD i fallback
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.vars : {σ : Type} → Lean.Elab.Term.Do.AltExpr σ → Array Lean.Elab.Term.Do.Var
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_mul : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a b : M₀},
  IsUnit a ∨ IsUnit b → Ring.inverse (a * b) = Ring.inverse b * Ring.inverse a
-- Mathlib.Data.Nat.Choose.Factorization
/-- The factorization of `p` in `choose n k` is the number of carries when `k` and `n - k`
are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
is any bound greater than `log p n`.  -/
Nat.factorization_choose : ∀ {p n k b : ℕ},
  Nat.Prime p →
    k ≤ n →
      Nat.log p n < b → (n.choose k).factorization p = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
-- Mathlib.Order.RelIso.Basic
/-- A function is a relation homomorphism from the preimage relation of `s` to `s`.  -/
RelHom.preimage : {α : Type u_1} → {β : Type u_2} → (f : α → β) → (s : β → β → Prop) → f ⁻¹'o s →r s
-- Lean.Environment
Lean.instInhabitedOLeanEntries.default : {α : Type} → [Inhabited α] → Lean.OLeanEntries α
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `S`.  -/
AddSubgroup.iSup_induction : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : G → Prop} {x : G},
  x ∈ ⨆ i, S i → (∀ (i : ι), ∀ x ∈ S i, C x) → C 0 → (∀ (x y : G), C x → C y → C (x + y)) → C x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {fallback : β} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).getD a fallback = fallback
-- Mathlib.Analysis.Normed.Module.Shrink
Shrink.instNormedSpace : {𝕜 : Type u_2} →
  {α : Type u_3} →
    [inst : Small.{v, u_3} α] →
      [inst_1 : NormedField 𝕜] →
        [inst_2 : SeminormedAddCommGroup α] → [NormedSpace 𝕜 α] → NormedSpace 𝕜 (Shrink.{v, u_3} α)
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [toHopfAlgebraStruct : HopfAlgebraStruct R A] →
          LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
              Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit →
            LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
                Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit →
              HopfAlgebra R A
-- Mathlib.Analysis.InnerProductSpace.Subspace
LinearIsometry.toSpanSingleton.congr_simp : ∀ (𝕜 : Type u_1) (E : Type u_4) [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {v v_1 : E} (e_v : v = v_1) (hv : ‖v‖ = 1),
  LinearIsometry.toSpanSingleton 𝕜 E hv = LinearIsometry.toSpanSingleton 𝕜 E ⋯
-- Mathlib.Algebra.Field.Defs
NNRat.smul_one_eq_cast : ∀ (K : Type u_1) [inst : DivisionSemiring K] (q : ℚ≥0), q • 1 = ↑q
-- Mathlib.Order.Filter.Basic
/-- Complete lattice structure on `Filter α`.  -/
Filter.instCompleteLatticeFilter : {α : Type u} → CompleteLattice (Filter α)
-- Mathlib.GroupTheory.Index
AddSubgroup.isFiniteRelIndex_of_le_left : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (L : AddSubgroup G) [H.IsFiniteRelIndex L],
  H ≤ K → K.IsFiniteRelIndex L
-- Mathlib.Order.RelClasses
instIsPreorderGe : ∀ {α : Type u} [inst : Preorder α], IsPreorder α fun x1 x2 => x2 ≤ x1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_nonpos_of_nonneg_of_nonpos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulMono α], 0 ≤ a → b ≤ 0 → a * b ≤ 0
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_lt_tprod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {i : ι}
  [L.NeBot] [L.LeAtTop],
  f ≤ g → f i < g i → Multipliable f L → Multipliable g L → ∏'[L] (n : ι), f n < ∏'[L] (n : ι), g n
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.mk.inj : ∀ {ns ns_1 : Array Aesop.RuleSetName}, { ns := ns } = { ns := ns_1 } → ns = ns_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for bitwise and of `BitVec`s.  -/
BitVec.reduceAnd : Lean.Meta.Simp.DSimproc
-- Std.Internal.Do.Order.Basic
/-- A complete lattice is a chain-complete partial order.  -/
Lean.Order.instCCPO_std : {α : Type u} → [Lean.Order.CompleteLattice α] → Lean.Order.CCPO α
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.ofNat_eq_iff_of_lt : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x y : ℕ},
  x < p → y < p → (OfNat.ofNat x = OfNat.ofNat y ↔ x = y)
-- Lean.Elab.Exception
Lean.Elab.throwPostpone : {m : Type u_1 → Type u_2} → {α : Type u_1} → [MonadExceptOf Lean.Exception m] → m α
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.copy_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (a : α),
  (ProbabilityTheory.Kernel.copy α) a = MeasureTheory.Measure.dirac (a, a)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.ext : Lean.Meta.Grind.AttrKind
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.exists_isBase : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → ∃ B, M.IsBase B ∧ I = B ∩ X
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.monoModSerre_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  P.monoModSerre f ↔ P (CategoryTheory.Limits.kernel f)
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- This is the pointwise power of `ArithmeticFunction`s.  -/
ArithmeticFunction.ppow : {R : Type u_1} → [inst : Semiring R] → ArithmeticFunction R → ℕ → ArithmeticFunction R
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C), (CategoryTheory.Mon.forget C).obj A = A.X
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_eq_nfpFamily : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Ordinal.nfp f = Ordinal.nfpFamily fun x => f
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.mapEmbedding_coe : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u v : V} (p : G.Path u v),
  ↑(SimpleGraph.Path.mapEmbedding f p) = SimpleGraph.Walk.map f.toHom ↑p
-- Mathlib.RingTheory.WittVector.Defs
WittVector.one_coeff_eq_of_pos : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] (n : ℕ), 0 < n → WittVector.coeff 1 n = 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Function.Periodic.norm_qParam_le_of_one_half_le_im : ∀ {ξ : ℂ}, 1 / 2 ≤ ξ.im → ‖Function.Periodic.qParam 1 ξ‖ ≤ Real.exp (-Real.pi)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.triggerKind : Lean.Lsp.SignatureHelpContext → Lean.Lsp.SignatureHelpTriggerKind
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_of_top_eq_bot`. -/
isSolvable_of_top_eq_bot : ∀ (G : Type u_1) [inst : Group G], ⊤ = ⊥ → Group.IsSolvable G
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.mem_support_of_adj_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v}, p.toSubgraph.Adj u' v' → u' ∈ p.support
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.iSup_basicOpen_eq_top_iff' : ∀ {R : Type u} [inst : CommSemiring R] {s : Set R}, ⨆ i ∈ s, PrimeSpectrum.basicOpen i = ⊤ ↔ Ideal.span s = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The inclusion `X ⟶ X ⊗ Δ[1]` which is `1` on the second factor.  -/
SSet.ι₁ : {X : SSet} → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 })
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence holds if and only if all non-negative distances between points with different
indices are the same.  -/
congruent_iff_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_add : ∀ (a b : UInt64), (a + b).toUInt32 = a.toUInt32 + b.toUInt32
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] {f : α ↪ β} {l : α →₀ M},
  Finsupp.embDomain f l = 0 ↔ l = 0
-- Mathlib.RingTheory.DedekindDomain.PID
/-- Let `P` be a prime ideal, `x ∈ P \ P²` and `x ∉ Q` for all prime ideals `Q ≠ P`.
Then `P` is generated by `x`.  -/
Ideal.eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne : ∀ {R : Type u_1} [inst : CommRing R] {P : Ideal R},
  P.IsPrime →
    ∀ [IsDedekindDomain R] {x : R},
      x ∈ P → x ∉ P ^ 2 → (∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q) → P = Ideal.span {x}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.isoCartesianComon_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Comon C), (CategoryTheory.isoCartesianComon A).hom.hom = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →+ N`, and `z w : N`, there exist `z' w' : M` and `d : S`
such that `f z' - f d = z` and `f w' - f d = w`.  -/
AddSubmonoid.LocalizationMap.surj₂ : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (z w : N), ∃ z' w' d, z + f ↑d = f z' ∧ w + f ↑d = f w'
-- Init.Data.List.Impl
List.find?.eq_def : ∀ {α : Type u} (p : α → Bool) (x : List α),
  List.find? p x =
    match x with
    | [] => none
    | a :: as =>
      match p a with
      | true => some a
      | false => List.find? p as
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.isMultiplicative_id : ArithmeticFunction.id.IsMultiplicative
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.of'_mul_modOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (g : G) (x : AddMonoidAlgebra k G),
  (AddMonoidAlgebra.of' k G g * x).modOf g = 0
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.abs_discr_ge : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  1 < Module.finrank ℚ K → 4 / 9 * (3 * Real.pi / 4) ^ Module.finrank ℚ K ≤ ↑|NumberField.discr K|
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instIsCentralScalar : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X] [inst_2 : SMul Mᵐᵒᵖ X] [IsCentralScalar M X],
  IsCentralScalar M (UniformSpace.Completion X)
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- Given an `R`-algebra `A` and a family `ι → Submodule R A` of submodules
parameterized by an additive monoid `ι`
and satisfying `SetLike.GradedMonoid M` (essentially, is multiplicative)
such that `DirectSum.IsInternal M` (`A` is the direct sum of the `M i`),
we endow `A` with the structure of a graded algebra.
The submodules are the *homogeneous* parts.  -/
DirectSum.IsInternal.gradedAlgebra : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {ι : Type u_7} →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] →
                {M : ι → Submodule R A} → [SetLike.GradedMonoid M] → DirectSum.IsInternal M → GradedAlgebra M
-- Mathlib.RingTheory.QuasiFinite.Weakly
Localization.localAlgHom.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] [inst_4 : Algebra R P] (I : Ideal S) [inst_5 : I.IsPrime] (J : Ideal P) [inst_6 : J.IsPrime]
  (f f_1 : S →ₐ[R] P) (e_f : f = f_1) (hIJ : I = Ideal.comap f J),
  Localization.localAlgHom I J f hIJ = Localization.localAlgHom I J f_1 ⋯
-- Mathlib.Algebra.Ring.Defs
NonAssocCommRing.toNonUnitalNonAssocCommRing : {α : Type u} → [self : NonAssocCommRing α] → NonUnitalNonAssocCommRing α
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instConcreteCategoryOrderHomFinHAddNatLenOfNat : CategoryTheory.ConcreteCategory SimplexCategory fun i j => Fin (i.len + 1) →o Fin (j.len + 1)
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom_eq_map : ∀ (V : Type u_1) (p : ↑unitInterval) [Countable V],
  SimpleGraph.binomialRandom V p =
    MeasureTheory.Measure.map SimpleGraph.fromEdgeSet (ProbabilityTheory.setBernoulli Sym2.diagSetᶜ p)
-- Mathlib.MeasureTheory.Integral.Pi
MeasureTheory.integrable_eval : ∀ {ι : Type u_2} [inst : Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)}
  {μ : (i : ι) → MeasureTheory.Measure (X i)} [inst_1 : (i : ι) → NormedAddCommGroup (X i)]
  [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] {i : ι},
  MeasureTheory.Integrable id (μ i) → MeasureTheory.Integrable (fun x => x i) (MeasureTheory.Measure.pi μ)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.ObjectProperty.eqToHom_hom : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory} (h : X = Y), (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasColimit (F i)]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)] (k : (i : α) → I i) (s : α)
  {Z : C} (h : CategoryTheory.Limits.colimit (F s) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pointwiseProduct F) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Pi.π (fun s => CategoryTheory.Limits.colimit (F s)) s) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π ((CategoryTheory.Functor.pi F).obj k) s)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F s) (k s)) h)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.mul_left : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul α α] {s t : Set α},
  IsOpen t → IsOpen (s * t)
-- Mathlib.CategoryTheory.Monoidal.Arrow
/-- The symmetric category instance induced by the pushout-product.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : CategoryTheory.CartesianMonoidalCategory C] →
          [inst_4 : CategoryTheory.MonoidalClosed C] →
            [inst_5 : CategoryTheory.BraidedCategory C] → CategoryTheory.SymmetricCategory (CategoryTheory.Arrow C)
-- Batteries.Tactic.PrintDependents
/-- Collect the results for a given constant.  -/
Batteries.Tactic.CollectDependents.collect : Lean.Name → Batteries.Tactic.CollectDependents.M Bool