mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.φ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z),
  f.φ =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (n + 1)) f.a +
      ∑ i,
        CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P ↑i).f (n + 1))
          (CategoryTheory.CategoryStruct.comp (X.δ i.rev.succ) (f.b i.rev))
-- Init.Data.ByteArray.Lemmas
ByteArray.append_eq_append_iff_of_size_eq_left : ∀ {ws xs ys zs : ByteArray}, ws.size = xs.size → (ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Any.imp : ∀ {α : Type u_1} {P Q : α → Prop}, (∀ (a : α), P a → Q a) → ∀ {t : Ordnode α}, Ordnode.Any P t → Ordnode.Any Q t
-- Init.Data.Array.Mem
Array.sizeOf_get : ∀ {α : Type u_1} [inst : SizeOf α] (as : Array α) (i : ℕ) (h : i < as.size), sizeOf as[i] < sizeOf as
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- For a group with zero, `PosMulReflectLT G₀`
allows us to upgrade `MulPosMono G₀` to `MulPosReflectLE G₀`.
The other implication holds without the `PosMulReflectLT G₀` assumption,
see `MulPosReflectLT.toMulPosStrictMono` for a stronger version below.

This theorem shows that in the presence of the assumption `PosMulReflectLT G₀`,
it makes no sense to optimize between assumptions `MulPosMono G₀`, `MulPosStrictMono G₀`,
`MulPosReflectLT G₀`, and `MulPosReflectLE G₀`.  -/
MulPosReflectLE.of_posMulReflectLT_of_mulPosMono : ∀ (G₀ : Type u_3) [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀],
  MulPosReflectLE G₀
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Pi.summable : ∀ {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [inst : (x : α) → AddCommMonoid (X x)]
  [inst_1 : (x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x},
  Summable f L ↔ ∀ (x : α), Summable (fun i => f i x) L
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) [Finite ι],
  (⨅ i, I i).ideal = ⨅ i, (I i).ideal
-- Mathlib.Order.Lattice.Nat
Nat.eq_Ici_of_nonempty_of_upward_closed : ∀ {s : Set ℕ}, s.Nonempty → (∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) → s = Set.Ici (sInf s)
-- Mathlib.Algebra.Ring.Defs
nsmul_eq_mul : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : ℕ) (a : α), n • a = ↑n * a
-- Batteries.Data.Vector.Basic
/-- Set an element of a vector using a `USize` index and a proof that the index is within bounds.
 -/
Vector.uset : {α : Type u_1} → {n : ℕ} → Vector α n → (i : USize) → α → i.toNat < n → Vector α n
-- Mathlib.Analysis.Normed.Module.Completion
/-- Embedding of a normed space to its completion as a linear isometry.  -/
UniformSpace.Completion.toComplₗᵢ : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : UniformContinuousConstSMul 𝕜 E] → E →ₗᵢ[𝕜] UniformSpace.Completion E
-- Mathlib.MeasureTheory.Integral.CircleIntegral
lipschitzWith_circleMap : ∀ (c : ℂ) (R : ℝ), LipschitzWith (Real.nnabs R) (circleMap c R)
-- Mathlib.RingTheory.Adjoin.Field
IsIntegral.mem_range_algHom_of_minpoly_splits : ∀ {R : Type u_1} {K : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra R K] {x : L} [inst_4 : Algebra R L],
  IsIntegral R x → (Polynomial.map (algebraMap R K) (minpoly R x)).Splits → ∀ (f : K →ₐ[R] L), x ∈ f.range
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Client.ofNative.sizeOf_spec : ∀ (native : Std.Internal.UV.TCP.Socket), sizeOf { native := native } = 1 + sizeOf native
-- Batteries.CodeAction.Match
/-- Inner loop for `findAllInfos`.  -/
Batteries.CodeAction.findAllInfos.loop : (Lean.Elab.Info → Bool) → Lean.Elab.InfoTree → Array Lean.Elab.Info → Array Lean.Elab.Info
-- Mathlib.Tactic.Ring.Compare
/-- **Alias** of `Mathlib.Tactic.Ring.ltOfPartialOrder`.

---

`PartialOrder` implies `LT`.  -/
Mathlib.Tactic.Ring.lt_of_po : (α : Type u_1) → [PartialOrder α] → LT α
-- Mathlib.Order.BooleanAlgebra.Basic
himp_eq : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x ⇨ y = y ⊔ xᶜ
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj { unmop := c } d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuousOn.continuousOn : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  UniformContinuousOn f s → ContinuousOn f s
-- Mathlib.Algebra.Order.Star.Basic
StarRingHomClass.instOrderHomClass : ∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R]
  [inst_2 : StarRing R] [StarOrderedRing R] [inst_4 : NonUnitalSemiring S] [inst_5 : PartialOrder S]
  [inst_6 : StarRing S] [StarOrderedRing S] [inst_8 : FunLike F R S] [inst_9 : NonUnitalRingHomClass F R S]
  [NonUnitalStarRingHomClass F R S], OrderHomClass F R S
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.mk : String → Lean.Lsp.SymbolKind → Array Lean.Lsp.SymbolTag → Lean.Lsp.Location → Option String → Lean.Lsp.SymbolInformation
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u} (err : ε)
  (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred), ⦃ epost.head err ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.openPartialHomeomorphCoe_target : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [inst_5 : OrderTopology 𝕜]
  [inst_6 : DiscreteTopology ↥(AddSubgroup.zmultiples p)], (AddCircle.openPartialHomeomorphCoe p a).target = {↑a}ᶜ
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_union_Iic_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → Set.Ici b ∪ Set.Iic a = Set.univ
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.right.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g), h.right = CategoryTheory.Retract.map h CategoryTheory.Arrow.rightFunc
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.hrecv : ∀ {α : Type} (self : Std.CloseableChannel.Bounded.State✝ α),
  Std.CloseableChannel.Bounded.State.recvIdx✝ self < Std.CloseableChannel.Bounded.State.capacity✝ self
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- Just like exact integration, the trapezoidal integration from `a` to `a` is zero.  -/
trapezoidal_integral_eq : ∀ (f : ℝ → ℝ) (N : ℕ) (a : ℝ), trapezoidal_integral f N a a = 0
-- Mathlib.Order.RelIso.Set
RelIso.subrelUnivIso_symm_apply : ∀ {α : Type u_1} {r : α → α → Prop} {p : α → Prop} (h : ∀ (x : α), p x) (x : α),
  (RelIso.subrelUnivIso h).symm x = ⟨x, ⋯⟩
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
/-- If two continuous linear maps `u, v : E → F` agree on a subspace `A` of `E` with finite
codimension, then `u` is strict with closed range if and only if `v` is strict with closed range.  -/
ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u v : E →L[𝕜] F) (A : Submodule 𝕜 E) [A.CoFG],
  Set.EqOn ⇑u ⇑v ↑A → (Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔ Topology.IsStrictMap ⇑v ∧ IsClosed ↑(↑v).range)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isClosedBelow_iff : ∀ {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}}, Ordinal.IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.map_inv_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [inst_2 : CategoryTheory.IsIso f] {F_1 : D → D → Type uF}
  {carrier : D → Type w} {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_3 : CategoryTheory.ConcreteCategory D F_1] (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (F.map f))
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.inv f))) x) =
    x
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The coefficients of the regularized hypergeometric series.  -/
Complex.regularizedHGFunCoeff : Multiset ℂ → Multiset ℂ → ℕ → ℂ
-- Mathlib.Order.Basic
LT.lt.gt : ∀ {α : Type u_2} [inst : LT α] {a b : α}, a < b → b > a
-- Mathlib.Combinatorics.SimpleGraph.Cayley
/-- `addCayley` is a left (order-)adjoint.  -/
SimpleGraph.addCayley_gc : ∀ (M : Type u_1) [inst : Add M],
  GaloisConnection (fun x => SimpleGraph.addCayley x) fun x => {g | ∀ (a : M), a + g ≠ a → x.Adj (a + g) a}
-- Mathlib.LinearAlgebra.AffineSpace.Independent
affineIndependent_smul : ∀ (k : Type u_1) {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G},
  AffineIndependent k (a • p) ↔ AffineIndependent k p
-- Aesop.Tree.Data
Aesop.GoalOrigin.subgoal.sizeOf_spec : sizeOf Aesop.GoalOrigin.subgoal = 1
-- Mathlib.Algebra.Ring.Defs
/-- The canonical map `ℕ → R` is a homomorphism.  -/
Semiring.natCast_succ : ∀ {α : Type u} [self : Semiring α] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.alternatizeUncurryFin_curryLeft : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N),
  AlternatingMap.alternatizeUncurryFin f.curryLeft = (n + 1) • f
-- Lean.Message
/-- A suffix added to diagnostic name-containing tags to indicate that they should be used as an error
code.
 -/
Lean.errorNameSuffix : String
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ → Std.Internal.List.DistinctKeys (Std.Internal.List.insertList l₁ l₂)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
SimpleGraph.extremalNumber.eq_1 : ∀ (n : ℕ) {W : Type u_1} (H : SimpleGraph W),
  SimpleGraph.extremalNumber n H = {G | H.Free G}.sup fun x => x.edgeFinset.card
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y_1).left.left =
    Y_1.left.left
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.toPresentation : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → Algebra.PreSubmersivePresentation R S ι σ → Algebra.Presentation R S ι σ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (n : ℕ),
  groupHomology.map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) n =
    CategoryTheory.CategoryStruct.id (groupHomology A n)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRoiSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Roi.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RoiSlice α β)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.i₁_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.Precylinder A),
  CategoryTheory.CategoryStruct.comp self.i₁ self.π = CategoryTheory.CategoryStruct.id A
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.elabCommand.go : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_max!_eq_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {hc : t.max! ∈ t}, t.get t.max! hc = t.max ⋯
-- Mathlib.Topology.Algebra.ConstMulAction
OrderDual.continuousConstSMul' : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α],
  ContinuousConstSMul Mᵒᵈ α
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BiconeMorphism.wπ : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J), CategoryTheory.CategoryStruct.comp self.hom (B.π j) = A.π j
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
IsUltraUniformity.comap : ∀ {X : Type u_1} {Y : Type u_2} {u : UniformSpace Y}, IsUltraUniformity Y → ∀ (f : X → Y), IsUltraUniformity X
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_conv'Aux_eq_zero : ∀ {K : Type u_1} [inst : DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)}, GenContFract.convs'Aux s 0 = 0
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.single_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ) (r : R)
  (m : M), PolynomialModule.single R i (r • m) = r • PolynomialModule.single R i m
-- Aesop.Forward.LevelIndex
Aesop.LevelIndex : Type
-- Mathlib.FieldTheory.Tower
/-- In a tower of field extensions `A / K / F`, if `A / F` is finite, so is `K / F`.

(In fact, it suffices that `A` is a nontrivial ring.)

Note this cannot be an instance as Lean cannot infer `A`.
 -/
Module.Finite.left : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Ring F] [inst_1 : Ring K] [inst_2 : Module F K]
  [inst_3 : AddCommGroup A] [inst_4 : Module K A] [Module.IsTorsionFree K A] [inst_6 : Module F A] [IsNoetherian F A]
  [IsScalarTower F K A] [IsDomain K] [Nontrivial A], Module.Finite F K
-- Mathlib.RingTheory.WittVector.Defs
WittVector.neg_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  (-x).coeff n = WittVector.peval (WittVector.wittNeg p n) ![x.coeff]
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.mutually_singular_measure_sub : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], (μ - ν).MutuallySingular (ν - μ)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.norm_sqrt : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  (a : A), autoParam (0 ≤ a) CFC.norm_sqrt._auto_1 → ‖CFC.sqrt a‖ = √‖a‖
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.toDual_eq_top : ∀ (α : Type u) [inst : Bot α] {a : α}, OrderDual.toDual a = ⊤ ↔ a = ⊥
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- The graph induced by the adjacency matrix of `G` is `G` itself.  -/
SimpleGraph.toGraph_adjMatrix_eq : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : MulZeroOneClass α]
  [inst_2 : Nontrivial α], ⋯.toGraph = G
-- Mathlib.Algebra.Order.Interval.Basic
/-- The length of an interval is its first component minus its second component. This measures the
accuracy of the approximation by an interval.  -/
Interval.length : {α : Type u_2} → [AddCommGroup α] → [inst : PartialOrder α] → Interval α → α
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The square cylinders formed from measurable sets generate the product σ-algebra.  -/
MeasureTheory.generateFrom_squareCylinders : ∀ {ι : Type u_2} {α : ι → Type u_1} [inst : (i : ι) → MeasurableSpace (α i)],
  MeasurableSpace.generateFrom (MeasureTheory.squareCylinders fun i => {s | MeasurableSet s}) = MeasurableSpace.pi
-- Mathlib.Algebra.Order.IsBotOne
min_zero : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Zero α] [IsBotZeroClass α] (a : α), min a 0 = 0
-- Mathlib.RingTheory.TensorProduct.Basic
AlgHom.liftEquiv_symm_apply : ∀ {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra S B] [inst_6 : Algebra R S]
  [inst_7 : Algebra R B] [inst_8 : IsScalarTower R S B] (f : TensorProduct R S A →ₐ[S] B) (a : A),
  ((AlgHom.liftEquiv R S A B).symm f) a = f (1 ⊗ₜ[R] a)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKeyD_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a fallback : α},
      m.getKeyD a fallback = Std.Internal.List.getKeyD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback
-- Mathlib.LinearAlgebra.Matrix.Unique
/-- `M₁(A)` and `A` are equivalent as rings.  -/
Matrix.uniqueRingEquiv : {m : Type u_1} → {A : Type u_3} → [inst : Unique m] → [inst_1 : NonUnitalNonAssocSemiring A] → Matrix m m A ≃+* A
-- Mathlib.Algebra.Order.Floor.Div
Nat.instCeilDiv : CeilDiv ℕ ℕ
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_bot : ∀ {G : Type u_1} [inst : Group G], Nat.card ↥⊥ = 1
-- Init.Data.List.Basic
List.Mem.brecOn : ∀ {α : Type u} {a : α} {motive : (a_1 : List α) → List.Mem a a_1 → Prop} {a_1 : List α} (t : List.Mem a a_1),
  (∀ (a_2 : List α) (t : List.Mem a a_2), List.Mem.below t → motive a_2 t) → motive a_1 t
-- Aesop.Util.Basic
Aesop.runTacticsCapturingPostState : Array Lean.Syntax.Tactic →
  Lean.Meta.SavedState → List Lean.MVarId → Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_zero : ∀ (m n : ℕ), BitVec.setWidth m 0#n = 0#m
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsFixedBlock.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : SMul G X] (B : Set X), MulAction.IsFixedBlock G B = ∀ (g : G), g • B = B
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F : TopCat.Sheaf C X} {G : TopCat.Presheaf C X} (f : F.obj ⟶ G),
  (∀ (x : ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))) ↔
    ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U)))
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.instantiateMVarsAtInductive : Lean.InductiveType → Lean.Elab.TermElabM Lean.InductiveType
-- Mathlib.Algebra.Algebra.Equiv
/-- See Note [custom simps projection]  -/
AlgEquiv.Simps.symm_apply : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₂ → A₁
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.IsMetric.le_caratheodory : ∀ {X : Type u_2} [inst : EMetricSpace X] {μ : MeasureTheory.OuterMeasure X} [inst_1 : MeasurableSpace X] [BorelSpace X],
  μ.IsMetric → inst_1 ≤ μ.caratheodory
-- Mathlib.Topology.Category.Compactum
/-- Any continuous map between Compacta is a morphism of compacta.  -/
Compactum.homOfContinuous : {X Y : Compactum} → (f : X.A → Y.A) → Continuous f → (X ⟶ Y)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The supremum of a subspace and the span of a set of points is equal to the span of the union of
the subspace and the set of points.  -/
Projectivization.Subspace.sup_span : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
  W ⊔ Projectivization.Subspace.span S = Projectivization.Subspace.span (↑W ∪ S)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.instFullProdCurry : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E], CategoryTheory.Functor.curry.Full
-- Std.Http.Data.Response
/-- Optional dynamic metadata attached to the response.
 -/
Std.Http.Response.extensions : {t : Type} → Std.Http.Response t → Std.Http.Extensions
-- Mathlib.CategoryTheory.Category.Cat.AsSmall
/-- Assigning to each category `C` the small category `AsSmall C` induces a functor `Cat ⥤ Cat`.  -/
CategoryTheory.Cat.asSmallFunctor : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsCoseparating →
    ∀ {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (α : C ≌ D), (P.strictMap α.functor).IsCoseparating
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.integral_normed_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {X : Type u_2}
  [inst_8 : NormedAddCommGroup X] [inst_9 : NormedSpace ℝ X] [CompleteSpace X] (z : X),
  ∫ (x : E), f.normed μ x • z ∂μ = z
-- Mathlib.MeasureTheory.Group.AEStabilizer
MeasureTheory.smul_ae_eq_self_of_mem_zpowers : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {x_1 y : G} {s : Set α},
  x_1 • s =ᵐ[μ] s → y ∈ Subgroup.zpowers x_1 → y • s =ᵐ[μ] s