mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.below.comp_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} {x y z : C} (f : x ⟶ y) (g : y ⟶ z)
  (hf : W.multiplicativeClosure f) (hg : W g),
  CategoryTheory.MorphismProperty.multiplicativeClosure.below hf →
    motive f hf → CategoryTheory.MorphismProperty.multiplicativeClosure.below ⋯
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.finrank_le_iff_rank_le : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {n : ℕ}, Module.finrank K V ≤ n ↔ Module.rank K V ≤ ↑n
-- Mathlib.Order.Hom.Basic
/-- Embedding of a subtype into the ambient type as an `OrderEmbedding`.  -/
OrderEmbedding.subtype : {α : Type u_2} → [inst : Preorder α] → (p : α → Prop) → Subtype p ↪o α
-- Mathlib.Combinatorics.Quiver.Covering
/-- The `Quiver.Costar` at a vertex is the collection of arrows whose target is the vertex.
The type `Quiver.Costar v` is defined to be `Σ (u : U), (u ⟶ v)`.  -/
Quiver.Costar : {U : Type u_1} → [Quiver U] → U → Type (max u_1 u)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.insertMany t l) k =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l).getD
          (Std.DTreeMap.Raw.Const.get! t k)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 1st group homology of `A`, defined as the 1st homology of the complex of inhomogeneous
chains, is isomorphic to `cycles₁ A ⧸ boundaries₁ A`, which is a simpler type.  -/
groupHomology.H1Iso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupHomology.H1 A ≅ (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.H
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticMap.Equivalent.sigNeg_eq : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : AddCommGroup M] [inst_1 : AddCommGroup M'] [inst_2 : CommRing R]
  [inst_3 : LinearOrder R] [inst_4 : Module R M] {Q : QuadraticForm R M} [inst_5 : Module R M']
  {Q' : QuadraticForm R M'}, QuadraticMap.Equivalent Q Q' → sigNeg Q = sigNeg Q'
-- Mathlib.Topology.Algebra.Module.Equiv
/-- `ContinuousSemilinearEquivClass F σ M M₂` asserts `F` is a type of bundled continuous
`σ`-semilinear equivs `M → M₂`.  See also `ContinuousLinearEquivClass F R M M₂` for the case
where `σ` is the identity map on `R`.  A map `f` between an `R`-module and an `S`-module over a ring
homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y`
and `f (c • x) = (σ c) • f x`.  -/
ContinuousSemilinearEquivClass : (F : Type u_1) →
  {R : outParam (Type u_2)} →
    {S : outParam (Type u_3)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          (σ : outParam (R →+* S)) →
            {σ' : outParam (S →+* R)} →
              [RingHomInvPair σ σ'] →
                [RingHomInvPair σ' σ] →
                  (M : outParam (Type u_4)) →
                    [TopologicalSpace M] →
                      [inst_5 : AddCommMonoid M] →
                        (M₂ : outParam (Type u_5)) →
                          [TopologicalSpace M₂] →
                            [inst_7 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → [EquivLike F M M₂] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_iff_forall_surjective : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ},
  G.Colorable n → (G.chromaticNumber = ↑n ↔ ∀ (C : G.Coloring (Fin n)), Function.Surjective ⇑C)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_inf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s t : ClosedSubmodule R M), ↑(s ⊓ t) = ↑s ⊓ ↑t
-- Mathlib.Analysis.Analytic.Within
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`  -/
analyticWithinAt_iff_exists_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {s : Set E} {x : E}, AnalyticWithinAt 𝕜 f s x ↔ ∃ g, f =ᶠ[nhdsWithin x (insert x s)] g ∧ AnalyticAt 𝕜 g x
-- Mathlib.Data.ENat.Defs
instInhabitedENat : Inhabited ℕ∞
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- **Alias** of `GradedAlgHom.coe_toAlgHom_mk`. -/
GradedAlgHom.coe_algHom_mk : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {f : A →ₐ[R] B}
  (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f.toRingHom x ∈ ℬ i), ↑{ toAlgHom := f, map_mem := h } = f
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_zero : ∀ {n : ℕ}, DihedralGroup.r 0 = 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.mk_smul_of_tower_mk : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S)
  (r : M) (x : α) (hx : x ∈ s), r • ⟨x, hx⟩ = ⟨r • x, ⋯⟩
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.not_isInfix : ∀ {α : Type u} {a : α} {l : List α}, NoRepetition✝ a l → ¬[a, a] <:+: l
-- Mathlib.Topology.Constructions.SumProd
isOpenQuotientMap_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Nonempty X],
  IsOpenQuotientMap Prod.snd
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hasMap_of_iso : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p], Y.HasMap p
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.exists_list_of_mem_closure : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {x : M}, x ∈ Submonoid.closure s → ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.comap_freeLocus_le : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra R A],
  PrimeSpectrum.comap (algebraMap R A) ⁻¹' Module.freeLocus R M ⊆ Module.freeLocus A (TensorProduct R A M)
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Rewrite.mk.sizeOf_spec : ∀ (symm : Bool) (proof replacement : Lean.Expr) (stringLength : ℕ) (extraGoals : Array (Lean.MVarId × Lean.BinderInfo))
  (makesNewMVars : Bool),
  sizeOf
      { symm := symm, proof := proof, replacement := replacement, stringLength := stringLength,
        extraGoals := extraGoals, makesNewMVars := makesNewMVars } =
    1 + sizeOf symm + sizeOf proof + sizeOf replacement + sizeOf stringLength + sizeOf extraGoals + sizeOf makesNewMVars
-- Init.Data.Iterators.Combinators.Monadic.Append
/-- Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values
of `it₁` in order and then all values of `it₂` in order.

**Marble diagram:**

```text
it₁                 ---a----b---c--⊥
it₂                                 --d--e--⊥
it₁.append it₂      ---a----b---c-----d--e--⊥
```

**Termination properties:**

* `Finite` instance: only if `it₁` and `it₂` are finite
* `Productive` instance: only if `it₁` and `it₂` are productive

Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not.
The standard library does not provide a `Productive` instance for this case.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
 -/
Std.IterM.append : {m : Type w → Type w'} →
  {β α₁ α₂ : Type w} → [Std.Iterator α₁ m β] → [Std.Iterator α₂ m β] → Std.IterM m β → Std.IterM m β → Std.IterM m β
-- Mathlib.Control.Traversable.Basic
/-- The identity applicative transformation from an applicative functor to itself.  -/
ApplicativeTransformation.idTransformation : {F : Type u → Type v} → [inst : Applicative F] → ApplicativeTransformation F F
-- Mathlib.Logic.Equiv.Defs
/-- If `α₁` is equivalent to `α₂` and `β₁` is equivalent to `β₂`, then the type of maps `α₁ → β₁`
is equivalent to the type of maps `α₂ → β₂`.  -/
Equiv.arrowCongr : {α₁ : Sort u_1} → {β₁ : Sort u_2} → {α₂ : Sort u_3} → {β₂ : Sort u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → (α₁ → β₁) ≃ (α₂ → β₂)
-- Init.Data.SInt.Lemmas
Int32.toBitVec_sub : ∀ {a b : Int32}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Lean.Meta.Tactic.Cases
/-- Given a metavariable `mvarId` representing the goal
```
Ctx |- T
```
and an expression `e : I A j`, where `I A j` is an inductive datatype where `A` are parameters,
and `j` the indices. Generate the goal
```
Ctx, j' : J, h' : I A j' |- j == j' -> e == h' -> T
```
Remark: `(j == j' -> e == h')` is a "telescopic" equality.
Remark: `j` is sequence of terms, and `j'` a sequence of free variables.
The result contains the fields
- `mvarId`: the new goal
- `indicesFVarIds`: `j'` ids
- `fvarId`: `h'` id
- `numEqs`: number of equations in the target

If `varName?` is not none, it is used to name `h'`.
 -/
Lean.Meta.generalizeIndices' : Lean.MVarId → Lean.Expr → optParam (Option Lean.Name) none → Lean.MetaM Lean.Meta.GeneralizeIndicesSubgoal
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- A map `f : E × F → G` satisfies `IsBoundedBilinearMap 𝕜 f` if it is bilinear and
continuous.  -/
IsBoundedBilinearMap : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : Semiring 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [Module 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [Module 𝕜 F] → [inst_5 : SeminormedAddCommGroup G] → [Module 𝕜 G] → (E × F → G) → Prop
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- A structure on a lax transformation that promotes it to a strong transformation.

See `StrongTrans.mkOfLax`.  -/
CategoryTheory.Lax.LaxTrans.StrongCore : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (F ⟶ G) → Type (max (max u₁ v₁) w₂)
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.mem_innerDual : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E] {s : Set E}
  {y : E}, y ∈ ProperCone.innerDual s ↔ ∀ ⦃x : E⦄, x ∈ s → 0 ≤ inner ℝ x y
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.match_1.congr_eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (x : Option s.Pos)
  (h_1 : (pos : s.Pos) → x = some pos → motive (some pos)) (h_2 : x = none → motive none) (heq_1 : x = none),
  (match hd : x with
    | some pos => h_1 pos hd
    | none => h_2 hd) ≍
    h_2 heq_1
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_compl : ∀ {α : Type u} {s : Set α} [inst : DecidableEq α] [inst_1 : Fintype α] (hs : s.Finite) (h : sᶜ.Finite),
  h.toFinset = hs.toFinsetᶜ
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b c : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (x₀ : (i : ↥(Finset.Iic a)) → X ↑i) (hbc : b ≤ c),
  MeasureTheory.Measure.map (Preorder.frestrictLe₂ hbc) ((ProbabilityTheory.Kernel.partialTraj κ a c) x₀) =
    (ProbabilityTheory.Kernel.partialTraj κ a b) x₀
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.induce_refl : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V), SimpleGraph.Iso.refl.induce ⋯ = SimpleGraph.Iso.refl
-- Init.Data.Fin.Lemmas
_private.Init.Data.Fin.Lemmas.0.Fin.reverseInduction.go.match_1.eq_2 : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_2} (i : Fin (n + 1))
  (motive_1 : (j : ℕ) → (h : j < n + 1) → ↑i ≤ j → motive ⟨j, h⟩ → ¬↑i = j → Sort u_1) (j : ℕ) (h : j + 1 < n + 1)
  (h2 : ↑i ≤ j + 1) (x : motive ⟨j + 1, h⟩) (hi : ¬↑i = j + 1)
  (h_1 : (h : 0 < n + 1) → (h2 : ↑i ≤ 0) → (x : motive ⟨0, h⟩) → (hi : ¬↑i = 0) → motive_1 0 h h2 x hi)
  (h_2 :
    (j : ℕ) →
      (h : j + 1 < n + 1) →
        (h2 : ↑i ≤ j + 1) → (x : motive ⟨j + 1, h⟩) → (hi : ¬↑i = j + 1) → motive_1 j.succ h h2 x hi),
  (match j.succ, h, h2, x, hi with
    | 0, h, h2, x, hi => h_1 h h2 x hi
    | j.succ, h, h2, x, hi => h_2 j h h2 x hi) =
    h_2 j h h2 x hi
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (k' ∈ m.alter k f ↔ if (k == k') = true then (f m[k]?).isSome = true else k' ∈ m)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The functor taking an `R`-linear `G`-representation to its `G`-invariant submodule.  -/
TopRep.invariantsFunctor : (k : Type u) →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] → (G : Type v) → [inst_2 : Group G] → CategoryTheory.Functor (TopRep k G) (TopModuleCat k)
-- Std.Data.DTreeMap.Basic
/-- Retrieves the key-value pair, whose key matches `a`. Ensures that such a mapping exists by requiring a proof of `a ∈ m`. The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DTreeMap.getEntry : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → (a : α) → a ∈ t → (a : α) × β a
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.instIsTopologicalAddGroup : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommRing 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : IsTopologicalAddGroup 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  IsTopologicalAddGroup (WeakSpace 𝕜 E)
-- Mathlib.RingTheory.HopfAlgebra.Convolution
HopfAlgebra.antipode_mul_distrib : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : HopfAlgebra R A] (a b : A),
  (HopfAlgebraStruct.antipode R) (a * b) = (HopfAlgebraStruct.antipode R) a * (HopfAlgebraStruct.antipode R) b
-- Init.Data.Array.Lemmas
Array.eq_empty_iff_forall_not_mem : ∀ {α : Type u_1} {xs : Array α}, xs = #[] ↔ ∀ (a : α), a ∉ xs
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_C_mul : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R}, (Polynomial.C a * p).divX = Polynomial.C a * p.divX
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instPartialOrderFiniteIndexNormalAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → PartialOrder (FiniteIndexNormalAddSubgroup G)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEntry.default : Lean.Meta.Grind.Entry
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip)
  (X Y Z : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂ β).app X).app Y).app Z =
    (β.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).app Z
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.bot_orthogonal_eq_top : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊥ᗮ = ⊤
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.ext : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {χ₁ χ₂ : LieModule.Weight R L M}, (∀ (x : L), χ₁ x = χ₂ x) → χ₁ = χ₂
-- Mathlib.Analysis.CStarAlgebra.Basic
Metric.star_sphere : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x : E) (r : ℝ),
  star (Metric.sphere x r) = Metric.sphere (star x) r
-- Init.Data.Iterators.Combinators.FilterMap
/-- If `it` is an iterator, then `it.filterMapM f` is another iterator that applies a monadic
function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad.
If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

If `f` is pure, then the simpler variant `it.filterMap` can be used instead.

**Marble diagram (without monadic effects):**

```text
it                ---a --b--c --d-e--⊥
it.filterMapM     ---a'-----c'-------⊥
```

(given that `f a = pure (some a)'`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail,
then `it.filterMapM` will be finite even if `it` isn't. In such cases, the termination proof needs
to be done manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned `Option` value.
 -/
Std.Iter.filterMapM : {α β γ : Type w} →
  [Std.Iterator α Id β] →
    {m : Type w → Type w'} →
      [inst : Monad m] → [inst_1 : MonadAttach m] → (f : β → m (Option γ)) → Std.Iter β → Std.IterM m γ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} →
        (f : V₀.V ⟶ V₁.V) →
          autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map f) = CategoryTheory.CategoryStruct.comp f V₁.str)
              CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam →
            V₀.Hom V₁
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.instRespectsIsoScheme : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q], P.RespectsIso
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instLawfulSingletonProd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp],
  LawfulSingleton (α × β) (Std.ExtTreeMap α β cmp)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ediam_image_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X]
  (s : Set (Metric.Snowflaking X α hα₀ hα₁)),
  Metric.ediam (⇑Metric.Snowflaking.ofSnowflaking '' s) = Metric.ediam s ^ α⁻¹
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.BVVar.mk : {width : ℕ} → ℕ → Std.Tactic.BVDecide.BVExpr.bitblast.BVVar width
-- Mathlib.Tactic.Simps.Basic
/-- Syntax for a single rule in `initialize_simps_projections`.  -/
Lean.Parser.Command.simpsRule : Lean.ParserDescr
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuousWithinAt_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {a : α}
  {s : Set α}, ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShape.rel₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} [self : TotalComplexShape c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' → c₁₂.Rel (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂'))
-- Mathlib.Topology.Category.TopPair
/-- Two maps between topological pairs are homotopic if there is a homotopy between them.  -/
TopPair.Homotopic : {X Y : TopPair} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.zsmul_apply : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommGroup N] (f : M →+ N) (z : ℤ) (x : M),
  (z • f) x = z • f x
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Given a `TransvectionStruct` on `n` and an equivalence between `n` and `p`, define the
corresponding `TransvectionStruct` on `p`.  -/
Matrix.TransvectionStruct.reindexEquiv : {n : Type u_1} → {p : Type u_2} → {R : Type u₂} → n ≃ p → Matrix.TransvectionStruct n R → Matrix.TransvectionStruct p R
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousMap.measurable : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] (f : C(α, γ)), Measurable ⇑f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (size : ℕ) (k' : α) (v' : β k')
  (l r : Std.DTreeMap.Internal.Impl α β) (hlk_2 : k ∈ Std.DTreeMap.Internal.Impl.inner size k' v' l r),
  (Std.DTreeMap.Internal.Impl.inner size k' v' l r).get k hlk_2 =
    match h : compare k k' with
    | Ordering.lt => l.get k ⋯
    | Ordering.gt => r.get k ⋯
    | Ordering.eq => cast ⋯ v'
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.ite.sizeOf_spec : sizeOf Lean.Meta.SplitKind.ite = 1
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instSInfHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β], sInfHomClass (sInfHom α β) α β
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.restrictScalars_map_app : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R')
  {X Y : PresheafOfModules R'} (φ' : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((PresheafOfModules.restrictScalars α).map φ').app X_1 =
    (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X_1))).map (φ'.app X_1)
-- Init.Data.List.Nat.TakeDrop
List.drop_length_cons : ∀ {α : Type u_1} {l : List α} (h : l ≠ []) (a : α), List.drop l.length (a :: l) = [l.getLast h]
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.DevosAddRel.eq_1 : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α],
  DevosAddRel✝ =
    Function.onFun (Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 > x2) fun x1 x2 => x1 < x2)) fun x =>
      ((x.1 + x.2).card, x.1.card + x.2.card, x.1.card)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- `AffineEquiv.linear` on automorphisms is a `MonoidHom`.  -/
AffineEquiv.linearHom : {k : Type u_1} →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → (P₁ ≃ᵃ[k] P₁) →* V₁ ≃ₗ[k] V₁