mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
List.swap.eq_2 : ∀ {α : Type u_1} (a : α) (xs : List α), (a :: xs).swap 0 0 = a :: xs
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_id_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.map_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] [inst_3 : OrderBot J] {X Y : C} {f : X ⟶ Y} [inst_4 : SuccOrder J]
  [inst_5 : WellFoundedLT J] (c : CategoryTheory.TransfiniteCompositionOfShape J f) (F : CategoryTheory.Functor C D)
  [inst_6 : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F]
  [inst_7 : CategoryTheory.Limits.PreservesColimitsOfShape J F], (c.map F).isoBot = F.mapIso c.isoBot
-- Lean.Elab.Tactic.Simp
Lean.Meta.DSimp.ConfigWithOptions.mk.sizeOf_spec : ∀ (config : Lean.Meta.DSimp.Config) (userConfig : Lean.Options),
  sizeOf { config := config, userConfig := userConfig } = 1 + sizeOf config + sizeOf userConfig
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.coe_smul : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} [inst : Zero A] [inst_1 : Zero B] [inst_2 : SMulZeroClass M B] (m : M)
  (f : ZeroHom A B), ⇑(m • f) = m • ⇑f
-- Mathlib.Geometry.Convex.Cone.Pointed
ConvexCone.coe_toPointedCone : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : ConvexCone R E) (hC : C.Pointed), ↑(C.toPointedCone hC) = C
-- Mathlib.Data.List.Cycle
/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the next
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.

For example:
* `next [1, 2, 3] 2 _ = 3`
* `next [1, 2, 3] 3 _ = 1`
* `next [1, 2, 3, 2, 4] 2 _ = 3`
* `next [1, 2, 3, 2] 2 _ = 3`
* `next [1, 1, 2, 3, 2] 1 _ = 1`
 -/
List.next : {α : Type u_1} → [DecidableEq α] → (l : List α) → (x : α) → x ∈ l → α
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablySeparated_of_hasCountableSeparatingOn : ∀ {α : Type u_1} [inst : MeasurableSpace α] [h : HasCountableSeparatingOn α MeasurableSet Set.univ],
  MeasurableSpace.CountablySeparated α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_along_fiber_subset : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : One M] (f : ι × κ → M) (i : ι),
  (Function.mulSupport fun j => f (i, j)) ⊆ Prod.snd '' Function.mulSupport f
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal),
  (l.toFilterDistortion I c).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π}
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.Const.IteratedSlowInsertionInto : {α : Type u} → {β : Type v} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => β) → Type (max 0 u v)
-- Init.Data.List.Nat.Range
List.head?_zipIdx : ∀ {α : Type u_1} {l : List α} {k : ℕ}, (l.zipIdx k).head? = Option.map (fun a => (a, k)) l.head?
-- Mathlib.Algebra.Group.PUnit
PUnit.add_eq : ∀ (x y : PUnit.{u_1 + 1}), x + y = PUnit.unit
-- Init.Data.Order.Ord
Array.instLawfulBEqOrd : ∀ {α : Type u_1} [inst : Ord α] [inst_1 : BEq α] [Std.LawfulBEqOrd α], Std.LawfulBEqOrd (Array α)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- The first leg of a pushout cocone is a normal epimorphism if the left component is too.

See also `pushout.fstOfEpi` for the basic epimorphism version, and
`normalOfIsPushoutSndOfNormal` for the flipped version.
 -/
CategoryTheory.normalOfIsPushoutFstOfNormal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q R S : C} →
        {f : P ⟶ Q} →
          {g : P ⟶ R} →
            {h : Q ⟶ S} →
              {k : R ⟶ S} →
                [CategoryTheory.NormalEpi f] →
                  (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm) →
                      CategoryTheory.NormalEpi k
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Def.mk.injEq : ∀ {γ : Type} (builtinName name : Lean.Name) (descr : String) (valueTypeName : Lean.Name)
  (evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key)
  (onAdded : Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit) (builtinName_1 name_1 : Lean.Name)
  (descr_1 : String) (valueTypeName_1 : Lean.Name)
  (evalKey_1 : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key)
  (onAdded_1 : Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit),
  ({ builtinName := builtinName, name := name, descr := descr, valueTypeName := valueTypeName, evalKey := evalKey,
        onAdded := onAdded } =
      { builtinName := builtinName_1, name := name_1, descr := descr_1, valueTypeName := valueTypeName_1,
        evalKey := evalKey_1, onAdded := onAdded_1 }) =
    (builtinName = builtinName_1 ∧
      name = name_1 ∧ descr = descr_1 ∧ valueTypeName = valueTypeName_1 ∧ evalKey = evalKey_1 ∧ onAdded = onAdded_1)
-- Mathlib.GroupTheory.Perm.Subgroup
/-- **Cayley's theorem**: Every group G is isomorphic to a subgroup of the symmetric group acting on
`G`. Note that we generalize this to an arbitrary "faithful" group action by `G`. Setting `H = G`
recovers the usual statement of Cayley's theorem via `RightCancelMonoid.faithfulSMul`  -/
Equiv.Perm.subgroupOfMulAction : (G : Type u_1) →
  (H : Type u_2) →
    [inst : Group G] → [inst_1 : MulAction G H] → [FaithfulSMul G H] → G ≃* ↥(MulAction.toPermHom G H).range
-- Mathlib.Data.Finset.Defs
Finset.forall_coe : ∀ {α : Type u_4} (s : Finset α) (p : ↥s → Prop), (∀ (x : ↥s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
-- Mathlib.Topology.Homeomorph.TransferInstance
/-- An equivalence `e : α ≃ β` gives a homeomorphism `α ≃ₜ β` where the topological space structure
on `α` is the one obtained by transporting the topological space structure on `β` back along `e`.  -/
Equiv.homeomorph : {α : Type u_2} → {β : Type u_3} → [inst : TopologicalSpace β] → (e : α ≃ β) → α ≃ₜ β
-- Init.Data.List.Control
/-- Maps `f` over the list and collects the results with `<|>`. The result for the end of the list is
`failure`.

Examples:
 * `[[], [1, 2], [], [2]].firstM List.head? = some 1`
 * `[[], [], []].firstM List.head? = none`
 * `[].firstM List.head? = none`
 -/
List.firstM : {m : Type u → Type v} → [Alternative m] → {α : Type w} → {β : Type u} → (α → m β) → List α → m β
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.Pair.mk.injEq : ∀ {α : Type u_1} (a b a_1 b_1 : α), ({ a := a, b := b } = { a := a_1, b := b_1 }) = (a = a_1 ∧ b = b_1)
-- Mathlib.Data.List.Basic
List.getElem?_length : ∀ {α : Type u} (l : List α), l[l.length]? = none
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.pathEquivList_cons : ∀ {α : Type u_1} (p : Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α))
  (a : Quiver.SingleObj.star α ⟶ Quiver.SingleObj.star α),
  Quiver.SingleObj.pathEquivList (p.cons a) = a :: Quiver.SingleObj.pathToList p
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.quotientEquivOfIsTopCompl_apply_mk : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q) (x : M),
  (p.quotientEquivOfIsTopCompl q h) (Submodule.Quotient.mk x) = (q.projectionOnto p ⋯) x
-- Mathlib.Data.Finset.Card
/-- **Alias** of the reverse direction of `Finset.card_ne_zero`. -/
Finset.Nonempty.card_ne_zero : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s.card ≠ 0
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapM.match_1.splitter : {β β' : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → n (Option β')} →
      [inst : MonadAttach n] →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
              ((hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩) →
                ((out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩) →
                  motive __do_lift
-- Init.Data.String.Lemmas.FindPos
String.le_offset_posGE : ∀ {s : String} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos}, p ≤ (s.posGE p h).offset
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X),
  (∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) → P f
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  {a : X} [inst_5 : LinearOrder X] [CompactIccSpace X] [NoMaxOrder X] [OrderTopology X],
  MeasureTheory.IntegrableOn f (Set.Ioi a) μ ↔
    MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧
      MeasureTheory.IntegrableAtFilter f (nhdsWithin a (Set.Ioi a)) μ ∧
        MeasureTheory.LocallyIntegrableOn f (Set.Ioi a) μ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∃ X, CategoryTheory.Limits.IsZero X) → CategoryTheory.Limits.HasZeroObject C
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {T : CategoryTheory.Monad C} {c c' : CategoryTheory.Kleisli T}
  {x y : c.Hom c'}, x = y ↔ x.of = y.of
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Differentiable.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {g : (i : ι) → E → F i →L[𝕜] G i} [Finite ι],
  Differentiable 𝕜 f →
    (∀ (i : ι), Differentiable 𝕜 (g i)) → Differentiable 𝕜 fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x
-- Mathlib.Order.Category.BddDistLat
/-- The category of bounded distributive lattices with bounded lattice morphisms.  -/
BddDistLat : Type (u_1 + 1)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.isMulCommutative_iff_card_le_three : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], IsMulCommutative ↥(alternatingGroup α) ↔ Nat.card α ≤ 3
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.top_coe : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], ↑⊤ = Set.univ
-- Mathlib.MeasureTheory.Group.AddCircle
AddCircle.closedBall_ae_eq_ball : ∀ {T : ℝ} [hT : Fact (0 < T)] {x : AddCircle T} {ε : ℝ}, Metric.closedBall x ε =ᵐ[MeasureTheory.volume] Metric.ball x ε
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.simprocNames : Lean.Meta.Simprocs → Lean.PHashSet Lean.Name
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.match_3.splitter : {α : Type u_1} →
  (motive : (xs : List α) → xs ≠ [] → Sort u_2) →
    (xs : List α) → (h : xs ≠ []) → ((y : α) → (ys : List α) → (h : y :: ys ≠ []) → motive (y :: ys) h) → motive xs h
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instCommMonoid : {R : Type u_1} →
  [inst : CommMonoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → CommMonoid (OreLocalization S R)
-- Lean.Util.NumApps
_private.Lean.Util.NumApps.0.Lean.Expr.numApps.unsafe_1 : Lean.Expr → Lean.NameMap ℕ
-- Init.Data.UInt.Basic
instComplementUInt32 : Complement UInt32
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime.congr_simp : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P P_1 : Ideal ↥A) (e_P : P = P_1) [inst_1 : P.IsPrime],
  A.ofPrime P = A.ofPrime P_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The colimit cofan which defines the simplicial `n`-chains
`(X.chainComplex R).X n`.  -/
SSet.chainComplexXCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [CategoryTheory.Preadditive C] → (X : SSet) → (R : C) → (n : ℕ) → CategoryTheory.Limits.Cofan fun x => R
-- Init.MetaTypes
Lean.Meta.Occurrences.neg.inj : ∀ {idxs idxs_1 : List ℕ}, Lean.Meta.Occurrences.neg idxs = Lean.Meta.Occurrences.neg idxs_1 → idxs = idxs_1
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instInter : Inter ZFSet.{u_1}
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasurableEmbedding.rnDeriv_map_aux : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
  {f : α → β},
  MeasurableEmbedding f →
    μ.AbsolutelyContinuous ν →
      ∀ [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
        (fun x => (MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.mk_single : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R] (x : M)
  {nonneg : 0 ≤ fun₀ | x => 1} {total : ((fun₀ | x => 1).sum fun x r => r) = 1},
  { weights := fun₀ | x => 1, nonneg := nonneg, total := total } = Convexity.StdSimplex.single x
-- Init.Data.SInt.Lemmas
ISize.not_maxValue_lt : ∀ {a : ISize}, ¬ISize.maxValue < a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.induction_linear : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {motive : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M),
  motive 0 →
    (∀ (x y : AddMonoidAlgebra R M), motive x → motive y → motive (x + y)) →
      (∀ (m : M) (r : R), motive (AddMonoidAlgebra.single m r)) → motive x
-- Init.Data.Vector.Lemmas
Vector.flatMap_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : ℕ} {f : α → Vector β m} {x : α}, #v[x].flatMap f = Vector.cast ⋯ (f x)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.ker_map_of_surjective : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  Function.Surjective ⇑(algebraMap A B) →
    (KaehlerDifferential.map R R A B).ker =
      Submodule.map (Finsupp.linearCombination A ⇑(KaehlerDifferential.D R A))
        (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)).ker
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.opObjEquiv_opObjEquiv_symm_apply : ∀ {d n : ℕ} (f : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (d + 1)),
  (SSet.opObjEquiv (SSet.stdSimplex.opObjEquiv.symm f)) i = (f i.rev).rev
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β}
  (f : β → α), Function.Injective g → ∑' (x : ↑(Set.range g)), f ↑x = ∑' (x : γ), f (g x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_filter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  t.WF → ((Std.TreeSet.Raw.filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = false)
-- Mathlib.RingTheory.ReesAlgebra
instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} [IsNoetherianRing R], IsNoetherianRing ↥(reesAlgebra I)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le : ∀ {𝕜 : Type u} {E : Type wE} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Subsingleton ι] (i : ι),
  ‖(ContinuousAlternatingMap.ofSubsingleton 𝕜 E E i) (ContinuousLinearMap.id 𝕜 E)‖₊ ≤ 1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a + x) ⁻¹' Set.Ici b = Set.Ici (b - a)
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.SearchStep.ofSliceFrom.match_1.eq_1 : ∀ {s : String.Slice} {p : s.Pos} (motive : String.Slice.Pattern.SearchStep (s.sliceFrom p) → Sort u_1)
  (l r : (s.sliceFrom p).Pos)
  (h_1 : (l r : (s.sliceFrom p).Pos) → motive (String.Slice.Pattern.SearchStep.rejected l r))
  (h_2 : (l r : (s.sliceFrom p).Pos) → motive (String.Slice.Pattern.SearchStep.matched l r)),
  (match String.Slice.Pattern.SearchStep.rejected l r with
    | String.Slice.Pattern.SearchStep.rejected l r => h_1 l r
    | String.Slice.Pattern.SearchStep.matched l r => h_2 l r) =
    h_1 l r
-- Lean.DocString.Extension
/-- A deferred check that lacked sufficient information when it was used (e.g. a forward references to
a name in a downstream module). The `index` identifies it among the docstring's deferred checks
that are stored in an environment extension. Inline and block deferred checks use the same
counter.
 -/
Lean.ElabInline.deferred : ℕ → Lean.ElabInline
-- Init.Data.SInt.Lemmas
Int8.maxValue_le_iff : ∀ {a : Int8}, Int8.maxValue ≤ a ↔ a = Int8.maxValue
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.eq_2 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option β')} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (out' : β') (h' : (f out).Property (some out'))
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨some out', h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_2 out' h'
-- Mathlib.GroupTheory.IsSubnormal
/-- If the additive subgroup `H` of a group `G` is trivial, then it is subnormal.  -/
AddSubgroup.IsSubnormal.of_subsingleton : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [Subsingleton ↥H], H.IsSubnormal
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun_eq_pi_basisFun : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜],
  PiLp.basisFun p 𝕜 ι = (Pi.basisFun 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_eq_sInf : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  Algebra.adjoin R s = sInf {p | s ⊆ ↑p}
-- Init.Grind.AC
Lean.Grind.AC.Context.mk.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α] (vars : Lean.RArray (PLift α)) (op : α → α → α),
  sizeOf { vars := vars, op := op } = 1 + sizeOf vars
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_lineMap_right : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c d : k),
  (AffineMap.lineMap p₀ ((AffineMap.lineMap p₀ p₁) c)) d = (AffineMap.lineMap p₀ p₁) (d * c)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Makes a localization map from a `CommMonoid` hom satisfying the characteristic predicate.  -/
MonoidHom.toLocalizationMap : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          (f : M →* N) →
            (∀ (y : ↥S), IsUnit (f ↑y)) →
              (∀ (z : N), ∃ x, z * f ↑x.2 = f x.1) →
                (∀ (x y : M), f x = f y → ∃ c, ↑c * x = ↑c * y) → S.LocalizationMap N
-- Mathlib.GroupTheory.PresentedGroup
/-- The free product (Coproduct) of presentations is isomorphic to the presentation of the union over
the `FreeGroup (α ⊕ β)`
 -/
PresentedGroup.coprodPresentations : {α : Type u_1} →
  {β : Type u_2} →
    (rels₁ : Set (FreeGroup α)) →
      (rels₂ : Set (FreeGroup β)) →
        PresentedGroup (⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂) ≃*
          Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Simple function defined on a finite type.  -/
MeasureTheory.SimpleFunc.ofFinite : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [Finite α] → [MeasurableSingletonClass α] → (α → β) → MeasureTheory.SimpleFunc α β
-- Lean.MonadEnv
Lean.getConstInfoInduct : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.InductiveVal
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Get all potential rewrite lemmas from the imported environment.
By setting the `librarySearch.excludedModules` option, all lemmas from certain modules
can be excluded.  -/
Mathlib.Tactic.LibraryRewrite.getImportCandidates : Lean.Expr → Lean.MetaM (Array (Array Mathlib.Tactic.LibraryRewrite.RewriteLemma))
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppAddEquivDFinsupp_apply : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : AddZeroClass N] (a : (i : ι) × η i →₀ N),
  sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a
-- Mathlib.NumberTheory.Padics.Hensel
padic_polynomial_dist : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  (F : Polynomial R) (x y : ℤ_[p]), ‖(Polynomial.aeval x) F - (Polynomial.aeval y) F‖ ≤ ‖x - y‖
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsRightUniformGroup.mk : ∀ {G : Type u_7} [inst : UniformSpace G] [inst_1 : Group G] [toIsTopologicalGroup : IsTopologicalGroup G],
  uniformity G = Filter.comap (fun x => x.2 * x.1⁻¹) (nhds 1) → IsRightUniformGroup G