mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.WF.below.mk : ∀ {α : Type u_1} {cmp : α → α → Ordering} {motive : (a : RBTree.RBNode α) → RBTree.RBNode.WF cmp a → Prop}
  {t : RBTree.RBNode α} {c : RBTree.RBColor} {n : ℕ} (a : RBTree.RBNode.Ordered cmp t) (a_1 : t.Balanced c n),
  RBTree.RBNode.WF.below ⋯
-- Mathlib.Topology.MetricSpace.IsometricSMul
AddUnits.isIsometricVAdd : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X]
  [inst_3 : AddMonoid M], IsIsometricVAdd (AddUnits M) X
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_iSup : ∀ {X Y : SSet} {ι : Type u_1} (S : ι → X.Subcomplex) (f : X ⟶ Y), (⨆ i, S i).image f = ⨆ i, (S i).image f
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_def : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x x_1 : CategoryTheory.FreeMonoidalCategory C) (x_2 : x.Hom x_1),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f x_2 =
    match x, x_1, x_2 with
    | x, .(x), CategoryTheory.FreeMonoidalCategory.Hom.id .(x) =>
      CategoryTheory.CategoryStruct.id (CategoryTheory.FreeMonoidalCategory.projectObj f x)
    | .((X.tensor Y).tensor Z), .(X.tensor (Y.tensor Z)), CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z =>
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.projectObj f X)
          (CategoryTheory.FreeMonoidalCategory.projectObj f Y) (CategoryTheory.FreeMonoidalCategory.projectObj f Z)).hom
    | .(X.tensor (Y.tensor Z)), .((X.tensor Y).tensor Z), CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z =>
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.projectObj f X)
          (CategoryTheory.FreeMonoidalCategory.projectObj f Y) (CategoryTheory.FreeMonoidalCategory.projectObj f Z)).inv
    | .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), a, CategoryTheory.FreeMonoidalCategory.Hom.l_hom .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).hom
    | a, .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), CategoryTheory.FreeMonoidalCategory.Hom.l_inv .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).inv
    | .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), a, CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).hom
    | a, .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).inv
    | x, x_3, f_1.comp g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.projectMapAux f f_1)
        (CategoryTheory.FreeMonoidalCategory.projectMapAux f g)
    | .(X.tensor Y₁), .(X.tensor Y₂), CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X p =>
      CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.FreeMonoidalCategory.projectObj f X)
        (CategoryTheory.FreeMonoidalCategory.projectMapAux f p)
    | .(X₁.tensor X), .(X₂.tensor X), p.whiskerRight X =>
      CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.FreeMonoidalCategory.projectMapAux f p)
        (CategoryTheory.FreeMonoidalCategory.projectObj f X)
    | .(W.tensor X), .(Y.tensor Z), f_1.tensor g =>
      CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.FreeMonoidalCategory.projectMapAux f f_1)
        (CategoryTheory.FreeMonoidalCategory.projectMapAux f g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.mono_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C},
  sq.IsPullback → ∀ [CategoryTheory.Mono sq.f₃₄], CategoryTheory.Mono sq.f₁₂
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_irrefl : ∀ (x : PSet.{u_1}), x ∉ x
-- Mathlib.Data.List.Pairwise
List.pairwise_iff_forall_infix : ∀ {α : Type u_3} {l : List α} {R : α → α → Prop},
  List.Pairwise R l ↔ ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets is closed by difference.  -/
MeasureTheory.IsSetAlgebra.sdiff_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetAlgebra 𝒜 → s ∈ 𝒜 → t ∈ 𝒜 → s \ t ∈ 𝒜
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.isPrimePow_iff : ∀ {a : Cardinal.{u_1}}, IsPrimePow a ↔ Cardinal.aleph0 ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
-- Mathlib.Data.Rel
SetRel.image_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (R : SetRel α β) (s : ι → Set α), R.image (⋃ i, s i) = ⋃ i, R.image (s i)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.rel_eq_coe : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), ⇑c.toSetoid = ⇑c
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_of_isPrincipal_mul_opow : ∀ {b o : Ordinal.{u}},
  1 < b → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) (b ^ o) → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Mathlib.Algebra.Category.Grp.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
GrpCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- **Alias** of `IsUniformInducing.of_comp_iff`. -/
IsUniformInducing.isUniformInducing_comp_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {g : β → γ}, IsUniformInducing g → ∀ {f : α → β}, IsUniformInducing (g ∘ f) ↔ IsUniformInducing f
-- Mathlib.RingTheory.OreLocalization.Basic
_private.Mathlib.RingTheory.OreLocalization.Basic.0.OreLocalization.add''_char : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S) (rb sb : R),
  sb * ↑s₁ = rb * ↑s₂ → ∀ (h : sb * ↑s₁ ∈ S), OreLocalization.add''✝ r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `Over.map` preserves identities.  -/
CategoryTheory.MorphismProperty.Over.mapId : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          [inst_2 : P.IsStableUnderComposition] →
            [inst_3 : P.IsMultiplicative] →
              [Q.RespectsIso] →
                (X : T) →
                  (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X)) →
                    (hf :
                        autoParam (f = CategoryTheory.CategoryStruct.id X)
                          CategoryTheory.MorphismProperty.Over.mapId._auto_1) →
                      CategoryTheory.MorphismProperty.Over.map Q ⋯ ≅ CategoryTheory.Functor.id (P.Over Q X)
-- Std.Data.Internal.List.Associative
Std.Internal.List.beq_of_getEntry_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a}
  {k : α} {h₁ : Std.Internal.List.containsKey k l = true}, Std.Internal.List.getEntry k l h₁ = p → (p.fst == k) = true
-- Lean.Data.Lsp.Internal
/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`.  -/
Lean.Lsp.RefIdent.fromJson? : Lean.Json → Except String Lean.Lsp.RefIdent
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal edistance of a point to a set  -/
Metric.infEDist : {α : Type u} → [PseudoEMetricSpace α] → α → Set α → ENNReal
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The real part of the inner product, in terms of the norm.  -/
re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.re (inner 𝕜 x y) = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedOrder_toSubring : ∀ {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [inst : Ring R] (p : MvPowerSeries σ R) (T : Subring R)
  (hp : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T),
  MvPowerSeries.weightedOrder w (p.toSubring T hp) = MvPowerSeries.weightedOrder w p
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β k → β k},
  (t.modify k f).getKey! k = if k ∈ t then k else default
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecls.mk.injEq : ∀ (decls decls_1 : Lean.Meta.DiscrTree Mathlib.Meta.FunProp.FunPropDecl),
  ({ decls := decls } = { decls := decls_1 }) = (decls = decls_1)
-- Aesop.Forward.State
Aesop.instInhabitedHyp.default : Aesop.Hyp
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  (Metric.closedBall x ε₁ ∩ Metric.closedBall y ε₂).Nonempty → dist x y ≤ ε₁ + ε₂
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.

`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.find?`.

Examples:
* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 5) = pure (some 1)`
* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 1) = pure none`
 -/
Std.IterM.Total.find? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Finite α m] → Std.IterM.Total m β → (β → Bool) → m (Option β)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.Ω`.

---

Notation for the `Ω` in an arbitrary choice of a subobject classifier  -/
CategoryTheory.HasClassifier.Ω : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.HasSubobjectClassifier C] → C
-- Lean.Expr
/-- Instantiates the loose bound variables in `e` using the `subst` array,
where a loose `Expr.bvar i` at "binding depth" `d` is instantiated with `subst[i - d]` if `0 <= i - d < subst.size`,
and otherwise it is replaced with `Expr.bvar (i - subst.size)`; non-loose bound variables are not touched.

If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order,
then conceptually `instantiate` is instantiating the last `n` of these and reindexing the remaining ones.
Warning: `instantiate` uses the de Bruijn indexing to index the `subst` array, which might be the reverse order from what you might expect.
See also `Lean.Expr.instantiateRev`.

**Terminology.** The "binding depth" of a subexpression is the number of bound variables available to that subexpression
by virtue of being in the bodies of `Expr.forallE`, `Expr.lam`, and `Expr.letE` expressions.
A bound variable `Expr.bvar i` is "loose" if its de Bruijn index `i` is not less than its binding depth.)

**About instantiation.** Instantiation isn't mere substitution.
When an expression from `subst` is being instantiated, its internal loose bound variables have their de Bruijn indices incremented
by the binding depth of the replaced loose bound variable.
This is necessary for the substituted expression to still refer to the correct binders after instantiation.
Similarly, the reason loose bound variables not instantiated using `subst` have their de Bruijn indices decremented like `Expr.bvar (i - subst.size)`
is that `instantiate` can be used to eliminate binding expressions internal to a larger expression,
and this adjustment keeps these bound variables referring to the same binders.
 -/
Lean.Expr.instantiate : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.Topology.NoetherianSpace
Topology.IsInducing.noetherianSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.NoetherianSpace α] {i : β → α}, Topology.IsInducing i → TopologicalSpace.NoetherianSpace β
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousOn.fun_zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f s → ∀ (z : ℤ), ContinuousOn (fun i => z • f i) s
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_surjective : Function.Surjective Ordinal.pred
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_3.eq_2 : ∀ (motive : List Lean.MVarId → Sort u_1) (g : Lean.MVarId) (gs : List Lean.MVarId) (h_1 : Unit → motive [])
  (h_2 : (g : Lean.MVarId) → (gs : List Lean.MVarId) → motive (g :: gs)),
  (match g :: gs with
    | [] => h_1 ()
    | g :: gs => h_2 g gs) =
    h_2 g gs
-- Mathlib.Algebra.Polynomial.Roots
/-- A version of `mem_rootSet'` that requires `Module.IsTorsionFree` and for the polynomial to be
non-zero instead of requiring it to be non-zero after mapping.  -/
Polynomial.mem_rootSet : ∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : S},
  a ∈ p.rootSet S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
-- Init.Data.Vector.Lemmas
Vector.prod_empty : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α], #v[].prod = 1
-- Mathlib.Data.Seq.Computation
Computation.terminates_map : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α) [s.Terminates], (Computation.map f s).Terminates
-- Mathlib.Analysis.Convex.KreinMilman
/-- A continuous affine map is surjective from the extreme points of a compact set to the extreme
points of the image of that set. This inclusion is in general strict.  -/
surjOn_extremePoints_image : ∀ {E : Type u_1} {F : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T2Space E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} [inst_7 : AddCommGroup F]
  [inst_8 : Module ℝ F] [inst_9 : TopologicalSpace F] [T1Space F] (f : E →ᴬ[ℝ] F),
  IsCompact s → Set.SurjOn (⇑f) (Set.extremePoints ℝ s) (Set.extremePoints ℝ (⇑f '' s))
-- Lean.Meta.Tactic.Grind.Split
/-- Computes the anchor reference information for the case-split candidate `c`.
The candidate list must be the one stored in the goal before the case-split is selected and
performed (i.e., before `selectNextSplit?` prunes the list and before `c` is marked as resolved),
so that it matches the list inspected by the `cases` tactic when replaying the generated script.
 -/
Lean.Meta.Grind.mkSplitAnchorRefInfo : Lean.Meta.Grind.SplitInfo →
  optParam (Option (List Lean.Meta.Grind.SplitInfo)) none → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitAnchorRefInfo
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimitsOfShape : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget MonCat)
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The option `linter.style.cases` of the deprecated syntax linter flags usages of
the `cases'` tactic, which is a backward-compatible version of Lean 3's `cases` tactic.
Unlike `obtain`, `rcases` and Lean 4's `cases`, variables introduced by `cases'` are not
required to be separated by case, which hinders readability.
 -/
Mathlib.Linter.Style.linter.style.cases : Lean.Option Bool
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Creates a packed float from a sign, an exponent and a mantissa.  -/
Float.Model.UnpackedFloat.packComponents : (spec : Float.Model.Format) →
  Float.Model.UnpackedFloat.Sign →
    BitVec spec.exponentBits → BitVec spec.mantissaBitsWithoutImplicit → BitVec spec.numBits
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_mk : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : A →+* B)
  (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f x ∈ ℬ i), ⇑{ toRingHom := f, map_mem := h } = ⇑f
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.first?_eq_first?_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] {it : Std.Iter β},
  it.first? = it.toIterM.first?.run
-- Mathlib.Algebra.Group.End
/-- Isomorphic groups have isomorphic automorphism groups.  -/
AddAut.congr : {G : Type u_3} → [inst : AddGroup G] → {H : Type u_7} → [inst_1 : AddGroup H] → G ≃+ H → AddAut G ≃+ AddAut H
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.fieldInst : Lean.Meta.Grind.Arith.FieldNormNum.Context✝ → Lean.Expr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ringHom_ext'_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  {f g : SkewMonoidAlgebra k G →+* k},
  f = g ↔
    f.comp SkewMonoidAlgebra.singleOneRingHom = g.comp SkewMonoidAlgebra.singleOneRingHom ∧
      (↑f).comp (SkewMonoidAlgebra.of k G) = (↑g).comp (SkewMonoidAlgebra.of k G)
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The complex exponential function is uniformly continuous on left half planes.  -/
UniformContinuousOn.cexp : ∀ (a : ℝ), UniformContinuousOn Complex.exp {x | x.re ≤ a}
-- Init.Data.List.Nat.Basic
List.mem_eraseIdx_iff_getElem? : ∀ {α : Type u_1} {x : α} {l : List α} {k : ℕ}, x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l[i]? = some x
-- Mathlib.RepresentationTheory.Basic
Representation.self_comp_norm : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : AddCommMonoid V] [inst_4 : Module k V] (ρ : Representation k G V) (g : G), ρ g ∘ₗ ρ.norm = ρ.norm
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Let `s` be a subset of an additive monoid `M` such that the closure of `s` is
the whole monoid. Then `AddMonoidHom.ofClosureEqTopRight` defines an additive monoid
homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `y ∈ s`.  -/
AddMonoidHom.ofClosureMEqTopRight : {M : Type u_4} →
  {N : Type u_5} →
    [inst : AddMonoid M] →
      [inst_1 : AddMonoid N] →
        {s : Set M} →
          (f : M → N) → AddSubmonoid.closure s = ⊤ → f 0 = 0 → (∀ (x y : M), y ∈ s → f (x + y) = f x + f y) → M →+ N
-- Init.Data.Option.Lemmas
Option.exists_ne_none : ∀ {α : Type u_1} {p : Option α → Prop}, (∃ x, x ≠ none ∧ p x) ↔ ∃ x, p (some x)
-- Mathlib.Data.Set.Card
Set.ncard_le_one_iff_subset_singleton : ∀ {α : Type u_1} {s : Set α} [Nonempty α],
  autoParam s.Finite Set.ncard_le_one_iff_subset_singleton._auto_1 → (s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x})
-- Mathlib.Data.W.Constructions
/-- The naturals are equivalent to their associated `WType`  -/
WType.equivNat : WType WType.Natβ ≃ ℕ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse, version subtracting vectors.  -/
Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.somePath.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F F_1 : Set X} (e_F : F = F_1) (h : JoinedIn F x y),
  h.somePath = ⋯.somePath
-- Mathlib.RingTheory.Localization.Defs
/-- `IsLocalization.toLocalizationMap M S` shows `S` is the monoid localization of `R` at `M`.  -/
IsLocalization.toLocalizationMap : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → M.LocalizationMap S
-- Batteries.Data.List.Lemmas
List.getElem_findIdxs_eq_findIdxNth : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : List α} {h : n < (List.findIdxs p xs).length},
  (List.findIdxs p xs)[n] = List.findIdxNth p xs n
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_comap_eq_self : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H : AddSubgroup N},
  H ≤ f.range → AddSubgroup.map f (AddSubgroup.comap f H) = H
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (y : ↥Y), IsCompact (⇑f ⁻¹' {y})
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y  -/
CategoryTheory.Over.iteratedSliceEquiv : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → (f : CategoryTheory.Over X) → CategoryTheory.Over f ≌ CategoryTheory.Over f.left
-- Mathlib.Combinatorics.HalesJewett
/-- The proposition that all lines in a color-focused collection have the same endpoint.  -/
Combinatorics.Line.ColorFocused.is_focused : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} (self : Combinatorics.Line.ColorFocused C),
  ∀ p ∈ self.lines, ↑p.line none = self.focus
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- A version of `continuousOn_cfc` over `ℝ≥0` instead of `RCLike 𝕜`.  -/
continuousOn_cfc_nnreal : ∀ (A : Type u_2) [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal),
      autoParam (ContinuousOn f s) continuousOn_cfc_nnreal._auto_1 →
        ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum NNReal a ⊆ s}
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_le_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] {s : Finset ι} {f g : ι → α} [PosSMulMono ℚ≥0 α],
  (∀ i ∈ s, f i ≤ g i) → (s.expect fun i => f i) ≤ s.expect fun i => g i
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ico_ae_eq_Icc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α},
  μ {b} = 0 → Set.Ico a b =ᵐ[μ] Set.Icc a b
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.id_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {X : CategoryTheory.Comma L R},
  (CategoryTheory.CategoryStruct.id X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.aemeasurable_fun_prod : ∀ {M : Type u_2} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Multiset (α → M)),
  (∀ f ∈ s, AEMeasurable f μ) → AEMeasurable (fun x => (Multiset.map (fun f => f x) s).prod) μ
-- Init.Data.BitVec.Bitblast
BitVec.mulRec_succ_eq : ∀ {w : ℕ} (x y : BitVec w) (s : ℕ),
  x.mulRec y (s + 1) = x.mulRec y s + if y.getLsbD (s + 1) = true then x <<< (s + 1) else 0