mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_forgetStalk_hom : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom
        ⇑(CommRingCat.Hom.hom
            (CategoryTheory.Limits.colimit.ι
              ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)))
      (smoothSheafCommRing.forgetStalk IM I M R x).hom =
    CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf) U
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (mid : C) →
          (ι : X ⟶ mid) →
            (π : mid ⟶ Y) →
              autoParam (CategoryTheory.CategoryStruct.comp ι π = f) CategoryTheory.Factorisation.ι_π._autoParam →
                CategoryTheory.Factorisation f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_b₆_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).b₆ = W.b₆
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_left_le_size_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.GroupTheory.Exponent
/-- The exponent of finite product of additive monoids is the `Finset.lcm` of the
exponents of the constituent additive monoids.  -/
AddMonoid.exponent_pi : ∀ {ι : Type u_1} [inst : Fintype ι] {M : ι → Type u_2} [inst_1 : (i : ι) → AddMonoid (M i)],
  AddMonoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun x => AddMonoid.exponent (M x)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- The additive Roth number of a finset is the cardinality of its biggest 3AP-free
subset.

The usual Roth number corresponds to `addRothNumber (Finset.range n)`, see `rothNumberNat`.  -/
addRothNumber : {α : Type u_2} → [DecidableEq α] → [AddMonoid α] → Finset α →o ℕ
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.instHasFiniteWidePullbacksOppositeOfHasFiniteWidePushouts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteWidePushouts C],
  CategoryTheory.Limits.HasFiniteWidePullbacks Cᵒᵖ
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, subtracting vectors, vector inner product
form.  -/
norm_sub_sq_eq_norm_sq_add_norm_sq_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  inner ℝ x y = 0 → ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)]
  (l : Std.DHashMap.Internal.AssocList α β), sizeOf { l := l } = 1 + sizeOf l
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Integral of a simple function `α →ₛ ℝ≥0∞` as a bilinear map.  -/
MeasureTheory.SimpleFunc.lintegralₗ : {α : Type u_1} →
  {m : MeasurableSpace α} → MeasureTheory.SimpleFunc α ENNReal →ₗ[ENNReal] MeasureTheory.Measure α →ₗ[ENNReal] ENNReal
-- Init.Data.List.Nat.Pairwise
/-- Given a list `is` of monotonically increasing indices into `l`, getting each index
produces a sublist of `l`.   -/
List.map_getElem_sublist : ∀ {α : Type u_1} {l : List α} {is : List (Fin l.length)},
  List.Pairwise (fun x1 x2 => x1 < x2) is → (List.map (fun x => l[x]) is).Sublist l
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙ_real_eq_nnreal : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Module ℝ A] [IsSemitopologicalRing A] [inst_7 : IsScalarTower ℝ A A]
  [inst_8 : SMulCommClass ℝ A A] [T2Space A] [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_11 : NonnegSpectrumClass ℝ A] {f : ℝ → ℝ} (a : A),
  (∀ x ∈ quasispectrum ℝ a, 0 ≤ f x) →
    autoParam (0 ≤ a) cfcₙ_real_eq_nnreal._auto_1 → cfcₙ f a = cfcₙ (fun x => (f ↑x).toNNReal) a
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.mulLeft₀_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : PosMulReflectLT G₀] (a : G₀)
  (ha : 0 < a) (x : G₀), (RelIso.symm (OrderIso.mulLeft₀ a ha)) x = a⁻¹ * x
-- Mathlib.Algebra.Lie.Ideal
instIsLieTowerSubtypeMemLieIdeal_1 : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : LieRingModule L M] [inst_4 : LieAlgebra R L] (I : LieIdeal R L), IsLieTower L (↥I) M
-- Mathlib.Tactic.DefEqAbuse
/-- Collect and combine values of type `α` produced by visiting all trace nodes in a `MessageData`
tree.

Automatically recurses through structural wrappers, invoking `onTrace` only for
`.trace` nodes. The `onTrace` callback receives the arguments of `.trace`:
- the `TraceData` (class name, timing, etc.)
- the trace node's header message
- the trace node's child messages

Each call to `onTrace` is expected to produce either a `descend`, in which case the children of the
trace nodes will be visited, or an `ascend`, in which case they will not. Both may take an argument
`butFirst := some a`, which will cause `a` to be `combine`d into the accumulated value.

We assume `x = combine empty x = combine x empty`. `empty` is attempted to be synthesized as the
`EmptyCollection`, and `combine` is attempted to be synthesized first via the notation `(· ++ ·)`
then via `(· ∪ ·)` as a fallback.

Note that the children may be visited manually via a recursive call to `collectWith` or
`collectWithAndAscend`.

Note: `.ofLazy` nodes are skipped (return `empty`) because they contain unevaluated
formatting thunks, not trace tree structure. This is consistent with `hasTag`
in `Lean.Message` which also skips `.ofLazy`.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.visitTraceNodesM : {m : Type → Type} →
  [Monad m] →
    {α : Type} →
      Lean.MessageData →
        (Lean.TraceData → Lean.MessageData → Array Lean.MessageData → m (Lean.MessageData.VisitStep✝ α)) →
          autoParam α Lean.MessageData.visitTraceNodesM._auto_1✝ →
            autoParam (α → α → α) Lean.MessageData.visitTraceNodesM._auto_3✝ → m α
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.coe_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), ⇑(↑φ).toLinearMap = ⇑φ
-- Mathlib.Data.List.Defs
List.iterateTR.loop.eq_2 : ∀ {α : Type u_1} (f : α → α) (a : α) (l : List α) (n_1 : ℕ),
  List.iterateTR.loop f a n_1.succ l = List.iterateTR.loop f (f a) n_1 (a :: l)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.linearMap_eq_iff_of_eq_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_8}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {V : Submodule R M} (f g : ↥V →ₗ[R] N) {S : Set M}
  (hV : V = Submodule.span R S), f = g ↔ ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
-- Lean.Elab.Tactic.Omega.Core
/-- Run the `omega` algorithm (for now without dark and grey shadows!) on a problem.
 -/
Lean.Elab.Tactic.Omega.Problem.runOmega : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Data.Matrix.Mul
Matrix.add_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (L M : Matrix l m α) (N : Matrix m n α), (L + M) * N = L * N + M * N
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are coplanar.  -/
coplanar_triple : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ p₃ : P), Coplanar k {p₁, p₂, p₃}
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The inverse of a homotopy equivalence.  -/
CategoryTheory.ShortComplex.HomotopyEquiv.symm : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.HomotopyEquiv S₂ → S₂.HomotopyEquiv S₁
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.hasFiniteSupport : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : AddCommMonoid M] [inst_1 : SetLike S M]
  [inst_2 : AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun i => ↥(A i)),
  Function.HasFiniteSupport fun i => ↑(x i)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Closed balls defined using the distance or the edistance coincide  -/
Metric.closedEBall_coe : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, Metric.closedEBall x ↑ε = Metric.closedBall x ↑ε
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitorImpl_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.leftUnitorImpl.inv.F =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Maps.0.SimpleGraph.Walk.transfer.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    (H : SimpleGraph V) →
      (motive : (u v : V) → (p : G.Walk u v) → (∀ e ∈ p.edges, e ∈ H.edgeSet) → Sort u_2) →
        (u v : V) →
          (p : G.Walk u v) →
            (h : ∀ e ∈ p.edges, e ∈ H.edgeSet) →
              ((u : V) → (h : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∈ H.edgeSet) → motive u u SimpleGraph.Walk.nil h) →
                ((u w v : V) →
                    (h : G.Adj u v) →
                      (p : G.Walk v w) →
                        (h_2 : ∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet) →
                          motive u w (SimpleGraph.Walk.cons h p) h_2) →
                  motive u v p h
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated additive subgroups is finitely generated.  -/
AddSubgroup.FG.prod : ∀ {G : Type u_3} [inst : AddGroup G] {G' : Type u_5} [inst_1 : AddGroup G'] {P : AddSubgroup G} {Q : AddSubgroup G'},
  P.FG → Q.FG → (P.prod Q).FG
-- Aesop.Rule.Name
Aesop.BuilderName.apply : Aesop.BuilderName
-- Init.Data.SInt.Lemmas
Int32.ofIntLE.congr_simp : ∀ (i i_1 : ℤ) (e_i : i = i_1) (_hl : Int32.minValue.toInt ≤ i) (_hr : i ≤ Int32.maxValue.toInt),
  Int32.ofIntLE i _hl _hr = Int32.ofIntLE i_1 ⋯ ⋯
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.commAlgEquiv_C : ∀ {R : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [inst : CommSemiring R] (p : MvPolynomial S₂ R),
  (MvPolynomial.commAlgEquiv R S₁ S₂) (MvPolynomial.C p) = (MvPolynomial.map MvPolynomial.C) p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_7 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (len w start : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match len, Std.Tactic.BVDecide.BVExpr.extract start len expr with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_7 len w start expr
-- Init.Data.BitVec.Lemmas
BitVec.instAssociativeHAdd : ∀ {n : ℕ}, Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Data.Sum.Lattice
Sum.Lex.instLattice : {α : Type u_1} → {β : Type u_2} → [Lattice α] → [Lattice β] → Lattice (α ⊕ₗ β)
-- Mathlib.Algebra.Order.Hom.Monoid
antitone_iff_map_nonpos : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], Antitone ⇑f ↔ ∀ (a : α), 0 ≤ a → f a ≤ 0
-- Mathlib.Analysis.PSeries
/-- for a series of `NNReal` version.  -/
NNReal.summable_schlomilch_iff : ∀ {C : ℕ} {u : ℕ → ℕ} {f : ℕ → NNReal},
  (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      StrictMono u → C ≠ 0 → SuccDiffBounded C u → ((Summable fun k => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Iio_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioo a b ⊆ Finset.Iio b
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- `fromEdgeSet` constructs a `SimpleGraph` from a set of edges, without loops.  -/
SimpleGraph.fromEdgeSet : {V : Type u} → Set (Sym2 V) → SimpleGraph V
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Ioc : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a b : R},
  Int.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_Option : ∀ {α : Type} {epost : Prop} {post : α → Prop} (err : PUnit.{1}), ⦃ epost ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.Data.Rel
SetRel.comm : ∀ {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm], (a, b) ∈ R ↔ (b, a) ∈ R
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : CommSemigroup M],
  Filter.Germ.instCommSemigroup = { toSemigroup := Filter.Germ.instSemigroup, mul_comm := ⋯ }
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabFootnote.mk.inj : ∀ {name name_1 : Lean.StrLit}, { name := name } = { name := name_1 } → name = name_1
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.extend_ι_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [inst_1 : CategoryTheory.IsIso η] (X : P.I)
  (X_1 : Cᵒᵖ) (a : ((P.F.comp CategoryTheory.yoneda).obj X).obj X_1),
  (CategoryTheory.ConcreteCategory.hom (((P.extend η).ι.app X).app X_1)) a =
    (η.app X_1).hom' (((P.cocone.ι.app X).app X_1).hom' a)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_homOfLE : ∀ (X : AlgebraicGeometry.Scheme) {U V W : X.Opens} (e₁ : U ≤ V) (e₂ : V ≤ W),
  CategoryTheory.CategoryStruct.comp (X.homOfLE e₁) (X.homOfLE e₂) = X.homOfLE ⋯
-- Batteries.Data.List.Basic
/-- `swapAt xs i v` sets position `i` of `xs` to `v` and returns the displaced
element, or `v` itself (with `xs` unchanged) if `i` is out of bounds.  -/
List.swapAt : {α : Type u_1} → List α → ℕ → α → α × List α
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasFDerivAt_list_prod_attach' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {l : List ι} {x : { i // i ∈ l } → 𝔸},
  HasFDerivAt (fun x => (List.map x l.attach).prod)
    (∑ i,
      (List.map x (List.take (↑i) l.attach)).prod •
        MulOpposite.op (List.map x (List.drop (↑i).succ l.attach)).prod •
          ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i])
    x
-- Mathlib.Order.Extension.Well
/-- A type alias for `α`, intended to extend a well-founded order on `α` to a well-order.  -/
WellOrderExtension : Type u_1 → Type u_1
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.map_eq_one_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N) {x : M}, h x = 1 ↔ x = 1
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsLittleO.rpow : ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
  0 < r → 0 ≤ᶠ[l] g → f =o[l] g → (fun x => f x ^ r) =o[l] fun x => g x ^ r
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommMonoidWithZero : {M₀ : Type u_1} →
  [inst : TopologicalSpace M₀] →
    [inst_1 : CommMonoidWithZero M₀] → [ContinuousMul M₀] → CommMonoidWithZero (SeparationQuotient M₀)
-- Mathlib.Order.OrderIsoNat
/-- If `f` is a strictly `r`-decreasing sequence, then this returns `f` as an order embedding.  -/
RelEmbedding.natGT : {α : Type u_1} →
  {r : α → α → Prop} →
    [IsStrictOrder α r] → (f : ℕ → α) → (∀ (n : ℕ), r (f (n + 1)) (f n)) → (fun x1 x2 => x1 > x2) ↪r r
-- Init.Data.List.Perm
List.perm_insertIdx : ∀ {α : Type u_1} (x : α) (l : List α) {i : ℕ}, i ≤ l.length → (l.insertIdx i x).Perm (x :: l)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GCommSemiring.toGCommMonoid : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddCommMonoid ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] → [self : DirectSum.GCommSemiring A] → GradedMonoid.GCommMonoid A
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `encodingBoolBool`.  -/
Computability.finEncodingBoolBool : Computability.Encoding Bool Bool
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.norm_kerFun_eq_sqrt_norm_kernel : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x : X),
  ‖RKHS.kerFun H x‖ = √‖RKHS.kernel H x x‖
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.fst : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {M' : Type u_3} [inst_1 : Zero M'] {f : α → M × M'},
  Function.HasFiniteSupport f → Function.HasFiniteSupport fun a => (f a).1
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIicIoi_symm_apply_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} (h : y ≤ x), (OrderIso.sumLexIicIoi x).symm y = toLex (Sum.inl ⟨y, h⟩)
-- Init.Data.Vector.Lemmas
Vector.replicate_one : ∀ {α : Type u_1} {a : α}, Vector.replicate 1 a = #v[a]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.penultimate_cons_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).penultimate = u
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.mk : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α},
  y ∈ ChainCompletePartialOrder.bot x f →
    (∀ {z : α}, z ∈ ChainCompletePartialOrder.bot x f → z < y → f z ≤ y) → ChainCompletePartialOrder.IsExtremePt x f y
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_3.eq_1 : ∀ (motive : Std.HashSet Lean.Syntax.Range → Lean.Syntax → Sort u_1) (curr : Std.HashSet Lean.Syntax.Range)
  (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax)
  (h_1 :
    (curr : Std.HashSet Lean.Syntax.Range) →
      (s : Lean.Syntax) →
        (info : Lean.SourceInfo) →
          (kind : Lean.SyntaxNodeKind) →
            (args : Array Lean.Syntax) →
              s = Lean.Syntax.node info kind args → motive curr (Lean.Syntax.node info kind args))
  (h_2 :
    (curr : Std.HashSet Lean.Syntax.Range) → (info : Lean.SourceInfo) → motive curr (Lean.Syntax.atom info "where"))
  (h_3 : (curr : Std.HashSet Lean.Syntax.Range) → (x : Lean.Syntax) → motive curr x),
  (match curr, Lean.Syntax.node info kind args with
    | curr, s@h:(Lean.Syntax.node info kind args) => h_1 curr s info kind args h
    | curr, Lean.Syntax.atom info "where" => h_2 curr info
    | curr, x => h_3 curr x) =
    h_1 curr (Lean.Syntax.node info kind args) info kind args ⋯
-- Mathlib.Topology.Order.Hom.Esakia
/-- Composition of `EsakiaHom`s as an `EsakiaHom`.  -/
EsakiaHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [inst_1 : Preorder α] →
          [inst_2 : TopologicalSpace β] →
            [inst_3 : Preorder β] →
              [inst_4 : TopologicalSpace γ] → [inst_5 : Preorder γ] → EsakiaHom β γ → EsakiaHom α β → EsakiaHom α γ
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The relations that can be used for rewriting.  -/
Mathlib.Tactic.ClickSuggestions.GrwInfo.gpos : Mathlib.Tactic.ClickSuggestions.GrwInfo → Array Mathlib.Tactic.ClickSuggestions.GrwPos
-- Mathlib.InformationTheory.Hamming
hammingDist_lt_one : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  hammingDist x y < 1 ↔ x = y
-- Mathlib.Analysis.Convex.Segment
Prod.image_mk_openSegment_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (x₁ x₂ : E) (y : F),
  (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The additive kernel of an `AddMonoidHom` is the `AddSubmonoid` of elements such that
`f x = 0`.  -/
AddMonoidHom.mker : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid M
-- Mathlib.Order.Comparable
not_le_iff_lt_or_incompRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], ¬b ≤ a ↔ a < b ∨ IncompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_option : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : Option α → M),
  ∑ i, f i = f none + ∑ i, f (some i)
-- Lean.Meta.Basic
Lean.Meta.recordUnfoldAxiom : Lean.Name → Lean.MetaM Unit