mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr₂.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (motive : List α → List β → γ → Sort u_3) (x : List α) (c : γ)
  (h_1 : (x : List β) → (c : γ) → motive [] x c) (h_2 : (x : List α) → (c : γ) → motive x [] c)
  (h_3 : (x : α) → (xr : List α) → (y : β) → (yr : List β) → (c : γ) → motive (x :: xr) (y :: yr) c),
  (x = [] → False) →
    (match x, [], c with
      | [], x, c => h_1 x c
      | x, [], c => h_2 x c
      | x :: xr, y :: yr, c => h_3 x xr y yr c) =
      h_2 x c
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Adjunction.strongEpi_map_of_strongEpi : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor D C}
  {A B : C} (adj : F ⊣ F') (f : A ⟶ B) [F'.PreservesMonomorphisms] [F.PreservesEpimorphisms]
  [CategoryTheory.StrongEpi f], CategoryTheory.StrongEpi (F.map f)
-- Mathlib.Data.DFinsupp.Defs
/-- `DFinsupp.single a b` is injective in `a`. For the statement that it is injective in `b`, see
`DFinsupp.single_injective`  -/
DFinsupp.single_left_injective : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {b : (i : ι) → β i},
  (∀ (i : ι), b i ≠ 0) → Function.Injective fun i => fun₀ | i => b i
-- Init.Data.SInt.Basic
Int64.instOfNat : {n : ℕ} → OfNat Int64 n
-- ProofWidgets.Presentation.Expr
ProofWidgets.evalExprPresenter : Lean.Environment → Lean.Options → Lean.Name → Except String ProofWidgets.ExprPresenter
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₂ → Std.DTreeMap.Raw.Const.getD (m₁ ∩ m₂) k fallback = fallback
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_sdiv_inter_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s₁ s₂ t₁ t₂ : Set β}, s₁ ∪ s₂ /ₛ t₁ ∩ t₂ ⊆ s₁ /ₛ t₁ ∪ (s₂ /ₛ t₂)
-- Mathlib.SetTheory.Cardinal.Regular
/-- A countable supremum of countable ordinals is countable.  -/
Ordinal.iSup_lt_omega_one : ∀ {α : Type u_1} [Countable α] {f : α → Ordinal.{u_2}}, (∀ (i : α), f i < Ordinal.omega 1) → ⨆ i, f i < Ordinal.omega 1
-- Mathlib.Order.Fin.Basic
Fin.bot_eq_zero : ∀ (n : ℕ) [inst : NeZero n], ⊥ = 0
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_nsmul : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → AddMonoid (G i)] [inst_7 : AddMonoid C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f)
  (n : ℕ), DirectLimit.lift f (fun x => ⇑(g x)) h (n • x) = n • DirectLimit.lift f (fun x => ⇑(g x)) h x
-- Mathlib.Order.RelIso.Basic
RelIso.apply_eq_iff_eq_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {x : α} {y : β} (f : r ≃r s),
  f x = y ↔ x = f.symm y
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.one : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R], Matrix.PosDef 1
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.pi_norm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] (x : WithCStarModule A ((i : ι) → E i)),
  ‖x‖ = √‖∑ i, inner A (x i) (x i)‖
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.existsUnique : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F),
  ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) l = t.ι.app j
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- On a set with unique derivatives, a `C^n` function has derivatives less than `n` which are
differentiable.  -/
ContDiffOn.differentiableOn_iteratedDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : WithTop ℕ∞} {m : ℕ},
  ContDiffOn 𝕜 n f s → ↑m < n → UniqueDiffOn 𝕜 s → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
-- Mathlib.Geometry.Manifold.SmoothEmbedding
Manifold.IsSmoothEmbedding.of_opens : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] {H : Type u_6} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
  (s : TopologicalSpace.Opens M), Manifold.IsSmoothEmbedding I I n Subtype.val
-- Init.Data.Array.Lemmas
Array.filter_replicate : ∀ {stop n : ℕ} {α : Type u_1} {a : α} {p : α → Bool},
  stop = n → Array.filter p (Array.replicate n a) 0 stop = if p a = true then Array.replicate n a else #[]
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackFst_apply : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z)
  (x : ↑(TopCat.of { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 })),
  (CategoryTheory.ConcreteCategory.hom (TopCat.pullbackFst f g)) x = (↑x).1
-- Mathlib.Order.SupClosed
SupClosed.sSup_mem : ∀ {α : Type u_3} [inst : CompleteLattice α] {s t : Set α}, SupClosed s → t.Finite → ⊥ ∈ s → t ⊆ s → sSup t ∈ s
-- Init.Data.Array.Lemmas
Array.getElem?_extract : ∀ {α : Type u_1} {i : ℕ} {xs : Array α} {start stop : ℕ},
  (xs.extract start stop)[i]? = if i < min stop xs.size - start then xs[start + i]? else none
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- `g ∘ f` is `C^n` within `s` at `x` if `g` is `C^n` at `f x` and
`f` is `C^n` within `s` at `x`.  -/
ContMDiffAt.comp_contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {g : M' → M''} (x : M),
  ContMDiffAt I' I'' n g (f x) → ContMDiffWithinAt I I' n f s x → ContMDiffWithinAt I I'' n (g ∘ f) s x
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_mul_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (a b : R),
  (MvPowerSeries.monomial m) a * (MvPowerSeries.monomial n) b = (MvPowerSeries.monomial (m + n)) (a * b)
-- Mathlib.RingTheory.Finiteness.Subalgebra
Submodule.FG.pow : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {M : Submodule R A}, M.FG → ∀ (n : ℕ), (M ^ n).FG
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.Homotopy.smul_h₁ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R), (h.smul a).h₁ = a • h.h₁
-- Mathlib.Algebra.Order.Hom.Ring
/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `RingEquivClass F α β`
into an actual `OrderRingIso`.
This is declared as the default coercion from `F` to `α ≃+*o β`.  -/
OrderRingIsoClass.toOrderRingIso : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : EquivLike F α β] →
        [inst_1 : Mul α] →
          [inst_2 : Add α] →
            [inst_3 : LE α] →
              [inst_4 : Mul β] →
                [inst_5 : Add β] → [inst_6 : LE β] → [OrderIsoClass F α β] → [RingEquivClass F α β] → F → α ≃+*o β
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.instPreservesLimitsOfShapeFunctorColim : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] {D : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} D] [CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) → HasStrictFDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_reverse`. -/
List.SortedLE.of_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedLE → l.SortedGE
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = none ↔ k ∉ t
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Adjunction.mapGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal],
  a.mapGrp =
    {
      unit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapGrpIdIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapGrpNatTrans a.unit)
            CategoryTheory.Functor.mapGrpCompIso.hom),
      counit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapGrpCompIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapGrpNatTrans a.counit)
            CategoryTheory.Functor.mapGrpIdIso.hom),
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  (m.insertIfNew k v)[a]? = if (k == a) = true ∧ k ∉ m then some v else m[a]?
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompAssociator_hom_app_down_down : ∀ (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] (X : E),
  ((CategoryTheory.sum.inrCompAssociator C D E).hom.app X).down.down = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Polynomial.Sequence
Polynomial.Sequence.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : SizeOf R] (elems' : ℕ → Polynomial R)
  (degree_eq' : ∀ (i : ℕ), (elems' i).degree = ↑i), sizeOf { elems' := elems', degree_eq' := degree_eq' } = 1
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
_private.Mathlib.Analysis.Calculus.FormalMultilinearSeries.0.FormalMultilinearSeries.removeZero.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Functor.Const
/-- The canonical isomorphism
`const D ⋙ (whiskeringLeft J _ _).obj F ≅ const J`  -/
CategoryTheory.Functor.constCompWhiskeringLeftIso : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D] →
            (F : CategoryTheory.Functor J D) →
              (CategoryTheory.Functor.const D).comp ((CategoryTheory.Functor.whiskeringLeft J D C).obj F) ≅
                CategoryTheory.Functor.const J
-- Mathlib.RepresentationTheory.Irreducible
Representation.isSimpleModule_iff_irreducible_ofModule : ∀ {G : Type u_1} {k : Type u_2} [inst : Monoid G] [inst_1 : Field k] (M : Type u_5) [inst_2 : AddCommGroup M]
  [inst_3 : Module (MonoidAlgebra k G) M],
  IsSimpleModule (MonoidAlgebra k G) M ↔ (Representation.ofModule M).IsIrreducible
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product induces the norm.  -/
InnerProductSpace.norm_sq_eq_re_inner : ∀ {𝕜 : Type u_4} {E : Type u_5} {inst : RCLike 𝕜} {inst_1 : SeminormedAddCommGroup E} [self : InnerProductSpace 𝕜 E]
  (x : E), ‖x‖ ^ 2 = RCLike.re (inner 𝕜 x x)
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The `AddCon` generated by a relation respecting scalar multiplication is a `ModuleCon`.  -/
SMulCon.addConGen' : {S : Type u_2} →
  {M : Type u_3} →
    [inst : AddZeroClass M] →
      [inst_1 : DistribSMul S M] →
        (r : M → M → Prop) → (∀ (s : S) {m m' : M}, r m m' → r (s • m) (s • m')) → ModuleCon S M
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_indicator_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Zero β] {s : Set α},
  MeasurableSet s →
    (MeasureTheory.AEStronglyMeasurable (s.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
-- Mathlib.Analysis.Convex.Strong
strongConcaveOn_iff_convex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {s : Set E} {m : ℝ} {f : E → ℝ},
  StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x => f x + m / 2 * ‖x‖ ^ 2
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Countable unions of σ-compact sets are σ-compact.  -/
isSigmaCompact_iUnion : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [Countable ι] (s : ι → Set X),
  (∀ (i : ι), IsSigmaCompact (s i)) → IsSigmaCompact (⋃ i, s i)
-- Mathlib.Algebra.Group.Commute.Units
Units.pow_ofPowEqOne : ∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {a : M} (ha : a ^ n = 1) (hn : n ≠ 0), Units.ofPowEqOne a n ha hn ^ n = 1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.Iso.inv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ≅ Y), CategoryTheory.inv f.inv = f.hom
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instNoMaxOrder : NoMaxOrder Cardinal.{u}
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.prod_norm_le_norm_add : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  (x : WithCStarModule A (E × F)), ‖x‖ ≤ ‖x.1‖ + ‖x.2‖
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_iff : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {x y : M}, IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  G.neighborFinset v = (G.neighborSet v).toFinset
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.X_sub_C_dvd_nodal : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} (v : ι → R) {i : ι},
  i ∈ s → Polynomial.X - Polynomial.C (v i) ∣ Lagrange.nodal s v
-- Mathlib.Topology.Order.LowerUpperTopology
/-- Every set open in the lower topology is a lower set.  -/
Topology.IsLower.isLowerSet_of_isOpen : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {s : Set α},
  IsOpen s → IsLowerSet s
-- Mathlib.Algebra.Homology.SpectralObject.Homology
/-- The short complex `E^{n-1}(f₅, f₆, f₇) ⟶ E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃)`
given by the differentials of a spectral object.  -/
CategoryTheory.Abelian.SpectralObject.dShortComplex : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} →
              (i₀ ⟶ i₁) →
                (i₁ ⟶ i₂) →
                  (i₂ ⟶ i₃) →
                    (i₃ ⟶ i₄) →
                      (i₄ ⟶ i₅) →
                        (i₅ ⟶ i₆) →
                          (i₆ ⟶ i₇) →
                            (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1 →
                                autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3 →
                                  autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5 →
                                    autoParam (n₃ + 1 = n₄)
                                        CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7 →
                                      CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F]
  (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a))
      (CategoryTheory.CategoryStruct.comp ((L.rightKanExtensionCounit (F.comp G)).app a) h) =
    CategoryTheory.CategoryStruct.comp (G.map ((L.rightKanExtensionCounit F).app a)) h
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.homMk.congr_simp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X}
  (f f_1 : U.right ⟶ V.right) (e_f : f = f_1) (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom),
  CategoryTheory.Under.homMk f w = CategoryTheory.Under.homMk f_1 ⋯
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.add_eq_max_of_ne : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p}, f.norm ≠ g.norm → (f + g).norm = max f.norm g.norm
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipToSpace : Lean.Parser.ParserFn
-- Init.Data.Array.Basic
List.getElem_toArray : ∀ {α : Type u} {xs : List α} {i : ℕ} (h : i < xs.toArray.size), xs.toArray[i] = xs[i]
-- Mathlib.Data.List.Basic
List.instDecidablePredForall : {α : Type u} → (p : α → Prop) → [DecidablePred p] → DecidablePred (List.Forall p)
-- Mathlib.CategoryTheory.Filtered.Small
/-- Implementation detail for the instance
`EssentiallySmall.{max v w} (FullSubcategory (cofilteredClosure f))`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofilteredOrEmpty C] → {α : Type w} → (α → C) → ℕ → (t : Type (max v w)) × (t → C)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurable_singularPart_fun_right : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α),
  Measurable fun x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.Retract.injectiveDimension_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (h : CategoryTheory.Retract X Y), CategoryTheory.injectiveDimension X ≤ CategoryTheory.injectiveDimension Y
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.new : {α : Type} → (capacity : ℕ) → 0 < capacity → BaseIO (Std.CloseableChannel.Bounded✝ α)
-- Mathlib.Data.Num.ZNum
Num.dvd_iff_mod_eq_zero : ∀ {m n : Num}, m ∣ n ↔ n % m = 0
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.invalid : ByteArray.utf8DecodeChar?.FirstByte
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mul_injective_of_disjoint : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G}, Disjoint H₁ H₂ → Function.Injective fun g => ↑g.1 * ↑g.2
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.equiv.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f f_1 : M₁ →ₗ[R] M₂ →ₗ[R] M} (e_f : f = f_1) (h : IsTensorProduct f), h.equiv = ⋯.equiv
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rco_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m...n).toList[i]! = 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ofHom_apply : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y] (f : X →+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (AddCommMonCat.ofHom f)) x = f x