mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_smul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {γ : Type u_3} [inst_5 : SMul γ β]
  [inst_6 : IsScalarTower γ β β] (c : γ) (f : CauSeq β abv), c • CauSeq.Completion.mk f = CauSeq.Completion.mk (c • f)
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_deleteEdges : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β),
  (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α}, -s = ∅ ↔ s = ∅
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- **Slutsky's theorem**: if `X n` converges in distribution to `Z`, and `Y n` converges in
probability to a constant `c`, then the pair `(X n, Y n)` converges in distribution to `(Z, c)`.  -/
MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'}
  {μ' : MeasureTheory.Measure Ω'} [inst : MeasureTheory.IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''}
  {μ'' : MeasureTheory.Measure Ω''} [inst_1 : MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E}
  {l : Filter ι} [inst_2 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_4 : BorelSpace E] {E' : Type u_6}
  {mE' : MeasurableSpace E'} [inst_5 : SeminormedAddCommGroup E'] [inst_6 : SecondCountableTopology E']
  [inst_7 : BorelSpace E'] [l.IsCountablyGenerated] (X : ι → Ω'' → E) (Y : ι → Ω'' → E') (Z : Ω' → E) {c : E'},
  MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ' →
    (MeasureTheory.TendstoInMeasure μ'' Y l fun x => c) →
      (∀ (i : ι), AEMeasurable (Y i) μ'') →
        MeasureTheory.TendstoInDistribution (fun n ω => (X n ω, Y n ω)) l (fun ω => (Z ω, c)) (fun x => μ'') μ'
-- Mathlib.Data.Set.Function
Set.BijOn.extendDomain : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g : Equiv.Perm α}
  {s t : Set α}, Set.BijOn (⇑g) s t → Set.BijOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommGroup β] [inst_1 : AddCommGroup γ]
  (a : FreeAbelianGroup α) (f : α → β) (g : β →+ γ),
  (FreeAbelianGroup.lift (⇑g ∘ f)) a = g ((FreeAbelianGroup.lift f) a)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The inverse functor of `ofCostructuredArrowProjEquivalence.functor`.  -/
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse : {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) →
              CategoryTheory.Functor (CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y)
                (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X)
-- Mathlib.Topology.Instances.TrivSqZeroExt
/-- `TrivSqZeroExt.inl` as a continuous linear map.  -/
TrivSqZeroExt.inlCLM : (R : Type u_3) →
  (M : Type u_4) →
    [inst : TopologicalSpace R] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : CommSemiring R] → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → R →L[R] TrivSqZeroExt R M
-- Init.Core
DoResultSBC.pureReturn.injEq : ∀ {α σ : Type u} (a : α) (a_1 : σ) (a_2 : α) (a_3 : σ),
  (DoResultSBC.pureReturn a a_1 = DoResultSBC.pureReturn a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.Zoomed.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.Path.root)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) → (x : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent x r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (x : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l x parent)),
  (match RBTree.RBNode.Path.root with
    | RBTree.RBNode.Path.root => h_1 ()
    | RBTree.RBNode.Path.left c parent x r => h_2 c parent x r
    | RBTree.RBNode.Path.right c l x parent => h_3 c l x parent) =
    h_1 ()
-- Batteries.Data.DList.Lemmas
Batteries.DList.mk.congr_simp : ∀ {α : Type u} (apply apply_1 : List α → List α) (e_apply : apply = apply_1)
  (invariant : ∀ (l : List α), apply l = apply [] ++ l),
  { apply := apply, invariant := invariant } = { apply := apply_1, invariant := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.toEuclideanCLM.eq_1 : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  Matrix.toEuclideanCLM =
    (LinearMap.toMatrixOrthonormal (EuclideanSpace.basisFun n 𝕜)).symm.trans
      (let __src := LinearMap.toContinuousLinearMap;
      { toFun := (↑__src).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
        map_star' := ⋯, map_smul' := ⋯ })
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddMonoid M],
  AddMonoidAlgebra.mapDomainRingHom R (AddMonoidHom.id M) = RingHom.id (AddMonoidAlgebra R M)
-- Mathlib.Data.Fin.SuccPred
Fin.pred_one' : ∀ {n : ℕ} [inst : NeZero n] (h : optParam (1 ≠ 0) ⋯), Fin.pred 1 h = 0
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_symm_apply : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (x : ↑S × ↑T),
  hST.equiv.symm x = ↑x.1 * ↑x.2
-- Mathlib.Data.Stream.Defs
/-- Given functions `f : α → β` and `g : α → α`, `corec f g` creates a stream by:
1. Starting with an initial value `a : α`
2. Applying `g` repeatedly to get a stream of α values
3. Applying `f` to each value to convert them to β
 -/
Stream'.corec : {α : Type u} → {β : Type v} → (α → β) → (α → α) → α → Stream' β
-- Mathlib.Order.Filter.Germ.Basic
/-- Germ of the constant function `fun x : α ↦ c` at a filter `l`.  -/
Filter.Germ.const : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → β → l.Germ β
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_inf_comap_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S],
  Function.Surjective ⇑f → ∀ (I J : Ideal S), Ideal.map f (Ideal.comap f I ⊓ Ideal.comap f J) = I ⊓ J
-- Mathlib.Data.Nat.Digits.Defs
/-- The digits in the base b expansion of n are all less than b, if b ≥ 2  -/
Nat.digits_lt_base : ∀ {b m d : ℕ}, 1 < b → d ∈ b.digits m → d < b
-- Init.Data.SInt.Lemmas
Int16.lt_or_lt_of_ne : ∀ {a b : Int16}, a ≠ b → a < b ∨ b < a
-- Mathlib.Data.List.Prime
perm_of_prod_eq_prod : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] [Subsingleton Mˣ] {l₁ l₂ : List M},
  l₁.prod = l₂.prod → (∀ p ∈ l₁, Prime p) → (∀ p ∈ l₂, Prime p) → l₁.Perm l₂
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The counit isomorphism of the equivalence `equivalence₂` between `A` and `B`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso : {A : Type u_1} →
  {A' : Type u_2} →
    {B : Type u_3} →
      {B' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] →
                {eA : A ≌ A'} →
                  (eB : B ≌ B') →
                    {e' : A' ≌ B'} →
                      {F : CategoryTheory.Functor A B'} →
                        (eA.functor.comp e'.functor ≅ F) →
                          ((eB.functor.comp (e'.inverse.comp eA.inverse)).comp (F.comp eB.inverse) ≅
                            CategoryTheory.Functor.id B)
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_eq_natCast : ∀ {r : ℝ} {n : ℕ}, n ≠ 0 → (ENNReal.ofReal r = ↑n ↔ r = ↑n)
-- Mathlib.Order.CompleteLattice.Defs
iInf_le_iff_forall_lt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLinearOrder α] {l : α} {f : ι → α},
  iInf f ≤ l ↔ ∀ (b : α), l < b → ∃ i, f i < b
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.coe_negOrderIso_symm_apply : ∀ {G : Type u_2} [inst : AddGroup G] (a : AddSubmonoid G), ↑((RelIso.symm AddSubmonoid.negOrderIso) a) = -↑a
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- An equivalence of groups, from the center of the special linear group to the roots of unity.  -/
Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          n → ↥(Subgroup.center (Matrix.SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)
-- Mathlib.Logic.Equiv.Defs
Equiv.exists_congr_right : ∀ {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β), (∃ a, q (e a)) ↔ ∃ b, q b
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValue?.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : List ((_ : α) × β) → Sort u_3) →
      (x : List ((_ : α) × β)) →
        (Unit → motive []) → ((k : α) → (v : β) → (l : List ((_ : α) × β)) → motive (⟨k, v⟩ :: l)) → motive x
-- Init.Data.Option.Basic
/-- Lifts an ordering relation to `Option` such that `none` is the *greatest* element.

It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
and `β`.

Caution: Given `LE α`, `Option.SomeLtNone.le LE.le` differs from the `LE (Option α)` instance,
which is implemented by `Option.le LE.le`.

Examples:
 * `Option.le (fun n k : Nat => n < k) none none = True`
 * `Option.le (fun n k : Nat => n < k) none (some 3) = False`
 * `Option.le (fun n k : Nat => n < k) (some 3) none = True`
 * `Option.le (fun n k : Nat => n < k) (some 4) (some 5) = True`
 * `Option.le (fun n k : Nat => n < k) (some 5) (some 4) = False`
 * `Option.le (fun n k : Nat => n < k) (some 4) (some 4) = True`
 -/
Option.SomeLtNone.le : {β : Type u_1} → {α : Type u_2} → (α → β → Prop) → Option α → Option β → Prop
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Set.EqOn.iteratedDeriv_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {s : Set 𝕜} {f g : 𝕜 → F},
  Set.EqOn f g s → IsOpen s → ∀ (n : ℕ), Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- In a preprimitive action, stabilizers are maximal subgroups  -/
MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive : ∀ (G : Type u_3) [inst : Group G] {X : Type u_4} [inst_1 : MulAction G X] [Nontrivial X] [MulAction.IsPreprimitive G X]
  (a : X), IsCoatom (MulAction.stabilizer G a)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.mk.inj : ∀ {V : Type u_1} {G : SimpleGraph V} {E : Type u_3} {inst : MetricSpace E} {p : V ↪ E}
  {unit_dist : ∀ {u v : V}, G.Adj u v → dist (p u) (p v) = 1} {p_1 : V ↪ E}
  {unit_dist_1 : ∀ {u v : V}, G.Adj u v → dist (p_1 u) (p_1 v) = 1},
  { p := p, unit_dist := unit_dist } = { p := p_1, unit_dist := unit_dist_1 } → p = p_1
-- Mathlib.Algebra.Group.Defs
isCancelMul_iff_forall_isRegular : ∀ {R : Type u_2} [inst : Mul R], IsCancelMul R ↔ ∀ (r : R), IsRegular r
-- Mathlib.Algebra.GroupWithZero.Defs
SemigroupWithZero.toZero : {S₀ : Type u} → [self : SemigroupWithZero S₀] → Zero S₀
-- Init.Data.String.Subslice
String.Slice.Subslice.ext_iff : ∀ {s : String.Slice} {x y : s.Subslice}, x = y ↔ x.startInclusive = y.startInclusive ∧ x.endExclusive = y.endExclusive
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Hom.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.OplaxTrans.Hom η θ}, x = y ↔ x.as = y.as
-- Init.Data.List.Basic
List.intersperseTR.eq_1 : ∀ {α : Type u} (sep : α), List.intersperseTR sep [] = []
-- Lean.Expr
Lean.Nat.mkInstHSub : Lean.Expr
-- Mathlib.Tactic.FunProp.Theorems
/-- Environment extension storing lambda theorems.  -/
Mathlib.Meta.FunProp.LambdaTheoremsExt : Type
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithTop.map` for `ZeroHom`s  -/
ZeroHom.withTopMap : {M : Type u_1} → {N : Type u_2} → [inst : Zero M] → [inst_1 : Zero N] → ZeroHom M N → ZeroHom (WithTop M) (WithTop N)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_mul_basis_toMatrix : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} {n' : Type u_13} {m' : Type u_14}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : Fintype n'] [inst_10 : Fintype m']
  [inst_11 : DecidableEq n'] [inst_12 : DecidableEq m'] (c₁ : Module.Basis n' R M₁) (c₂ : Module.Basis m' R M₂)
  (B : M₁ →ₗ[R] M₂ →ₗ[R] R),
  (b₁.toMatrix ⇑c₁).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (LinearMap.toMatrix₂ c₁ c₂) B
-- Mathlib.Data.FunLike.Group
FunLike.addGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : Neg F] [inst_5 : Sub F] [inst_6 : SMul ℤ F] [inst_7 : AddGroup β]
  [inst_8 : IsZeroApply F α β] [inst_9 : IsAddApply F α β] [inst_10 : IsNegApply F α β] [inst_11 : IsSubApply F α β]
  [inst_12 : IsSMulApply ℕ F α β] [inst_13 : IsSMulApply ℤ F α β],
  FunLike.addGroup = Function.Injective.addGroup (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.sum_indicator_eq_sum_inter : ∀ {ι : Type u_1} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → β),
  ∑ i ∈ s, (↑t).indicator f i = ∑ i ∈ s ∩ t, f i
-- Init.Data.SInt.Lemmas
Int64.zero_lt_one : 0 < 1
-- Init.Data.Vector.Algebra
/-- The zero vector.  -/
Vector.zero : {α : Type u_1} → {n : ℕ} → [Zero α] → Vector α n
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.smul_apply : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] [inst_2 : Module R A]
  (c : CharacterModule A) (r : R) (a : A), (r • c) a = c (r • a)
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app._auto_1) {Z : Cᵒᵖᵒᵖ}
  (h : (CategoryTheory.opOp C).obj ((CategoryTheory.shiftFunctor C n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso C n).inv.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op h)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keyAtIdx?_eq_getElem? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced → ∀ {i : ℕ}, t.keyAtIdx? i = Option.map (fun x => x.fst) t.toListModel[i]?
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instInhabited : {α : Type u} → [inst : Group α] → Inhabited (GroupTopology α)
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasSum.hasSum_at_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (a : ℕ → E), HasSum (fun n => 0 ^ n • a n) (a 0)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- A `ℝ`-basis of the mixed space that is also a `ℤ`-basis of the image of `𝓞 K`.  -/
NumberField.mixedEmbedding.latticeBasis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℝ
        (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.RingTheory.Jacobson.Ring
/-- Used to bootstrap the proof of `isJacobsonRing_polynomial_iff_isJacobsonRing`.
That theorem is more general and should be used instead of this one.  -/
_private.Mathlib.RingTheory.Jacobson.Ring.0.Polynomial.isJacobsonRing_polynomial_of_domain : ∀ (R : Type u_5) [inst : CommRing R] [IsDomain R] [hR : IsJacobsonRing R] (P : Ideal (Polynomial R)) [P.IsPrime],
  (∀ (x : R), Polynomial.C x ∈ P → x = 0) → P.jacobson = P
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.laxMonoidalPi' : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            [inst_3 : CategoryTheory.MonoidalCategory D] →
              (F : (i : I) → CategoryTheory.Functor D (C i)) →
                [(i : I) → (F i).LaxMonoidal] → (CategoryTheory.Functor.pi' F).LaxMonoidal
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.continuousAt_arg_coe_angle : ∀ {x : ℂ}, x ≠ 0 → ContinuousAt (Real.Angle.coe ∘ Complex.arg) x
-- Mathlib.Topology.Sequences
/-- A sequentially continuous function defined on a sequential space is continuous.  -/
SeqContinuous.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SequentialSpace X]
  {f : X → Y}, SeqContinuous f → Continuous f
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
MeasureTheory.limsup_ae_eq_of_forall_ae_eq : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} (s : ℕ → Set α) {t : Set α}, (∀ (n : ℕ), s n =ᵐ[μ] t) → Filter.limsup s Filter.atTop =ᵐ[μ] t
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_cons_cons_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {n : ℕ} (a : K) (x : Fin n → K),
  Height.mulHeight (Matrix.vecCons a (Matrix.vecCons 0 x)) = Height.mulHeight (Matrix.vecCons a x)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
SimpleGraph.IsExtremal.prop : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {p : SimpleGraph V → Prop},
  G.IsExtremal p → p G
-- Mathlib.Algebra.Star.StarAlgHom
DistribMulActionSemiHomClass.toDistribMulActionHom.congr_simp : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B] {F : Type u_10}
  [inst_6 : FunLike F A B] [inst_7 : DistribMulActionSemiHomClass F (⇑φ) A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.pu8 : Std.Internal.Parsec.ByteArray.Parser UInt8
-- Init.Data.Array.Sort.Lemmas
Array.mergeSort_eq_toArray_mergeSort_toList : ∀ {α : Type u_1} {xs : Array α} {le : α → α → Bool}, xs.mergeSort le = (xs.toList.mergeSort le).toArray
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `add_left_cancel`. -/
add_left_cancel'' : ∀ {G : Type u_1} [inst : Add G] [IsLeftCancelAdd G] {a b c : G}, a + b = a + c → b = c
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.weight_sum : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : DecidableEq σ] [inst_2 : Fintype σ] (k : ℕ),
  ∑ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k, MvPolynomial.NewtonIdentities.weight✝ σ R k t = 0
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_zero_of_column_eq_zero : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A : Matrix n n R}
  (j : n), (∀ (i : n), A i j = 0) → A.det = 0
-- Mathlib.Probability.Martingale.Convergence
/-- If a stochastic process has a finite number of upcrossings from below `a` to above `b`,
then it does not frequently visit both below `a` and above `b`.  -/
MeasureTheory.not_frequently_of_upcrossings_lt_top : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω},
  a < b →
    MeasureTheory.upcrossings a b f ω ≠ ⊤ →
      ¬((∃ᶠ (n : ℕ) in Filter.atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in Filter.atTop, b < f n ω)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Postcomposition of bounded continuous functions into a normed module by a continuous linear map
is a continuous linear map.
Upgraded version of `ContinuousLinearMap.compLeftContinuous`, similar to `LinearMap.compLeft`.  -/
ContinuousLinearMap.compLeftContinuousBounded : (α : Type u) →
  {β : Type v} →
    {γ : Type w} →
      {𝕜 : Type u_1} →
        [inst : TopologicalSpace α] →
          [inst_1 : SeminormedAddCommGroup β] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NormedSpace 𝕜 β] →
                [inst_4 : SeminormedAddCommGroup γ] →
                  [inst_5 : NormedSpace 𝕜 γ] →
                    (β →L[𝕜] γ) → BoundedContinuousFunction α β →L[𝕜] BoundedContinuousFunction α γ
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprLocalTimeType.repr : Std.Time.TimeZone.LocalTimeType → ℕ → Std.Format
-- Mathlib.RingTheory.Flat.Basic
/-- An easier-to-use version of `Module.flat_iff`, with finiteness conditions removed.  -/
Module.Flat.iff_rTensor_injectiveₛ : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Function.Injective ⇑(LinearMap.rTensor M N.subtype)
-- Init.Data.Option.Lemmas
/-- An optional arbitrary element of a given type.

If `α` is non-empty, then there exists some `v : α` and this arbitrary element is `some v`.
Otherwise, it is `none`.
 -/
Option.choice : (α : Type u_1) → Option α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} {f : β → β} {hc : k' ∈ Std.ExtDTreeMap.Const.modify t k f},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.modify t k f) k' hc =
    if heq : cmp k k' = Ordering.eq then f (Std.ExtDTreeMap.Const.get t k ⋯) else Std.ExtDTreeMap.Const.get t k' ⋯
-- Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
/-- For `l : ℕ` and `u : ℤ × ℤ`, this is the complex shape on `ℤ × Fin l`, which
connects `a` to `b` when the equality `a + u = b` holds in `ℤ × ℤ`.  -/
ComplexShape.spectralSequenceFin : (l : ℕ) → ℤ × ℤ → ComplexShape (ℤ × Fin l)
-- Lean.Meta.WHNF
/-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument  -/
Lean.Meta.whnfEasyCases : Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_pi_apply : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] (a : δ), Measurable fun f => f a
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker_prod_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_5} {N' : Type u_6}
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* N) (g : M' →* N'),
  MonoidHom.mker (f.prodMap g) = (MonoidHom.mker f).prod (MonoidHom.mker g)