mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.Basic
/-- `StarMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under star.  -/
StarMemClass : (S : Type u_1) → (R : Type u_2) → [Star R] → [SetLike S R] → Prop
-- Mathlib.Order.CompleteLattice.Basic
iSup_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α}, (∀ (i : ι), f i ≤ a) → iSup f ≤ a
-- Mathlib.Data.Complex.Basic
Complex.I_im : Complex.I.im = 1
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.fixupBlock : Lean.Doc.Block Lean.ElabInline Lean.ElabBlock → Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.two_nsmul_covByVAdd : ∀ {G : Type u_2} [inst : AddGroup G] {K : ℝ} {A : Set G}, IsApproximateAddSubgroup K A → CovByVAdd G K (2 • A) A
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_roo' : ∀ {m n k : ℕ}, Array.map (fun x => k + x) (m<...n).toArray = ((k + m)<...k + n).toArray
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertEntryIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntryIfNew k v l) = true},
  Std.Internal.List.getValue a (Std.Internal.List.insertEntryIfNew k v l) h =
    if h' : (k == a) = true ∧ Std.Internal.List.containsKey k l = false then v else Std.Internal.List.getValue a l ⋯
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- If there is an absolute upper bound on the size of an independent set, then the maximality axiom
isn't needed to define a matroid by independent sets.  -/
IndepMatroid.ofBdd : {α : Type u_1} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) →
            (∀ (I : Set α), Indep I → I ⊆ E) → (∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) → IndepMatroid α
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.instIsPreimmersionFiberι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y),
  AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Scheme.Hom.fiberι f y)
-- Mathlib.Data.Fin.SuccPred
Fin.exists_succAbove_eq : ∀ {n : ℕ} {x y : Fin (n + 1)}, x ≠ y → ∃ z, y.succAbove z = x
-- Mathlib.Control.Functor
Functor.ext : ∀ {F : Type u_1 → Type u_2} {F1 F2 : Functor F} [LawfulFunctor F] [LawfulFunctor F],
  (∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x) → F1 = F2
-- Mathlib.CategoryTheory.Category.Factorisation
/-- Morphisms of `Factorisation f` consist of morphism between their midpoints and the obvious
commutativity conditions.  -/
CategoryTheory.Factorisation.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Factorisation f → CategoryTheory.Factorisation f → Type (max u v)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_pow_right_dvd_pow_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α} {k : ℕ}, gcd a (b ^ k) ∣ gcd a b ^ k
-- Mathlib.Logic.Equiv.Option
Equiv.optionEquivSumPUnit_some : ∀ {α : Type u_4} (a : α), (Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a
-- Qq.MetaM
/-- Like `Qq.isDefEqQ`, but throws an error if not defeq.  -/
Qq.assertDefEqQ : {u : Lean.Level} →
  {α :
      have u := u;
      Q(Sort u)} →
    (a b : Q(«$α»)) → Lean.MetaM (PLift («$a» =Q «$b»))
-- Mathlib.Algebra.Order.Module.Rat
abs_nnqsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : DistribMulAction ℚ≥0 α] [PosSMulMono ℚ≥0 α] (q : ℚ≥0) (a : α), |q • a| = q • |a|
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (c : F), HasDerivAt (fun x => c) 0 x
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.submatrix_cons_row : ∀ {α : Type u} {m : ℕ} {m' : Type uₘ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix m' n' α) (i : m') (row : Fin m → m')
  (col : o' → n'), A.submatrix (Matrix.vecCons i row) col = Matrix.vecCons (fun j => A i (col j)) (A.submatrix row col)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
irreducible_iff_prime_of_exists_prime_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  (∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a) → ∀ {p : α}, Irreducible p ↔ Prime p
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore.match_1.eq_2 : ∀ (motive : ℕ → ℕ → List Char → Sort u_1) (fuel n : ℕ) (ds : List Char)
  (h_1 : (x : ℕ) → (ds : List Char) → motive 0 x ds) (h_2 : (fuel n : ℕ) → (ds : List Char) → motive fuel.succ n ds),
  (match fuel.succ, n, ds with
    | 0, x, ds => h_1 x ds
    | fuel.succ, n, ds => h_2 fuel n ds) =
    h_2 fuel n ds
-- Init.Data.Array.Attach
Array.foldl_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : β → α → β} {x : β},
  Array.foldl f x xs.unattach =
    Array.foldl
      (fun s x =>
        match x with
        | ⟨x, h⟩ => binderNameHint s f (binderNameHint x (f s) (binderNameHint h () (f s (wfParam x)))))
      x xs
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- Auxiliary definition for `presheafHom_isSheafFor`.  -/
CategoryTheory.PresheafHom.IsSheafFor.app : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        {F G : CategoryTheory.Functor Cᵒᵖ A} →
          {X : C} →
            {S : CategoryTheory.Sieve X} →
              (⦃Y : C⦄ →
                  (f : Y ⟶ X) →
                    CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)) →
                (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows) →
                  {Y : C} → x.Compatible → (Y ⟶ X) → (F.obj (Opposite.op Y) ⟶ G.obj (Opposite.op Y))
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.toLower_ofLower : ∀ {α : Type u_1} (a : Topology.WithLower α), Topology.WithLower.toLower (Topology.WithLower.ofLower a) = a
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_eq_zero_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}, essSup f μ = 0 ↔ f =ᵐ[μ] 0
-- Mathlib.Data.Set.Lattice
Set.directedOn_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} {r : α → α → Prop} {f : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) f → (∀ (x : ι), DirectedOn r (f x)) → DirectedOn r (⋃ x, f x)
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'.loop.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldRedeclInfo.injEq : ∀ (i i_1 : Lean.Elab.FieldRedeclInfo),
  (Lean.Elab.Info.ofFieldRedeclInfo i = Lean.Elab.Info.ofFieldRedeclInfo i_1) = (i = i_1)
-- Init.Data.Array.MapIdx
Array.mem_mapIdx : ∀ {β : Type u_1} {α : Type u_2} {f : ℕ → α → β} {b : β} {xs : Array α},
  b ∈ Array.mapIdx f xs ↔ ∃ i, ∃ (h : i < xs.size), f i xs[i] = b
-- Mathlib.Algebra.Group.Basic
AddCommGroup.toGrindIntModule : (α : Type u_5) → [s : AddCommGroup α] → Lean.Grind.IntModule α
-- Init.Data.Nat.Sqrt.Lemmas
_private.Init.Data.Nat.Sqrt.Lemmas.0.Nat.sqrt.lt_iter_succ_sq : ∀ (n guess : ℕ), n < (guess + 1) * (guess + 1) → n < (Nat.sqrt.iter n guess + 1) * (Nat.sqrt.iter n guess + 1)
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.id_val : ∀ {M : Type u_1} [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] (x : CategoryTheory.ActionCategory M X),
  ↑(CategoryTheory.CategoryStruct.id x) = 1
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.mk : {A : Type u_1} →
  [toNonUnitalNormedRing : NonUnitalNormedRing A] →
    [toStarRing : StarRing A] →
      [toCompleteSpace : CompleteSpace A] →
        [toCStarRing : CStarRing A] →
          [toNormedSpace : NormedSpace ℂ A] →
            [toIsScalarTower : IsScalarTower ℂ A A] →
              [toSMulCommClass : SMulCommClass ℂ A A] → [toStarModule : StarModule ℂ A] → NonUnitalCStarAlgebra A
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.global.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : α), sizeOf (Lean.ScopedEnvExtension.Entry.global a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Left unitality of the enriched structure  -/
CategoryTheory.MonoidalClosed.id_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y : C)
  [inst_2 : CategoryTheory.Closed x] {Z : C} (h : x ⟹ y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (x ⟹ y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalClosed.id x) (x ⟹ y))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp x x y) h)) =
    h
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.atom.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (idx : α), sizeOf (Std.Sat.AIG.Decl.atom idx) = 1 + sizeOf idx
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_dvd_leadingCoeff : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {a p : Polynomial R}, a ∣ p → a.leadingCoeff ∣ p.leadingCoeff
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.MkEqOfNaturality.mk : {m : Type → Type} →
  (Lean.Expr →
      Lean.Expr →
        Mathlib.Tactic.BicategoryLike.IsoLift →
          Mathlib.Tactic.BicategoryLike.IsoLift →
            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
              Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr) →
    Mathlib.Tactic.BicategoryLike.MkEqOfNaturality m
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X)
  (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
  F.fromLeftDerivedZero.app X =
    CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom
      (CategoryTheory.CategoryStruct.comp
        (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom
        (P.fromLeftDerivedZero' F))
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.noMVars.sizeOf_spec : sizeOf Lean.Meta.PreprocessKind.noMVars✝ = 1
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_top_of_isLocalized₀_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_5 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M},
      (∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = ⊤) → N = ⊤
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one_one_eq_chebyshev_T : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2] (n : ℕ),
  Polynomial.dickson 1 1 n = 2 * (Polynomial.Chebyshev.T R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.isLittleO_of_lt_exps_left : ∀ {left right : Tactic.ComputeAsymptotics.Basis} {t1 t2 : Tactic.ComputeAsymptotics.Monomial},
  Tactic.ComputeAsymptotics.WellFormedBasis (left ++ right) →
    List.length t1.unit = List.length left + List.length right →
      List.length t2.unit = List.length right →
        t2.coef ≠ 0 →
          t1.unit < List.replicate (List.length left) 0 ++ t2.unit →
            t1.toFun (left ++ right) =o[Filter.atTop] t2.toFun right
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_ball_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ}, μ (Metric.ball x r) < ⊤
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.mk.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (toFun toFun_1 : α → MeasureTheory.Measure β) (e_toFun : toFun = toFun_1) (measurable' : Measurable toFun),
  { toFun := toFun, measurable' := measurable' } = { toFun := toFun_1, measurable' := ⋯ }
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_finsetProd' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (∏ i ∈ t, f i) x
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.integrable_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s → MeasureTheory.Integrable (fun x => κ.density ν a x s) (ν a)
-- Init.Data.SInt.Basic
instShiftRightInt16 : ShiftRight Int16
-- Mathlib.Data.List.Permutation
List.permutationsAux.eq_1 : ∀ {α : Type u_1} (l₁ l₂ : List α),
  l₁.permutationsAux l₂ =
    List.permutationsAux.rec (fun x => [])
      (fun t ts is IH1 IH2 => List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) l₁ l₂
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
/-- **Alias** of `MeasureTheory.exists_accPt_of_nullSingletonClass`. -/
MeasureTheory.exists_accPt_of_noAtoms : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E],
  0 < μ E → ∃ x, AccPt x (Filter.principal E)
-- Mathlib.CategoryTheory.Widesubcategory
/-- The type of morphisms in `InducedWideCategory D F P` between `X` and `Y`
is a 2-field structure consisting of a morphism `F X ⟶ F Y` in `D` that satisfies
the property `P`.  -/
CategoryTheory.InducedWideCategory.Hom : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      {F : C → D} →
        {P : CategoryTheory.MorphismProperty D} →
          [inst_1 : P.IsMultiplicative] →
            CategoryTheory.InducedWideCategory D F P → CategoryTheory.InducedWideCategory D F P → Type v₁
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α] (n : ℕ)
  (lhs : aig.RefVec w) (rhs : aig.RefVec n) (pow : ℕ),
  sizeOf { n := n, lhs := lhs, rhs := rhs, pow := pow } = 1 + sizeOf n + sizeOf lhs + sizeOf rhs + sizeOf pow
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.of_sub_of : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Sub A] (f g : Matrix m n A),
  CStarMatrix.ofMatrix f - CStarMatrix.ofMatrix g = CStarMatrix.ofMatrix (f - g)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.contract_expand : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) {f : Polynomial R},
  p ≠ 0 → Polynomial.contract p ((Polynomial.expand R p) f) = f
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfMkEq_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (f : A ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (h : CategoryTheory.Subobject.mk f = X),
  (CategoryTheory.Subobject.isoOfMkEq f X h).hom = CategoryTheory.Subobject.ofMkLE f X ⋯
-- Init.Data.Sum.Basic
Sum.getRight?_inr : ∀ {α : Type u_1} {β : Type u_2} {x : β}, (Sum.inr x).getRight? = some x
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_map_app : ∀ {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 Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D),
  (CategoryTheory.Functor.uncurry.map T).app X_1 = (T.app X_1.1).app X_1.2
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {w x : C} {y z : D} (f : w ⟶ x) (g : y ⟶ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w g)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f y)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x g)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.eLpNorm_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [OpensMeasurableSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν → ∀ (p : ENNReal), MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p ν
-- Mathlib.Topology.Algebra.Group.Matrix
/-- If `R` is a commutative ring with the discrete topology, then `SL(n, R)` has the discrete
topology.  -/
Matrix.SpecialLinearGroup.instDiscreteTopology : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [DiscreteTopology R], DiscreteTopology (Matrix.SpecialLinearGroup n R)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_univ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f Set.univ ↔ ContDiff 𝕜 n f
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring c lhs) = 1 + sizeOf c + sizeOf lhs
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.δ_fst_assoc : ∀ {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) [inst_4 : F.OplaxMonoidal] (X Y : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) h
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.nsmul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → ∀ (n : ℕ), AntivaryOn (n • f) g s
-- Mathlib.Data.NNRat.Defs
NNRat.num_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).num = OfNat.ofNat n
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBasis_iff_isBasis_closure_of_subset : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α},
  I ⊆ X →
    autoParam (X ⊆ M.E) Matroid.isBasis_iff_isBasis_closure_of_subset._auto_1 →
      (M.IsBasis I X ↔ M.IsBasis I (M.closure X))
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.mapToComposableArrows_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (ψ : S₂ ⟶ S₃),
  CategoryTheory.ShortComplex.mapToComposableArrows (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapToComposableArrows φ)
      (CategoryTheory.ShortComplex.mapToComposableArrows ψ)
-- Mathlib.GroupTheory.Torsion
CommGroup.isMulTorsion_quotient_range_powMonoidHom : ∀ (G : Type u_1) [inst : CommGroup G] {n : ℕ}, n ≠ 0 → IsMulTorsion (G ⧸ (powMonoidHom n).range)
-- Mathlib.Topology.IndicatorConstPointwise
tendsto_indicator_const_iff_tendsto_pi_pure : ∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3} (L : Filter ι)
  {As : ι → Set α} [T1Space β] (b : β) [NeZero b],
  Filter.Tendsto (fun i => (As i).indicator fun x => b) L (nhds (A.indicator fun x => b)) ↔
    Filter.Tendsto (fun i x => x ∈ As i) L (Filter.pi fun x => pure (x ∈ A))
-- Mathlib.FieldTheory.Relrank
/-- **Alias** of the reverse direction of `IntermediateField.relrank_eq_one_iff`. -/
IntermediateField.relrank_eq_one_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  B ≤ A → A.relrank B = 1
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mem_supported : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  {s : Set M} {x : AddMonoidAlgebra S M}, x ∈ AddMonoidAlgebra.supported R S s ↔ ↑x.coeff.support ⊆ s
-- Mathlib.Analysis.Normed.Operator.Banach
/-- A choice of anti-Lipschitz constant for `f : E →L[𝕜] F` injective with closed range
(assuming `E` and `F` are Banach spaces).  -/
ContinuousLinearMap.antilipschitzConstant_of_injective_of_isClosed_range : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_5} →
      {F : Type u_6} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                [CompleteSpace E] →
                  [CompleteSpace F] → (f : E →L[𝕜] F) → Function.Injective ⇑f → IsClosed (Set.range ⇑f) → NNReal
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_3.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Data.TypeVec
/-- similar to `toSubtype` adapted to relations (i.e. predicate on product)  -/
TypeVec.toSubtype' : {n : ℕ} →
  {α : TypeVec.{u} n} →
    (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
      TypeVec.Arrow (fun i => { x // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.1 x.2)) }) (TypeVec.Subtype_ p)