mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X (n + 1) ⟶ X n) (n : ℕ),
  (CategoryTheory.Functor.ofOpSequence f).map (CategoryTheory.homOfLE ⋯).op = f n
-- Init.Data.String.Defs
/-- A `Slice.Pos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
character boundary.
 -/
String.Slice.Pos : String.Slice → Type
-- Mathlib.Logic.Lemmas
iff_left_comm : ∀ {a b c : Prop}, (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.const.inj : ∀ {e : Q(ℕ)} {value value_1 : Mathlib.Tactic.Ring.Common.btℕ e},
  Mathlib.Tactic.Ring.Common.ExProdNat.const value = Mathlib.Tactic.Ring.Common.ExProdNat.const value_1 →
    value = value_1
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) (X X_1 X_2 : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁ F).app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj X_1) (F.obj X_2)).hom
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.notMem_bot : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X}, x ∉ ⊥
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_of_lt_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b c : α},
  b < c → a < 1 → b * a < c
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMap_symm_apply : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₂ e₂]
  (p : B × (F₁ →SL[σ] F₂)),
  ↑(Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂).symm p =
    ⟨p.1, Bundle.Trivialization.symmL 𝕜₂ e₂ p.1 ∘SL p.2 ∘SL Bundle.Trivialization.continuousLinearMapAt 𝕜₁ e₁ p.1⟩
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `x ↦ fderiv 𝕜 (f x) (g x)` is continuous.  -/
Continuous.fderiv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F → G} {g : E → F},
  ContDiff 𝕜 n (Function.uncurry f) → Continuous g → 1 ≤ n → Continuous fun x => fderiv 𝕜 (f x) (g x)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.map_apply : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'},
  MeasurableSet A → (ν.map f_aemble) A = ν (f ⁻¹' A)
-- Mathlib.Data.Finset.Max
Finset.max_mono : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α}, s ⊆ t → s.max ≤ t.max
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.tendsto_card_div_pow₅ : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Fintype ι],
  (fun x =>
      ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ Fintype.card ι *
        (↑⌊x⌋₊ / x) ^ Fintype.card ι) =ᶠ[Filter.atTop]
    fun x => ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.cyclesIso₀ A =
    HomologicalComplex.iCyclesIso (groupHomology.inhomogeneousChains A) 0 0 groupHomology.cyclesIso₀._proof_1 ⋯ ≪≫
      groupHomology.chainsIso₀ A
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨿ Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl)
        (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag (Y ⨿ Y')) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g g') h
-- Mathlib.Order.KrullDimension
Order.height_pos : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, 0 < Order.height x ↔ ¬IsMin x
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple_mul_simple_cancel_left : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (i : B),
  cs.simple i * (cs.simple i * w) = w
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivOfSurj_symm_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (c : RingCon M) {f : N →+* M}
  (hf : Function.Surjective ⇑f) {d : RingCon N} (hcd : d = c.comap f) (x : N),
  (c.comapQuotientEquivOfSurj f hf hcd).symm ↑(f x) = ↑x
-- Mathlib.GroupTheory.Torsion
CommGroup.le_comap_torsion : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] (f : G →* H),
  CommGroup.torsion G ≤ Subgroup.comap f (CommGroup.torsion H)
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.toBEq : {α : Type u} → [self : Std.PreorderPackage α] → BEq α
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), ⊤.inverseImage F = ⊤
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_iUnion_mem_option : ∀ {α : Type u_1} [inst : EDist α] {ι : Type u_3} (o : Option ι) (s : ι → Set α),
  (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instTypeNameElabFootnote : TypeName Lean.Doc.ElabFootnote✝
-- Mathlib.CategoryTheory.Sums.Products
/-- A consequence of `functorEquiv`: we can construct a natural transformation of functors
`A ⊕ A' ⥤ B` from the data of natural transformations of their whiskering with `inl_` and `inr_`.  -/
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            {F G : CategoryTheory.Functor (A ⊕ A') B} →
              ((CategoryTheory.Sum.inl_ A A').comp F ⟶ (CategoryTheory.Sum.inl_ A A').comp G) →
                ((CategoryTheory.Sum.inr_ A A').comp F ⟶ (CategoryTheory.Sum.inr_ A A').comp G) → (F ⟶ G)
-- Std.Data.Iterators.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Combinators.Monadic.Zip.0.Option.SomeLtNone.lt.match_1.eq_3 : ∀ {β : Type u_2} {α : Type u_1} (motive : Option α → Option β → Sort u_3) (x : α) (y : β)
  (h_1 : (x : Option β) → motive none x) (h_2 : (val : α) → motive (some val) none)
  (h_3 : (x : α) → (y : β) → motive (some x) (some y)),
  (match some x, some y with
    | none, x => h_1 x
    | some val, none => h_2 val
    | some x, some y => h_3 x y) =
    h_3 x y
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instMul : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → Mul (TruncatedWittVector p n R)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
map_complEDS : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (b c d : R) (k n : ℤ), f (complEDS b c d k n) = complEDS (f b) (f c) (f d) k n
-- Mathlib.Tactic.TermCongr
/-- Returns a proof of `lhs ↔ rhs`. Uses `CongrResult.eq`.  -/
Mathlib.Tactic.TermCongr.CongrResult.iff : Mathlib.Tactic.TermCongr.CongrResult → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.map_eq_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x y : P}, e x = e y ↔ x = y
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.snd_decompAffineEquiv : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q]
  (f : V →ᴬ[R] Q), ((ContinuousAffineMap.decompAffineEquiv R S V Q) f).2 = f.contLinear
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} (I II : Set A.N) (inter : I ∩ II = ∅) (union : I ∪ II = Set.univ) (p : ↑II ≃ ↑I),
  sizeOf { I := I, II := II, inter := inter, union := union, p := p } = 1 + sizeOf inter + sizeOf union + sizeOf p
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₁_ne_type₂' : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) (s t : self.ι),
  { dim := self.dim s + 1, simplex := self.simplex s } ≠
    { dim := self.dim t,
      simplex :=
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (self.index t))) (self.simplex t) }
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.notMem_of_notMem_closure : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {P : M}, P ∉ Submonoid.closure s → P ∉ s
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.isZero_iff_subsingleton : ∀ {R : Type u} [inst : Semiring R] {M : SemimoduleCat R}, CategoryTheory.Limits.IsZero M ↔ Subsingleton ↑M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, t.size ≤ (Std.DTreeMap.Internal.Impl.insert! k v t).size
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instLinearMapClass : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N], LinearMapClass (M →ₗ⁅R,L⁆ N) R M N
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.equivalence_inverse_map : ∀ {X Y : MonCat} (f : X ⟶ Y),
  AddMonCat.equivalence.inverse.map f = AddMonCat.ofHom (MonoidHom.toAdditive (MonCat.Hom.hom f))
-- Lean.Compiler.ExternAttr
Lean.ExternAttrData.mk.inj : ∀ {entries entries_1 : List Lean.ExternEntry}, { entries := entries } = { entries := entries_1 } → entries = entries_1
-- Mathlib.Algebra.Star.Basic
commute_star_comm : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y : R}, Commute (star x) y ↔ Commute x (star y)
-- Init.Data.BitVec.Lemmas
BitVec.ssubOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w),
  x.ssubOverflow y = (decide (x.toInt - y.toInt ≥ 2 ^ (w - 1)) || decide (x.toInt - y.toInt < -2 ^ (w - 1)))
-- Lean.Util.Trace
Lean.instMonadAlwaysExceptStateT : {m : Type → Type} →
  [Monad m] → {ε σ : Type} → [always : Lean.MonadAlwaysExcept ε m] → Lean.MonadAlwaysExcept ε (StateT σ m)
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
/-- The row permutation on the rows of `A`.  -/
Echelon.Decomposition.σ : {m : Type u_1} →
  [inst : Fintype m] →
    [inst_1 : LinearOrder m] →
      {n : Type u_2} →
        [inst_2 : LinearOrder n] →
          {R : Type u_3} → [inst_3 : CommRing R] → {A : Matrix m n R} → Echelon.Decomposition A → Equiv.Perm m
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {km kmi : α}, t.minKey? = some km → (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h.π h.homologyIso.inv =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.homologyπ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.keys → k ∈ t
-- Mathlib.Algebra.Group.Basic
eq_one_div_of_mul_eq_one_left : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, b * a = 1 → b = 1 / a
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `c` is a colimit cokernel cofork for `f : X ⟶ Y`, and `f' : X' ⟶ Y` is another
morphism, then there is a colimit cokernel cofork for `f'` with the same point as `c` if for any
morphism `φ : Y ⟶ W`, there is an equivalence `f ≫ φ = 0 ↔ f' ≫ φ = 0`.  -/
CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {c : CategoryTheory.Limits.CokernelCofork f} →
            CategoryTheory.Limits.IsColimit c →
              {X' : C} →
                (f' : X' ⟶ Y) →
                  (iff :
                      ∀ ⦃W : C⦄ (φ : Y ⟶ W),
                        CategoryTheory.CategoryStruct.comp f φ = 0 ↔ CategoryTheory.CategoryStruct.comp f' φ = 0) →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯)
-- Init.Data.Array.MapIdx
Array.mapIdx_append : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs ys : Array α},
  Array.mapIdx f (xs ++ ys) = Array.mapIdx f xs ++ Array.mapIdx (fun i => f (i + xs.size)) ys
-- Mathlib.Topology.Constructions
continuous_quot_map : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {r : X → X → Prop}
  {r' : Y → Y → Prop} {f : X → Y} (hr : ∀ (a b : X), r a b → r' (f a) (f b)), Continuous f → Continuous (Quot.map f hr)
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context.mk.sizeOf_spec : ∀ (exceptionSet : Lean.ExprSet) (kind : Lean.Meta.SplitKind),
  sizeOf { exceptionSet := exceptionSet, kind := kind } = 1 + sizeOf exceptionSet + sizeOf kind
-- Init.Data.List.MinMaxOn
List.foldl.eq_def : ∀ {α : Type u} {β : Type v} (f : α → β → α) (x : α) (x_1 : List β),
  List.foldl f x x_1 =
    match x, x_1 with
    | a, [] => a
    | a, b :: l => List.foldl f (f a b) l
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsNonneg.add : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {I₁ I₂ : R →+* R} [inst_3 : Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₛₗ[I₂] R},
  B.IsNonneg → C.IsNonneg → (B + C).IsNonneg
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.size =
    if Std.DTreeMap.Internal.Impl.contains k t = true then t.size else t.size + 1
-- Mathlib.Data.List.PeriodicityLemma
List.HasPeriod.getElem?_mod : ∀ {α : Type u_1} (p i : ℕ) (w : List α), w.HasPeriod p → i < w.length → w[i % p]? = w[i]?
-- Mathlib.Analysis.Complex.Exponential
Real.exp_bound_div_one_sub_of_interval' : ∀ {x : ℝ}, 0 < x → x < 1 → Real.exp x < 1 / (1 - x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getEntryGT? k = Std.DTreeMap.Internal.Impl.getEntryGT?.go k none
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.of_le : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {m n : WithTop ℕ∞},
  ContMDiff I I' n f → m ≤ n → ContMDiff I I' m f
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.run : {α : Type} →
  Aesop.EqualUpToIdsM α → Option Lean.MetavarContext → Lean.MetavarContext → Lean.MetavarContext → Bool → Lean.MetaM α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.length_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_sub : ∀ {V W : SemiNormedGrp} (f g : V ⟶ W), SemiNormedGrp.Hom.hom (f - g) = SemiNormedGrp.Hom.hom f - SemiNormedGrp.Hom.hom g
-- Lean.Meta.Constructions.CtorIdx
Lean.isCtorIdx? : Lean.Name → Lean.MetaM (Option Lean.InductiveVal)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.to_from : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const), GenLoop.toLoop i (GenLoop.fromLoop i p) = p
-- ProofWidgets.Component.FilterDetails
ProofWidgets.FilterDetailsProps.mk.injEq : ∀ (summary filtered all : ProofWidgets.Html) (initiallyFiltered : Bool) (summary_1 filtered_1 all_1 : ProofWidgets.Html)
  (initiallyFiltered_1 : Bool),
  ({ summary := summary, filtered := filtered, all := all, initiallyFiltered := initiallyFiltered } =
      { summary := summary_1, filtered := filtered_1, all := all_1, initiallyFiltered := initiallyFiltered_1 }) =
    (summary = summary_1 ∧ filtered = filtered_1 ∧ all = all_1 ∧ initiallyFiltered = initiallyFiltered_1)
-- Aesop.Search.SearchM
Aesop.SearchM.Context.mk.sizeOf_spec : ∀ (ruleSet : Aesop.LocalRuleSet) (normSimpContext : Aesop.NormSimpContext) (options : Aesop.Options'),
  sizeOf { ruleSet := ruleSet, normSimpContext := normSimpContext, options := options } =
    1 + sizeOf ruleSet + sizeOf normSimpContext + sizeOf options
-- Batteries.Data.List.Matcher
List.Matcher.mk.inj : ∀ {α : Type u_1} {toMatcher : Array.Matcher α} {pattern : List α} {toMatcher_1 : Array.Matcher α} {pattern_1 : List α},
  { toMatcher := toMatcher, pattern := pattern } = { toMatcher := toMatcher_1, pattern := pattern_1 } →
    toMatcher = toMatcher_1 ∧ pattern = pattern_1
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_smul_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  {c : NNReal} (hc : c ≠ 0), (c • μ').haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
-- Mathlib.Order.InitialSeg
PrincipalSeg.strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] (f : α <i β),
  StrictMono ⇑f.toRelEmbedding
-- Lean.Data.KVMap
Lean.instCoeNameDataValue : Coe Lean.Name Lean.DataValue
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.natCast_lt_natCast_of_lt : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a b : ℕ), a < b → ↑a < ↑b
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearMap.rank_le_of_surjective : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M →ₗ[R] M₁),
  Function.Surjective ⇑f → Module.rank R M₁ ≤ Module.rank R M
-- Mathlib.Probability.Martingale.Basic
/-- A predictable martingale is a.e. equal to its initial state.  -/
MeasureTheory.Martingale.eq_zero_of_predictable' : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Martingale f 𝒢 μ → MeasureTheory.IsStronglyPredictable 𝒢 f → ∀ (n : ℕ), f n =ᵐ[μ] f 0
-- Init.Data.String.Basic
String.Slice.Pos.get_eq_get_copy : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos}, pos.get h = pos.copy.get ⋯
-- Init.SizeOf
UInt32.ofBitVec.sizeOf_spec : ∀ (toBitVec : BitVec 32), sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
-- Lean.Meta.Constructions.NoConfusion
/-- Telescoping `mkEqNDRec`: given
* motive `∀ y1 .. yn, P y1 .. yn`
* expression of type `P x1 .. xn`
* produces an expression of type (x1 = y1) → .. → (xn = yn) → P y1 .. yn
  (possibly using `HEq`)
produce an expression of type `motive y1 … yn`
by repeatedly applying `Eq.ndRec` (and `eq_of_heq` if needed).
 -/
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkEqNDRecTelescope : Lean.Expr → Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_union_self : ∀ {α : Type u_1} (s : Set α), sᶜ ∪ s = Set.univ
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If you add multiples of previous rows to the next row, the determinant doesn't change.  -/
Matrix.det_eq_of_forall_row_eq_smul_add_pred : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R} (c : Fin n → R),
  (∀ (j : Fin (n + 1)), A 0 j = B 0 j) →
    (∀ (i : Fin n) (j : Fin (n + 1)), A i.succ j = B i.succ j + c i * A i.castSucc j) → A.det = B.det
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- `WithLp.equiv` as a group isomorphism.  -/
WithLp.addEquiv : (p : ENNReal) → (V : Type u_4) → [inst : AddCommGroup V] → WithLp p V ≃+ V