mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Attach
Vector.toArray_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.attach.toArray = xs.toArray.attachWith (fun x => x ∈ xs) ⋯
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommMonCat MonCat)
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.Config.mk.injEq : ∀ (toConfig : Lean.Meta.Rewrite.Config) (useRewrite implicationHyp useKAbstract : Bool)
  (toConfig_1 : Lean.Meta.Rewrite.Config) (useRewrite_1 implicationHyp_1 useKAbstract_1 : Bool),
  ({ toConfig := toConfig, useRewrite := useRewrite, implicationHyp := implicationHyp, useKAbstract := useKAbstract } =
      { toConfig := toConfig_1, useRewrite := useRewrite_1, implicationHyp := implicationHyp_1,
        useKAbstract := useKAbstract_1 }) =
    (toConfig = toConfig_1 ∧
      useRewrite = useRewrite_1 ∧ implicationHyp = implicationHyp_1 ∧ useKAbstract = useKAbstract_1)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- The `𝕜`-submodule of elements of `α →ₘ[μ] E` whose `Lp` norm is finite.  This is `Lp E p μ`,
with extra structure.  -/
MeasureTheory.Lp.LpSubmodule : {α : Type u_1} →
  (𝕜 : Type u_2) →
    (E : Type u_4) →
      {m : MeasurableSpace α} →
        ENNReal →
          (μ : MeasureTheory.Measure α) →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedRing 𝕜] → [inst_2 : Module 𝕜 E] → [inst_3 : IsBoundedSMul 𝕜 E] → Submodule 𝕜 (α →ₘ[μ] E)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.ArrayStxBuilder.push : Lean.Elab.Term.Quotation.ArrayStxBuilder → Lean.Syntax → Lean.Elab.Term.Quotation.ArrayStxBuilder
-- Mathlib.GroupTheory.GroupAction.Support
/-- A set `s` supports `b` if `g • b = b` whenever `g • a = a` for all `a ∈ s`.  -/
MulAction.Supports : (G : Type u_1) → {α : Type u_3} → {β : Type u_4} → [SMul G α] → [SMul G β] → Set α → β → Prop
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- A vertex is in the ball of radius `⊤` iff it is reachable from the center.  -/
SimpleGraph.mem_ball_top : ∀ {V : Type u_1} {G : SimpleGraph V} {c v : V}, v ∈ G.ball c ⊤ ↔ G.Reachable v c
-- Init.Data.String.Basic
/-- Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos`
is not between `p₀` and `p₁`.
 -/
String.Slice.Pos.sliceOrPanic : {s : String.Slice} → s.Pos → (p₀ p₁ : s.Pos) → {h : p₀ ≤ p₁} → (s.slice p₀ p₁ h).Pos
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.lit.sizeOf_spec : ∀ (v : Lean.Literal), sizeOf (Lean.Meta.RefinedDiscrTree.Key.lit v) = 1 + sizeOf v
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_neg : ∀ (a : BitVec 8), Int8.ofBitVec (-a) = -Int8.ofBitVec a
-- Mathlib.Combinatorics.Additive.FreimanHom
_private.Mathlib.Combinatorics.Additive.FreimanHom.0.Fin.aux : ∀ {k m n : ℕ}, m ≠ 0 → m * k ≤ n → k < n + 1
-- Mathlib.Analysis.Convex.Star
/-- If `s` is an order-connected set in an ordered module over an ordered semiring
and all elements of `s` are comparable with `x ∈ s`, then `s` is `StarConvex` at `x`.  -/
Set.OrdConnected.starConvex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] {x : E} {s : Set E},
  s.OrdConnected → x ∈ s → (∀ y ∈ s, x ≤ y ∨ y ≤ x) → StarConvex 𝕜 x s
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The (exact) short complex `H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f)`
of a spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`.  -/
CategoryTheory.Abelian.SpectralObject.sc₃ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    CategoryTheory.CategoryStruct.comp f g = fg →
                      (n₀ n₁ : ℤ) →
                        autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₃._auto_1 →
                          CategoryTheory.ShortComplex C
-- Mathlib.Topology.MetricSpace.Completion
LipschitzWith.completion_map : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {K : NNReal},
  LipschitzWith K f → LipschitzWith K (UniformSpace.Completion.map f)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.of_ne_one : ∀ {α : Type u} (x : α), FreeCommRing.of x ≠ 1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instMonoMapOfIsStableUnderCoproductsOfShapeMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u_1)
  [(CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderCoproductsOfShape J] {X₁ X₂ : J → C}
  (f : (j : J) → X₁ j ⟶ X₂ j) [inst_2 : CategoryTheory.Limits.HasCoproduct X₁]
  [inst_3 : CategoryTheory.Limits.HasCoproduct X₂] [∀ (j : J), CategoryTheory.Mono (f j)],
  CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map f)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postComp_inv_app_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor T D)
  (G : CategoryTheory.Functor D E) (X_1 : CategoryTheory.Under X),
  ((CategoryTheory.Under.postComp F G).inv.app X_1).right = CategoryTheory.CategoryStruct.id (G.obj (F.obj X_1.right))
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ →
    s₂ ⊆ s₃ →
      μ.real (s₃ \ s₁) = 0 →
        autoParam (μ (s₃ \ s₁) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_sdiff._auto_1 →
          μ.real s₂ = μ.real s₃
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {x y : CategoryTheory.PresheafOfGroups.OneCochain G U}, x.ev = y.ev → x = y
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_sdiff_isBasis_sdiff : ∀ {α : Type u_1} {M : Matroid α} {I J X Y : Set α},
  M.IsBasis I X → M.IsBasis J Y → I ⊆ J → (M.contract I).IsBasis (J \ I) (Y \ X)
-- Mathlib.CategoryTheory.Functor.Functorial
/-- A functorial map preserves identities.  -/
CategoryTheory.Functorial.map_id : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : C → D} [self : CategoryTheory.Functorial F] {X : C},
  CategoryTheory.map F (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X)
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.IntInterval.lo?.match_1.eq_1 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (lo hi : ℤ)
  (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.co lo hi with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_1 lo hi
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- A variant of `mk_mul_mk` that is `rfl` but has a stranger multiplication order.  -/
LocalizedModule.mk_mul_mk' : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {a₁ a₂ : A} {s₁ s₂ : ↥S}, LocalizedModule.mk a₁ s₁ * LocalizedModule.mk a₂ s₂ = LocalizedModule.mk (a₁ * a₂) (s₂ * s₁)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The topology of weak convergence on `MeasureTheory.FiniteMeasure Ω` is inherited (induced)
from the weak-\* topology on `WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)` via the function
`MeasureTheory.FiniteMeasure.toWeakDualBCNN`.  -/
MeasureTheory.FiniteMeasure.instTopologicalSpace : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] → [OpensMeasurableSpace Ω] → TopologicalSpace (MeasureTheory.FiniteMeasure Ω)
-- Mathlib.Probability.Martingale.BorelCantelli
/-- An a.e. monotone strongly adapted process `f` with uniformly bounded differences converges to
`+∞` if and only if its predictable part also converges to `+∞`.  -/
MeasureTheory.tendsto_sum_indicator_atTop_iff : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  (∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω) →
    MeasureTheory.StronglyAdapted ℱ f →
      (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
        (∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R) →
          ∀ᵐ (ω : Ω) ∂μ,
            Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop ↔
              Filter.Tendsto (fun n => MeasureTheory.predictablePart f ℱ μ n ω) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Module.Congruence.Defs
/-- A `VAddCon` is closed under additive action.  -/
VAddCon.vadd : ∀ {S : Type u_2} {M : Type u_3} [inst : VAdd S M] (self : VAddCon S M) (s : S) {x y : M},
  self.toSetoid x y → self.toSetoid (s +ᵥ x) (s +ᵥ y)
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.clm_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {x : 𝕜}
  {G : Type u_2} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G}
  {d : 𝕜 → E →L[𝕜] F} {d' : E →L[𝕜] F},
  HasStrictDerivAt c c' x →
    HasStrictDerivAt d d' x → HasStrictDerivAt (fun y => c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') x
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.setIntegral_compProd_univ_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] (f : β × γ → E) {s : Set β},
  MeasurableSet s →
    MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ((κ.compProd η) a) →
      ∫ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Analysis.Convex.MetricSpace
/-- **Alias** of `Convexity.continuous_convexCombPair`.

---

The convex combination `(t, p, q) ↦ t • p + (1 - t) • q` is continuous on `[0, 1] × X × X`
for a convex metric space `X`.  -/
Convexity.continuous_convexComboPair : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X],
  Continuous fun x => Convexity.convexCombPair (↑x.1) (1 - ↑x.1) ⋯ ⋯ ⋯ x.2.1 x.2.2
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.minView! k v l r =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf => { k := k, v := v, tree := r }
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' =>
      have d := Std.DTreeMap.Internal.Impl.minView! k' v' l' r';
      { k := d.k, v := d.v, tree := Std.DTreeMap.Internal.Impl.balanceR! k v d.tree r }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)}
  {k : α}, Std.Internal.List.DistinctKeys l → Std.Internal.List.getKey! k (Std.Internal.List.eraseKey k l) = default
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `SMul` across an `Equiv`  -/
Equiv.smul : (M : Type u_1) → {α : Type u_2} → {β : Type u_3} → α ≃ β → [SMul M β] → SMul M α
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.extendScalars_val : ∀ {R : Type u} (S : Type v) {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_2}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  (P : Algebra.Generators R T ι) (a : ι), (Algebra.Generators.extendScalars S P).val a = P.val a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- Mapping a walk to its own subgraph and then to `G[s]` where `s` contains the walk's support is
the same as inducing the walk to `s`.  -/
SimpleGraph.Walk.map_mapToSubgraph_eq_induce : ∀ {V : Type u} {G : SimpleGraph V} (s : Set V) {u v : V} (w : G.Walk u v) (hs : ∀ x ∈ w.support, x ∈ s),
  SimpleGraph.Walk.map { toFun := fun x => ⟨↑x, ⋯⟩, map_rel' := ⋯ } w.mapToSubgraph = SimpleGraph.Walk.induce s w hs
-- Std.Time.Duration
Std.Time.instDecidableEqDuration : DecidableEq Std.Time.Duration
-- Lean.Exception
Lean.MonadError : (Type → Type) → Type 1
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_neg : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  [inst_3 : Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n R), ↑(-g) = -↑g
-- Mathlib.Probability.Martingale.Convergence
/-- Part c of the **L¹ martingale convergence theorem**: Given an integrable function `g` which
is measurable with respect to `⨆ n, ℱ n` where `ℱ` is a filtration, the martingale defined by
`𝔼[g | ℱ n]` converges almost everywhere to `g`.

This martingale also converges to `g` in L¹ and this result is provided by
`MeasureTheory.Integrable.tendsto_eLpNorm_condExp`  -/
MeasureTheory.Integrable.tendsto_ae_condExp : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {g : Ω → ℝ},
  MeasureTheory.Integrable g μ →
    MeasureTheory.StronglyMeasurable g →
      ∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun n => μ[g | ↑ℱ n] x) Filter.atTop (nhds (g x))
-- Mathlib.Topology.Algebra.UniformConvergence
instSubUniformFun : {α : Type u_1} → {β : Type u_2} → [Sub β] → Sub (UniformFun α β)
-- Mathlib.Data.Finset.Max
Finset.ofDual_max' : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty),
  OrderDual.ofDual (s.max' hs) = (Finset.image (⇑OrderDual.ofDual) s).min' ⋯
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `grind.ematch.diagnostics` is set  -/
Lean.Meta.Grind.isEmatchDiagEnabled : Lean.Meta.Grind.GrindM Bool
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.prime_of_degree_eq_one : ∀ {R : Type u} [inst : Field R] {p : Polynomial R}, p.degree = 1 → Prime p
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key in the tree map, panicking if the map is empty.
 -/
Std.DTreeMap.Raw.maxKey! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
/-- Product of two infinite sums indexed by arbitrary types.
See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable, and
`tsum_mul_tsum_of_summable_norm'` when the space is not complete.  -/
tsum_mul_tsum_of_summable_norm : ∀ {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : NormedRing R] [CompleteSpace R] {f : ι → R} {g : ι' → R},
  (Summable fun x => ‖f x‖) →
    (Summable fun x => ‖g x‖) → (∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.1 * g z.2
-- Mathlib.Probability.Independence.BoundedContinuousFunction
process_indepFun_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4} {H : Type u_7}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H]
  [HasOuterApproxClosed H] {X : (s : S) → Ω → E s} {U : Ω → H} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    AEMeasurable U P →
      (∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ⇑g ∘ U) x ∂P =
            (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) U P
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite sum of antitone functions is antitone.  -/
Antitone.finsetSum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [AddLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {f : ι → γ → N}, (∀ i ∈ s, Antitone (f i)) → Antitone fun x => ∑ i ∈ s, f i x
-- Std.Data.TreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.getKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α → α
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.full_mono : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D E : Set C},
  D ⊆ E → CategoryTheory.Subgroupoid.full D ≤ CategoryTheory.Subgroupoid.full E
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `QuotientAddGroup.quotientBot`.  -/
QuotientAddGroup.quotientBotIsometryEquiv : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → M ⧸ ⊥ ≃ᵢ M
-- Lean.Meta.Basic
/-- Number of times each axiom was tried to be unfolded, which may point to an inaccessible def value.
 -/
Lean.Meta.Diagnostics.unfoldAxiomCounter : Lean.Meta.Diagnostics → Lean.PHashMap Lean.Name ℕ
-- Init.Control.Lawful.Instances
StateT.run_controlAt : ∀ {m : Type u → Type u_1} {σ α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ),
  (controlAt m f).run s = f fun {β} x => x.run s
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.term : Lean.Term → Aesop.RuleTerm
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedΓ'.default : Turing.PartrecToTM2.Γ'
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoal.mk.injEq : ∀ (goal : String) (range : Lean.Lsp.Range) (goal_1 : String) (range_1 : Lean.Lsp.Range),
  ({ goal := goal, range := range } = { goal := goal_1, range := range_1 }) = (goal = goal_1 ∧ range = range_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.op_boundary : ∀ (n : ℕ), (SSet.boundary n).op.preimage (SSet.stdSimplex.opIso { len := n }).inv = SSet.boundary n
-- Mathlib.RingTheory.Adjoin.Tower
Algebra.adjoin_res_eq_adjoin_res : ∀ (C : Type u_1) (D : Type u_2) (E : Type u_3) (F : Type u_4) [inst : CommSemiring C] [inst_1 : CommSemiring D]
  [inst_2 : CommSemiring E] [inst_3 : CommSemiring F] [inst_4 : Algebra C D] [inst_5 : Algebra C E]
  [inst_6 : Algebra C F] [inst_7 : Algebra D F] [inst_8 : Algebra E F] [inst_9 : IsScalarTower C D F]
  [inst_10 : IsScalarTower C E F] {S : Set D} {T : Set E},
  Algebra.adjoin C S = ⊤ →
    Algebra.adjoin C T = ⊤ →
      Subalgebra.restrictScalars C (Algebra.adjoin E (⇑(algebraMap D F) '' S)) =
        Subalgebra.restrictScalars C (Algebra.adjoin D (⇑(algebraMap E F) '' T))
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.sum_smul_index_linearMap' : ∀ {α : Type u_1} {R : Type u_3} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂},
  ((c • v).sum fun a => ⇑(h a)) = c • v.sum fun a => ⇑(h a)
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected space, any disjoint family of non-empty clopen subsets has at most one
element.  -/
subsingleton_of_disjoint_isClopen : ∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α},
  (∀ (i : ι), (s i).Nonempty) → Pairwise (Function.onFun Disjoint s) → (∀ (i : ι), IsClopen (s i)) → Subsingleton ι
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_eq_one_iff_mem : ∀ {ι : Type u_1} (M₀ : Type u_4) [inst : MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀],
  s.indicator 1 i = 1 ↔ i ∈ s
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_C_right : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R) (x : R),
  (MvPolynomial.bind₁ f) (MvPolynomial.C x) = MvPolynomial.C x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.code.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (code code_1 : Lean.Compiler.LCNF.Code pu),
  (Lean.Compiler.LCNF.DeclValue.code code = Lean.Compiler.LCNF.DeclValue.code code_1) = (code = code_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.congr_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cochain F G n},
  z₁ = z₂ → ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
-- Mathlib.Order.Filter.IsBounded
isBoundedUnder_ge_finset_inf' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β}
  {s : Finset ι} (hs : s.Nonempty),
  (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f (F i)) →
    Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f fun a => s.inf' hs fun i => F i a
-- Mathlib.Topology.MetricSpace.Bounded
/-- If a function is continuous at every point of a compact set `k`, then it is bounded on
some open neighborhood of `k`.  -/
Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k : Set β} {f : β → α},
  IsCompact k → (∀ x ∈ k, ContinuousAt f x) → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
-- Mathlib.Data.Int.ModEq
Int.ModEq.add : ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n]
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
regionBetween_subset : ∀ {α : Type u_1} (f g : α → ℝ) (s : Set α), regionBetween f g s ⊆ s ×ˢ Set.univ
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An object `J` is injective iff every morphism into `J` can be obtained by extending a monomorphism.
 -/
CategoryTheory.Injective.factors : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : C} [self : CategoryTheory.Injective J] {X Y : C}
  (g : X ⟶ J) (f : X ⟶ Y) [CategoryTheory.Mono f], ∃ h, CategoryTheory.CategoryStruct.comp f h = g
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_mks : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A → B} (h₁ : ∀ (x y : A), f (x + y) = f x + f y)
  (h₂ :
    ∀ (m : R) (x : A),
      { toFun := f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₁ }.toFun x)
  (h₃ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ } = CoalgebraStruct.counit)
  (h₄ :
    TensorProduct.map { toFun := f, map_add' := h₁, map_smul' := h₂ } { toFun := f, map_add' := h₁, map_smul' := h₂ } ∘ₗ
        CoalgebraStruct.comul =
      CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ }),
  ⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f