mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.rel_eq : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (p q r s : ℤ),
  IsEllipticNet.rel W p q r s = IsEllipticNet.atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s
-- Init.Data.UInt.Lemmas
UInt32.le_trans : ∀ {a b c : UInt32}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `HasFDerivWithinAt.finsetProd`. -/
HasFDerivWithinAt.finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) →
    HasFDerivWithinAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0),
  ↑(CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf) = CochainComplex.HomComplex.Cochain.toSingleMk f h
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u} [inst_1 : CategoryTheory.Category.{v, u} D]
  {x y : C} (f : x ⟶ y) (F : CategoryTheory.Functor C D),
  CategoryTheory.nerve.homEquiv ((CategoryTheory.nerve.edgeMk f).map (CategoryTheory.nerveMap F)) = F.map f
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instFinitenessRelation₁ : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [inst_2 : Monad m] →
            [Std.Iterators.Finite α₁ m] →
              [Std.Iterators.Productive α₂ m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Zip α₁ m α₂ β₂) m
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.forget₂_map_associator_inv : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] (X Y Z : QuadraticModuleCat R),
  (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map
      (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    (CategoryTheory.MonoidalCategoryStruct.associator X.toModuleCat Y.toModuleCat Z.toModuleCat).inv
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `=` on `BitVec`s.  -/
BitVec.reduceEq : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Complex.Trigonometric
Complex.norm_exp_ofReal_mul_I : ∀ (x : ℝ), ‖Complex.exp (↑x * Complex.I)‖ = 1
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A subset of a concyclic set is concyclic.  -/
EuclideanGeometry.Concyclic.subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps₁ ps₂ : Set P},
  ps₁ ⊆ ps₂ → EuclideanGeometry.Concyclic ps₂ → EuclideanGeometry.Concyclic ps₁
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_add_succ_right_eq_push : ∀ {m n : ℕ}, (m<...=m + n + 1).toArray = (m<...=m + n).toArray.push (m + n + 1)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_le_iff_le_comap : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {f : K →+* L} {s : Subfield K}
  {t : Subfield L}, Subfield.map f s ≤ t ↔ s ≤ Subfield.comap f t
-- Mathlib.Analysis.Complex.Norm
Complex.re_le_norm : ∀ (z : ℂ), z.re ≤ ‖z‖
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.isBuiltinSimproc : Lean.Name → Lean.CoreM Bool
-- Mathlib.Data.FinEnum.Option
_private.Mathlib.Data.FinEnum.Option.0.FinEnum.recEmptyOption.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : 0 = 0 → motive 0) (h_2 : (n : ℕ) → 0 = n.succ → motive n.succ),
  (match cardeq : 0 with
    | 0 => h_1 cardeq
    | n.succ => h_2 n cardeq) =
    h_1 ⋯
-- Mathlib.CategoryTheory.Subobject.Limits
/-- Precomposing by an isomorphism does not change the image subobject.  -/
CategoryTheory.Limits.imageSubobject_iso_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C}
  (h : X' ⟶ X) [inst_2 : CategoryTheory.IsIso h] (f : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) = CategoryTheory.Limits.imageSubobject f
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.mk.inj : ∀ {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}
  {φK : h₁.K ⟶ h₂.K} {φH : h₁.H ⟶ h₂.H}
  {commi :
    autoParam (CategoryTheory.CategoryStruct.comp φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commi._autoParam}
  {commf' :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.f' φK = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f')
      CategoryTheory.ShortComplex.LeftHomologyMapData.commf'._autoParam}
  {commπ :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.π φH = CategoryTheory.CategoryStruct.comp φK h₂.π)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commπ._autoParam}
  {φK_1 : h₁.K ⟶ h₂.K} {φH_1 : h₁.H ⟶ h₂.H}
  {commi_1 :
    autoParam (CategoryTheory.CategoryStruct.comp φK_1 h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commi._autoParam}
  {commf'_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.f' φK_1 = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f')
      CategoryTheory.ShortComplex.LeftHomologyMapData.commf'._autoParam}
  {commπ_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.π φH_1 = CategoryTheory.CategoryStruct.comp φK_1 h₂.π)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commπ._autoParam},
  { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ } =
      { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 } →
    φK = φK_1 ∧ φH = φH_1
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall : ∀ {C : Type u} {hC : CategoryTheory.Category.{v, u} C} (κ : Cardinal.{w}) {hκ : Fact κ.IsRegular}
  [self : CategoryTheory.HasCardinalFilteredGenerator C κ], CategoryTheory.LocallySmall.{w, v, u} C
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse.eq_1 : ∀ (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],
  CategoryTheory.Equivalence.symmEquivInverse C D =
    { obj := fun e => Opposite.op e.symm,
        map := fun {e f} α =>
          (CategoryTheory.Equivalence.mkHom
              ((CategoryTheory.conjugateEquiv e.symm.toAdjunction f.symm.toAdjunction).invFun
                (CategoryTheory.Equivalence.asNatTrans α))).op,
        map_id := ⋯, map_comp := ⋯ }.leftOp
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice : ∀ (K : Type u_1) [inst : Field K] [NumberField K], DiscreteTopology ↥(NumberField.mixedEmbedding.integerLattice K)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnMonoidHom.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Monoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G], ContMDiffMap.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.neg_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L),
  -x = { left := -x.left, right := -x.right }
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.OverMkHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      {f : I ⟶ J} →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
          [CategoryTheory.ExponentiableMorphism f] → CategoryTheory.ExponentiableMorphism (CategoryTheory.Over.mk f).hom
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
/-- A version of **Markov's inequality** for two functions. It doesn't follow from the standard
Markov's inequality because we only assume measurability of `g`, not `f`.  -/
MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f ≤ᵐ[μ] g → AEMeasurable g μ → ∀ (ε : ENNReal), ∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
-- Lean.Elab.Util
Lean.Elab.MacroStackElem.after : Lean.Elab.MacroStackElem → Lean.Syntax
-- Aesop.Forward.State
/-- A hypothesis that was matched against a premise, or a rule pattern
substitution.  -/
Aesop.Hyp : Type
-- Lean.LocalContext
/-- Sets the `nondep` flag of an `ldecl`, otherwise returns `cdecl`s unchanged.

This is a low-level function, and it is the responsibility of the caller to ensure that
transitions of `nondep` are valid.

Rules:
- If the declaration is not under the caller's control, then setting `nondep := false` must not be done.
  General nondependent `ldecl`s should be treated like `cdecl`s.
  See also the docstring for `LocalDecl.ldecl` about the `value` not necessarily being type correct.
- Setting `nondep := true` is usually fine.
  - Caution: be sure any relevant caches are cleared so that the value associated to this `FVarId` does not leak.
  - Caution: be sure that metavariables dependent on this declaration created before and after the transition are not mixed,
    since unification does not check "`nondep`-compatibility" of local contexts when assigning metavariables.

For example, setting `nondep := false` is fine from within a telescope combinator, to update the local context
right before calling `mkLetFVars`:
```lean
let lctx ← getLCtx
letTelescope e fun xs b => do
  let lctx' ← xs.foldlM (init := lctx) fun lctx' x => do
    let decl ← x.fvarId!.getDecl
    -- Clear the flag if it's not a prop.
    let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
    pure <| lctx'.addDecl decl'
  withLCtx' lctx' do
    mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b
```
1. The declarations for `xs` are in the control of this metaprogram.
2. `mkLetFVars` does make use of `MetaM` caches.
3. Even if `e` has metavariables, these do not include `xs` in their contexts,
   so the change of the `nondep` flag does not cause any issues in the `abstractM` system used by `mkLetFVars`.
 -/
Lean.LocalDecl.setNondep : Lean.LocalDecl → Bool → Lean.LocalDecl
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_eq_sub : ∀ {p t : ℝ}, p ≠ 1 → 0 < t → p.rpowIntegrand₀₁ t = fun x => t ^ (p - 1) - t ^ p * (t + x)⁻¹
-- Mathlib.Algebra.Group.Hom.Defs
instSubsingletonAddMonoidHom : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] [Subsingleton M], Subsingleton (M →+ N)
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.parallelComp_self_comp_copy : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsDeterministic κ],
  (κ.parallelComp κ).comp (ProbabilityTheory.Kernel.copy α) = (ProbabilityTheory.Kernel.copy β).comp κ
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Fold a function on the values from right to left (in decreasing order).  -/
RBTree.RBSet.foldr : {α : Type u_1} → {σ : Sort u_2} → {cmp : α → α → Ordering} → (α → σ → σ) → σ → RBTree.RBSet α cmp → σ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km : α} (hc : k ∈ t), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : Monoid β] {s : Set α} {t : Set β},
  ThreeGPFree s → ThreeGPFree t → ThreeGPFree (s ×ˢ t)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toNondegComplex_fromNondegComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.CategoryStruct.comp s.toNondegComplex s.fromNondegComplex = AlgebraicTopology.DoldKan.PInfty
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_mul : ∀ {R : Type u_1} [inst : NonUnitalCommRing R] [inst_1 : StarRing R] (x y : ↥(selfAdjoint R)), ↑(x * y) = ↑x * ↑y
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_of_notMem_mulTSupport : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  [inst_11 : One M'] {x : M}, x ∉ mulTSupport f → ∀ (n : WithTop ℕ∞) (s : Set M), ContMDiffWithinAt I I' n f s x
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.Pattern.Model.find?_eq_some_iff.match_1_2.eq_1 : ∀ {s : String.Slice} (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (s_1 endPos : s.Pos)
  (h_1 : (s_2 endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched s_2 endPos))
  (h_2 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos)),
  (match String.Slice.Pattern.SearchStep.matched s_1 endPos with
    | String.Slice.Pattern.SearchStep.matched s_2 endPos => h_1 s_2 endPos
    | String.Slice.Pattern.SearchStep.rejected startPos endPos => h_2 startPos endPos) =
    h_1 s_1 endPos
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_eq' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Fintype σ] (X : σ → R) (f : MvPolynomial σ R),
  (MvPolynomial.eval X) f = ∑ d ∈ f.support, MvPolynomial.coeff d f * ∏ i, X i ^ d i
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basisAux_map_smul : ∀ {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (a : A)
  (x : TensorProduct R A M), (Algebra.TensorProduct.basisAux A b) (a • x) = a • (Algebra.TensorProduct.basisAux A b) x
-- Init.Data.Bool
Bool.beq_eq_decide_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : DecidableEq α] (a b : α), (a == b) = decide (a = b)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.mk : ∀ {k : Type u} [inst : Field k], (∀ (p : Polynomial k), p.Splits) → IsAlgClosed k
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_bind : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} [inst : Monad m] [LawfulMonad m] {x : Std.Iterators.HetT m α}
  {f : α → Std.Iterators.HetT m β}, (x.bind f).Property = fun b => ∃ a, x.Property a ∧ (f a).Property b
-- Init.Data.ToString.Name
/-- Uses the separator `sep` (usually `"."`) to combine the components of the `Name` into a string.
See the documentation for `Name.toStringWithToken` for an explanation of `escape` and `isToken`.
 -/
Lean.Name.toStringWithSep : String → Bool → Lean.Name → (optParam (String → Bool) fun x => false) → String
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The preimage of a set `s` under a continuous linear equiv `f` has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E ≃L[ℝ] E) (s : Set E),
  μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑↑f.symm| * μ s
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.sparsePairs_mono : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε ε' : 𝕜},
  ε ≤ ε' → P.sparsePairs G ε ⊆ P.sparsePairs G ε'
-- Mathlib.Order.CompleteLattice.Group
iSup_add_le : ∀ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] [inst_1 : Add α] [AddLeftMono α] [AddRightMono α]
  (u v : ι → α), ⨆ i, u i + v i ≤ (⨆ i, u i) + ⨆ i, v i
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : RightCancelSemigroup M],
  Filter.Germ.instRightCancelSemigroup = { toSemigroup := Filter.Germ.instSemigroup, toIsRightCancelMul := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  k' ∈ Std.DHashMap.Const.alter m k f ↔
    if (k == k') = true then (f (Std.DHashMap.Const.get? m k)).isSome = true else k' ∈ m
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearEquiv.ofBijective_symm_apply_apply : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : (↑f).ker = ⊥) (hsurj : (↑f).range = ⊤) (x : E),
  (ContinuousLinearEquiv.ofBijective f hinj hsurj).symm (f x) = x
-- Lean.Expr
Lean.Expr.binderInfoEx : Lean.Expr → Lean.BinderInfo
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- For any `j`, the map `(functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j)`
is a transfinite composition of pushouts of monomorphisms in the
family `generatingMonomorphisms G`.  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeMapFromBot : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : C} →
      [inst_1 : CategoryTheory.Abelian C] →
        (hG : CategoryTheory.IsSeparator G) →
          {X : C} →
            [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
              (A₀ : CategoryTheory.Subobject X) →
                {J : Type w} →
                  [inst_3 : LinearOrder J] →
                    [inst_4 : OrderBot J] →
                      [inst_5 : SuccOrder J] →
                        [inst_6 : WellFoundedLT J] →
                          (j : J) →
                            (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms
                                    G).pushouts.TransfiniteCompositionOfShape
                              (↑(Set.Iic j))
                              ((CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor hG A₀ J).map
                                (CategoryTheory.homOfLE ⋯))
-- Mathlib.Order.Hom.Basic
/-- Given two bundled monotone maps `f`, `g`, `f.prod g` is the map `x ↦ (f x, g x)` bundled as a
`OrderHom`. This is a fully bundled version.  -/
OrderHom.prodₘ : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Preorder γ] → (α →o β) →o (α →o γ) →o α →o β × γ
-- Mathlib.Order.ModularLattice
covBy_sup_of_inf_covBy_of_inf_covBy_left : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P) (m : M) (n : N), (LinearMap.rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m
-- Mathlib.Data.Matrix.Basis
/-- `M` is a scalar matrix if and only if it commutes with every `single`.  -/
Matrix.mem_range_scalar_iff_commute_single' : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α] {M : Matrix n n α},
  M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), Commute (Matrix.single i j 1) M
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.extensiveCoverage.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.extensiveCoverage C =
    {
      coverings := fun B =>
        {S |
          ∃ α,
            ∃ (x : Finite α),
              ∃ X π,
                S = CategoryTheory.Presieve.ofArrows X π ∧ CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)},
      pullback := ⋯ }
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_mono_set : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ (n : ℕ) (a : α) (x : γ) {s s' : Set β}, s ⊆ s' → κ.densityProcess ν n a x s ≤ κ.densityProcess ν n a x s'
-- Init.Grind.Ring.Basic
Lean.Grind.PowIdentity.pow : ∀ {α : Type u_1} {p : ℕ} [inst : Lean.Grind.CommSemiring α] [Lean.Grind.PowIdentity α p] (x : α), x ^ p = x
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then
`f` is a strictly monotone function.  -/
strictAnti_of_hasDerivAt_neg : ∀ {f f' : ℝ → ℝ}, (∀ (x : ℝ), HasDerivAt f (f' x) x) → (∀ (x : ℝ), f' x < 0) → StrictAnti f
-- Mathlib.GroupTheory.Finiteness
/-- A subgroup is finitely generated if and only if it is finitely generated as a submonoid.  -/
Subgroup.fg_iff_submonoid_fg : ∀ {G : Type u_3} [inst : Group G] (P : Subgroup G), P.FG ↔ P.FG
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Mon.denote : Nat.Internal.Linear.Context → Nat.Internal.SOM.Mon → ℕ
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
/-- The natural map between `Unitization 𝕜 A` and `𝕜 × A`, transferred to their `WithLp 1`
synonyms.  -/
WithLp.unitization_addEquiv_prod : (𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] → [NormedSpace 𝕜 A] → WithLp 1 (Unitization 𝕜 A) ≃+ WithLp 1 (𝕜 × A)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.maxDegree.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  G.maxDegree = WithBot.unbotD 0 (Finset.image (fun v => G.degree v) Finset.univ).max