mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SupClosed
/-- A meet-semilattice where every inf-closed set has a greatest lower bound is automatically
complete.  -/
SemilatticeInf.toCompleteSemilatticeInf : {α : Type u_3} →
  [inst : SemilatticeInf α] →
    (sInf : Set α → α) → (∀ (s : Set α), InfClosed s → IsGLB s (sInf s)) → CompleteSemilatticeInf α
-- Std.Time.Format
/-- The Time24Hour format, which follows the pattern `HH:mm:ss` for representing time
in a 24-hour clock format.
 -/
Std.Time.Formats.time24Hour : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.CategoryTheory.ComposableArrows.Basic
Fin.castSuccFunctor_map : ∀ (n : ℕ) {X Y : Fin n} (hij : X ⟶ Y), (Fin.castSuccFunctor n).map hij = hij
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k km : α} (hc : k ∈ t), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Algebra.Ring.Divisibility.Basic
MulEquivClass.toMulEquiv.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : MulEquivClass F α β] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- Star algebra homomorphisms commute with the continuous functional calculus.  -/
StarAlgHomClass.map_cfc : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop}
  [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R]
  [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A] [inst_7 : TopologicalSpace A]
  [inst_8 : Algebra R A] [inst_9 : Ring B] [inst_10 : StarRing B] [inst_11 : TopologicalSpace B] [inst_12 : Algebra R B]
  [inst_13 : CommSemiring S] [inst_14 : Algebra R S] [inst_15 : Algebra S A] [inst_16 : Algebra S B]
  [IsScalarTower R S A] [IsScalarTower R S B] [inst_19 : ContinuousFunctionalCalculus R A p]
  [inst_20 : ContinuousFunctionalCalculus R B q] [ContinuousMap.UniqueHom R B] [inst_22 : FunLike F A B]
  [AlgHomClass F S A B] [StarHomClass F A B] (φ : F) (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) StarAlgHomClass.map_cfc._auto_1 →
    autoParam (Continuous ⇑φ) StarAlgHomClass.map_cfc._auto_3 →
      autoParam (p a) StarAlgHomClass.map_cfc._auto_5 →
        autoParam (q (φ a)) StarAlgHomClass.map_cfc._auto_7 → φ (cfc f a) = cfc f (φ a)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- The Zarankiewicz function is at most the corresponding extremal number.  -/
SimpleGraph.zarankiewicz_le_extremalNumber : ∀ {m n s t : ℕ} {α : Type u_3} {β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β],
  Fintype.card α = s →
    Fintype.card β = t →
      SimpleGraph.zarankiewicz m n s t ≤ SimpleGraph.extremalNumber (m + n) (completeBipartiteGraph α β)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (k, v) ∈ t.toArray ↔ t.getKey? k = some k ∧ t[k]? = some v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.WF → t.isEmpty = (t.size == 0)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.aeval_add_of_sq_eq_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Polynomial R)
  (x y : S),
  y ^ 2 = 0 → (Polynomial.aeval (x + y)) p = (Polynomial.aeval x) p + (Polynomial.aeval x) (Polynomial.derivative p) * y
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hom_ext_iff : ∀ {X Y : AddSemigrp} {f g : X ⟶ Y}, f = g ↔ AddSemigrp.Hom.hom f = AddSemigrp.Hom.hom g
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.uniformContinuous_inl : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M] [inst_2 : Zero M],
  UniformContinuous TrivSqZeroExt.inl
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F) (x : E), (ContinuousLinearMap.ofIsTopCompl h φ ψ) x = (LinearMap.ofIsCompl ⋯ ↑φ ↑ψ) x
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3) →
      (x : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
        (Unit → motive Lean.PersistentHashMap.Entry.null) →
          ((k : α) → (v : β) → motive (Lean.PersistentHashMap.Entry.entry k v)) →
            ((node : Lean.PersistentHashMap.Node α β) → motive (Lean.PersistentHashMap.Entry.ref node)) → motive x
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α →ₘ[μ] E} {g : ↥(MeasureTheory.Lp F p μ)},
  (∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ ‖↑↑g x‖₊) → f ∈ MeasureTheory.Lp E p μ
-- Lean.AuxRecursor
Lean.mkBelowName : Lean.Name → Lean.Name
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.coe_multiples : ∀ {M : Type u_1} [inst : AddMonoid M] (x : M), ↑(AddSubmonoid.multiples x) = Set.range fun n => n • x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- The short complex `Hⁱ(G, X₁) ⟶ Hⁱ(G, X₂) ⟶ Hⁱ(G, X₃)` associated to a short complex of
representations `X₁ ⟶ X₂ ⟶ X₃`.  -/
groupCohomology.mapShortComplex₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → CategoryTheory.ShortComplex (Rep.{u, u, u} k G) → ℕ → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mem_baseSet_at : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (x : B),
  x ∈ self.baseSet (self.indexAt x)
-- Mathlib.Data.DFinsupp.Sigma
/-- The natural map between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.  -/
DFinsupp.sigmaCurry : {ι : Type u} →
  {α : ι → Type u_2} →
    {δ : (i : ι) → α i → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → (j : α i) → Zero (δ i j)] →
          (Π₀ (i : (x : ι) × α x), δ i.fst i.snd) → Π₀ (i : ι) (j : α i), δ i j
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- **Alias** of `Ordinal.pred_eq_of_isSuccPrelimit`. -/
Order.IsSuccPrelimit.ordinalPred_eq : ∀ {o : Ordinal.{u_4}}, Order.IsSuccPrelimit o → o.pred = o
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {L₀ L₁ L₂ L₃ : CategoryTheory.ShortComplex C} {v₀₁ : L₀ ⟶ L₁} {v₁₂ : L₁ ⟶ L₂} {v₂₃ : L₂ ⟶ L₃}
  {w₀₂ :
    autoParam (CategoryTheory.CategoryStruct.comp v₀₁ v₁₂ = 0) CategoryTheory.ShortComplex.SnakeInput.w₀₂._autoParam}
  {w₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp v₁₂ v₂₃ = 0) CategoryTheory.ShortComplex.SnakeInput.w₁₃._autoParam}
  {h₀ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁ w₀₂)}
  {h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃ w₁₃)} {L₁_exact : L₁.Exact}
  {epi_L₁_g : CategoryTheory.Epi L₁.g} {L₂_exact : L₂.Exact} {mono_L₂_f : CategoryTheory.Mono L₂.f}
  {L₀_1 L₁_1 L₂_1 L₃_1 : CategoryTheory.ShortComplex C} {v₀₁_1 : L₀_1 ⟶ L₁_1} {v₁₂_1 : L₁_1 ⟶ L₂_1}
  {v₂₃_1 : L₂_1 ⟶ L₃_1}
  {w₀₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp v₀₁_1 v₁₂_1 = 0)
      CategoryTheory.ShortComplex.SnakeInput.w₀₂._autoParam}
  {w₁₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp v₁₂_1 v₂₃_1 = 0)
      CategoryTheory.ShortComplex.SnakeInput.w₁₃._autoParam}
  {h₀_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁_1 w₀₂_1)}
  {h₃_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃_1 w₁₃_1)}
  {L₁_exact_1 : L₁_1.Exact} {epi_L₁_g_1 : CategoryTheory.Epi L₁_1.g} {L₂_exact_1 : L₂_1.Exact}
  {mono_L₂_f_1 : CategoryTheory.Mono L₂_1.f},
  { L₀ := L₀, L₁ := L₁, L₂ := L₂, L₃ := L₃, v₀₁ := v₀₁, v₁₂ := v₁₂, v₂₃ := v₂₃, w₀₂ := w₀₂, w₁₃ := w₁₃, h₀ := h₀,
        h₃ := h₃, L₁_exact := L₁_exact, epi_L₁_g := epi_L₁_g, L₂_exact := L₂_exact, mono_L₂_f := mono_L₂_f } =
      { L₀ := L₀_1, L₁ := L₁_1, L₂ := L₂_1, L₃ := L₃_1, v₀₁ := v₀₁_1, v₁₂ := v₁₂_1, v₂₃ := v₂₃_1, w₀₂ := w₀₂_1,
        w₁₃ := w₁₃_1, h₀ := h₀_1, h₃ := h₃_1, L₁_exact := L₁_exact_1, epi_L₁_g := epi_L₁_g_1, L₂_exact := L₂_exact_1,
        mono_L₂_f := mono_L₂_f_1 } →
    L₀ = L₀_1 ∧ L₁ = L₁_1 ∧ L₂ = L₂_1 ∧ L₃ = L₃_1 ∧ v₀₁ ≍ v₀₁_1 ∧ v₁₂ ≍ v₁₂_1 ∧ v₂₃ ≍ v₂₃_1 ∧ h₀ ≍ h₀_1 ∧ h₃ ≍ h₃_1
-- Mathlib.Algebra.Group.Action.Defs
/-- `SMul` version of `comp_mul_left`  -/
comp_smul_left : ∀ (M : Type u_1) {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (a₁ a₂ : M),
  ((fun x => a₁ • x) ∘ fun x => a₂ • x) = fun x => (a₁ * a₂) • x
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instMonadMor₂MonoidalM : Mathlib.Tactic.BicategoryLike.MonadMor₂ Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.equivalenceOfIsInitial_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.Under.equivalenceOfIsInitial hX).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        CategoryTheory.Under.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Under X)).obj Y).right) ⋯)
      ⋯
-- Std.Tactic.Do.Syntax
/-- After `with`, there is an optional tactic that runs on all branches, and
then a list of alternatives.
 -/
Lean.Parser.Tactic.vcAlts : Lean.ParserDescr
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_core_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_of_core_cert p₁ p₂ p₃ = p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k 1 (-1) p₁ p₂)
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.X.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.combine.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (a₁ a₂ : α) (n₁ n₂ : Batteries.BinomialHeap.Imp.HeapNode α),
  Batteries.BinomialHeap.Imp.combine le a₁ a₂ n₁ n₂ =
    if le a₁ a₂ = true then (a₁, Batteries.BinomialHeap.Imp.HeapNode.node a₂ n₂ n₁)
    else (a₂, Batteries.BinomialHeap.Imp.HeapNode.node a₁ n₁ n₂)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_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 SetLike.coe
-- Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
/-- Deterministic morphisms commute with discarding.  -/
CategoryTheory.Deterministic.discard_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.CopyDiscardCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Deterministic f],
  CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit
-- Init.Omega.Coeffs
/-- Shim for `IntList.neg`.  -/
Lean.Omega.Coeffs.neg : Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Init.Data.List.Lemmas
List.append_right_eq_self : ∀ {α : Type u_1} {xs ys : List α}, xs ++ ys = xs ↔ ys = []
-- Lean.Elab.Task
/-- Given a monadic value in `TacticM`, creates a task that runs it in the current state,
returning a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Elab.Tactic.TacticM.asTask' : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM (Task (Lean.Elab.Tactic.TacticM α))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  (F : CategoryTheory.PreZeroHypercover X) (x : E.I₀ ⊕ F.I₀),
  (E.sum F).f x =
    match x with
    | Sum.inl i => E.f i
    | Sum.inr i => F.f i
-- Mathlib.Topology.Category.TopPair
/-- The homotopy on the second space.  -/
TopPair.Homotopy.snd : {X Y : TopPair} → {f g : X ⟶ Y} → TopPair.Homotopy f g → TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g)
-- Mathlib.Computability.Encoding
/-- The encoding function  -/
Computability.Encoding.encode : {α : Type u} → {Γ : Type v} → Computability.Encoding α Γ → α → List Γ
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.instPowFinCoOfNatIntCast : ∀ {n : ℕ} [i : NeZero n], Lean.Grind.ToInt.Pow (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Init.Data.Array.Extract
Array.mem_extract_iff_getElem : ∀ {α : Type u_1} {as : Array α} {a : α} {i j : ℕ},
  a ∈ as.extract i j ↔ ∃ k, ∃ (hm : k < min j as.size - i), as[i + k] = a
-- Mathlib.Data.Finset.Erase
/-- `erase s a` is the set `s - {a}`, that is, the elements of `s` which are
not equal to `a`.  -/
Finset.erase : {α : Type u_1} → [DecidableEq α] → Finset α → α → Finset α
-- Mathlib.NumberTheory.PythagoreanTriples
_private.Mathlib.NumberTheory.PythagoreanTriples.0.coprime_sq_sub_sq_sum_of_odd_odd : ∀ {m n : ℤ},
  m.gcd n = 1 →
    m % 2 = 1 →
      n % 2 = 1 →
        2 ∣ m ^ 2 + n ^ 2 ∧
          2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
-- Aesop.Builder.Basic
Aesop.instInhabitedPhaseSpec : Inhabited Aesop.PhaseSpec
-- Mathlib.CategoryTheory.Monad.Limits
/-- The coreflector always preserves initial objects. Note this in general doesn't apply to any
other colimit.
 -/
CategoryTheory.rightAdjoint_preservesInitial_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.Coreflective R],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{v + 1})
    (CategoryTheory.comonadicRightAdjoint R)
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.majorTypeIndices : Lean.Meta.Cases.Context → Array Lean.Expr
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.singleton_eq_pair_iff : ∀ {x y z : ZFSet.{u_1}}, {x} = {y, z} ↔ x = y ∧ x = z
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurableSet_closure : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α],
  MeasurableSet (closure s)
-- Init.Data.Array.Extract
Array.extract_sub_one : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, j < as.size → as.extract i (j - 1) = (as.extract i j).pop
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toContinuousENorm : ContinuousENorm E] →
      [toAddMonoid : AddMonoid E] → ‖0‖ₑ = 0 → (∀ (x y : E), ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ) → ESeminormedAddMonoid E
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- If `f` is a box additive function on subboxes of `I` and `π₁`, `π₂` are two prepartitions of
`I` that cover the same part of `I`, then `∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J`.  -/
BoxIntegral.BoxAdditiveMap.sum_boxes_congr : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι}
  [Finite ι] (f : BoxIntegral.BoxAdditiveMap ι M I₀),
  ↑I ≤ I₀ → ∀ {π₁ π₂ : BoxIntegral.Prepartition I}, π₁.iUnion = π₂.iUnion → ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_ne_zero_iff : ∀ {r : ℝ}, ENNReal.ofReal r ≠ 0 ↔ 0 < r
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_coeff_cert.eq_1 : ∀ (k₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (k₂ : ℤ) (p₂ : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.dvd_coeff_cert k₁ p₁ k₂ p₂ k = (k != 0).and' ((k₁.beq' (k.mul k₂)).and' (p₁.beq' (p₂.mul_k k)))
-- Lean.Meta.Basic
/-- Contextual information for the `MetaM` monad.
 -/
Lean.Meta.Context : Type
-- Init.WFComputable
WellFounded.fixF.eq_1 : ∀ {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x),
  WellFounded.fixF F x a = Acc.rec (fun x₁ h ih => F x₁ ih) a
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsLocalizationPlusQhQuasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Plus.Qh.IsLocalization (HomotopyCategory.Plus.quasiIso C)
-- Lean.Parser.Term
Lean.Parser.Term.inaccessible.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.ext : ∀ {n : ℕ} {a b : SimplexCategory.Truncated n} (f g : a ⟶ b),
  SimplexCategory.Hom.toOrderHom f.hom = SimplexCategory.Hom.toOrderHom g.hom → f = g
-- Init.Data.BitVec.Lemmas
BitVec.mul_two : ∀ {w : ℕ} {x : BitVec w}, x * 2#w = x + x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary cofan gives a binary fan in the opposite category.  -/
CategoryTheory.Limits.BinaryCofan.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.BinaryCofan X Y → CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_add_apply : ∀ {α : Type u_1} {x : MeasurableSpace α} {s : Set α} {μ₁ μ₂ : MeasureTheory.Measure α},
  autoParam (μ₁ s ≠ ⊤) MeasureTheory.measureReal_add_apply._auto_1 →
    autoParam (μ₂ s ≠ ⊤) MeasureTheory.measureReal_add_apply._auto_3 → (μ₁ + μ₂).real s = μ₁.real s + μ₂.real s
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {W : CategoryTheory.MorphismProperty C} {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} {m : M} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  (e : CategoryTheory.Localization.SmallShiftedHom W X Y m),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (CategoryTheory.Localization.SmallShiftedHom.chgUniv e) =
    (CategoryTheory.Localization.SmallShiftedHom.equiv W L) e
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonShowDocumentClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.ShowDocumentClientCapabilities
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `𝓕 : Filter (β × β)`, this is the set of all `UniformFun.gen α β V` for
`V ∈ 𝓕` as a bundled `FilterBasis` over `(α →ᵤ β) × (α →ᵤ β)`. This will only be applied to
`𝓕 = 𝓤 β` when `β` is equipped with a `UniformSpace` structure, but it is useful to define it for
any filter in order to be able to state that it has a lower adjoint
(see `UniformFun.gc`).  -/
UniformFun.basis : (α : Type u_1) → (β : Type u_2) → Filter (β × β) → FilterBasis (UniformFun α β × UniformFun α β)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback v : β}, Std.ExtDHashMap.Const.getD (m.insert k v) k fallback = v
-- Mathlib.Topology.Homotopy.Basic
/-- `ContinuousMap.HomotopyLike F f₀ f₁` states that `F` is a type of homotopies between `f₀` and
`f₁`.

You should extend this class when you extend `ContinuousMap.Homotopy`.  -/
ContinuousMap.HomotopyLike : {X : outParam (Type u_3)} →
  {Y : outParam (Type u_4)} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (F : Type u_5) → outParam C(X, Y) → outParam C(X, Y) → [FunLike F (↑unitInterval × X) Y] → Prop
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 15 ≤ n → n < 2 ^ 15 → (Int16.ofInt n).toNatClampNeg = n.toNat
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_erase : ∀ {M : Type u_5} [inst : AddCommMonoid M] {s : Multiset M} {a : M} [inst_1 : DecidableEq M],
  a ∈ s → a + (s.erase a).sum = s.sum
-- Mathlib.Data.Seq.Computation
Computation.empty_promises : ∀ {α : Type u} (a : α), (Computation.empty α).Promises a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.π_comp_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (f_1 : s ⟶ t), CategoryTheory.CategoryStruct.comp s.π f_1.hom = t.π
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- If the weight is `coyoneda.obj (op j) : J ⥤ Type _`, this is the limit
weighted cone for `F : J ⥤ C` with point `F.obj j`.  -/
CategoryTheory.Limits.WeightedCone.coyoneda : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (F : CategoryTheory.Functor J C) →
          (j : J) → CategoryTheory.Limits.WeightedCone (CategoryTheory.coyoneda.obj (Opposite.op j)) F
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.varsToUnderscore : Lean.Meta.Match.Example → Lean.Meta.Match.Example
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.lintegral_prod_left' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {f : α × β → ENNReal},
  AEMeasurable f (μ.prod ν) → AEMeasurable (fun y => ∫⁻ (x : α), f (x, y) ∂μ) ν
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_mul : ∀ {F : Type u_2} {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N]
  [inst_3 : FunLike F M N] [MulHomClass F M N] (f : F) (x y : MonoidAlgebra R M),
  MonoidAlgebra.mapDomain (⇑f) (x * y) = MonoidAlgebra.mapDomain (⇑f) x * MonoidAlgebra.mapDomain (⇑f) y
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The free product of the collection of `R`-algebras `A i`, as a quotient of
`FreeTensorAlgebra R A`  -/
LinearAlgebra.FreeProduct : {I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) → [inst_1 : (i : I) → Semiring (A i)] → [(i : I) → Algebra R (A i)] → Type (max (max u v) w)
-- Mathlib.Order.Concept
/-- **Alias** of `Concept.extent_min`. -/
Concept.extent_inf : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r), (c ⊓ d).extent = c.extent ∩ d.extent
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- `X ⟶ X` is the initial object of `P.Under ⊤ X`.  -/
CategoryTheory.MorphismProperty.Under.mkIdInitial : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [inst_1 : P.ContainsIdentities] →
          CategoryTheory.Limits.IsInitial
            (CategoryTheory.MorphismProperty.Under.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.isometryEquivBoundedOfCompact_symm_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  ⇑(ContinuousMap.isometryEquivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap