mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.WSeq.Defs
_private.Mathlib.Data.WSeq.Defs.0.Stream'.WSeq.length.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (s' : Stream'.Seq (Option α))
  (h_1 : Unit → motive none) (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (val : α) → (s' : Stream'.Seq (Option α)) → motive (some (some val, s'))),
  (match some (none, s') with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some val, s') => h_3 val s') =
    h_2 s'
-- Mathlib.Algebra.BigOperators.Finprod
/-- Monotonicity of `finprod`. See `finprod_le_finprod` for a variant where
`M` is a `CommMonoidWithZero`.  -/
finprod_le_finprod' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M} [inst_1 : PartialOrder M] [MulLeftMono M],
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → f ≤ g → ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_noncommProd_right : ∀ {α : Type u_1} {g : Equiv.Perm α} {ι : Type u_2} {k : ι → Equiv.Perm α} {s : Finset ι}
  (hs : (↑s).Pairwise fun i j => Commute (k i) (k j)), (∀ i ∈ s, g.Disjoint (k i)) → g.Disjoint (s.noncommProd k hs)
-- Mathlib.Logic.Embedding.Set
Equiv.asEmbedding_range : ∀ {α : Sort u_1} {β : Type u_2} {p : β → Prop} (e : α ≃ Subtype p), Set.range ⇑e.asEmbedding = Set.ofPred p
-- Mathlib.Algebra.Group.Action.Defs
SMul.comp.eq_1 : ∀ {M : Type u_1} {N : Type u_2} (α : Type u_5) [inst : SMul M α] (g : N → M),
  SMul.comp α g = { smul := SMul.comp.smul g }
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.exists_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (X : D), ∃ f, CategoryTheory.Epi f
-- Mathlib.Data.Tree.Basic
BinaryTree.left.eq_1 : ∀ {α : Type u}, BinaryTree.nil.left = BinaryTree.nil
-- Init.WFComputable
Acc.ndrecOnC.eq_1 : ∀ {α : Sort u_1} {r : α → α → Prop} {C : α → Sort v} {a : α} (n : Acc r a)
  (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x), n.ndrecOnC m = Acc.recC m n
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandSuffices : Lean.Macro
-- Std.Data.TreeMap.Basic
/-- Computes the intersection of the given tree maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map.
 -/
Std.TreeMap.inter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.TreeMap α β cmp → Std.TreeMap α β cmp
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsFiniteKernel.comapRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : γ → β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ]
  (hf : MeasurableEmbedding f), ProbabilityTheory.IsFiniteKernel (κ.comapRight hf)
-- Mathlib.Tactic.FunProp.Theorems
/-- Composition theorem e.g. `Continuous f → Continuous g → Continuous fun x ↦ f (g x)`  -/
Mathlib.Meta.FunProp.LambdaTheoremType.comp : Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Data.Set.Lattice
Set.iUnion_dite : ∀ {α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [inst : DecidablePred p] (f : (i : ι) → p i → Set α)
  (g : (i : ι) → ¬p i → Set α),
  (⋃ i, if h : p i then f i h else g i h) = (⋃ i, ⋃ (h : p i), f i h) ∪ ⋃ i, ⋃ (h : ¬p i), g i h
-- Mathlib.Order.Heyting.Basic
ofDual_sdiff : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : αᵒᵈ),
  OrderDual.ofDual (a \ b) = OrderDual.ofDual b ⇨ OrderDual.ofDual a
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.algebraMap_mk_of_liesOver : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] (x : A),
  (algebraMap (A ⧸ p) (B ⧸ P)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk P) ((algebraMap A B) x)
-- Std.Data.DTreeMap.Internal.Balanced
/-- Inner node is balanced if it is locally balanced, both children are balanced and size
information is correct.
 -/
Std.DTreeMap.Internal.Impl.Balanced.inner : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size →
        sz = l.size + 1 + r.size → (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.ofSubsingletonₗᵢ_apply : ∀ (𝕜 : Type u) {ι : Type v} (G : Type wG) {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G']
  [inst_4 : NormedSpace 𝕜 G'] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (a : G →L[𝕜] G'),
  (ContinuousMultilinearMap.ofSubsingletonₗᵢ 𝕜 G i) a = (ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i).toFun a
-- Mathlib.Data.Nat.Cast.Basic
/-- `Nat.cast : ℕ → α` as an `AddMonoidHom`.  -/
Nat.castAddMonoidHom : (α : Type u_3) → [inst : AddMonoidWithOne α] → ℕ →+ α
-- Mathlib.NumberTheory.MahlerMeasure
/-- If an integer polynomial has Mahler measure equal to 1, then all its complex nonzero roots are
roots of unity.  -/
Polynomial.isPrimitiveRoot_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 →
    ∀ {z : ℂ}, z ≠ 0 → z ∈ p.aroots ℂ → ∃ n, 0 < n ∧ IsPrimitiveRoot z n
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_pow : ∀ {α : Type u_1} (P : RegularExpression α) (n : ℕ), (P ^ n).matches' = P.matches' ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasSum_fintype_support : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Fintype β] (f : β → α)
  (L : SummationFilter β) [L.HasSupport] [inst_4 : DecidablePred fun x => x ∈ L.support],
  HasSum f (∑ b ∈ L.support.toFinset, f b) L
-- Mathlib.RingTheory.Localization.FractionRing
/-- `AlgHom` version of `IsFractionRing.lift`.  -/
IsFractionRing.liftAlgHom : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_4} →
      [inst_1 : CommRing A] →
        {K : Type u_5} →
          [inst_2 : Field K] →
            {L : Type u_7} →
              [inst_3 : Field L] →
                [inst_4 : Algebra A K] →
                  [IsFractionRing A K] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Algebra R K] →
                        [IsScalarTower R A K] →
                          [inst_9 : Algebra R L] → {g : A →ₐ[R] L} → Function.Injective ⇑g → K →ₐ[R] L
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] [inst_1 : Zero β] {x : MeasurableSpace α} (f : α → β)
  (μ : MeasureTheory.Measure α),
  MeasureTheory.AEFinStronglyMeasurable f μ = ∃ g, MeasureTheory.FinStronglyMeasurable g μ ∧ f =ᵐ[μ] g
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : ℝ → F` on `f '' s` coincides with the integral of `(-f' x) • g ∘ f` on `s` .  -/
MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitoneOn : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      AntitoneOn f s → ∀ (g : ℝ → F), ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, -f' x • g (f x)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.LazyEntry.mk.inj : ∀ {previous : Option Lean.Meta.RefinedDiscrTree.ExprInfo} {stack : List Lean.Meta.RefinedDiscrTree.StackEntry}
  {mctx : Lean.MetavarContext} {labelledStars? : Option (Array Lean.MVarId)}
  {computedKeys : List Lean.Meta.RefinedDiscrTree.Key} {previous_1 : Option Lean.Meta.RefinedDiscrTree.ExprInfo}
  {stack_1 : List Lean.Meta.RefinedDiscrTree.StackEntry} {mctx_1 : Lean.MetavarContext}
  {labelledStars?_1 : Option (Array Lean.MVarId)} {computedKeys_1 : List Lean.Meta.RefinedDiscrTree.Key},
  { previous := previous, stack := stack, mctx := mctx, labelledStars? := labelledStars?,
        computedKeys := computedKeys } =
      { previous := previous_1, stack := stack_1, mctx := mctx_1, labelledStars? := labelledStars?_1,
        computedKeys := computedKeys_1 } →
    previous = previous_1 ∧
      stack = stack_1 ∧ mctx = mctx_1 ∧ labelledStars? = labelledStars?_1 ∧ computedKeys = computedKeys_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.HoverParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.Analysis.Normed.Group.Hom
/-- Normed group homomorphisms themselves form a normed group with respect to
the operator norm.  -/
NormedAddGroupHom.toNormedAddCommGroup : {V₁ : Type u_5} →
  {V₂ : Type u_6} →
    [inst : NormedAddCommGroup V₁] → [inst_1 : NormedAddCommGroup V₂] → NormedAddCommGroup (NormedAddGroupHom V₁ V₂)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Submodule.coe_toNonUnitalSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p), ↑(p.toNonUnitalSubalgebra h_mul) = ↑p
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_comp_rename_inl : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R],
  (↑(MvPolynomial.sumAlgEquiv R S₁ S₂)).comp (MvPolynomial.rename Sum.inl) =
    MvPolynomial.mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_leftUnitor_hom : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {L : CategoryTheory.Functor A B} {R : CategoryTheory.Functor B A} (adj : L ⊣ R),
  (CategoryTheory.conjugateEquiv adj (CategoryTheory.Adjunction.id.comp adj)) L.leftUnitor.hom = R.rightUnitor.inv
-- Mathlib.Analysis.Calculus.VectorField
VectorField.fderivWithin_pullbackWithin : ∀ {𝕜 : 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] {s : Set E}
  {f : E → F} {V : F → F} {x : E},
  (fderivWithin 𝕜 f s x).IsInvertible → (fderivWithin 𝕜 f s x) (VectorField.pullbackWithin 𝕜 f V s x) = V (f x)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.str : (self : Semigrp) → Semigroup ↑self
-- Lean.Compiler.LCNF.Basic
/-- Traverse the given block of potentially mutually recursive functions
and mark a declaration `f` as recursive if there is an application
`f ...` in the block.
This is an overapproximation, and relies on the fact that our frontend
computes strongly connected components.
See comment at `recursive` field.
 -/
Lean.Compiler.LCNF.markRecDecls : {pu : Lean.Compiler.LCNF.Purity} → Array (Lean.Compiler.LCNF.Decl pu) → Array (Lean.Compiler.LCNF.Decl pu)
-- Mathlib.Data.Num.Lemmas
Num.succ'.eq_1 : Num.zero.succ' = 1
-- Mathlib.Algebra.DirectSum.Basic
/-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence
`h : ι ≃ κ`.  -/
DirectSum.equivCongrLeft : {ι : Type v} →
  {β : ι → Type w} →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      {κ : Type u_1} → (h : ι ≃ κ) → (DirectSum ι fun i => β i) ≃+ DirectSum κ fun k => β (h.symm k)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The underlying expression of the node.  -/
Mathlib.Tactic.Widget.StringDiagram.AtomNode.atom : Mathlib.Tactic.Widget.StringDiagram.AtomNode → Mathlib.Tactic.BicategoryLike.Atom
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_injective : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W), Function.Injective (SimpleGraph.map ⇑f)
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Extend the domain of `α` from `Icc tmin tmax` to `ℝ` such that `α t = α tmin` for all `t ≤ tmin`
and `α t = α tmax` for all `t ≥ tmax`.  -/
ODE.FunSpace.compProj : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} → {t₀ : ↑(Set.Icc tmin tmax)} → {x₀ : E} → {r L : NNReal} → ODE.FunSpace t₀ x₀ r L → ℝ → E
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_right_cancel : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [IsRightCancelAdd α], z ≠ ⊥ → x + z = y + z → x = y
-- Batteries.Data.List.Interleave
List.IsPrefix.interleave : ∀ {α : Type u_1} {l₁ l₃ l₂ l₄ : List α},
  l₁.length = l₂.length ∨ l₁.length = l₂.length + 1 → l₁ <+: l₃ → l₂ <+: l₄ → l₁.interleave l₂ <+: l₃.interleave l₄
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.Integrable.condExpKernel_ae : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F},
  MeasureTheory.Integrable f μ → ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.Integrable f ((ProbabilityTheory.condExpKernel μ m) ω)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.pow_one_eq_id : ArithmeticFunction.pow 1 = ArithmeticFunction.id
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.State.mk.sizeOf_spec : ∀ (structs : Array Lean.Meta.Grind.Arith.Linear.Struct) (typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (exprToStructIdEntries : Lean.PArray (Lean.Expr × ℕ))
  (forbiddenNatModules : Lean.PHashSet Lean.Meta.Sym.ExprPtr)
  (natStructs : Array Lean.Meta.Grind.Arith.Linear.NatStruct)
  (natTypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToNatStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ),
  sizeOf
      { structs := structs, typeIdOf := typeIdOf, exprToStructId := exprToStructId,
        exprToStructIdEntries := exprToStructIdEntries, forbiddenNatModules := forbiddenNatModules,
        natStructs := natStructs, natTypeIdOf := natTypeIdOf, exprToNatStructId := exprToNatStructId } =
    1 + sizeOf structs + sizeOf typeIdOf + sizeOf exprToStructId + sizeOf exprToStructIdEntries +
            sizeOf forbiddenNatModules +
          sizeOf natStructs +
        sizeOf natTypeIdOf +
      sizeOf exprToNatStructId
-- Mathlib.Data.Sum.Basic
Function.Surjective.sumMap : ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'},
  Function.Surjective f → Function.Surjective g → Function.Surjective (Sum.map f g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ofList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {k : α} {v : β},
  Std.DTreeMap.Const.ofList [(k, v)] cmp = ∅.insert k v
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C),
  (β_ X₁ X₂).inv.left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).inv
      (CategoryTheory.Limits.pushoutSymmetry (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom)).inv
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_sub_left : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a b : E), dist (a - b) a = ‖b‖
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- The (sup metric) distance between `Pi.single i a` and `Pi.single j b` for
`i ≠ j` is `max (dist a 0) (dist b 0)`.  -/
dist_single_single : ∀ {β : Type u_2} [inst : Fintype β] {Y : Type u_4} [inst_1 : PseudoMetricSpace Y] [inst_2 : Zero Y]
  [inst_3 : DecidableEq β] (i j : β) (a b : Y), i ≠ j → dist (Pi.single i a) (Pi.single j b) = max (dist a 0) (dist b 0)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k l₁ = false →
    Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) = false
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α} {v : β},
  Array.find? (fun x => cmp x.1 k == Ordering.eq) t.toArray = some (k', v) ↔ t.getKey? k = some k' ∧ t[k]? = some v
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The sequence of norms of `x : lp E p` as a term of `ℓ^p(α, ℝ)`. Here `E : α → Type*`
is a dependent type and `ℓ^p(α, ℝ)` is the non-dependent `ℝ`-valued `lp` space.  -/
lp.toNorm : {α : Type u_3} →
  {E : α → Type u_4} → [inst : (i : α) → NormedAddCommGroup (E i)] → {p : ENNReal} → ↥(lp E p) → ↥(lp (fun x => ℝ) p)
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_one : ∀ (α : Type u), ↑1 = 1
-- Mathlib.Data.Seq.Computation
Computation.Results.mem : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.Results a n → a ∈ s
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_univ_right : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] [inst_2 : Fintype α] (s : Finset α),
  s.addEnergy Finset.univ = Fintype.card α * s.card ^ 2
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- If `s ⊆ t` are subsets in an `R`-algebra `A` such that `s` is algebraically independent over
`R`, and `A` is algebraic over the `R`-algebra generated by `t`, then there is a transcendence
basis of `A` over `R` between `s` and `t`, provided that `A` is a domain.

This may fail if only `R` is assumed to be a domain but `A` is not, because of failure of
transitivity of algebraicity: there may exist `a : A` such that `S := R[a]` is algebraic over
`R` and `A` is algebraic over `S`, but `A` nonetheless contains a transcendental element over `R`.
The only `R`-algebraically independent subset of `{a}` is `∅`, which is not a transcendence basis.
See the docstring of `IsAlgebraic.restrictScalars_of_isIntegral` for an example.  -/
exists_isTranscendenceBasis_between : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [NoZeroDivisors A]
  (s t : Set A),
  s ⊆ t →
    AlgebraicIndepOn R id s →
      ∀ [ht : Algebra.IsAlgebraic (↥(Algebra.adjoin R t)) A], ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
-- Mathlib.Computability.Language
Language.reverse_mem_reverse : ∀ {α : Type u_1} {l : Language α} {a : List α}, a.reverse ∈ l.reverse ↔ a ∈ l
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_of_finite : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [Finite G], H.FiniteIndex
-- Mathlib.Data.FP.Basic
FP.FloatCfg.prec : [self : FP.FloatCfg] → ℕ
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitRightBracket : Lean.Parser.Parser
-- Mathlib.Algebra.Star.Basic
/-- Any commutative semiring admits the trivial \*-structure.

See note [reducible non-instances].
 -/
starRingOfComm : {R : Type u_1} → [inst : CommSemiring R] → StarRing R
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
MulEquiv.hasEnoughRootsOfUnity : ∀ {n : ℕ} [NeZero n] {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst_1 : CommMonoid N]
  [hm : HasEnoughRootsOfUnity M n] (e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)), HasEnoughRootsOfUnity N n
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- If `Q : M → N` is a quadratic map of `R`-modules and `R` is an `S`-algebra,
then the restriction of scalars is a quadratic map of `S`-modules.  -/
QuadraticMap.restrictScalars : {S : Type u_1} →
  {R : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module S M] →
                      [inst_7 : Module S N] →
                        [inst_8 : Algebra S R] →
                          [IsScalarTower S R M] → [IsScalarTower S R N] → QuadraticMap R M N → QuadraticMap S M N
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.max!.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (x : α) → motive (some x)),
  (match none with
    | none => h_1 ()
    | some x => h_2 x) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
CategoryTheory.bijection_natural : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory D] [inst_6 : CategoryTheory.ExponentialIdeal i]
  [inst_7 : CategoryTheory.BraidedCategory C] (A B : C) (X X' : D)
  (f : (CategoryTheory.reflector i).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B) ⟶ X) (g : X ⟶ X'),
  (CategoryTheory.bijection i A B X') (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.bijection i A B X) f) g
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone is flat if it contains some nonzero vector `x` and its opposite `-x`.  -/
ConvexCone.Flat : {R : Type u_2} →
  {G : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommGroup G] → [inst_3 : SMul R G] → ConvexCone R G → Prop
-- Std.Sat.AIG.RelabelNat
/-- Proof that we inserted all atoms until `idx`.
 -/
Std.Sat.AIG.RelabelNat.State.inv2 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  (self : Std.Sat.AIG.RelabelNat.State α decls idx), Std.Sat.AIG.RelabelNat.State.Inv2 decls idx self.map
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.vonStaudtIndicator : ℕ → ℕ → ℚ
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctor_δ : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N) (m₁ m₂ : CategoryTheory.Discrete M),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Discrete.monoidalFunctor F) m₁ m₂ =
    CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.Data.Seq.Defs
Stream'.Seq.ext_iff : ∀ {α : Type u} {s t : Stream'.Seq α}, s = t ↔ ∀ (n : ℕ), s.get? n = t.get? n
-- Init.Data.BitVec.Basic
/-- Checks whether the subtraction of `x` and `y` results in *signed* overflow, treating `x` and `y` as
2's complement signed bitvectors.

SMT-Lib name: `bvssubo`.
 -/
BitVec.ssubOverflow : {w : ℕ} → BitVec w → BitVec w → Bool
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveCoyoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : Cᵒᵖ),
  CategoryTheory.preadditiveCoyoneda.obj X =
    (CategoryTheory.preadditiveCoyonedaObj (Opposite.unop X)).comp
      (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End (Opposite.unop X))ᵐᵒᵖ) AddCommGrpCat)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.summand_bound_of_mem_verticalStrip : ∀ {z : UpperHalfPlane} {k : ℝ},
  0 ≤ k →
    ∀ (x : Fin 2 → ℤ) {A B : ℝ} (hB : 0 < B),
      z ∈ UpperHalfPlane.verticalStrip A B →
        ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤
          EisensteinSeries.r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-k) * ‖x‖ ^ (-k)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkReturn : Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.CodeBlock