mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- To bound the Hausdorff measure (or, more generally, for a measure defined using
`MeasureTheory.Measure.mkMetric`) of a set, one may use coverings with maximum diameter tending to
`0`, indexed by any sequence of countable types.  -/
MeasureTheory.Measure.mkMetric_le_liminf_tsum : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
  {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal),
  Filter.Tendsto r l (nhds 0) →
    ∀ (t : (n : β) → ι n → Set X),
      (∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) →
        (∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
          ∀ (m : ENNReal → ENNReal),
            (MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑' (i : ι n), m (Metric.ediam (t n i))) l
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Lean.Server.Requests
Lean.Server.LspResponse.mk.inj : ∀ {α : Type} {response : α} {isComplete : Bool} {response_1 : α} {isComplete_1 : Bool},
  { response := response, isComplete := isComplete } = { response := response_1, isComplete := isComplete_1 } →
    response = response_1 ∧ isComplete = isComplete_1
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mk : {D : Type u_1} → {Q : Type u_2} → (Q → D) → Q → D ≀ᵣ Q
-- Std.Data.String.ToInt
String.toInt?_eq_none_iff : ∀ {s : String}, s.toInt? = none ↔ s.isInt = false
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
SSet.instIsLeftAdjointSd : SSet.sd.IsLeftAdjoint
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.arrowCongrEquivₛₗ_symm_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_5 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_8 : TopologicalSpace M₂]
  [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  {M₄ : Type u_7} [inst_12 : TopologicalSpace M₄] [inst_13 : AddCommMonoid M₄] [inst_14 : Module R₁ M₁]
  [inst_15 : Module R₂ M₂] [inst_16 : Module R₃ M₃] {R₄ : Type u_8} [inst_17 : Semiring R₄] [inst_18 : Module R₄ M₄]
  {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [inst_19 : RingHomInvPair σ₃₄ σ₄₃] [inst_20 : RingHomInvPair σ₄₃ σ₃₄]
  {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [inst_21 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
  [inst_22 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_23 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [inst_24 : SMulCommClass R₃ R₃ M₃]
  [inst_25 : SMulCommClass R₄ R₄ M₄] [inst_26 : ContinuousAdd M₃] [inst_27 : ContinuousConstSMul R₃ M₃]
  [inst_28 : ContinuousAdd M₄] [inst_29 : ContinuousConstSMul R₄ M₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃)
  (a : M₂ →SL[σ₂₃] M₃), ⋯ a = ⋯.invFun a
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.ι.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  SymmetricAlgebra.ι R M = ↑(SymmetricAlgebra.algHom R M) ∘ₗ TensorAlgebra.ι R
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.map_zero₂ : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (y : F),
  (f 0) y = 0
-- Mathlib.Algebra.IsPrimePow
Nat.Prime.isPrimePow : ∀ {p : ℕ}, Nat.Prime p → IsPrimePow p
-- Mathlib.Topology.Order.ProjIcc
continuous_projIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {h : a ≤ b} [inst_1 : TopologicalSpace α] [OrderTopology α],
  Continuous (Set.projIcc a b h)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep.sndSkip : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  {it₂' it₂ : Std.IterM m β},
  it₂.IsPlausibleStep (Std.IterStep.skip it₂') →
    Std.Iterators.Types.Append.PlausibleStep (Std.IterM.Intermediate.appendSnd α₁ it₂)
      (Std.IterStep.skip (Std.IterM.Intermediate.appendSnd α₁ it₂'))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.startsWith_string_eq_false_iff : ∀ {pat s : String}, s.startsWith pat = false ↔ ¬pat.toList <+: s.toList
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ ν : MeasureTheory.Measure α},
  MeasureTheory.IsFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ • s) (g₂ • s)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedState.default : Lean.Meta.State
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.instIsIsoFunctorTopCatHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') [CategoryTheory.IsIso f]
  (i : ι), CategoryTheory.IsIso (f.hom i)
-- Mathlib.Order.Defs.LinearOrder
/-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`.  -/
LinearOrder.compare_eq_compareOfLessAndEq : ∀ {α : Type u_2} [self : LinearOrder α] (a b : α), compare a b = compareOfLessAndEq a b
-- Mathlib.Data.List.Indexes
List.mapIdxMAux'.eq_1 : ∀ {m : Type v → Type w} [inst : Monad m] {α : Type u_7} (f : ℕ → α → m PUnit.{v + 1}) (x : ℕ),
  List.mapIdxMAux' f x [] = pure PUnit.unit
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.ker_snd : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'], (MonoidHom.snd G G').ker = ⊤.prod ⊥
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A subset of a coplanar set is coplanar.  -/
Coplanar.subset : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → Coplanar k s₂ → Coplanar k s₁
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux M).inv = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.Order.MinMax
instAssociativeMax : ∀ {α : Type u} [inst : LinearOrder α], Std.Associative max
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opUnopEquiv_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Functor.opUnopEquiv C D).inverse = CategoryTheory.Functor.opInv C D
-- Mathlib.Logic.Function.Coequalizer
Function.Coequalizer.mk_surjective : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β), Function.Surjective (Function.Coequalizer.mk f g)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_lt_pow : ∀ {n : ℕ}, n ≠ 0 → ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- `lightToProfinite` is fully faithful.  -/
lightToProfiniteFullyFaithful : lightToProfinite.FullyFaithful
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.hasBasis_zero_ball : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → (nhds 0).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball 0 sr.2
-- Mathlib.NumberTheory.LSeries.RiemannZeta
completedRiemannZeta₀.eq_1 : ∀ (s : ℂ), completedRiemannZeta₀ s = HurwitzZeta.completedHurwitzZetaEven₀ 0 s
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromLeftInv_leftInvEquiv_symm : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S),
  S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The `3`-division polynomial `ψ₃ = Ψ₃`.  -/
WeierstrassCurve.Ψ₃ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → Polynomial R
-- Mathlib.NumberTheory.Modular
ModularGroup.im_T_inv_smul : ∀ (z : UpperHalfPlane), (ModularGroup.T⁻¹ • z).im = z.im
-- Lean.Environment
/-- Import including information resulting from processing of the entire import DAG.  -/
Lean.EffectiveImport : Type
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtDHashMap.Const.ofList l).getKeyD k' fallback = k
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.objectEnd : Lean.Json.CompressWorkItemKind✝
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.exists_Finpartition_sum_gt : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s) {a : ENNReal},
  a < MeasureTheory.preVariationFun f s → ∃ P, a < ∑ p ∈ P.parts, f ↑p
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects colimits for `K : J ⥤ C` if
whenever the image of a cocone over `K` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
 -/
CategoryTheory.Limits.ReflectsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor J C → CategoryTheory.Functor C D → Prop
-- Mathlib.Analysis.Complex.Exponential
Real.prod_one_add_le_exp_sum : ∀ {ι : Type u_1} (s : Finset ι) {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → ∏ i ∈ s, (1 + f i) ≤ Real.exp (∑ i ∈ s, f i)
-- Mathlib.Data.Int.Init
Int.leInductionDown_sub_one : ∀ {m : ℤ} {motive : (n : ℤ) → n ≤ m → Sort u_1} (base : motive m ⋯)
  (pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯) (n : ℤ) (hnm : n ≤ m),
  Int.leInductionDown base pred (n - 1) ⋯ = pred n hnm (Int.leInductionDown base pred n hnm)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeWhile_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → (s.takeWhile pat).copy = (t.takeWhile pat).copy
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.star_val_eq : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : StarAddMonoid R] {x : ↥(skewAdjoint R)}, star ↑x = -↑x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instIsSimpleOrderOfSubsingleton : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] [Subsingleton P], IsSimpleOrder (AffineSubspace k P)
-- Mathlib.Order.WithBot
WithTop.map₂_top_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithTop β), WithTop.map₂ f ⊤ b = ⊤
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_dom : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : SeparationQuotient α → β},
  UniformContinuous f ↔ UniformContinuous (f ∘ SeparationQuotient.mk)
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- The Beck cofork is a coequalizer.  -/
CategoryTheory.Monad.beckCoequalizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → (X : T.Algebra) → CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.beckCofork X)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The left-inverse of a `MeasurableEmbedding`  -/
MeasurableEmbedding.invFun : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → {f : α → β} → [Nonempty α] → MeasurableEmbedding f → β → α
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d = (F.map f).unmop.app d
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Variant of `IsPushout.of_top` where `v₂₂` is induced from a morphism `v₁₃ : X₁₂ ⟶ X₃₂`, and
the universal property of the top square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
|            |
v₁₁          v₁₂
↓            ↓
X₂₁ - h₂₁ -> X₂₂
|            |
v₂₁          v₂₂
↓            ↓
X₃₁ - h₃₁ -> X₃₂
```
 -/
CategoryTheory.IsPushout.of_top' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₂ ⟶ X₃₂} {v₂₁ : X₂₁ ⟶ X₃₁}
  (s : CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) v₁₃ h₃₁)
  (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁),
  CategoryTheory.IsPushout h₂₁ v₂₁ (t.desc v₁₃ (CategoryTheory.CategoryStruct.comp v₂₁ h₃₁) ⋯) h₃₁
-- Mathlib.Algebra.Group.ULift
ULift.divInvMonoid : {α : Type u} → [DivInvMonoid α] → DivInvMonoid (ULift.{u_1, u} α)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.is_descending_rev_series_of_is_ascending : ∀ (G : Type u_1) [inst : AddGroup G] {H : ℕ → AddSubgroup G} {n : ℕ},
  H n = ⊤ → AddSubgroup.IsAscendingCentralSeries H → AddSubgroup.IsDescendingCentralSeries fun m => H (n - m)
-- Mathlib.Data.List.Permutation
List.length_permutationsAux2 : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts ys : List α) (f : List α → β),
  (List.permutationsAux2 t ts [] ys f).2.length = ys.length
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The fully faithful embedding of `LightProfinite` in `CompHaus`.  -/
lightProfiniteToCompHaus : CategoryTheory.Functor LightProfinite CompHaus
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.interior_setOfPred_re_le`. -/
Complex.interior_setOf_re_le : ∀ (a : ℝ), interior {z | z.re ≤ a} = {z | z.re < a}
-- Mathlib.Data.Finset.Slice
/-- **Alias** of the reverse direction of `Finset.subset_powersetCard_univ_iff`. -/
Set.Sized.subset_powersetCard_univ : ∀ {α : Type u_1} [inst : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  Set.Sized r ↑𝒜 → 𝒜 ⊆ Finset.powersetCard r Finset.univ
-- Mathlib.Algebra.Algebra.Equiv
/-- The two paths coercion can take to a `RingHom` are equivalent  -/
AlgEquiv.coe_ringHom_commutes : ∀ {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₂] (e : A₁ ≃ₐ[R] A₂), ↑↑e = ↑e.toRingEquiv
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_join.lem : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq β)}
  {U : Stream'.WSeq α → Stream'.WSeq β → Prop},
  Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T →
    (∀ (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq β),
        (∃ s t S T,
            s1 = s.append S.join ∧
              s2 = t.append T.join ∧ Stream'.WSeq.LiftRel R s t ∧ Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) →
          U s1 s2) →
      ∀ {a : Option (α × Stream'.WSeq α)}, a ∈ S.join.destruct → ∃ b ∈ T.join.destruct, Stream'.WSeq.LiftRelO R U a b
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid inherits a power operator.  -/
SubmonoidClass.instPow : {M : Type u_5} → [inst : Monoid M] → {A : Type u_4} → [inst_1 : SetLike A M] → [SubmonoidClass A M] → (S : A) → Pow ↥S ℕ
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Each member of the class tends to zero along the `cocompact` filter.  -/
ZeroAtInftyContinuousMapClass.zero_at_infty : ∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : TopologicalSpace α} {inst_1 : Zero β}
  {inst_2 : TopologicalSpace β} {inst_3 : FunLike F α β} [self : ZeroAtInftyContinuousMapClass F α β] (f : F),
  Filter.Tendsto (⇑f) (Filter.cocompact α) (nhds 0)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.ofTree_toTree : ∀ (p : DyckWord), DyckWord.ofTree p.toTree = p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.keysArray → k ∈ t
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_cons_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a l = true → Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true
-- Init.Data.Int.OfNat
Nat.ToInt.of_diseq : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range (sum over `ℤ`).  -/
HurwitzZeta.hasSum_int_hurwitzZetaOdd : ∀ (a : ℝ) {s : ℂ},
  1 < s.re → HasSum (fun n => ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  {f : (a : α) → β a → Bool} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl = true},
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKey k h' = t.getKey k ⋯
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.instSMul : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → {ps : DiscreteTiling.Protoset G X ιₚ} → SMul G (DiscreteTiling.PlacedTile ps)
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- Given the condition `[Sub n]` and a vector `v : n → α`,
we define `circulant v` to be the circulant matrix generated by `v` of type `Matrix n n α`.
The `(i,j)`th entry is defined to be `v (i - j)`.  -/
Matrix.circulant : {α : Type u_1} → {n : Type u_3} → [Sub n] → (n → α) → Matrix n n α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.instIsLeftAdjointPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint], (SheafOfModules.pullback φ).IsLeftAdjoint
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_comp : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y) (g : Y.Hom Z),
  ⟦f.comp g⟧ = CategoryTheory.CategoryStruct.comp ⟦f⟧ ⟦g⟧
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_id : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.id X⟧ = CategoryTheory.CategoryStruct.id X
-- Lean.DocString.Extension
Lean.doc.verso.module : Lean.Option Bool
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] → [inst_1 : Semiring R] → [IsTopologicalSemiring R] → Semiring (SeparationQuotient R)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- If `c` is a fork, then `c.op.unop` is isomorphic to `c`.  -/
CategoryTheory.Limits.Fork.opUnopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f g : X ⟶ Y} → (c : CategoryTheory.Limits.Fork f g) → c.op.unop ≅ c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} {l : List α} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.Const.insertManyIfNewUnit t l) k = ()
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_equiv_inf : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  {a₁ b₁ a₂ b₂ : CauSeq α abs}, a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⊓ b₁ ≈ a₂ ⊓ b₂
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Ioc_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Ioc (Fin.castLE h i) (Fin.castLE h j) = Set.Ioc i j
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.Equiv ∅ ↔ m.isEmpty = true
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKeyD k' fallback = k
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instInhabitedSubalgebra : {R : Type u} →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Inhabited (Subalgebra R A)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- **Alias** of `MeasureTheory.lintegral_inter_add_sdiff`. -/
MeasureTheory.lintegral_inter_add_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {B : Set α} (f : α → ENNReal) (A : Set α),
  MeasurableSet B → ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lcs_sup : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N₁ N₂ : LieSubmodule R L M} {k : ℕ},
  LieSubmodule.lcs k (N₁ ⊔ N₂) = LieSubmodule.lcs k N₁ ⊔ LieSubmodule.lcs k N₂
-- Mathlib.Algebra.Order.Group.PosPart
negPart_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α], 0⁻ = 0