mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instIsScalarTower_2 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower M N αᵒᵈ
-- Init.Data.List.ToArray
List.toArray_appendList : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray
-- Mathlib.Topology.Instances.Real.Lemmas
/-- The limit of an antitone, bounded below function `f : ι → ℝ` is a greatest lower bound
of the function.  -/
Real.isGLB_of_tendsto_antitone_bddBelow : ∀ {ι : Type u_1} [inst : Preorder ι] [Nonempty ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {f : ι → ℝ} {x : ℝ},
  Filter.Tendsto f Filter.atTop (nhds x) → Antitone f → BddBelow (Set.range f) → IsGLB (Set.range f) x
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.ncard_inv : ∀ {G : Type u_1} [inst : InvolutiveInv G] (s : Set G), s⁻¹.ncard = s.ncard
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.coe_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (S : Subsemigroup M),
  ↑(Subsemigroup.map f S) = ⇑f '' ↑S
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ext_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α],
  (∀ (k : α), Std.ExtDHashMap.Const.get? m₁ k = Std.ExtDHashMap.Const.get? m₂ k) → m₁ = m₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfc_le_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
  (a : A) {c : ℝ},
  0 ≤ c →
    autoParam (ContinuousOn f (spectrum 𝕜 a)) norm_cfc_le_iff._auto_1 →
      autoParam (p a) norm_cfc_le_iff._auto_3 → (‖cfc f a‖ ≤ c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖ ≤ c)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.memP_reverse : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.MemP cut t.reverse ↔ RBTree.RBNode.MemP (fun x => (cut x).swap) t
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum_succ_le_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  {hs : IsCofinal s} [inst_3 : SuccOrder α] {a o : α},
  o ∈ s → ↑((Order.enum s hs) a) < o → ↑((Order.enum s hs) (Order.succ a)) ≤ o
-- Std.Time.Format.Basic
Std.Time.Format.mk : {f : Type} →
  {typ : Type → f → Type} →
    ((fmt : f) → typ String fmt) →
      ({α : Type} → (fmt : f) → typ (Option α) fmt → String → Except String α) → Std.Time.Format f typ
-- Std.Http.Server.Config
/-- Maximum number of spaces in delimiter sequences (default: 16)
 -/
Std.Http.Config.maxSpaceSequence : Std.Http.Config → ℕ
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The `Cfg` states map to `Cfg'` states almost one to one, except that in normal operation the
local store contains an arbitrary garbage value. To make the final theorem cleaner we explicitly
clear it in the halt state so that there is exactly one configuration corresponding to output `v`.
 -/
Turing.PartrecToTM2.TrCfg : Turing.ToPartrec.Cfg → Turing.PartrecToTM2.Cfg' → Prop
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, (s.copy.takeWhile pat).copy = (s.takeWhile pat).copy
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.iterateInduction.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive x
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.unitsScalar : {M : Type u_2} → [inst : Monoid M] → SMul (ConjAct Mˣ) M
-- Mathlib.Algebra.Lie.Basic
LieRing.mk : {L : Type v} →
  [toAddCommGroup : AddCommGroup L] →
    [toBracket : Bracket L L] →
      (∀ (x y z : L), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆) →
        (∀ (x y z : L), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆) →
          (∀ (x : L), ⁅x, x⁆ = 0) → (∀ (x y z : L), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆) → LieRing L
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Retrieve an element in the set that is equivalent to `x` in the order,
if it exists.

```
find 1 {1, 2, 3} = some 1
find 4 {1, 2, 3} = none
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
find (1, 1) {(0, 1), (1, 2)} = some (1, 2)
find (3, 1) {(0, 1), (1, 2)} = none
```  -/
Ordnode.find : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Option α
-- Mathlib.MeasureTheory.Measure.Stieltjes
notMem_botSet_of_lt : ∀ {R : Type u_1} [inst : LinearOrder R] {x y : R}, x < y → y ∉ botSet
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
instMulHomogeneousIdeal : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → Mul (HomogeneousIdeal 𝒜)
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- **Alias** of `Matrix.symm_reindexAlgEquiv`. -/
Matrix.reindexAlgEquiv_symm : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), (Matrix.reindexAlgEquiv R A e).symm = Matrix.reindexAlgEquiv R A e.symm
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_source_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M}, x ∈ f.source → (f.extend I).source ∈ nhds x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The `faceOppositeCentroid` is the affine combination of the complement vertices with equal
weights `1/n`.  -/
Affine.Simplex.faceOppositeCentroid_eq_affineCombination : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i = (Finset.affineCombination k {i}ᶜ s.points) fun x => (↑n)⁻¹
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommSemiringOfIsTopologicalSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : CommSemiring β] → [IsTopologicalSemiring β] → CommSemiring C(α, β)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.coe_op : ∀ {M : Type u_2} [inst : MulOneClass M] (x : Submonoid M), ↑x.op = MulOpposite.unop ⁻¹' ↑x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Add β] [ContinuousAdd β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : β), MeasureTheory.AEStronglyMeasurable (fun x => c + f x) μ
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.hom_ext : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {X : C}
  {f f' : CategoryTheory.Limits.colimit F ⟶ X},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) f') →
    f = f'
-- Mathlib.Order.Bounds.Defs
IsCofinalFor.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s t : Set α), IsCofinalFor s t = ∀ ⦃a : α⦄, a ∈ s → ∃ b ∈ t, a ≤ b
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec.eq_1 : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X], X.isoSpec = CategoryTheory.asIso X.toSpecΓ
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.instIsUpperProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] [OrderTop α]
  [inst_4 : Preorder β] [inst_5 : TopologicalSpace β] [Topology.IsUpper β] [OrderTop β], Topology.IsUpper (α × β)
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.heval_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) {a b : PowerSeries R},
  (PowerSeries.heval x) (a * b) = (PowerSeries.heval x) a * (PowerSeries.heval x) b
-- Mathlib.Analysis.Normed.Affine.AddTorsor
/-- Scaling by an element `k` of the scalar ring as a `DilationEquiv` with ratio `‖k‖₊`, mapping
from a normed space to a normed torsor over that space sending `0` to `c`.  -/
DilationEquiv.smulTorsor : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NormedDivisionRing 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [NormSMulClass 𝕜 E] →
            {P : Type u_3} → [inst_4 : PseudoMetricSpace P] → [NormedAddTorsor E P] → P → {k : 𝕜} → k ≠ 0 → E ≃ᵈ P
-- Mathlib.Data.Ordmap.Ordset
Ordset.instMembership : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → Membership α (Ordset α)
-- Mathlib.Algebra.BigOperators.Finprod
Finset.support_of_fiberwise_sum_subset_image : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq β] (s : Finset α)
  (f : α → M) (g : α → β), (Function.support fun b => ∑ a ∈ s with g a = b, f a) ⊆ ↑(Finset.image g s)
-- Mathlib.Probability.Kernel.Defs
/-- A kernel is s-finite if it can be written as the sum of countably many finite kernels.  -/
ProbabilityTheory.IsSFiniteKernel : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
GroupWithZero.zpow_neg' : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Mathlib.Topology.Order.LawsonTopology
/-- An upper set is Lawson open if and only if it is Scott open  -/
Topology.lawsonOpen_iff_scottOpen_of_isUpperSet' : ∀ {α : Type u_1} [inst : Preorder α] (L S : TopologicalSpace α) [Topology.IsLawson α] [Topology.IsScott α Set.univ]
  (s : Set α), IsUpperSet s → (IsOpen s ↔ IsOpen s)
-- Lean.Meta.TryThis
/-- Original suggestion that this `TryThisInfo` was derived from.
Stored so that meta-code downstream can extract the suggestions
produced by a tactic from the `InfoTree`.
 -/
Lean.Meta.Tactic.TryThis.TryThisInfo.suggestion : Lean.Meta.Tactic.TryThis.TryThisInfo → Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_counitIso_hom_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core D), (E.core.counitIso.hom.app X).iso.hom = E.counitIso.hom.app X.of
-- Lean.Data.Lsp.Communication
_private.Lean.Data.Lsp.Communication.0.Lean.IO.FS.Stream.readHeaderFields : IO.FS.Stream → IO (List (String × String))
-- Mathlib.Algebra.Order.AddTorsor
instContravariantClassHVAddLeOfIsOrderedCancelVAdd : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : LE P] [inst_2 : VAdd G P] [IsOrderedCancelVAdd G P],
  ContravariantClass G P (fun x1 x2 => x1 +ᵥ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univBall_source : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  (OpenPartialHomeomorph.univBall c r).source = Set.univ
-- Init.Data.Vector.Algebra
Vector.zero_smul : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMul α β],
  (∀ (c : β), 0 • c = 0) → ∀ (c : Vector β n), 0 • c = 0
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.comp.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ),
  q.comp p n = ∑ c, q.compAlongComposition p c
-- Mathlib.Analysis.Normed.Module.Basic
SeminormedSpace.Core.norm_nonneg : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Norm E]
  [inst_3 : Module 𝕜 E], SeminormedSpace.Core 𝕜 E → ∀ (x : E), 0 ≤ ‖x‖
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_nil : ∀ {V : Type u} {G : SimpleGraph V} (u : V) {i : ℕ}, SimpleGraph.Walk.nil.getVert i = u
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of the reverse direction of `le_compl_iff_disjoint_right`. -/
Disjoint.le_compl_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, Disjoint a b → a ≤ bᶜ
-- Mathlib.Topology.Neighborhoods
/-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of s:
it contains an open set containing `s`.  -/
exists_open_set_nhds' : ∀ {X : Type u} [inst : TopologicalSpace X] {s U : Set X}, U ∈ ⨆ x ∈ s, nhds x → ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.iInf : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Sort u_5} [Countable ι] {f : ι → δ → α}, (∀ (i : ι), Measurable (f i)) → Measurable fun b => ⨅ i, f i b
-- Init.Data.Option.Lemmas
Option.filter_eq_none_iff : ∀ {α : Type u_1} {o : Option α} {p : α → Bool}, Option.filter p o = none ↔ ∀ (a : α), o = some a → ¬p a = true
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  (c.rotate u hu).IsCycle ↔ c.IsCycle
-- Mathlib.RingTheory.Ideal.Quotient.Index
Submodule.index_smul_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  {N : Submodule R M} [Finite (R ⧸ I)] (s : Finset M),
  Submodule.span R ↑s = N →
    (I • N).toAddSubgroup.index ≤ (Submodule.toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
/-- The group of group homomorphisms from a finite cyclic group `G` of order `n` into the
group of units of a ring `M` with all roots of unity is isomorphic to `G`  -/
IsCyclic.monoidHom_equiv_self : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [IsCyclic G] [inst_3 : CommMonoid M]
  [HasEnoughRootsOfUnity M (Nat.card G)], Nonempty ((G →* Mˣ) ≃* G)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} [hi : Inhabited (β k')] {f : β k → β k},
  m.WF →
    (m.modify k f).get! k' =
      if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.id_def : ∀ (Ω : Type w) (S : CategoryTheory.SmallCategoryOfSet Ω) (X : ↑S.obj), CategoryTheory.CategoryStruct.id X = S.id X
-- Mathlib.NumberTheory.FLT.Four
/-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has positive `c`.  -/
Fermat42.neg_of_minimal : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → Fermat42.Minimal a b (-c)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.instEssentiallySmallRetractClosureOfLocallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P.retractClosure
-- Mathlib.Algebra.BigOperators.Finprod
/-- If a function `f` equals `1` on a set `s`, then the product of `f i` over `i ∈ s` equals `1`.  -/
finprod_mem_of_eqOn_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
  Set.EqOn f 1 s → ∏ᶠ (i : α) (_ : i ∈ s), f i = 1
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_bot_ae_eq : ∀ {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ),
  ProbabilityTheory.condVar ⊥ X μ =ᵐ[μ] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F₁ F₂ : CategoryTheory.Functor C D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂), F₂.PreservesZeroMorphisms
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulHom.eqLocus.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f g : M →ₙ* N),
  f.eqLocus g = { carrier := {x | f x = g x}, mul_mem' := ⋯ }
-- Mathlib.Topology.MetricSpace.Defs
dist_ofAdd : ∀ {X : Type u_1} [inst : Dist X] (a b : X), dist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = dist a b
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Ico : ∀ (a b : ℝ), UniqueDiffOn ℝ (Set.Ico a b)
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.mk : {R : Type u} →
  [inst : CommRing R] → (carrier : Type v) → [isRing : Ring carrier] → [isAlgebra : Algebra R carrier] → AlgCat R
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.comp_hom₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : C} (h : Z.obj₃ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom₃ h =
    CategoryTheory.CategoryStruct.comp f.hom₃ (CategoryTheory.CategoryStruct.comp g.hom₃ h)
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefKind.proofWanted : WantedRefKind✝
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- A graph homomorphism from a finite subgraph of G to F.  -/
SimpleGraph.FinsubgraphHom : {V : Type u} → {W : Type v} → {G : SimpleGraph V} → G.Finsubgraph → SimpleGraph W → Type (max u v)
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly.ext : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f g : ⦃R : Type u⦄ → [CommRing R] → WittVector p R → WittVector p R},
  WittVector.IsPoly p f →
    WittVector.IsPoly p g →
      (∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) (n : ℕ),
          (WittVector.ghostComponent n) (f x) = (WittVector.ghostComponent n) (g x)) →
        ∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R), f x = g x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_insert_le_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {k fallback : α}, (cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mixedEmbedding_apply_isReal : ∀ (K : Type u_1) [inst : Field K] (x : K) (w : { w // w.IsReal }),
  ((NumberField.mixedEmbedding K) x).1 w = (NumberField.InfinitePlace.embedding_of_isReal ⋯) x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α), (t₁.erase k).Equiv (t₂.erase k)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_sum_apply : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {ι : Type u_6} (s : Finset ι) (f : ι → AdicCompletion I M) (n : ℕ), ↑(∑ i ∈ s, f i) n = ∑ i ∈ s, ↑(f i) n
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.mk.inj : ∀ {α : Type u} {inst : Ord α} {β : α → Type v} {k : α → Ordering} {inner : Option ((a : α) × β a)}
  {property : ∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner = some p → k p.fst = Ordering.eq}
  {inner_1 : Option ((a : α) × β a)}
  {property_1 : ∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner_1 = some p → k p.fst = Ordering.eq},
  { inner := inner, property := property } = { inner := inner_1, property := property_1 } → inner = inner_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List α} {k fallback : α}, k ∉ t → l.contains k = false → (t.insertMany l).getD k fallback = fallback
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_naturality_2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
        ((F.mapComp' f g fg hfg).inv.toNatTrans.app Y)) =
    (F.map fg).toFunctor.map a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoHaveVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.Algebra.GroupWithZero.Action.End
AddMonoid.End.smul_def : ∀ {α : Type u_4} [inst : AddMonoid α] (f : AddMonoid.End α) (a : α), f • a = f a
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.insertListₘ.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (hd : (a : α) × β a) → (tl : List ((a : α) × β a)) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.length : Lean.Grind.AC.Seq → ℕ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedParam : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Param a)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Expression of `circleAverage` in terms of interval averages.  -/
Real.circleAverage_eq_intervalAverage : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  Real.circleAverage f c R = ⨍ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.mapπ₀_comp_apply : ∀ {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X.π₀),
  SSet.mapπ₀ (CategoryTheory.CategoryStruct.comp f g) x = SSet.mapπ₀ g (SSet.mapπ₀ f x)
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular], P.isoClosure.IsCardinalFilteredGenerator κ ↔ P.IsCardinalFilteredGenerator κ