mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Lint
/-- `#grind_lint check` analyzes all theorems annotated for theorem instantiation using E-matching.

It creates artificial goals and reports the number of instances each theorem produces.
The command helps detect long or unbounded theorem instantiation chains.

Usage examples:
```
#grind_lint check
#grind_lint check (min:=10) (detailed:=50)
#grind_lint check in Foo Bar -- restrict analysis to these namespaces
#grind_lint check in module Foo -- restrict analysis to theorems defined in module `Foo` or any of its submodules
```

Options can include any valid `grind` configuration option, and `min` and `detailed`.
- `min`:      minimum number of instantiations to print a summary (default: 10)
- `detailed`: minimum number of instantiations to print detailed breakdown (default: 50)
If the option `trace.grind.*` is enabled, additional details are printed.

By default, `#grind_lint` uses the following `grind` configuration:
```
  splits       := 0
  lookahead    := false
  mbtc         := false
  ematch       := 20
  instances    := 100
  gen          := 10
```
Consider using `#grind_lint inspect <thm>` to focus on specific theorems.
 -/
Lean.Grind.grindLintCheck : Lean.ParserDescr
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Construct a Hahn series from any function whose support is bounded below.  -/
HahnSeries.ofSuppBddBelow : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : Zero R] →
      [inst_1 : LinearOrder Γ] → [LocallyFiniteOrder Γ] → (f : Γ → R) → BddBelow (Function.support f) → HahnSeries Γ R
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instLawfulToBackwardSearcherModelForallCharBoolDefaultBackwardSearcher : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.LawfulToBackwardSearcherModel p
-- Mathlib.Tactic.Zify
Mathlib.Tactic.Zify.Nat.cast_sub_of_lt : ∀ {R : Type u_1} [inst : AddGroupWithOne R] {m n : ℕ}, m < n → ↑(n - m) = ↑n - ↑m
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix.eq_1 : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁),
  LinearMap.BilinForm.toMatrix b = LinearMap.toMatrix₂ b b
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonLeanDiagnosticTag : Lean.FromJson Lean.Lsp.LeanDiagnosticTag
-- Init.Data.BitVec.Basic
/-- Checks whether the signed division of `x` by `y` results in overflow.
For BitVecs `x` and `y` with nonzero width, this only happens if `x = intMin` and `y = allOnes w`.

SMT-LIB name: `bvsdivo`.
 -/
BitVec.sdivOverflow : {w : ℕ} → BitVec w → BitVec w → Bool
-- Init.Data.Nat.Lemmas
Nat.sub_lt_iff_lt_add : ∀ {a b c : ℕ}, b ≤ a → (a - b < c ↔ a < c + b)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_toArray_eq_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β), (↑m).toArray.toList = (↑m).toList
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.not_isHamiltonian_of_isEmpty : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α] [IsEmpty α], ¬G.IsHamiltonian
-- Mathlib.Order.WithBot
WithTop.canLift : ∀ {α : Type u_1}, CanLift (WithTop α) α WithTop.some fun r => r ≠ ⊤
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `grind.debug` is set  -/
Lean.Meta.Grind.isDebugEnabled : Lean.Meta.Grind.GrindM Bool
-- Init.Data.Iterators.Consumers.Access
/-- If possible, takes `n` steps with the iterator `it` and
returns the `n`-th emitted value, or `none` if `it` finished
before emitting `n` values.

This variant terminates after finitely many steps and requires a proof that the iterator is
productive. If such a proof is not available, consider using `Iter.toArray`.
 -/
Std.Iter.Total.atIdxSlow? : {α β : Type u_1} → [inst : Std.Iterator α Id β] → [Std.Iterators.Productive α Id] → ℕ → Std.Iter.Total β → Option β
-- Batteries.Util.ProofWanted
def_wanted.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.neg_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) {m : ℕ}
  (β : CategoryTheory.Abelian.Ext Y Z m) {p : ℕ} (h : n + m = p), (-α).comp β h = -α.comp β h
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.map_coe : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : SSet.RelativeMorphism A B φ)
  {n : SimplexCategoryᵒᵖ} (a : ↑(A.obj n)),
  (CategoryTheory.ConcreteCategory.hom (f.map.app n)) ↑a = ↑((CategoryTheory.ConcreteCategory.hom (φ.app n)) a)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α} {h : k ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l)[k] = ()
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainAlgHom_id : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M], AddMonoidAlgebra.mapDomainAlgHom R A (AddMonoidHom.id M) = AlgHom.id R (AddMonoidAlgebra A M)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddMonCat)
-- Mathlib.Analysis.Normed.Order.UpperLower
IsUpperSet.cthickening' : ∀ {α : Type u_1} [inst : NormedCommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α},
  IsUpperSet s → ∀ (ε : ℝ), IsUpperSet (Metric.cthickening ε s)
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.mk.inj : ∀ {α : Type u} {β : α → Type v} {l l_1 : Std.DHashMap.Internal.AssocList α β}, { l := l } = { l := l_1 } → l = l_1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  ProfiniteGrp.limitCone F =
    {
      pt :=
        ProfiniteGrp.ofProfinite
          (Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite))).pt,
      π :=
        { app := fun j => { hom' := { toFun := fun x => ↑x j, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } },
          naturality := ⋯ } }
-- Mathlib.Topology.Closure
/-- **Alias** of the forward direction of `dense_iff_inter_open`.

---

A set is dense if and only if it has a nonempty intersection with each nonempty open set.  -/
Dense.inter_open_nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_mk : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃ[𝕜] P₂)
  (he : ∀ (x : V), ‖e.linear x‖ = ‖x‖), ⇑{ toAffineEquiv := e, norm_map := he } = ⇑e
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.neg_pos_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_of_neg_pos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, 0 < -a → a < 0
-- Mathlib.RingTheory.Ideal.Maps
Ideal.IsMaximal.map_of_surjective_of_ker_le : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {f : F},
  Function.Surjective ⇑f → ∀ {m : Ideal R} [m.IsMaximal], RingHom.ker f ≤ m → (Ideal.map f m).IsMaximal
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.csSup_le_iff : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddAbove s → s.Nonempty → (sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given `α : F ⟶ L ⋙ F'`, the property `F'.IsLeftKanExtension α` asserts that
`(F', α)` is an initial object in the category `LeftExtension L F`, i.e. that `(F', α)`
is a left Kan extension of `F` along `L`.  -/
CategoryTheory.Functor.IsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} → {F : CategoryTheory.Functor C H} → (F ⟶ L.comp F') → Prop
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- Given a functor `F : C ⥤ H`, and a localization functor `L : C ⥤ D` for `W`,
this is the right derived functor `D ⥤ H` of `F`, i.e. the left Kan extension
of `F` along `L`.  -/
CategoryTheory.Functor.totalRightDerived : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (F : CategoryTheory.Functor C H) →
              (L : CategoryTheory.Functor C D) →
                (W : CategoryTheory.MorphismProperty C) →
                  [L.IsLocalization W] → [F.HasRightDerivedFunctor W] → CategoryTheory.Functor D H
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.adaptRhs : (Lean.Term → Lean.Elab.TermElabM Lean.Term) →
  Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT_I : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n : ℕ∞) (l : ℕ), (Topology.RelCWComplex.skeletonLT C n).I l = {x | ↑l < n}
-- Mathlib.Order.UpperLower.Closure
lowerClosure.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), lowerClosure s = { carrier := {x | ∃ a ∈ s, x ≤ a}, lower' := ⋯ }
-- Mathlib.Computability.Primrec.Basic
Primrec.fin_val : ∀ {n : ℕ}, Primrec fun i => ↑i
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.nnnorm_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  ‖a‖₊ = ‖DoubleCentralizer.toProdHom a‖₊
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.replaceHead.eq_2 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 : ι) (x_2 : M x) (x_3 : x_2 ≠ 1) (j k : ι)
  (hne : j ≠ k) (w₁ : Monoid.CoprodI.NeWord M x j) (w₂ : Monoid.CoprodI.NeWord M k x_1),
  Monoid.CoprodI.NeWord.replaceHead x_2 x_3 (w₁.append hne w₂) =
    (Monoid.CoprodI.NeWord.replaceHead x_2 x_3 w₁).append hne w₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.ofList_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {l : List (α × β)},
  (Std.DHashMap.Const.ofList l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.map_snd_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν],
  MeasureTheory.Measure.map Prod.snd (μ.prod ν) = μ Set.univ • ν
-- Mathlib.Data.NNReal.Defs
/-- Coercion `ℝ≥0 → ℝ`.  -/
NNReal.toReal : NNReal → ℝ
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- Functoriality of `connectedComponents`  -/
Continuous.connectedComponentsMap : {α : Type u} →
  [inst : TopologicalSpace α] →
    {β : Type u_3} →
      [inst_1 : TopologicalSpace β] → {f : α → β} → Continuous f → ConnectedComponents α → ConnectedComponents β
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.closure_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] {s t : Set M},
  s ⊆ t → SubAddAction.closure R s ≤ SubAddAction.closure R t
-- Mathlib.Algebra.Polynomial.CoeffMem
_private.Mathlib.Algebra.Polynomial.CoeffMem.0.Polynomial.«termCoeffs(_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C},
  (∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g],
      CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G) →
    CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G
-- Mathlib.Topology.MetricSpace.Isometry
/-- A uniform embedding from a uniform space to a metric space is an isometry with respect to the
induced metric space structure on the source space.  -/
IsUniformEmbedding.to_isometry : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : MetricSpace β] {f : α → β} (h : IsUniformEmbedding f),
  Isometry f
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftToTerminal_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z)
  {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.liftToTerminal F hZ).map f =
    match X, Y, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      F.map (CategoryTheory.WithTerminal.down f)
    | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => hZ.from (F.obj x)
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
-- Init.Data.Nat.ToString
Nat.eight_eq_digitChar : ∀ {n : ℕ}, '8' = n.digitChar ↔ n = 8
-- Mathlib.GroupTheory.Congruence.Basic
Con.coe_smul : ∀ {α : Type u_4} {M : Type u_5} [inst : MulOneClass M] [inst_1 : SMul α M] [inst_2 : IsScalarTower α M M] (c : Con M)
  (a : α) (x : M), ↑(a • x) = a • ↑x
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformly_iff_forall_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι},
  TendstoLocallyUniformly F f p ↔ ∀ (x : α), Filter.Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)
-- Mathlib.Algebra.Order.Invertible
pos_invOf_of_invertible_cast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (n : ℕ) [inst_3 : Invertible ↑n],
  0 < ⅟↑n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β) (e_m : m = m_1) (a : α) (hma : m.contains a = true),
  m.get a hma = m_1.get a ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKey!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.contains k = true → (cmp k t.maxKey!).isLE = true
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod.unsafe_impl_5 : Lean.ModuleData × Lean.CompactedRegion → System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.tail_transpose : ∀ {α : Type u} {n : ℕ} {m' : Type uₘ} (A : Matrix m' (Fin n.succ) α),
  Matrix.vecTail (Matrix.of.symm A.transpose) = Matrix.transpose (Matrix.vecTail ∘ A)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.mutuallySingularSetSlice.eq_1 : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α),
  κ.mutuallySingularSetSlice η a = {x | 1 ≤ κ.rnDerivAux (κ + η) a x}
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_nonpos : ∀ {K : Type u_1} [inst : RCLike K] {x : ℝ}, ↑x ≤ 0 ↔ x ≤ 0
-- Mathlib.Order.Category.HeytAlg
HeytAlg.Iso.mk_inv : ∀ {α β : HeytAlg} (e : ↑α ≃o ↑β),
  (HeytAlg.Iso.mk e).inv =
    HeytAlg.ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomologicalComplex.liftCycles.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0),
  K.liftCycles k j hj hk = (K.sc i).liftCycles k ⋯
-- Mathlib.Topology.Algebra.Ring.Ideal
topologicalRingQuotientTopology : {R : Type u_1} → [TopologicalSpace R] → [inst : CommRing R] → (N : Ideal R) → TopologicalSpace (R ⧸ N)
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center_sum : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_2} [inst_1 : AddZeroClass N],
  AddSubmonoid.center (M × N) = (AddSubmonoid.center M).prod (AddSubmonoid.center N)
-- Mathlib.Topology.Order.DenselyOrdered
/-- `Set.Ico a b` is only closed if it is empty.  -/
isClosed_Ico_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  IsClosed (Set.Ico a b) ↔ b ≤ a
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.instModule : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} → [inst : Semiring R] → [inst_1 : Semiring S] → [Module R S] → Module R (MonoidAlgebra S M)
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.isCyclotomicExtension : ∀ (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [IsDomain A] [IsFractionRing A K] [NeZero ↑n], IsCyclotomicExtension {n} A (CyclotomicRing n A K)
-- Lean.Elab.Do.Basic
/-- Create a fresh `α` that would fit in `m α`.  -/
Lean.Elab.Do.mkFreshResultType : optParam Lean.Name `α → optParam Lean.MetavarKind Lean.MetavarKind.natural → Lean.Elab.Do.DoElabM Lean.Expr
-- Lean.Syntax
/-- Compares syntax structures and position ranges, but not whitespace. We generally assume that if
syntax trees equal in this way generate the same elaboration output, including positions contained
in e.g. diagnostics and the info tree. However, as we have a few request handlers such as `goalsAt?`
that are sensitive to whitespace information in the info tree, we currently use `eqWithInfo` instead
for reuse checks.
 -/
Lean.Syntax.structRangeEq : Lean.Syntax → Lean.Syntax → Bool
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.orderOf_frobeniusAlgHom : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [Finite L], orderOf (FiniteField.frobeniusAlgHom K L) = Module.finrank K L
-- Mathlib.Control.Fold
Monoid.Foldl.ofFreeMonoid.eq_1 : ∀ {α β : Type u} (f : β → α → β),
  Monoid.Foldl.ofFreeMonoid f =
    { toFun := fun xs => MulOpposite.op (TypeCat.ofHom (flip (List.foldl f) (FreeMonoid.toList xs))), map_one' := ⋯,
      map_mul' := ⋯ }
-- Init.Data.Nat.Basic
Nat.add_le_add : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → a + c ≤ b + d
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.isBounded_iff_bddBelow_bddAbove : ∀ {α : Type u_1} {inst : Bornology α} {inst_1 : Preorder α} [self : IsOrderBornology α] (s : Set α),
  Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.ortho_smul_left : ∀ {K : Type u_13} {K₁ : Type u_14} {K₂ : Type u_15} {V : Type u_16} {V₁ : Type u_17} {V₂ : Type u_18} [inst : Field K]
  [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : Field K₁] [inst_4 : AddCommGroup V₁] [inst_5 : Module K₁ V₁]
  [inst_6 : Field K₂] [inst_7 : AddCommGroup V₂] [inst_8 : Module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K}
  {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V} {x : V₁} {y : V₂} {a : K₁}, a ≠ 0 → (B.IsOrtho x y ↔ B.IsOrtho (a • x) y)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_iff_exists_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ : P}, p₁ ∈ s → (s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
-- Mathlib.Order.Monotone.Defs
antitoneOn_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {c : β} {s : Set α}, AntitoneOn (fun x => c) s
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.setLIntegral_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  Measurable f → ∀ {s : Set α}, MeasurableSet s → ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_of_map_neZero : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β}, NeZero (MeasureTheory.Measure.map f μ) → AEMeasurable f μ
-- Mathlib.Analysis.Convex.Intrinsic
/-- Naturality of intrinsic frontier under a map whose induced map on affine spans is a
homeomorphism. It is introduced here to share the proof of the affine equivalence and affine
isometry versions below.  -/
_private.Mathlib.Analysis.Convex.Intrinsic.0.intrinsicFrontier_image_of_homeomorph_affineSpan : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module 𝕜 W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f : P → Q} {s : Set P}
  (e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))),
  (∀ [inst_9 : Nonempty ↑s], IsHomeomorph e) →
    (∀ [inst_9 : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x) →
      intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s
-- Mathlib.Data.List.Sublists
List.length_sublists' : ∀ {α : Type u} (l : List α), l.sublists'.length = 2 ^ l.length
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_toNonneg : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : SemilatticeSup α] {a : α}, ↑(Nonneg.toNonneg a) = a ⊔ 0