mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, a ∉ t → t[a]! = default
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f: M → N` and `g: M' → N'` are submersions at `x` and `x'`, respectively,
then `f × g: M × M' → N × N'` is a submersion at `(x, x')`.  -/
Manifold.IsSubmersion.prodMap : ∀ {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {H : Type u_7} {H' : Type u_8} {G : Type u_9}
  {G' : Type u_10} {E : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  [inst_5 : NormedAddCommGroup E''] [inst_6 : NormedSpace 𝕜 E''] [inst_7 : NormedAddCommGroup E''']
  [inst_8 : NormedSpace 𝕜 E'''] [inst_9 : TopologicalSpace H] [inst_10 : TopologicalSpace H']
  [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11}
  {M' : Type u_12} {N : Type u_13} {N' : Type u_14} [inst_13 : TopologicalSpace M] [inst_14 : ChartedSpace H M]
  [inst_15 : TopologicalSpace M'] [inst_16 : ChartedSpace H' M'] [inst_17 : TopologicalSpace N]
  [inst_18 : ChartedSpace G N] [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞}
  {f : M → N} {g : M' → N'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'],
  Manifold.IsSubmersion I J n f →
    Manifold.IsSubmersion I' J' n g → Manifold.IsSubmersion (I.prod I') (J.prod J') n (Prod.map f g)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₈ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] →
      Lean.Expr →
        Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.all.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.all pat = (s.skipPrefixWhile pat == s.endPos)
-- Aesop.Tree.Data
Aesop.Goal.instBEq : BEq Aesop.Goal
-- Mathlib.Data.Stream.Init
Stream'.append_append_stream : ∀ {α : Type u} (l₁ l₂ : List α) (s : Stream' α), l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loopless_iff : ∀ {α : Type u_1} (M : Matroid α), M.Loopless ↔ M.loops = ∅
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux : ∀ {M : Type w} {α : Type u'} {β : Type v'} {n m : ℕ} {g : α → β ⊕ Fin n} {v : β → M} {xs : Fin (n + m) → M},
  Sum.elim v xs ∘ FirstOrder.Language.BoundedFormula.relabelAux g m =
    Sum.elim (Sum.elim v (xs ∘ Fin.castAdd m) ∘ g) (xs ∘ Fin.natAdd n)
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- **Alias** of `ArithmeticFunction.carmichael_finsetProd`. -/
ArithmeticFunction.carmichael_finset_prod : ∀ {α : Type u_2} {s : Finset α} {f : α → ℕ},
  (↑s).Pairwise (Function.onFun Nat.Coprime f) →
    ArithmeticFunction.carmichael (s.prod f) = s.lcm (⇑ArithmeticFunction.carmichael ∘ f)
-- Mathlib.Order.Filter.Pointwise
Filter.div_mem_div : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s / t ∈ f / g
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- This prevents `ofCLM A` being printed as `{ toCLM := x }` by `delabStructureInstance`.  -/
ContinuousLinearMapWOT.delabOfCLM : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Array.Lemmas
Array.foldl_cons_eq_append : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {bs : List β} {f : α → β},
  stop = as.size → Array.foldl (fun acc a => f a :: acc) bs as 0 stop = (Array.map f as).reverse.toList ++ bs
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F], IsUniformEmbedding ContinuousMultilinearMap.toUniformOnFun
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.is_basis : ∀ {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α), TopologicalSpace.IsTopologicalBasis (Set.range F.F.f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l l'' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.Tree α β (l.size + l''.size) → Sort u_3) (ℓ : Std.DTreeMap.Internal.Impl α β)
  (hℓ₁ : ℓ.Balanced) (hℓ₂ : ℓ.size = l.size + l''.size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = l.size + l''.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Probability.Density
MeasureTheory.pdf.eq_of_map_eq_withDensity' : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ]
  (f : E → ENNReal),
  AEMeasurable f μ → (MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Algebra.Order.Group.Abs
/-- `|a / b|ₘ < n` if `1 ≤ a < n` and `1 ≤ b < n`.  -/
mabs_div_lt_of_one_le_of_lt : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b n : G},
  1 ≤ a → a < n → 1 ≤ b → b < n → |a / b|ₘ < n
-- Mathlib.Topology.UniformSpace.Compact
/-- A useful consequence of the Lebesgue number lemma: given any compact set `K` contained in an
open set `U`, we can find an (open) entourage `V` such that the ball of size `V` about any point of
`K` is contained in `U`.  -/
lebesgue_number_of_compact_open : ∀ {α : Type ua} [inst : UniformSpace α] {K U : Set α},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ uniformity α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_le_smul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {s t : SetSemiring A} {M N : Submodule R A}, SetSemiring.down s ⊆ SetSemiring.down t → M ≤ N → s • M ≤ t • N
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_eq_of_lt_right : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v x < v y → v (x + y) = v y
-- Mathlib.MeasureTheory.Measure.IntegralCharFun
/-- For a probability measure on a normed space `E` and `L : Dual ℝ E`, a bound on the measure
of the set `{x | r < |L x|}` in terms of the integral of the characteristic function.  -/
MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] (L : StrongDual ℝ E)
  {r : ℝ},
  0 < r → μ.real {x | r < |L x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - MeasureTheory.charFunDual μ (t • L)‖
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_last : ∀ {n : ℕ}, (finRotate (n + 1)) (Fin.last n) = 0
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- A zero object is a left unit for categorical product.  -/
CategoryTheory.Limits.zeroProdIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → 0 ⨯ X ≅ X
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.instAddTorsorForall : {k : Type u_1} → [inst : Ring k] → {ι : Type u_4} → AddTorsor (ι → k) (ι → k)
-- Mathlib.Data.Fintype.Quotient
Quotient.liftOn₂.congr_simp : ∀ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ q₁_1 : Quotient s₁),
  q₁ = q₁_1 →
    ∀ (q₂ q₂_1 : Quotient s₂),
      q₂ = q₂_1 →
        ∀ (f f_1 : α → β → φ) (e_f : f = f_1)
          (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂),
          q₁.liftOn₂ q₂ f c = q₁_1.liftOn₂ q₂_1 f_1 ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The natural semigroup hom from a subsemigroup of semigroup `M` to `M`.  -/
MulMemClass.subtype : {M : Type u_1} →
  {A : Type u_3} → [inst : Mul M] → [inst_1 : SetLike A M] → [hA : MulMemClass A M] → (S' : A) → ↥S' →ₙ* M
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1CLM_indicatorConst : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α}
  [inst_3 : CompleteSpace F'] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : F'),
  (MeasureTheory.condExpL1CLM F' hm μ) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs hμs x) =
    (MeasureTheory.condExpInd F' hm μ s) x
-- Mathlib.Analysis.Distribution.DerivNotation
InnerProductSpace.canonicalCovariantTensor.congr_simp : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  InnerProductSpace.canonicalCovariantTensor E = InnerProductSpace.canonicalCovariantTensor E
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- `UniformOnFun.gen` is antitone in the first argument and monotone in the second.  -/
UniformOnFun.gen_mono : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {S S' : Set α} {V V' : Set (β × β)},
  S' ⊆ S → V ⊆ V' → UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ExprConfigCacheKey.mk.inj : ∀ {expr : Lean.Expr} {configKey : UInt64} {expr_1 : Lean.Expr} {configKey_1 : UInt64},
  { expr := expr, configKey := configKey } = { expr := expr_1, configKey := configKey_1 } →
    expr = expr_1 ∧ configKey = configKey_1
-- Init.Core
imp_false : ∀ {a : Prop}, a → False ↔ ¬a
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If a monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M` such that its natural powers are dense in `M`,
and `μ` is a finite inner regular measure on `X` which is ergodic with respect to the action of `M`,
then the scalar multiplication by `g` is an ergodic map.  -/
ergodic_smul_of_denseRange_pow : ∀ {X : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : MeasurableSpace X] [BorelSpace X] {M : Type u_3}
  [inst_4 : Monoid M] [inst_5 : TopologicalSpace M] [inst_6 : MulAction M X] [ContinuousSMul M X] {g : M},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ],
      Ergodic (fun x => g • x) μ
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (a b : A), D (a * b) = a • D b + b • D a
-- Mathlib.Order.Concept
upperPolar_empty : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop), upperPolar r ∅ = Set.univ
-- Lean.ErrorExplanation
Lean.ErrorExplanation.instToJsonMetadata.toJson : Lean.ErrorExplanation.Metadata → Lean.Json
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening of the empty set is empty.  -/
Metric.cthickening_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ), Metric.cthickening δ ∅ = ∅
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackId_hom : ∀ (X : AlgebraicGeometry.Scheme),
  (CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id
        (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction (CategoryTheory.CategoryStruct.id X)))
      (AlgebraicGeometry.Scheme.Modules.pullbackId X).hom =
    (AlgebraicGeometry.Scheme.Modules.pushforwardId X).inv
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- The morphism of graded objects induced by a morphism of bicomplexes.  -/
HomologicalComplex₂.toGradedObjectMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {c₁ : ComplexShape I₁} →
            {c₂ : ComplexShape I₂} →
              {K L : HomologicalComplex₂ C c₁ c₂} → (K ⟶ L) → (K.toGradedObject ⟶ L.toGradedObject)
-- Lean.Meta.Basic
/-- `useEtaStruct inductName` return `true` if we eta for structures is enabled for
for the inductive datatype `inductName`.

Recall we have three different settings: `.none` (never use it), `.all` (always use it), `.notClasses`
(enabled only for non-recursive structure types that are not classes).

The parameter `inductName` affects the result only if the current setting is `.notClasses`.
 -/
Lean.Meta.useEtaStruct : Lean.Name → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (X : CategoryTheory.Endofunctor.Algebra F),
  (CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.inv.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.all_eq_allM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.all p it = Std.IterM.allM (fun x => pure { down := p x }) it
-- Mathlib.Algebra.Category.ModuleCat.Projective
ModuleCat.projective_of_module_projective : ∀ {R : Type u} [inst : Ring R] (P : ModuleCat R) [Small.{v, u} R] [CategoryTheory.Projective P], Module.Projective R ↑P
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G) (b : k),
  (SkewMonoidAlgebra.single a b).coeff = fun₀ | a => b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Nonneg.instContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : TopologicalSpace A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [NonnegSpectrumClass ℝ A], ContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.total : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : LE β] [Std.Total fun x1 x2 => x1 ≤ x2],
  Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finset.coe_einfsep : ∀ {α : Type u_1} [inst : EDist α] {s : Finset α}, (↑s).einfsep = s.offDiag.inf (Function.uncurry edist)
-- Mathlib.Data.EReal.Operations
EReal.sub_add_cancel_right : ∀ {a : EReal} {b : ℝ}, ↑b - (a + ↑b) = -a
-- Mathlib.Order.RelClasses
instAntisymmLe : ∀ {α : Type u} [inst : PartialOrder α], Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f (t.get? k)).isSome = true else k' ∈ t
-- Mathlib.Topology.Sheaves.Alexandrov
/-- The functor sending `x : X` to the principal open associated with `x`.  -/
Alexandrov.principals : (X : Type v) →
  [inst : TopologicalSpace X] →
    [inst_1 : Preorder X] → [Topology.IsUpperSet X] → CategoryTheory.Functor X (TopologicalSpace.Opens X)ᵒᵖ
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Opens.coe_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Opens α), ↑s.compl = (↑s)ᶜ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.σ_symm : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂] [inst_3 : TotalComplexShapeSymmetry c₂ c₁ c₁₂]
  [TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂), c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂
-- Lean.Util.Trace
Lean.trace.profiler.threshold : Lean.Option ℕ
-- Mathlib.Algebra.Order.Group.End
RelHom.coe_mul : ∀ {α : Type u_1} {r : α → α → Prop} (f g : r →r r), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Topology.Connected.LocallyPathConnected
Topology.IsOpenEmbedding.locallyPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  {e : Y → X}, Topology.IsOpenEmbedding e → LocallyPathConnectedSpace Y
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
_private.Mathlib.RingTheory.WittVector.FrobeniusFractionField.0.WittVector.frobeniusRotationCoeff.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.opNorm_le_bound₂ : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {C : ℝ},
  0 ≤ C → (∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) → ‖f‖ ≤ C
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns true if the given key `a` is in the RBSet.  -/
RBTree.RBSet.contains : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → α → Bool
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
AlgCat.tensorAlgebra_map : ∀ (R : Type u) [inst : CommRing R] {X Y : ModuleCat R} (f : X ⟶ Y),
  (AlgCat.tensorAlgebra R).map f = AlgCat.ofHom ((TensorAlgebra.lift R) (TensorAlgebra.ι R ∘ₗ ModuleCat.Hom.hom f))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.concat.eq_1 : ∀ (m₂ : Lean.Grind.CommRing.Mon), Lean.Grind.CommRing.Mon.unit.concat m₂ = m₂
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_map : ∀ {R : Type u} [inst : Ring R] {T : Type v} [inst_1 : Ring T] (f : R →+* T) (n : ℕ),
  Polynomial.map f (descPochhammer R n) = descPochhammer T n
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.validFor : ∀ {s : Substring.Raw}, s.Valid → ∃ l m r, Substring.Raw.ValidFor l m r s
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.rTensor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F) (x : TensorProduct 𝕜 E G),
  (LinearIsometry.rTensor G f) x = (LinearMap.rTensor G f.toLinearMap) x
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_sub_eq_left : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 < ArchimedeanClass.mk y → ArchimedeanClass.stdPart (x - y) = ArchimedeanClass.stdPart x
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_ne_bot : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≠ ⊥ ↔ p ≠ 0
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_one : ∀ (x : ℝ), bernoulliFun 1 x = x - 1 / 2
-- Mathlib.Tactic.Ring.RingNF
/-- Configuration for `ring_nf`.  -/
Mathlib.Tactic.RingNF.Config : Type
-- Mathlib.LinearAlgebra.DFinsupp
/-- The `DFinsupp` version of `Finsupp.lsum`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.  -/
DFinsupp.lsum : {ι : Type u_1} →
  {R : Type u_3} →
    (S : Type u_4) →
      {M : ι → Type u_5} →
        {N : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M i)] →
              [inst_2 : (i : ι) → Module R (M i)] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : Module R N] →
                    [DecidableEq ι] →
                      [inst_6 : Semiring S] →
                        [inst_7 : Module S N] →
                          [inst_8 : SMulCommClass R S N] → ((i : ι) → M i →ₗ[R] N) ≃ₗ[S] (Π₀ (i : ι), M i) →ₗ[R] N
-- Mathlib.Data.Finset.Prod
Finset.diag_eq_filter : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.diag = {a ∈ s ×ˢ s | a.1 = a.2}
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_eq_iSup_norm : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)), ‖f‖ = ⨆ x, ‖f x‖
-- Mathlib.Algebra.Module.LinearMap.End
/-- The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.

This is also known as a rank-one operator.
See `ContinuousLinearMap.smulRightL` for the continuous version of this, and see
`InnerProductSpace.rankOne` for the rank-one operator on Hilbert spaces.  -/
LinearMap.smulRightₗ : {R : Type u_1} →
  {M : Type u_4} →
    {M₂ : Type u_6} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M
-- Mathlib.Order.Monotone.Basic
StrictMono.wellFoundedLT : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} [WellFoundedLT β],
  StrictMono f → WellFoundedLT α
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult.mk.sizeOf_spec : ∀ (script : List Aesop.Script.Step) (postState : Lean.Meta.SavedState),
  sizeOf { script := script, postState := postState } = 1 + sizeOf script + sizeOf postState
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForwardNaturalityIso_hom_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (p : f ⟶ g)
  (X_1 : CategoryTheory.Over f),
  (CategoryTheory.Over.iteratedSliceForwardNaturalityIso p).hom.app X_1 =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Over.map (CategoryTheory.Over.Hom.left p)).obj
        (CategoryTheory.Over.mk (CategoryTheory.Over.Hom.left X_1.hom)))
-- Mathlib.Topology.Instances.CantorSet
cantorToBinary.eq_1 : ∀ (x : ℝ), cantorToBinary x = Stream'.map (fun x => if x ∈ Set.Icc 0 (1 / 3) then false else true) (cantorSequence x)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.mem_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β} {b : β},
  b ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_7} [inst_1 : Group N] (f : G →* N) (H : Subgroup N),
  Subgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }