mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
FractionalIdeal.absNorm.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K]
  [inst_6 : IsFractionRing R K], FractionalIdeal.absNorm = FractionalIdeal.absNorm
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- A *bi-Cartesian* square is a commutative square
```
  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

```
that is both a pullback square and a pushout square.
 -/
CategoryTheory.BicartesianSq : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {W X Y Z : C} → (W ⟶ X) → (W ⟶ Y) → (X ⟶ Z) → (Y ⟶ Z) → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.return.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId),
  sizeOf (Lean.Compiler.LCNF.Code.return fvarId) = 1 + sizeOf fvarId
-- Lean.Elab.Term.TermElabM
/-- Create an `Expr.const` using the given name and explicit levels.
Remark: fresh universe metavariables are created if the constant has more universe
parameters than `explicitLevels`.

If `checkDeprecated := true`, then `Linter.checkDeprecated` is invoked.
 -/
Lean.Elab.Term.mkConst : Lean.Name → optParam (List Lean.Level) [] → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.inftyNormedCommRing : {I : Type u_5} →
  {B : I → Type u_6} →
    [inst : (i : I) → NormedCommRing (B i)] → [∀ (i : I), NormOneClass (B i)] → NormedCommRing ↥(lp B ⊤)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldRev.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : (i : ℕ) → i < x → α → α) (x_2 : α),
  x.foldRev x_1 x_2 =
    match x, x_1, x_2 with
    | 0, f, a => a
    | n.succ, f, a => n.foldRev (fun i h => f i ⋯) (f n ⋯ a)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.liftCone_π_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : D ⟶ (CategoryTheory.Functor.const J).obj X) (c : CategoryTheory.Limits.Cone D) (p : c.pt ⟶ X)
  (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.π.app j) (s.app j) = p) (j : J),
  (CategoryTheory.Over.liftCone D s c p hp).π.app j = CategoryTheory.Over.homMk (c.π.app j) ⋯
-- Mathlib.Data.Finset.Density
Finset.dens_pos : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α}, 0 < s.dens ↔ s.Nonempty
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.ssubset_toFinset : ∀ {α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α}, s ⊂ ht.toFinset ↔ ↑s ⊂ t
-- Init.Grind.Offset
Lean.Grind.Nat.lo_eq_false_of_le : ∀ (u v k : ℕ), Lean.Grind.isLt 0 k = true → u ≤ v → (v + k ≤ u) = False
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)<...Std.PRange.succ hi).toList = List.map Std.PRange.succ (lo<...hi).toList
-- Mathlib.Dynamics.Ergodic.Function
/-- Let `f : α → α` be an ergodic map.
Let `g : α → X` be a null-measurable function from `α` to a nonempty measurable space
with a countable family of measurable sets separating the points of `X`.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant.  -/
Ergodic.ae_eq_const_of_ae_eq_comp₀ : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X]
  [inst_2 : MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : α → α} {g : α → X},
  Ergodic f μ → MeasureTheory.NullMeasurable g μ → g ∘ f =ᵐ[μ] g → ∃ c, g =ᵐ[μ] Function.const α c
-- Mathlib.LinearAlgebra.LinearPMap
/-- The graph of `-f` as a pushforward.  -/
LinearPMap.neg_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F),
  (-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_le_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupSeminorm E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β), (↑m).isEmpty = ((↑m).size == 0)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_pos : ∀ {ι : Type u_3} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {f : ι → M}, (∀ (i : ι), 0 ≤ f i) → (∃ i, 0 < f i) → Function.HasFiniteSupport f → 0 < ∑ᶠ (i : ι), f i
-- Lean.LocalContext
/-- Low level API for let declarations. Do not use directly. -/
Lean.LocalContext.mkLetDecl : Lean.LocalContext →
  Lean.FVarId →
    Lean.Name → Lean.Expr → Lean.Expr → optParam Bool false → optParam Lean.LocalDeclKind default → Lean.LocalContext
-- Mathlib.Tactic.MinImports
/-- `minImpsCore stx id` is the internal function to elaborate the `#min_imports in` command.
It collects the irredundant imports to parse and elaborate `stx` and logs
```lean
import A
import B
...
import Z
```
The `id` input is expected to be the name of the declaration that is currently processed.
It is used to provide the internally generated name for "nameless" `instance`s.
 -/
Mathlib.Command.MinImports.minImpsCore : Lean.Syntax → Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_le_maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t.isEmpty = false}, (cmp (t.maxKey he) ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ).op S₁.opcyclesOpIso.inv =
    CategoryTheory.CategoryStruct.comp S₂.opcyclesOpIso.inv
      (CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.ShortComplex.opMap φ))
-- Mathlib.Algebra.Opposites
MulOpposite.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited αᵐᵒᵖ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_exact._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticStx.inj : ∀ {stx stx_1 : Lean.Syntax}, Aesop.RuleTacDescr.tacticStx stx = Aesop.RuleTacDescr.tacticStx stx_1 → stx = stx_1
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- The multiplicative indicators of δ-thickenings of a set tend pointwise to the multiplicative
indicator of the set, as δ>0 tends to zero.  -/
tendsto_mulIndicator_thickening_mulIndicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] [inst_2 : TopologicalSpace β] (f : α → β)
  (E : Set α),
  Filter.Tendsto (fun δ => (Metric.thickening δ E).mulIndicator f) (nhdsWithin 0 (Set.Ioi 0))
    (nhds ((closure E).mulIndicator f))
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isEmbedding_coeFn : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)), Topology.IsEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_le_iff_of_isSuccLimit : ∀ {a b c : Ordinal.{u_4}}, Order.IsSuccLimit b → (a + b ≤ c ↔ ∀ d < b, a + d ≤ c)
-- Init.Data.Nat.ToString
Nat.digitChar_eq_b : ∀ {n : ℕ}, n.digitChar = 'b' ↔ n = 11
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_id_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (X ⨯ Y)
-- Aesop.Tree.Data
Aesop.instInhabitedIteration : Inhabited Aesop.Iteration
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey? = t.maxKey?
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.mk : {G : Type u} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      (toOpenSubgroup : OpenSubgroup G) →
        autoParam (↑toOpenSubgroup).Normal OpenNormalSubgroup.isNormal'._autoParam → OpenNormalSubgroup G
-- Mathlib.Tactic.ApplyWith
_private.Mathlib.Tactic.ApplyWith.0.Mathlib.Tactic.instEvalExprApplyConfig_mathlib.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.ApplyConfig
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_toLinearMap : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂), ⇑↑f = ⇑f
-- Mathlib.Topology.ContinuousMap.Basic
/-- The constant map as a continuous map.  -/
ContinuousMap.const : (α : Type u_1) → {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → β → C(α, β)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.antilipschitzWith_two_equiv_prod_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  [inst_10 : StarOrderedRing A], AntilipschitzWith 2 ⇑(WithCStarModule.equiv A (E × F))
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a norm, i.e., registering the distance and the metric
space structure from the norm properties. Note that in most cases this instance creates bad
definitional equalities (e.g., it does not take into account a possibly existing `UniformSpace`
instance on `E`).  -/
AddGroupNorm.toNormedAddCommGroup : {E : Type u_5} → [inst : AddCommGroup E] → AddGroupNorm E → NormedAddCommGroup E
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.isIso_prod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.Limits.prod.map f g)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.map_inv : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (A' : Type u_8) [inst_2 : Group A']
  [inst_3 : MulDistribMulAction M A'] (B' : Type u_9) [inst_4 : Group B'] [inst_5 : MulDistribMulAction N B']
  (f : A' →ₑ*[φ] B') (x : A'), f x⁻¹ = (f x)⁻¹
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {S : C} → J.OneHypercover S → CategoryTheory.PreOneHypercover S
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `f a = 0` when `a ∉ s`, then the sum of `f i` over `i ∈ insert a s` equals the sum
of `f i` over `i ∈ s`.  -/
finsum_mem_insert_of_eq_zero_if_notMem : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α} {s : Set α},
  (a ∉ s → f a = 0) → ∑ᶠ (i : α) (_ : i ∈ insert a s), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Init.Data.Int.DivMod.Lemmas
Int.lt_ediv_add_one_mul_self : ∀ (a : ℤ) {b : ℤ}, 0 < b → a < (a / b + 1) * b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.class.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.class = 1
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.alternatingFaceMapComplex_obj_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  ((AlgebraicTopology.alternatingFaceMapComplex C).obj X).d (n + 1) n =
    AlgebraicTopology.AlternatingFaceMapComplex.objD X n
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instLT.eq_1 : ∀ {M : Type u_1} [inst : AddGroup M] [inst_1 : Lattice M],
  ArchimedeanOrder.instLT = { lt := fun a b => ∀ (n : ℕ), n • |ArchimedeanOrder.val b| < |ArchimedeanOrder.val a| }
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
/-- The Jordan decomposition associated to the pair of mutually singular measures `μ - ν`
and `ν - μ`.  -/
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub : {X : Type u_1} →
  {mX : MeasurableSpace X} →
    (μ ν : MeasureTheory.Measure X) →
      [MeasureTheory.IsFiniteMeasure μ] → [MeasureTheory.IsFiniteMeasure ν] → MeasureTheory.JordanDecomposition X
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X : D),
  (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D)).app X =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso X).inv
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.zero_snd : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β], WithLp.snd 0 = 0
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.UniformEquicontinuousOn.mono : ∀ {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {H H' : Set (β → α)} {S : Set β},
  H.UniformEquicontinuousOn S → H' ⊆ H → H'.UniformEquicontinuousOn S
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.All.eq_def : ∀ {α : Type u_1} (p : α → Prop) (x : RBTree.RBNode α),
  RBTree.RBNode.All p x =
    match x with
    | RBTree.RBNode.nil => True
    | RBTree.RBNode.node c l v r => p v ∧ RBTree.RBNode.All p l ∧ RBTree.RBNode.All p r
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.coe_toBoundedContinuousFunction : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  ⇑{ toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } = ⇑f
-- Lean.Declaration
Lean.ConstantInfo.opaqueInfo : Lean.OpaqueVal → Lean.ConstantInfo
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.instInhabitedHomLaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → {F G : CategoryTheory.LaxFunctor B C} → {η : F ⟶ G} → Inhabited (η ⟶ η)
-- Lean.Parser.Level
Lean.Parser.Level.hole : Lean.Parser.Parser
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.compl_is_regular : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V], G.IsSRGWith n k ℓ μ → Gᶜ.IsRegularOfDegree (n - k - 1)
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.coe_parallelepiped : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (b : Module.Basis ι ℝ E), ↑b.parallelepiped = parallelepiped ⇑b
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- The set of measurable sets is measure-dense.  -/
MeasureTheory.measureDense_measurableSet : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X}, μ.MeasureDense {s | MeasurableSet s}
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
/-- Let `K` be a finite field of cardinality `p ^ f` and let `P` be a factor of the `n`-th
cyclotomic polynomial over `K`, where `p` and `n` are coprime. If the degree of `P` is
the multiplicative order of `p ^ f` modulo `n` then `P` is irreducible.  -/
Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ} {P : Polynomial K},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)],
      P ∣ Polynomial.cyclotomic n K → P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯) → Irreducible P
-- Mathlib.Data.Finset.Option
Finset.card_eraseNone_le : ∀ {α : Type u_1} (s : Finset (Option α)), (Finset.eraseNone s).card ≤ s.card
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} (x : α), CategoryTheory.IsFiltered.filteredClosure f (f x)
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.exists_neg : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit a → ∃ b, a + b = 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- A walk with its endpoints defeq is `Nil` if and only if it is equal to `nil`.  -/
SimpleGraph.Walk.eq_nil_iff_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v}, p = SimpleGraph.Walk.nil ↔ p.Nil
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_of_isEmpty : ∀ {ι : Type u_1} {M : Type u_3} {f : ι → M} [inst : CommMonoid M] [IsEmpty ι] (s : Finset ι), ∏ i ∈ s, f i = 1
-- Mathlib.Tactic.Translate.ToAdditive
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.ToAdditive.to_additive_dont_translate : Lean.ParserDescr
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_map : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  {S : NonUnitalStarSubalgebra R A} {f : F} {y : B}, y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constVAdd_symm : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : IsIsometricVAdd G X] (c : G), (IsometryEquiv.constVAdd c).symm = IsometryEquiv.constVAdd (-c)
-- Mathlib.Data.Finset.Prod
Finset.coe_offDiag : ∀ {α : Type u_1} (s : Finset α), ↑s.offDiag = (↑s).offDiag
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolutionExists_right_of_continuous_left : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddCommGroup G]
  [inst_9 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant],
  HasCompactSupport g → Continuous f → MeasureTheory.LocallyIntegrable g μ → MeasureTheory.ConvolutionExists f g L μ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_ne_nil_iff : ∀ {m n : ℕ}, (m...n).toList ≠ [] ↔ m < n
-- Init.Data.String.Basic
String.Pos.le_endPos : ∀ {s : String} (p : s.Pos), p ≤ s.endPos
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents.app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app' : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f) (app' Y).hom =
        CategoryTheory.CategoryStruct.comp (app' X).hom (G.map f))
  (X : C), (CategoryTheory.NatIso.ofComponents app' naturality).app X = app' X
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- It is possible to coerce an object of `C` into an object of `Karoubi C`.
See also the functor `toKaroubi`.  -/
CategoryTheory.Idempotents.Karoubi.coe : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CoeTC C (CategoryTheory.Idempotents.Karoubi C)
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.nextn : ∀ {s t₁ t₂ : String} {p : s.Pos},
  p.Splits t₁ t₂ →
    ∀ (i : ℕ), (p.nextn i).Splits (t₁ ++ String.ofList (List.take i t₂.toList)) (String.ofList (List.drop i t₂.toList))
-- Std.Do.PostCond
Std.Do.ExceptConds.true_and : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, (Std.Do.ExceptConds.true ∧ₑ x).entails x
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
_private.Mathlib.Analysis.Convex.SpecificFunctions.Deriv.0.Nat.iterate.match_1.splitter : {α : Sort u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((a : α) → motive 0 a) → ((k : ℕ) → (a : α) → motive k.succ a) → motive x x_1
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.sl2 : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H) (i : ι),
  IsSl2Triple (self.h i) (self.e i) (self.f i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGE_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, (compare a k).isGE = true},
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.Const.getEntryGE k t₂ ⋯ ⋯
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The space `ℝ^(r₁+r₂) × ℝ^r₂`, it is homeomorphic to the `realMixedSpace`, see
`homeoRealMixedSpacePolarSpace`.
 -/
NumberField.mixedEmbedding.polarSpace : (K : Type u_1) → [Field K] → Type u_1