mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.brecOn.go : {motive_1 : Lean.Parser.Tactic.MRefinePat → Sort u} →
  {motive_2 : List Lean.Parser.Tactic.MRefinePat → Sort u} →
    (t : Lean.Parser.Tactic.MRefinePat) →
      ((t : Lean.Parser.Tactic.MRefinePat) → t.below → motive_1 t) →
        ((t : List Lean.Parser.Tactic.MRefinePat) → Lean.Parser.Tactic.MRefinePat.below_1 t → motive_2 t) →
          motive_1 t ×' t.below
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w} {X : C}
  {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X)
  (h h_1 : ⦃W : C⦄ → (r : W ⟶ X) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W),
  h = h_1 →
    CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h =
      CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h_1
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_gcd : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.SPolResult.mk.injEq : ∀ (spol : Lean.Grind.CommRing.Poly) (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (spol_1 : Lean.Grind.CommRing.Poly) (k₁_1 : ℤ) (m₁_1 : Lean.Grind.CommRing.Mon) (k₂_1 : ℤ)
  (m₂_1 : Lean.Grind.CommRing.Mon),
  ({ spol := spol, k₁ := k₁, m₁ := m₁, k₂ := k₂, m₂ := m₂ } =
      { spol := spol_1, k₁ := k₁_1, m₁ := m₁_1, k₂ := k₂_1, m₂ := m₂_1 }) =
    (spol = spol_1 ∧ k₁ = k₁_1 ∧ m₁ = m₁_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1)
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.measurableSet_Ioo : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) [Countable ι], MeasurableSet (BoxIntegral.Box.Ioo I)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddCommMonoid N]
  (f : SkewMonoidAlgebra k G) (g : G → k → N), f.sum g = f.coeff.sum g
-- Std.Sync.Broadcast
/-- Try to send a value to the broadcast channel, if this can be completed right away without blocking return
`true`, otherwise don't send the value and return `false`.
 -/
Std.Broadcast.trySend : {α : Type} → Std.Broadcast α → α → BaseIO (Option ℕ)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_eq_right_of_det_mem_nonZeroDivisors : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] (A : Matrix m m R) (B : Matrix m n R), A.det ∈ nonZeroDivisors R → (A * B).rank = B.rank
-- Lean.Elab.PreDefinition.Structural.Main
_private.Lean.Elab.PreDefinition.Structural.Main.0.Lean.Elab.Structural.inferRecArgPos : Array Lean.Elab.PreDefinition →
  Array (Option Lean.Elab.TerminationMeasure) →
    Lean.MetaM (Array ℕ × Array Lean.Elab.PreDefinition × Lean.Elab.FixedParamPerms)
-- Mathlib.Topology.Connected.TotallyDisconnected
totallyDisconnectedSpace_iff : ∀ (α : Type u) [inst : TopologicalSpace α], TotallyDisconnectedSpace α ↔ IsTotallyDisconnected Set.univ
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.coe_apply : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι) (x : η → α) (i : ι),
  ↑l x i = Sum.elim id x (l.idxFun i)
-- Mathlib.Analysis.Distribution.Support
Distribution.dsupport_lineDerivOp_subset : ∀ {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E}
  {F : Type u_12} [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F]
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {f : Distribution Ω F ⊤} (m : E),
  Distribution.dsupport ⇑(LineDeriv.lineDerivOp m f) ⊆ Distribution.dsupport ⇑f
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.zero_convolution : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E'), DiscreteConvolution.convolution L 0 f = 0
-- Mathlib.Order.ModularLattice
infIooOrderIsoIooSup_symm_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (c : ↑(Set.Ioo b (a ⊔ b))),
  ↑((RelIso.symm (infIooOrderIsoIooSup a b)) c) = a ⊓ ↑c
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- Lift a (semi)linear map to `WithLp`.  -/
LinearMap.withLpMap : (p : ENNReal) →
  {K : Type u_1} →
    {K' : Type u_2} →
      {V : Type u_4} →
        {V' : Type u_5} →
          [inst : Semiring K] →
            [inst_1 : Semiring K'] →
              {σ : K →+* K'} →
                [inst_2 : AddCommGroup V] →
                  [inst_3 : Module K V] →
                    [inst_4 : AddCommGroup V'] → [inst_5 : Module K' V'] → (V →ₛₗ[σ] V') → WithLp p V →ₛₗ[σ] WithLp p V'
-- Batteries.Data.Nat.Bisect
Nat.le_add_one_of_avg_eq_right : ∀ {a b : ℕ}, a.avg b = b → a ≤ b + 1
-- Mathlib.Algebra.Module.Submodule.Union
Module.exists_dual_forall_apply_ne_zero : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [Finite ι] [Infinite K] (v : ι → M), (∀ (i : ι), v i ≠ 0) → ∃ f, ∀ (i : ι), f (v i) ≠ 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The natural equivalence
`StructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T'`.  -/
CategoryTheory.StructuredArrow.prodEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (S : D) →
                  (S' : D') →
                    (T : CategoryTheory.Functor C D) →
                      (T' : CategoryTheory.Functor C' D') →
                        CategoryTheory.StructuredArrow (S, S') (T.prod T') ≌
                          CategoryTheory.StructuredArrow S T × CategoryTheory.StructuredArrow S' T'
-- Batteries.Data.List.Lemmas
List.foldrIdx_eq_foldr_zipIdx : ∀ {α : Type u_1} {xs : List α} {α_1 : Type u_2} {f : ℕ → α → α_1 → α_1} {i : α_1} {s : ℕ},
  List.foldrIdx f i xs s = List.foldr (fun ab => f ab.2 ab.1) i (xs.zipIdx s)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.flatMapM.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List (List β) → Sort u_3) →
      (x : List α) →
        (x_1 : List (List β)) →
          ((bs : List (List β)) → motive [] bs) →
            ((a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs) → motive x x_1
-- Mathlib.Analysis.Normed.Module.Basic
SeminormedSpace.Core.norm_triangle : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Norm E]
  [inst_3 : Module 𝕜 E], SeminormedSpace.Core 𝕜 E → ∀ (x y : E), ‖x + y‖ ≤ ‖x‖ + ‖y‖
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from types to its "semiring id". We cache failures using `none`.
`ncstypeIdOf[type]` is `some id`, then `id < ncSemirings.size`.  -/
Lean.Meta.Grind.Arith.CommRing.State.ncstypeIdOf : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.toPseudoMetricSpace : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      {F : Type u_5} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜₂ F] →
                    {σ₁₂ : 𝕜 →+* 𝕜₂} → [RingHomIsometric σ₁₂] → PseudoMetricSpace (E →SL[σ₁₂] F)
-- Mathlib.Order.SetAccumulate
Set.accumulate.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] (s : α → Set β) (x : α), Set.accumulate s x = ⋃ y, ⋃ (_ : y ≤ x), s y
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.AbsolutelyContinuous.withDensity_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  ξ.AbsolutelyContinuous μ → ξ.AbsolutelyContinuous ν → ξ.AbsolutelyContinuous (ν.withDensity (μ.rnDeriv ν))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuation_def : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) x = (v.intValuation.extendToLocalization ⋯ K) x
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.tensor_right'_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.MonoidalCoherence Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCategory.whiskerLeftIso X CategoryTheory.MonoidalCoherence.iso ≪≫
      CategoryTheory.MonoidalCategoryStruct.rightUnitor X
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.Nat.unaryCast.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.Separation.Regular
lift'_nhdsSet_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] (u : Set X),
  IsClosed u → (nhdsSet u).lift' closure = nhdsSet u
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.positional.injEq : ∀ (name : Lean.Name) (type : Lean.Expr) (name_1 : Lean.Name) (type_1 : Lean.Expr),
  (Lean.Doc.ArgSpec.positional✝ name type = Lean.Doc.ArgSpec.positional✝ name_1 type_1) =
    (name = name_1 ∧ type = type_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.infinite_mul : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s t : Set α},
  (s * t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.PlausibleStep.drop : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {it' : Std.IterM m β} {out : β} {k : ℕ},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    it.internalState.remaining = k + 1 →
      Std.Iterators.Types.Drop.PlausibleStep it (Std.IterStep.skip (Std.IterM.drop k it'))
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorph.boundarylessManifold : ∀ {𝕜 : 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'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ {f : M → N}, IsLocalDiffeomorph I I' n f → ∀ [BoundarylessManifold I' N], BoundarylessManifold I M
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_right_strictMono : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (o : Ordinal.{u}), StrictMono (Ordinal.veblenWith f o)
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
/-- A sieve belongs to the coherent topology if and only if it contains a finite
`EffectiveEpiFamily`.
 -/
CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.coherentTopology C) X ↔
    ∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.add_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 g → (Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 f)
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject : Type
-- Mathlib.Data.Set.Basic
Set.Nonempty.eq_univ : ∀ {α : Type u} {s : Set α} [Subsingleton α], s.Nonempty → s = Set.univ
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.Paths.liftNatIso_hom_app : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (α_app : (v : V) → F.obj v ≅ G.obj v)
  (α_nat :
    ∀ {X Y : V} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y).hom =
        CategoryTheory.CategoryStruct.comp (α_app X).hom (G.map f.toPath))
  (X : CategoryTheory.Paths V), (CategoryTheory.Paths.liftNatIso α_app α_nat).hom.app X = (α_app X).hom
-- Mathlib.Probability.Kernel.Defs
/-- A kernel is a measurable map.

Do not use this lemma directly. Use `Kernel.measurable` instead.  -/
ProbabilityTheory.Kernel.measurable' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (self : ProbabilityTheory.Kernel α β), Measurable self.toFun
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- The space of continuous multilinear maps on `Π(i : Fin (n+1)), Ei i` is canonically isomorphic to
the space of continuous multilinear maps on `Π(i : Fin n), Ei <| castSucc i` with values in the
space of continuous linear maps on `Ei (last n)`, by separating the last variable. We register this
isomorphism as a continuous linear equiv in `continuousMultilinearCurryRightEquiv 𝕜 Ei G`.
The algebraic version (without topology) is given in `multilinearCurryRightEquiv 𝕜 Ei G`.

The direct and inverse maps are given by `f.curryRight` and `f.uncurryRight`. Use these
unless you need the full framework of linear isometric equivs.
 -/
continuousMultilinearCurryRightEquiv : (𝕜 : Type u) →
  {n : ℕ} →
    (Ei : Fin n.succ → Type wEi) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.forIn'_eq_match : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_6 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    match hs : Std.PRange.succ? r.lower with
    | none => pure init
    | some next =>
      if hu : next < r.upper then
        have hlt := ⋯;
        have hle := ⋯;
        do
        let __do_lift ← f next ⋯ init
        match __do_lift with
          | ForInStep.yield c => forIn' (next<...r.upper) c fun a ha acc => f a ⋯ acc
          | ForInStep.done c => pure c
      else pure init
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.Iso.trans.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z),
  α ≪≫ β =
    { hom := CategoryTheory.CategoryStruct.comp α.hom β.hom, inv := CategoryTheory.CategoryStruct.comp β.inv α.inv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
/-- The **Turán density** of a simple graph `H` is well-defined.  -/
SimpleGraph.tendsto_turanDensity : ∀ {W : Type u_1} (H : SimpleGraph W),
  Filter.Tendsto (fun n => ↑(SimpleGraph.extremalNumber n H) / ↑(n.choose 2)) Filter.atTop (nhds H.turanDensity)
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`HashSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
the variant {lean}`it.ensureTermination.toHashSet` always terminates after finitely many steps.
 -/
Std.Iter.toHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] → [inst_2 : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → Std.HashSet β
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.monoCLM_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω₁ Ω₂ : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n₁ n₂ : ℕ∞} [inst_6 : Algebra ℝ 𝕜]
  [inst_7 : IsScalarTower ℝ 𝕜 F], ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂) → TestFunction.monoCLM 𝕜 = 0
-- Lean.Elab.Term.TermElabM
Lean.Parser.Term.elabToSyntax.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Nat.Basic
Nat.pred_zero : Nat.pred 0 = 0
-- Mathlib.GroupTheory.Divisible
AddGroup.divisibleByIntOfDivisibleByNat.eq_1 : ∀ (A : Type u_1) [inst : AddGroup A] [inst_1 : DivisibleBy A ℕ],
  AddGroup.divisibleByIntOfDivisibleByNat A =
    {
      div := fun a z =>
        match z with
        | Int.ofNat n => DivisibleBy.div a n
        | Int.negSucc n => -DivisibleBy.div a (n + 1),
      div_zero := ⋯, div_cancel := ⋯ }
-- Mathlib.LinearAlgebra.Pi
LinearMap.ker_compLeft : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (I : Type u_1),
  (f.compLeft I).ker = Submodule.pi Set.univ fun x => f.ker
-- Aesop.Script.Tactic
Aesop.Script.STactic.mk.injEq : ∀ (numSubgoals : ℕ) (run : Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic) (numSubgoals_1 : ℕ)
  (run_1 : Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic),
  ({ numSubgoals := numSubgoals, run := run } = { numSubgoals := numSubgoals_1, run := run_1 }) =
    (numSubgoals = numSubgoals_1 ∧ run = run_1)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_of_addOrderOf_eq_card : ∀ {α : Type u_1} [inst : AddGroup α] [Finite α] (x : α), addOrderOf x = Nat.card α → IsAddCyclic α
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.center_le_centralizer : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.center G ≤ Subgroup.centralizer s
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The elements of the non-unital subsemiring closure of `M` are exactly the elements of the
additive closure of a multiplicative subsemigroup `M`.  -/
NonUnitalSubsemiring.coe_closure_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : Set R),
  ↑(NonUnitalSubsemiring.closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.natCast_iSup`. -/
ENat.coe_iSup : ∀ {ι : Sort u_1} {f : ι → ℕ}, BddAbove (Set.range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β)
  (hf : Continuous f) (K : TopologicalSpace.NonemptyCompacts α),
  (TopologicalSpace.NonemptyCompacts.map f hf K).toCompacts = TopologicalSpace.Compacts.map f hf K.toCompacts
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.congr_symm_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x : TensorProduct R C D),
  (Algebra.TensorProduct.congr f g).symm x = (Algebra.TensorProduct.map ↑f.symm ↑g.symm) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_some_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey? = some (t.minKey he)
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.Measure.AbsolutelyContinuous.trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ (hm : m ≤ m0), (μ.trim hm).AbsolutelyContinuous (ν.trim hm)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instSMulCommClass : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : AddCommMonoid R] {M : Type u_3} {N : Type u_4} [inst_4 : SMulZeroClass M R]
  [inst_5 : ContinuousConstSMul M R] [inst_6 : SMulZeroClass N R] [inst_7 : ContinuousConstSMul N R]
  [SMulCommClass M N R], SMulCommClass M N (ContinuousMapZero X R)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_unitBall : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜}, c ≠ 0 → c • Metric.ball 0 1 = Metric.ball 0 ‖c‖
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_comap : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) (x : A),
  x ∈ NonUnitalSubalgebra.comap f S ↔ f x ∈ S
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.range_eq : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {K : Type u_3} [inst_2 : AddGroup K]
  (f : AddMonoid.Coprod G H →+ K), f.range = (f.comp AddMonoid.Coprod.inl).range ⊔ (f.comp AddMonoid.Coprod.inr).range
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalₐ_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] (x : X) (x_1 : LocallyConstant X Y),
  (LocallyConstant.evalₐ R x) x_1 = x_1 x
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_quadratic_lt_degree_C_mul_X_cb : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  a ≠ 0 →
    (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree <
      (Polynomial.C a * Polynomial.X ^ 3).degree
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.Indep.symm : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ _mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ → ProbabilityTheory.Kernel.Indep m₂ m₁ κ μ
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instIsTopologicalAddGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G)
  [inst_3 : N.Normal], IsTopologicalAddGroup (G ⧸ N)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.cons_cons : ∀ {m a b : ℕ} {L' : List ℕ},
  a < b →
    SimplexCategoryGenRel.IsAdmissible (m + 1) (b :: L') → a ≤ m → SimplexCategoryGenRel.IsAdmissible m (a :: b :: L')