mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.precompCompactConvergenceCLM_apply`. -/
precomp_compactConvergenceCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} (G : Type u_6) [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F)
  (f : UniformConvergenceCLM τ G {S | IsCompact S}), (ContinuousLinearMap.precompCompactConvergenceCLM G L) f = f ∘SL L
-- Mathlib.Algebra.Order.Floor.Div
/-- Do not use this. Use `gc_smul_ceilDiv` or `gc_mul_ceilDiv` instead.  -/
CeilDiv.ceilDiv_gc : ∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : CeilDiv α β] ⦃a : α⦄,
  0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {u : Set α}, IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S
-- Std.Http.Protocol.H1
/-- Accumulates successfully accepted body bytes into the reader accounting.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.addBodyBytes : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → ℕ → Std.Http.Protocol.H1.Machine dir
-- Init.Data.Array.Monadic
Array.flatMapM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : α → m (Array β)}, Array.flatMapM f (wfParam xs) = Array.flatMapM f xs.attach.unattach
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {l : List (α × β)},
  m.WF → (m.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) m l)
-- Init.Grind.AC
Lean.Grind.AC.norm_ai : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (e : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq),
  e.toSeq.erase0.beq' s = true → Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget_createsLimitsOfSize.eq_1 : GrpCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Init.Data.BitVec.Lemmas
BitVec.le_intMin_of_msb_eq_false : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → x ≤ BitVec.intMin w
-- Mathlib.RingTheory.Ideal.Operations
/-- Generalize `Ideal.IsMaximal.exists_inv` to power of maximal ideals.  -/
Ideal.IsMaximal.exists_inv_pow : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R) [I.IsMaximal] {x : R},
  x ∉ I → ∀ (n : ℕ), ∃ y, ∃ i ∈ I ^ n, y * x + i = 1
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn_1.eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1}
  {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1}
  (t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp)
  (F_1 : (t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t)
  (F_2 : (t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_1 t → motive_2 t)
  (F_3 :
    (t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_2 t → motive_3 t)
  (F_4 :
    (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
      Lean.PrefixTreeNode.below_3 t → motive_4 t),
  Lean.PrefixTreeNode.brecOn_1 t F_1 F_2 F_3 F_4 = F_2 t (Lean.PrefixTreeNode.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  k ∉ t → (f (t.get? k)).isNone = true → (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size = t.size
-- Mathlib.Topology.Connected.PathConnected
Joined.map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  Joined x y → Continuous f → Joined (f x) (f y)
-- Mathlib.Data.Complex.BigOperators
Complex.re_expect : ∀ {α : Type u_1} (s : Finset α) (f : α → ℂ), (s.expect fun i => f i).re = s.expect fun i => (f i).re
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_div_same : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Group (α j)] (i : Fin (n + 1)) (x y : α i)
  (p : (j : Fin n) → α (i.succAbove j)), i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (h : X = Y),
  (CategoryTheory.eqToHom h).unop = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)),
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).obj X = X
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- The **proper decomposition** of semilinear sets: every semilinear set is a finite union of
proper linear sets.  -/
IsSemilinearSet.isProperSemilinearSet : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} [IsCancelAdd M], IsSemilinearSet s → IsProperSemilinearSet s
-- Init.Data.Int.OfNat
Nat.ToInt.mul_congr : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a * b) = a' * b'
-- Mathlib.Algebra.Category.Grp.AB
instAdditiveFunctorColim : ∀ {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] [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_3 : CategoryTheory.Preadditive C], CategoryTheory.Limits.colim.Additive
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} [inst_3 : Inhabited (β k)], (m₁.diff m₂).get! k = if m₂.contains k = true then default else m₁.get! k
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFiniteFPowerSeriesOnBall.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E},
  HasFiniteFPowerSeriesOnBall f p x n r → DifferentiableOn 𝕜 f (Metric.eball x r)
-- Mathlib.GroupTheory.Congruence.Hom
Con.ker_coeMulHom : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F), Con.ker ↑f = Con.ker f
-- Mathlib.Analysis.Convex.Basic
convex_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (c : E), Convex 𝕜 {c}
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_span_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {P : Submodule R A}
  {x y : A}, x ∈ (R ∙ y) * P ↔ ∃ z ∈ P, y * z = x
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.exists_right_complement'_of_coprime_aux' : ∀ {n : ℕ} {G : Type u} [inst : Group G] [Finite G],
  Nat.card G = n → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal
CategoryTheory.Enriched.HasConicalProducts.hasConicalTerminal : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u)
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  [CategoryTheory.Enriched.HasConicalProducts V C], CategoryTheory.Enriched.HasConicalTerminal V C
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries two unital binary operations that distribute over each other,
then these operations are commutative.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`.  -/
EckmannHilton.mul_comm : ∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
  EckmannHilton.IsUnital m₁ e₁ →
    EckmannHilton.IsUnital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → Std.Commutative m₂
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.comp_bfamilyOfFamily : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β),
  (fun i hi => g (Ordinal.bfamilyOfFamily f i hi)) = Ordinal.bfamilyOfFamily (g ∘ f)
-- Mathlib.Algebra.Category.Ring.Epi
/-- **Alias** of `CommRingCat.epi_iff_epi`. -/
CommRingCat.epi_iff_tmul_eq_tmul : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_injective : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], Function.Injective LieSubmodule.toSubmodule
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.preComp_a : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X X' : CategoryTheory.SimplicialObject C} {n : ℕ}
  {Z : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z) (g : X' ⟶ X),
  (f.preComp g).a = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op { len := n + 1 })) f.a
-- Lean.Parser.Syntax
Lean.Parser.Command.optKind : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.mul_right : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α},
  IsOpen s → IsOpen (s * t)
-- Batteries.Data.List.Basic
List.takeD_zero : ∀ {α : Type u_1} (l : List α) (a : α), List.takeD 0 l a = []
-- Mathlib.Data.Vector.Basic
List.Vector.toList.eq_1 : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), v.toList = ↑v
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.mk.sizeOf_spec : ∀ (processId? : Option ℤ) (clientInfo? : Option Lean.Lsp.ClientInfo) (rootUri? : Option String)
  (initializationOptions? : Option Lean.Lsp.InitializationOptions) (capabilities : Lean.Lsp.ClientCapabilities)
  (trace : Lean.Lsp.Trace) (workspaceFolders? : Option (Array Lean.Lsp.WorkspaceFolder)),
  sizeOf
      { processId? := processId?, clientInfo? := clientInfo?, rootUri? := rootUri?,
        initializationOptions? := initializationOptions?, capabilities := capabilities, trace := trace,
        workspaceFolders? := workspaceFolders? } =
    1 + sizeOf processId? + sizeOf clientInfo? + sizeOf rootUri? + sizeOf initializationOptions? + sizeOf capabilities +
        sizeOf trace +
      sizeOf workspaceFolders?
-- Mathlib.Topology.Algebra.Monoid
mulHomOfMemClosureRangeCoe_apply : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Mul M₁] [inst_3 : Mul M₂]
  [inst_4 : ContinuousMul M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : MulHomClass F M₁ M₂] (f : M₁ → M₂)
  (hf : f ∈ closure (Set.range fun f x => f x)), ⇑(mulHomOfMemClosureRangeCoe f hf) = f
-- Mathlib.MeasureTheory.Measure.Prod
/-- The symmetric version of Tonelli's Theorem: For `ℝ≥0∞`-valued almost everywhere measurable
functions on `α × β`, the integral of `f` is equal to the iterated integral, in reverse order.  -/
MeasureTheory.lintegral_prod_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (f : α × β → ENNReal),
  AEMeasurable f (μ.prod ν) → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
-- Init.Data.String.Basic
String.Pos.next_toSlice : ∀ {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.endPos}, p.toSlice.next h = (p.next ⋯).toSlice
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_apply_mem_cocycles₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{max u u_1, u, u} k G} (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ A)) x ∈ groupCohomology.cocycles₁ A
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Concatenate a bitvector with itself `n` times.
 -/
Std.Tactic.BVDecide.BVExpr.replicate : {w w' : ℕ} → (n : ℕ) → Std.Tactic.BVDecide.BVExpr w → w' = w * n → Std.Tactic.BVDecide.BVExpr w'
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equalizer morphism in any limit cone is a monomorphism.  -/
CategoryTheory.Limits.mono_of_isLimit_fork : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g}
  (i : CategoryTheory.Limits.IsLimit c), CategoryTheory.Mono c.ι
-- Mathlib.Analysis.Normed.Operator.Banach
/-- If `f : E →L[𝕜] F` is injective with closed range (and `E` and `F` are Banach spaces),
`f` is anti-Lipschitz.  -/
ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  [CompleteSpace F] (f : E →L[𝕜] F), Function.Injective ⇑f → IsClosed (Set.range ⇑f) → ∃ K, AntilipschitzWith K ⇑f
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.supClosure_apply_of_mem : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent G C) {s : Set α}, s ∈ C → (m.supClosure hC) s = m s
-- Init.Data.UInt.Bitwise
UInt64.and_assoc : ∀ (a b c : UInt64), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_def : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖₊ = nndist f 0
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.denote_fold_and : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α}
  (s : aig.RefVec len),
  ⟦assign, Std.Sat.AIG.RefVec.fold aig s Std.Sat.AIG.mkAndCached⟧ = true ↔
    ∀ (idx : ℕ) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredAsSmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C],
  CategoryTheory.IsFiltered (CategoryTheory.AsSmall C)
-- Batteries.Control.Nondet.Basic
/-- Lift a list of values to a nondeterministic value.
(The backtrackable state in each will be identical:
whatever the state was when we first read from the result.)
 -/
Nondet.ofList : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → List α → Nondet m α
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- The pseudodistance defines a pseudometric space structure on the torsor. This
is not an instance because it depends on `V` to define a `MetricSpace P`.  -/
pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor : (V : Type u_6) → (P : Type u_7) → [inst : SeminormedAddCommGroup V] → [AddTorsor V P] → PseudoMetricSpace P
-- Batteries.Data.BitVec.Lemmas
BitVec.ofNat_pow : ∀ (w x n : ℕ), BitVec.ofNat w (x ^ n) = BitVec.ofNat w x ^ n
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
AntitoneOn.memLp_isCompact : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {p : ENNReal} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact s → AntitoneOn f s → MeasureTheory.MemLp f p (μ.restrict s)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- `Nonempty P` is a typeclass saying there exists an object `X : C` that satisfies `P`.  -/
CategoryTheory.ObjectProperty.Nonempty : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_mem_uniformity : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} [inst : UniformSpace X],
  UniformContinuous T → U ∈ uniformity X → ∀ (n : ℕ), Dynamics.dynEntourage T U n ∈ uniformity X
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.tensorHom_inv_inv_mul_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.GrpObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
        (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h))
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0),
  imageToKernel f g w = (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) ⋯
-- Mathlib.RingTheory.Polynomial.Basic
/-- Given an ideal `I` of `R[X]`, make the ideal in `R` of
leading coefficients of polynomials in `I` with degree ≤ `n`.  -/
Ideal.leadingCoeffNth : {R : Type u} → [inst : Semiring R] → Ideal (Polynomial R) → ℕ → Ideal R
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.inner_orthogonalProjectionOnto_eq_of_mem_right`. -/
Submodule.inner_orthogonalProjection_eq_of_mem_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : ↥K) (v : E),
  inner 𝕜 (K.orthogonalProjectionOnto v) u = inner 𝕜 v ↑u
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Irreducible.normalizedFactors_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {p : α},
  Irreducible p → ∀ (k : ℕ), UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
-- Mathlib.Algebra.Notation.Support
Function.support_subset_comp : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] {g : M → N},
  (∀ {x : M}, g x = 0 → x = 0) → ∀ (f : ι → M), Function.support f ⊆ Function.support (g ∘ f)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.abs_repr : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [self : MvQPF F] {α : TypeVec.{u} n} (x : F α), MvQPF.abs (MvQPF.repr x) = x
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.le_exp_log : ∀ (x : ℝ), x ≤ Real.exp (Real.log x)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {L : Type u_1} {F : Type u_2} [inst_5 : Add L] [inst_6 : FunLike F L (Module.End R M)]
  [AddHomClass F L (Module.End R M)] (f : F) (μ : L → R) (k : ℕ∞),
  ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥ → (∀ (x y : L), Commute (f x) (f y)) → ∀ (x y : L), μ (x + y) = μ x + μ y
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instInhabited : Inhabited CommRingCat
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor],
  (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).pt =
    CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t
-- Mathlib.Topology.Perfect
Perfect.acc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α}, Perfect C → Preperfect C
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.julian0.inj : ∀ {day day_1 : Std.Time.Internal.Bounded.LE 0 365},
  Std.Time.TimeZone.TransitionSpec.julian0 day = Std.Time.TimeZone.TransitionSpec.julian0 day_1 → day = day_1
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- When `IsEmpty ι`, this lemma does not hold without the additional assumption `p ≠ ∞` because
the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
`PiLp.nnnorm_toLp_const` for a version which exchanges the hypothesis `Nonempty ι`.
for `p ≠ ∞`.  -/
PiLp.nnnorm_toLp_const' : ∀ {p : ENNReal} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5} [inst_1 : SeminormedAddCommGroup β]
  [Nonempty ι] (b : β), ‖WithLp.toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
-- Init.Grind.ToInt
/-- The half-infinite interval `[lo, ∞)`.  -/
Lean.Grind.IntInterval.ci : ℤ → Lean.Grind.IntInterval
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ),
  h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0
-- Mathlib.Logic.Nontrivial.Basic
nontrivial_iff_lt : ∀ {α : Type u_1} [inst : LinearOrder α], Nontrivial α ↔ ∃ x y, x < y
-- Mathlib.Data.Rat.Defs
Rat.divInt_div_divInt : ∀ (n₁ d₁ n₂ d₂ : ℤ), Rat.divInt n₁ d₁ / Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂) (d₁ * n₂)
-- Init.Data.Array.Nat
Array.sum_le_max_mul_length_of_max?_eq_some_nat : ∀ {x : ℕ} {xs : Array ℕ}, xs.max? = some x → xs.sum ≤ x * xs.size
-- Init.Data.SInt.Lemmas
Int8.minValue_div_neg_one : Int8.minValue / -1 = Int8.minValue
-- Mathlib.NumberTheory.SumFourSquares
Int.lt_of_sum_four_squares_eq_mul : ∀ {a b c d k m : ℕ}, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m → 2 * a < m → 2 * b < m → 2 * c < m → 2 * d < m → k < m
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.symm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x y → CommRingCat.Colimits.Relation F y x
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquivOfImageEq_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) (h : ⇑e '' s = t),
  ↑(e.toPartialEquivOfImageEq s t h).symm = ⇑e.symm