mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instSubsingletonHomLeft : ∀ {J : CategoryTheory.Limits.MultispanShape} (a b : J.L),
  Subsingleton (CategoryTheory.Limits.WalkingMultispan.left a ⟶ CategoryTheory.Limits.WalkingMultispan.left b)
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf.eq_def : ∀ (x : ℕ),
  x.zeckendorf =
    match x with
    | 0 => []
    | m@h:n.succ => m.greatestFib :: (m - Nat.fib m.greatestFib).zeckendorf
-- Mathlib.Data.Real.ConjExponents
ENNReal.isConjExponent_iff_eq_conjExponent : ∀ {p q : ENNReal}, 1 ≤ p → (p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map_of_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) {f : G →+ G'},
  Function.Injective ⇑f → (AddSubgroup.map f H).index = H.index * f.range.index
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) (J : Type u_1),
  T.rlp.IsStableUnderProductsOfShape J
-- Aesop.Tree.Data
Aesop.GoalData.mvars : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.UnorderedArraySet Lean.MVarId
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_toUSize : ∀ (n : UInt64), n.toUSize.toUInt32 = n.toUInt32
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) [inst_2 : CategoryTheory.IsFiltered J],
  h.coconeιApp i₀ = CategoryTheory.CategoryStruct.id (F.obj i₀)
-- Mathlib.Topology.FiberBundle.Basic
/-- The fiber of a fiber bundle core, as a convenience function for dot notation and
typeclass inference  -/
FiberBundleCore.Fiber : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} → [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → B → Type u_3
-- Init.Data.String.FindPos
/-- Returns the previous valid position before the given position, or panics if the position is
the start position.  -/
String.Pos.prev! : {s : String} → s.Pos → s.Pos
-- Mathlib.CategoryTheory.Sums.Basic
/-- Precomposing `swap` with the left inclusion gives the right inclusion.  -/
CategoryTheory.Sum.swapCompInl : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Sum.inl_ C D).comp (CategoryTheory.Sum.swap C D) ≅ CategoryTheory.Sum.inr_ D C
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.power_mul : ∀ {a b c : Cardinal.{u_1}}, a ^ (b * c) = (a ^ b) ^ c
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.coeAddMonoidHom_of : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] (A : ι → S) (i : ι) (x : ↥(A i)),
  (DirectSum.coeAddMonoidHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
_private.Mathlib.FieldTheory.PurelyInseparable.Exponent.0.IsPurelyInseparable.iterateFrobeniusAux : (K : Type u_2) →
  (L : Type u_3) →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → [IsPurelyInseparable.HasExponent K L] → ℕ → ℕ → L → K
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.mk : {α : Type u_1} →
  (Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α) →
    α → Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.map_intCast_injective : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [CharZero R],
  Function.Injective ⇑(Matrix.SpecialLinearGroup.map (Int.castRingHom R))
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder : ∀ {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [inst : Ring R] {f g : MvPowerSeries σ R} {d : σ →₀ ℕ},
  ↑((Finsupp.weight w) d) < MvPowerSeries.weightedOrder w g →
    (MvPowerSeries.coeff d) (f * (1 - g)) = (MvPowerSeries.coeff d) f
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.mk : Lean.FVarIdHashSet → Lean.FVarIdHashSet → Array Lean.LocalDecl → Array Lean.Expr → Lean.Meta.Closure.TopoSort✝
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of a Dirichlet character does not vanish on the right half-plane `re s > 1`.  -/
DirichletCharacter.LSeries_ne_zero_of_one_lt_re : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ}, 1 < s.re → LSeries (fun n => χ ↑n) s ≠ 0
-- Mathlib.Logic.Equiv.Basic
/-- A function is invariant to a swap if it is equal at both elements  -/
Equiv.apply_swap_eq_self : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] {v : α → β} {i j : α},
  v i = v j → ∀ (k : α), v ((Equiv.swap i j) k) = v k
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentialsRelations_G : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ), pres.differentialsRelations.G = ι
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.natCast_zero : ∀ {α : Type u_1}, ↑0 = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N),
  H.prod K = { toAddSubmonoid := H.prod K.toAddSubmonoid, neg_mem' := ⋯ }
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A noncomputable quotient to define the Euclidean domain structure. The GCD algorithm only takes
two steps to terminate. Given `GCD(x,y)`, if `x ∣ y` then `y%x = 0` so we're done in one step;
otherwise `y%x = y` and then `GCD(x,y) = GCD(y,x)` which brings us back to the first case.  -/
IsDiscreteValuationRing.quotient : {R : Type u_2} → [CommRing R] → R → R → R
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.not_isNontrivial_apply : ∀ {R : Type u_5} [inst : Semiring R] {S : Type u_6} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v : AbsoluteValue R S}, ¬v.IsNontrivial → ∀ {x : R}, x ≠ 0 → v x = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Mathlib.Algebra.Group.Hom.Defs
/-- `OneHom M N` is the type of functions `M → N` that preserve one.

When possible, instead of parametrizing results over `(f : OneHom M N)`,
you should parametrize over `(F : Type*) [OneHomClass F M N] (f : F)`.

When you extend this structure, make sure to also extend `OneHomClass`.
 -/
OneHom : (M : Type u_10) → (N : Type u_11) → [One M] → [One N] → Type (max u_10 u_11)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.open_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F},
  ApproximatesLinearOn f f' s c →
    ∀ (f'symm : f'.NonlinearRightInverse), IsOpen s → Subsingleton F ∨ c < f'symm.nnnorm⁻¹ → IsOpen (f '' s)
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.hasCoeToSort : {C : Type u₁} →
  {D : Type u₂} → (F : C → D) → {α : Sort u_1} → [CoeSort D α] → CoeSort (CategoryTheory.InducedCategory D F) α
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- An integer `n` is divisible by `ζ - 1` in `𝓞 K` if and only if it is divisible by `p`,
where `ζ` is a primitive `p ^ (k + 1)`-th root of unity.  -/
IsCyclotomicExtension.Rat.zeta_sub_one_dvd_intCast_iff : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {n : ℤ},
  hζ.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.mem_map_restrict_ae_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {s : Set α} {t : Set β}
  {f : α → β}, MeasurableSet s → (t ∈ Filter.map f (MeasureTheory.ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0)
-- Lean.Widget.InteractiveGoal
Lean.Widget.withGoalCtx : {n : Type → Type} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      [Lean.MonadError n] →
        [Lean.MonadOptions n] →
          [Lean.MonadMCtx n] → {α : Type} → Lean.MVarId → (Lean.LocalContext → Lean.MetavarDecl → n α) → n α
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.uniformity_toTopologicalSpace_eq : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)),
  (UniformConvergenceCLM.instUniformSpace σ F 𝔖).toTopologicalSpace = UniformConvergenceCLM.instTopologicalSpace σ F 𝔖
-- Mathlib.Data.Part
Part.getOrElse_of_not_dom : ∀ {α : Type u_1} (a : Part α), ¬a.Dom → ∀ [inst : Decidable a.Dom] (d : α), a.getOrElse d = d
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_left : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) (P : CategoryTheory.Functor C₀ᵒᵖ A) (i : data.multicospanShape.L),
  (data.multicospanIndex P).left i = P.obj (Opposite.op (data.X i))
-- Mathlib.Tactic.TacticAnalysis
/-- `ContextInfo` at the infotree node.  -/
Mathlib.TacticAnalysis.TacticNode.ctxI : Mathlib.TacticAnalysis.TacticNode → Lean.Elab.ContextInfo
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_subset_Icc_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a c ⊆ Set.Icc a b ∪ Set.Ico b c
-- Init.Prelude
/-- Unconditional error recovery that ignores which exception was thrown. Usually used via the `<|>`
operator.

If both computations throw exceptions, then the result is the second exception.
 -/
MonadExcept.orElse : {ε : Type u} → {m : Type v → Type w} → [MonadExcept ε m] → {α : Type v} → m α → (Unit → m α) → m α
-- Mathlib.Algebra.Group.TransferInstance
Equiv.group.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Group β], e.group = Function.Injective.group ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.GroupTheory.OrderOfElement
Submonoid.orderOf_le_card : ∀ {G : Type u_6} [inst : Group G] (s : Submonoid G), (↑s).Finite → ∀ {x : G}, x ∈ s → orderOf x ≤ Nat.card ↥s
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) {K₂ L₂ : CochainComplex C₂ ℤ} (f₂ : K₂ ⟶ L₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F]
  [inst_9 : K₁.HasMapBifunctor L₂ F] {Z : HomologicalComplex D (ComplexShape.up ℤ)}
  (h : (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor L₂ F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁)
        ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).map f₂) F (ComplexShape.up ℤ))
      (CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₂Iso L₂ F y).hom h) =
    CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₂Iso K₂ F y).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
          (HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) f₂ F (ComplexShape.up ℤ)))
        h)
-- Mathlib.Topology.Homotopy.Lifting
/-- The path lifting property (existence) for covering maps.  -/
IsCoveringMap.exists_path_lifts : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X},
  IsCoveringMap p → ∀ (γ : C(↑unitInterval, X)) (e : E), γ 0 = p e → ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e
-- Std.Data.String.ToNat
String.isNat_iff : ∀ {s : String},
  s.isNat = true ↔
    s ≠ "" ∧
      (∀ c ∈ s.toList, c.isDigit = true ∨ c = '_') ∧
        ¬['_', '_'] <:+: s.toList ∧ s.toList.head? ≠ some '_' ∧ s.toList.getLast? ≠ some '_'
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.closure_singleton_eq : ∀ {A : Type u_2} [inst : AddMonoid A] (x : A), AddSubmonoid.closure {x} = AddMonoidHom.mrange ((multiplesHom A) x)
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.algebraTensorAlgEquiv_symm_monomial : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (m : σ →₀ ℕ) (a : A),
  (MvPolynomial.algebraTensorAlgEquiv R A).symm ((MvPolynomial.monomial m) a) = a ⊗ₜ[R] (MvPolynomial.monomial m) 1
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial.eq_2 : Nat.doubleFactorial 1 = 1
-- Mathlib.Analysis.Complex.JensenFormula
/-- **Jensen's Inequality**: Estimates the number of zeros of `f` in a ball of radius `r`
given that `f` is analytic and bounded by `M` on a larger ball of radius `R`.
 -/
AnalyticOnNhd.sum_divisor_le : ∀ {c : ℂ} {r R M : ℝ} {f : ℂ → ℂ},
  0 < |r| →
    |r| < |R| →
      1 ≤ M →
        AnalyticOnNhd ℂ f (Metric.closedBall c |R|) →
          f c ≠ 0 →
            (∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ M) →
              ↑(∑ᶠ (u : ℂ), (MeromorphicOn.divisor f (Metric.closedBall c |r|)) u) ≤
                Real.log (M / ‖f c‖) / Real.log (R / r)
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.mk_eq_mk_of_inv_mul_mem : ∀ {α : Type u_1} {rels : Set (FreeGroup α)} {x y : FreeGroup α},
  x⁻¹ * y ∈ rels → (PresentedGroup.mk rels) x = (PresentedGroup.mk rels) y
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Ric.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Ric α} {s : Std.Rco α}, a ∈ Std.Ric.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Ric.LawfulRcoIntersection α
-- Mathlib.Topology.Order.Category.AlexDisc
alexDiscEquivPreord_functor : alexDiscEquivPreord.functor = (CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord
-- Lean.Meta.Basic
/-- Zeta reduction for unused let-declarations: `let x := v; e` reduces to `e` when `x` does not occur
in `e`.
This option takes precedence over `zeta` and `zetaHave`.
 -/
Lean.Meta.Config.zetaUnused : Lean.Meta.Config → Bool
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeUnion : {α : Type u} → [DecidableEq α] → (s t : Set α) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s ∪ t)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ContainsUnit.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C}, P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) → P.ContainsUnit
-- Mathlib.MeasureTheory.Measure.Prod
/-- Two finite measures on a product `(α × β) × γ` are equal iff they are equal on products of sets.
See `ext_prod₃_iff` for the same statement for `α × β × γ`.  -/
MeasureTheory.Measure.ext_prod₃_iff' : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ ν : MeasureTheory.Measure ((α × β) × γ)} [MeasureTheory.IsFiniteMeasure μ],
  μ = ν ↔
    ∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.lt_singleton : ∀ {α : Type u_1} {s : Multiset α} {a : α}, s < {a} ↔ s = 0
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.any_filterM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Monad m] [inst_4 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m (ULift.{w, 0} Bool)}
  {p : β → Bool},
  Std.IterM.any p (Std.Iter.filterM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then pure { down := p x } else pure { down := false })
      (Std.Iter.mapM pure it)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- Internal state of the `map` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.Map : Type w →
  {β γ : Type w} →
    (m : Type w → Type w') →
      (n : Type w → Type w'') →
        (⦃α : Type w⦄ → m α → n α) → [Functor n] → (β → Std.Iterators.PostconditionT n γ) → Type w
-- Qq.SortLocalDecls
Qq.SortLocalDecls.Context : Type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_erase_eq_of_not_compare_max!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.erase k).isEmpty = false → ¬cmp k t.max! = Ordering.eq → (t.erase k).max! = t.max!
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsAdjunction_homEquiv_apply_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] {X : Rep.{w, u, v} k G} {Y : ModuleCat k}
  (f : (Rep.coinvariantsFunctor k G).obj X ⟶ Y),
  (Rep.Hom.hom (((Rep.coinvariantsAdjunction k G).homEquiv X Y) f)).toLinearMap =
    ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app X) f)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallWithContext.mk.injEq : ∀ (ref : Lean.Syntax) (caller : ℕ) (params : Array Lean.Expr) (callee : ℕ) (args : Array Lean.Expr)
  (ctxt : Lean.Elab.WF.GuessLex.SavedLocalContext) (ref_1 : Lean.Syntax) (caller_1 : ℕ) (params_1 : Array Lean.Expr)
  (callee_1 : ℕ) (args_1 : Array Lean.Expr) (ctxt_1 : Lean.Elab.WF.GuessLex.SavedLocalContext),
  ({ ref := ref, caller := caller, params := params, callee := callee, args := args, ctxt := ctxt } =
      { ref := ref_1, caller := caller_1, params := params_1, callee := callee_1, args := args_1, ctxt := ctxt_1 }) =
    (ref = ref_1 ∧ caller = caller_1 ∧ params = params_1 ∧ callee = callee_1 ∧ args = args_1 ∧ ctxt = ctxt_1)
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.ofFn.go : {α : Type u_1} → {n : ℕ} → (Fin n → α) → (lb ub : ℕ) → lb < ub → ub ≤ n → Lean.RArray α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.coeff_le_of_forall_abs_le_one : ∀ {n : ℕ} {P : Polynomial ℝ},
  P.degree ≤ ↑n → (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) → P.coeff n ≤ 2 ^ (n - 1)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Occasionally useful for rewriting in the backwards direction.  -/
CategoryTheory.MorphismProperty.Arrow.forget_comp_rightFunc_map : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q W : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} (f : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Arrow.forget P Q W).comp CategoryTheory.Arrow.rightFunc).map f = f.right
-- Lean.Expr
Lean.instReprBinderInfo : Repr Lean.BinderInfo
-- Mathlib.Tactic.FunProp.Mor
/-- Is `name` a coercion from some function space to functions?  -/
Mathlib.Meta.FunProp.Mor.isCoeFunName : Lean.Name → Lean.CoreM Bool
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.mk : {R : Type u} → [inst : CommRing R] → (toModuleCat : ModuleCat R) → QuadraticForm R ↑toModuleCat → QuadraticModuleCat R
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerLeft_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ≅ Gᵣ) (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapIsoWhiskerLeft H α).inv.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (H.obj x))
    | CategoryTheory.Join.right x => (CategoryTheory.Join.inclRight E E').map (α.inv.app x)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The left homology of a short complex, given by the `H` field of a chosen left homology data.  -/
CategoryTheory.ShortComplex.leftHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasLeftHomology] → C
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_of_multiplicity_odd : ∀ (m : ℤ), 0 < m → ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], multiplicity (↑p) m % 2 = 1 → Irrational √↑m
-- Mathlib.Data.Num.Lemmas
PosNum.cast_to_num : ∀ (n : PosNum), ↑n = Num.pos n
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.coeff_eq_zero_of_not_le_supDegree`. -/
AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p : AddMonoidAlgebra R A} {a : A}, ¬D a ≤ AddMonoidAlgebra.supDegree D p → p.coeff a = 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insertMany_ind : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type v} [inst_2 : ForIn Id ρ α]
  {motive : Std.HashSet.Raw α → Prop} (m : Std.HashSet.Raw α) (l : ρ),
  motive m → (∀ (m : Std.HashSet.Raw α) (a : α), motive m → motive (m.insert a)) → motive (m.insertMany l)
-- Mathlib.Order.Filter.CountableInter
Filter.instCountableInterFilterCountableGenerate : ∀ {α : Type u_1} (g : Set (Set α)), CountableInterFilter (Filter.countableGenerate g)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.WithTop.completeLattice : {α : Type u_5} → [ConditionallyCompleteLattice α] → CompleteLattice (WithBot (WithTop α))
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.readAllowAssignmentDiff : Aesop.EqualUpToIdsM Bool
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.LaurentSeriesRingEquiv_def : ∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
  (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f) =
    {
      toCompletion :=
        (LaurentSeries.LaurentSeriesPkg K).compare LaurentSeries.ratfuncAdicComplPkg
          ((HahnSeries.ofPowerSeries ℤ K) f) }
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.symmDiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
  MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (symmDiff s₁ s₂)
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_nsmul : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
  [CompleteSpace 𝔸] (n : ℕ) (A : Matrix m m 𝔸), NormedSpace.exp (n • A) = NormedSpace.exp A ^ n