mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Binomial
Ring.choose_one_right' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R), Ring.choose r 1 = r ^ 1
-- Mathlib.Order.Cofinal
IsCofinal.mem_of_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a : α}, IsMax a → IsCofinal s → a ∈ s
-- Mathlib.Logic.Equiv.Basic
/-- The type of functions `f : ∀ a, β a` such that for all `a` we have `p a (f a)` is equivalent
to the type of functions `∀ a, {b : β a // p a b}`.  -/
Equiv.subtypePiEquivPi : {α : Sort u_1} →
  {β : α → Sort v} → {p : (a : α) → β a → Prop} → { f // ∀ (a : α), p a (f a) } ≃ ((a : α) → { b // p a b })
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- If `Fₙ` converges locally uniformly on a neighborhood of `x` within a set `s` to a function `f`
which is continuous at `x` within `s`, and `gₙ` tends to `x` within `s`, then `Fₙ (gₙ)` tends
to `f x`.  -/
tendsto_comp_of_locally_uniform_limit_within : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α},
  ContinuousWithinAt f s x →
    Filter.Tendsto g p (nhdsWithin x s) →
      (∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) →
        Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.submodule : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  {m : Submodule R M}, IsSemisimpleModule R ↥m
-- Mathlib.Order.Filter.Pointwise
Filter.one_prod_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : One β], 1 ×ˢ 1 = 1
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_eq_bot : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂}, f.range = ⊥ ↔ f = 0
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃a' : α⦄,
  (a, b, c) ∈ t → (a', b, c) ∈ t → a = a'
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mul_stabilizer_self : ∀ {G : Type u_1} [inst : CommGroup G] (s : Set G), s * ↑(MulAction.stabilizer G s) = s
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.instIsNormalEpiCategory : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C], CategoryTheory.IsNormalEpiCategory (HomologicalComplex C c)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- An object of the homotopy category is a vertex of `A`.  -/
SSet.Truncated.HomotopyCategory₂.pt : {A : SSet.Truncated 2} →
  A.HomotopyCategory₂ → A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })
-- Mathlib.Tactic.FieldSimp
/-- Extract a common factor `L` of two products-of-powers `l₁` and `l₂` in `M`, in the sense that
both `l₁` and `l₂` are quotients by `L` of products of *positive* powers.

The variable `cond` specifies whether we extract a *certified nonzero(/positive)* (and therefore
potentially smaller) common factor. If so, the metaprogram returns a "proof" that this common factor
is nonzero/positive, i.e. an expression `Q(NF.eval $(L.toNF) ≠ 0)` / `Q(0 < NF.eval $(L.toNF))`.  -/
Mathlib.Tactic.FieldSimp.qNF.gcd : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M) →
        ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
          (cond : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance)) →
            Lean.MetaM
              ((L : Mathlib.Tactic.FieldSimp.qNF M) ×
                (l₁' : Mathlib.Tactic.FieldSimp.qNF M) ×
                  (l₂' : Mathlib.Tactic.FieldSimp.qNF M) ×
                    (have a := l₁.toNF;
                      have a_1 := l₁'.toNF;
                      have a_2 := L.toNF;
                      Q(«$a_2».eval * «$a_1».eval = «$a».eval)) ×
                      (have a := l₂.toNF;
                        have a_1 := l₂'.toNF;
                        have a_2 := L.toNF;
                        Q(«$a_2».eval * «$a_1».eval = «$a».eval)) ×
                        Mathlib.Tactic.FieldSimp.DenomCondition.proof L cond)
-- Mathlib.LinearAlgebra.CrossProduct
/-- The scalar quadruple product identity, related to the Binet-Cauchy identity.  -/
cross_dot_cross : ∀ {R : Type u_1} [inst : CommRing R] (u v w x : Fin 3 → R),
  (crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_inf : ∀ {M : Type u_2} [inst : MulOneClass M] (S₁ S₂ : Submonoid Mᵐᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Check if `a` can be obtained by removing elements from `b`.  -/
Mathlib.Meta.FunProp.isOrderedSubsetOf : {α : Type u_1} → [Inhabited α] → [DecidableEq α] → Array α → Array α → Bool
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.div_congr : ∀ {R : Type u_2} [inst : Semifield R] {a a' b b' c : R}, a = a' → b = b' → a' / b' = c → a / b = c
-- Mathlib.Order.Interval.Set.Image
StrictAnti.mapsTo_Ioo : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictAnti f → Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.finite_setOfPred_mem : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] (x : R), x ≠ 0 → {I | x ∈ I}.Finite
-- Std.Http.Data.Body.Length
Std.Http.Body.instBEqLength : BEq Std.Http.Body.Length
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.IdNode.mk.sizeOf_spec : ∀ (vPos hPosSrc hPosTar : ℕ) (id : Mathlib.Tactic.BicategoryLike.Atom₁),
  sizeOf { vPos := vPos, hPosSrc := hPosSrc, hPosTar := hPosTar, id := id } =
    1 + sizeOf vPos + sizeOf hPosSrc + sizeOf hPosTar + sizeOf id
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_toArray : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {k : α},
  m.WF → (k ∈ m.toArray ↔ k ∈ m)
-- Batteries.Linter.UnnecessarySeqFocus
Batteries.Linter.UnnecessarySeqFocus.Entry.mk : Lean.Syntax → Bool → Batteries.Linter.UnnecessarySeqFocus.Entry
-- Mathlib.Analysis.Normed.Module.TransferInstance
Equiv.seminormedCommGroup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedCommGroup β] (e : α ≃ β),
  e.seminormedCommGroup =
    { toNorm := (SeminormedCommGroup.induced α β e.mulEquiv).toNorm,
      toCommGroup := (SeminormedCommGroup.induced α β e.mulEquiv).toCommGroup,
      toPseudoMetricSpace := e.pseudometricSpace, dist_eq := ⋯ }
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.linearEquivFunOnFinite_apply : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M] (a : α →₀ M) (a_1 : α), (Finsupp.linearEquivFunOnFinite R M α) a a_1 = a a_1
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the sine of the angle between three points is 0, they are collinear.  -/
EuclideanGeometry.collinear_of_sin_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}
-- Batteries.Data.String.Lemmas
String.any_eq : ∀ (s : String) (p : Char → Bool), String.Legacy.any s p = s.toList.any p
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The morphism `triangle φ₁ ⟶ triangle φ₂` that is induced by a commutative square.  -/
CochainComplex.mappingCone.triangleMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} →
          (φ₁ : K₁ ⟶ L₁) →
            (φ₂ : K₂ ⟶ L₂) →
              (a : K₁ ⟶ K₂) →
                (b : L₁ ⟶ L₂) →
                  CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂ →
                    (CochainComplex.mappingCone.triangle φ₁ ⟶ CochainComplex.mappingCone.triangle φ₂)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The interior and boundary of a manifold `M` are disjoint.  -/
ModelWithCorners.disjoint_interior_boundary : ∀ {𝕜 : 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],
  Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme : {S : AlgebraicGeometry.Scheme} → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Over S)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.eq_of_adj_right : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V}, M.IsMatching → M.Adj u w → M.Adj v w → u = v
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.assoc_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z W : C)
  [inst_2 :
    CategoryTheory.MonoidalCoherence
      (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) W],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCategoryStruct.associator X Y Z ≪≫ CategoryTheory.MonoidalCoherence.iso
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingSubgroup_empty : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α], fixingSubgroup M ∅ = ⊤
-- Mathlib.Algebra.Group.Action.Units
IsUnit.inv_smul : ∀ {α : Type u_5} [inst : Monoid α] {a : α} (h : IsUnit a), h.unit⁻¹ • a = 1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.symm_iff : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β}, e.symm.IsImage t s ↔ e.IsImage s t
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  {f f' : X ⟶ Y'} {s : Y ⟶ Y'} {hs : W s} {Y'_1 : C} {f_1 f'_1 : X ⟶ Y'_1} {s_1 : Y ⟶ Y'_1} {hs_1 : W s_1},
  { Y' := Y', f := f, f' := f', s := s, hs := hs } = { Y' := Y'_1, f := f_1, f' := f'_1, s := s_1, hs := hs_1 } →
    Y' = Y'_1 ∧ f ≍ f_1 ∧ f' ≍ f'_1 ∧ s ≍ s_1
-- Init.Data.Vector.Attach
Vector.attachWith_reverse : ∀ {α : Type u_1} {n : ℕ} {P : α → Prop} {xs : Vector α n} {H : ∀ a ∈ xs.reverse, P a},
  xs.reverse.attachWith P H = (xs.attachWith P ⋯).reverse
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp.congr_simp : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F)
  (U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ),
  AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U =
    AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.haveLebesgueDecomposition_of_sigmaFinite : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ], s.HaveLebesgueDecomposition μ
-- Mathlib.Data.Multiset.Powerset
Multiset.revzip_powersetAux_perm_aux' : ∀ {α : Type u_1} {l : List α}, (Multiset.powersetAux l).revzip.Perm (Multiset.powersetAux' l).revzip
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a linear map `f` from `M 0` to multilinear maps on `n` variables,
construct the corresponding multilinear map on `n+1` variables obtained by concatenating
the variables, given by `m ↦ f (m 0) (tail m)`  -/
LinearMap.uncurryLeft : {R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] → (M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂) → MultilinearMap R M M₂
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.commSemiring : {R : Type u_1} → {M : Type u_4} → [inst : CommSemiring R] → [CommMonoid M] → CommSemiring (MonoidAlgebra R M)
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.insertTrigger : Lean.NameMap (List (Lean.Name × Float)) → Lean.Name → Lean.Name → Float → Lean.NameMap (List (Lean.Name × Float))
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.Spec.birdDet.match_1.eq_2 : ∀ {R : Type u_1} (motive : (n : ℕ) → Matrix (Fin n) (Fin n) R → Sort u_2) (k : ℕ)
  (A : Matrix (Fin (k + 1)) (Fin (k + 1)) R) (h_1 : (A : Matrix (Fin 0) (Fin 0) R) → motive 0 A)
  (h_2 : (k : ℕ) → (A : Matrix (Fin (k + 1)) (Fin (k + 1)) R) → motive k.succ A),
  (match k.succ, A with
    | 0, A => h_1 A
    | k.succ, A => h_2 k A) =
    h_2 k A
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_Ioc : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.Ioc i j = Set.Ioc (Fin.castLE h i) (Fin.castLE h j)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasGoodReduction.toIsMinimal : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasGoodReduction R W], WeierstrassCurve.IsMinimal R W
-- Init.Data.List.Basic
List.isSuffixOf_nil_left : ∀ {α : Type u} {l : List α} [inst : BEq α], [].isSuffixOf l = true
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.mem_baseSet_trivializationAt' : ∀ {B : Type u_2} {F : Type u_3} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F} {E : B → Type u_5}
  {inst_2 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_3 : (b : B) → TopologicalSpace (E b)}
  [self : FiberBundle F E] (b : B), b ∈ (FiberBundle.trivializationAt' b).baseSet
-- Std.Time.Notation.Spec
/-- Syntax for defining a date spec and configuration of this date spec at compile time.
 -/
Std.Time.«termDatespec(_,_)» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ (i : I), AlgebraicGeometry.IsAffine (D.obj i)] (s : ↑(c.pt.presheaf.obj (Opposite.op ⊤))),
  ∃ i t, (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (c.π.app i))) t = s
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_eq_get?ₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (b : β), (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).1 = Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
NormedSpace.sphere_nonempty_rclike : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E]
  {r : ℝ}, 0 ≤ r → Nonempty ↑(Metric.sphere 0 r)
-- Mathlib.Topology.Order.SuccPred
SuccOrder.nhds_eq_pure : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {a : α}, nhds a = pure a ↔ ¬Order.IsSuccLimit a
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_add_measure_compl₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → μ s + μ sᶜ = μ Set.univ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.instTotalComplexShape : {I : Type u_7} → [inst : AddMonoid I] → (c : ComplexShape I) → [c.TensorSigns] → TotalComplexShape c c c
-- Mathlib.MeasureTheory.Measure.Prod
/-- For any measures `μ` and `ν` and any sets `s` and `t`,
we have `μ.prod ν (s ×ˢ t) ≤ μ s * ν t`.

If `ν` is an s-finite measure (which is usually true),
then this inequality becomes an equality, see `prod_prod` below.  -/
MeasureTheory.Measure.prod_prod_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} (s : Set α) (t : Set β), (μ.prod ν) (s ×ˢ t) ≤ μ s * ν t
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.comapSMul_def : ∀ {G : Type u_2} {M : Type u_6} {α : Type u_7} [inst : Monoid G] [inst_1 : AddCommMonoid M] [inst_2 : MulAction G α]
  (g : G) (f : SkewMonoidAlgebra M α), g • f = (SkewMonoidAlgebra.mapDomain fun x => g • x) f
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_sSup_apply : ∀ {E : Type u_3} [inst : AddGroup E] {s : Set (AddGroupSeminorm E)}, BddAbove s → ∀ {x : E}, (sSup s) x = ⨆ p, ↑p x
-- Std.Http.Protocol.H1
/-- Returns `true` if the reader is closed.
 -/
Std.Http.Protocol.H1.Machine.isReaderClosed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.State.mk : ℕ → Lean.Meta.Sym.DSimp.Cache → Lean.Meta.Sym.DSimp.State
-- Lean.Elab.Binders
/-- Expand `optional (binderTactic <|> binderDefault)`
```
def binderTactic  := leading_parser " := " >> " by " >> tacticParser
def binderDefault := leading_parser " := " >> termParser
```
 -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandBinderModifier : Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.ext_iff : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  {inst_2 : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst_3 : CategoryTheory.EnrichedCategory V D}
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  {x y : CategoryTheory.GradedNatTrans A F G}, x = y ↔ x.app = y.app
-- Mathlib.Data.Sign.Basic
sign_mul : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (x y : α),
  SignType.sign (x * y) = SignType.sign x * SignType.sign y
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.mem_iSup : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (p : ι → Submonoid M) {m : M},
  m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dShortComplex_X₁ : ∀ {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} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7),
  (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).X₁ = X.E f₅ f₆ f₇ n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isOpen_forall_mem_of_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) → ∀ {S : Set ι}, Filter.cofinite ≤ Filter.principal S → IsOpen {f | ∀ (i : ι), ↑f i ∈ A i}
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_open : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  {s t : Set E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E],
  Convex ℝ s →
    IsOpen s → Convex ℝ t → Disjoint s t → ∃ f u, (∀ a ∈ s, RCLike.re (f a) < u) ∧ ∀ b ∈ t, u ≤ RCLike.re (f b)
-- Lean.Data.PersistentArray
Lean.PersistentArray.any : {α : Type u} → Lean.PersistentArray α → (α → Bool) → Bool
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.approx.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {f f_1 : α → β} (e_f : f = f_1) [inst : TopologicalSpace β] {x : MeasurableSpace α}
  (hf : MeasureTheory.StronglyMeasurable f) (a a_1 : ℕ), a = a_1 → hf.approx a = ⋯.approx a_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.multicofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R),
  (CategoryTheory.Limits.Multicoequalizer.multicofork I).π b = CategoryTheory.Limits.Multicoequalizer.π I b
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.zpow : ∀ {f : ℝ → ℝ} (p : ℤ),
  AkraBazziRecurrence.GrowsPolynomially f →
    (∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) → AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
-- Init.Data.Array.Count
Array.count_replicate : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {n : ℕ},
  Array.count a (Array.replicate n b) = if (b == a) = true then n else 0
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The canonical map `K.truncLE n ⟶ K` for `K : CochainComplex C ℤ`.  -/
CochainComplex.ιTruncLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : CochainComplex C ℤ) →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] → (n : ℤ) → K.truncLE n ⟶ K
-- Mathlib.Order.Filter.Defs
Filter.mem_pure : ∀ {α : Type u_1} {a : α} {s : Set α}, s ∈ pure a ↔ a ∈ s
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of `ZeroHom`s as a `ZeroHom`.  -/
ZeroHom.comp : {M : Type u_4} →
  {N : Type u_5} →
    {P : Type u_6} → [inst : Zero M] → [inst_1 : Zero N] → [inst_2 : Zero P] → ZeroHom N P → ZeroHom M N → ZeroHom M P
-- Mathlib.Data.ULift
ULift.exists : ∀ {α : Type u} {p : ULift.{u_1, u} α → Prop}, (∃ x, p x) ↔ ∃ x, p { down := x }
-- Lean.Parser.Term
Lean.Parser.Term.leading_parser.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.maxKey? = none
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), H.IsComplement' K = Subgroup.IsComplement ↑H ↑K