mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.IsRelevant
Lean.Meta.Grind.Arith.isRelevantPred : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.sumElim : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_18} [inst_10 : TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'}
  {N : Type u_20} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace H' N] {f : M → N} {g : M' → N},
  ContMDiff I J n f → ContMDiff I J n g → ContMDiff I J n (Sum.elim f g)
-- Std.Data.TreeSet.Basic
/-- Returns a set that contains all mappings of `t₁` and `t₂.

This function ensures that `t₁` is used linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the
size of `t₂` as long as `t₁` is unshared.
 -/
Std.TreeSet.merge : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.TreeSet α cmp → Std.TreeSet α cmp
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- **Alias** of `CategoryTheory.Mon.uniqueHomToTrivial`. -/
CategoryTheory.uniqueHomToTrivial : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] →
      (A : CategoryTheory.Mon D) → Unique (A ⟶ CategoryTheory.Mon.trivial D)
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The comultiplication is coassociative  -/
Coalgebra.coassoc : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  [self : Coalgebra R A],
  ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
    LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.coe_liftAlgHom : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {A : Type u_4} [inst_5 : CommSemiring A]
  [inst_6 : Algebra A R] [inst_7 : Algebra A S] [inst_8 : Algebra A P] [inst_9 : IsScalarTower A R S] {f : R →ₐ[A] P}
  (hf : IsUnit (f x)), ⇑(IsLocalization.Away.liftAlgHom x hf) = ⇑(IsLocalization.Away.lift x hf)
-- Mathlib.Analysis.Convex.Segment
openSegment_subset_iff : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {x y : E},
  openSegment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
-- Mathlib.Topology.Category.Compactum
/-- Any morphism of compacta is continuous.  -/
Compactum.continuous_of_hom : ∀ {X Y : Compactum} (f : X ⟶ Y), Continuous ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, 0 ≤ f i) → 0 ≤ ∑ i ∈ s, f i
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff_isLongestMatchAt_toSlice : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔
    String.Slice.Pattern.Model.IsLongestMatchAt pat.toSlice pos₁ pos₂
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.isSimpleModule_weylGroupRootRep : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.IsIrreducible],
  IsSimpleModule (MonoidAlgebra R ↥P.weylGroup) P.weylGroupRootRep.asModule
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.SemanticTokensState.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.hom_apply : ∀ {X Y : FintypeCat} (f : X ⟶ Y) (x : X.obj),
  (CategoryTheory.ConcreteCategory.hom f.hom) x = (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_one_right : ∀ (n : ℕ), (n + 1).stirlingFirst 1 = n.factorial
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.id_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : J.OneHypercover S) {i j : E.I₀} (x : E.I₁ i j),
  (CategoryTheory.CategoryStruct.id E).h₁ x = CategoryTheory.CategoryStruct.id (E.Y x)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instModuleCarrierMkOfSMul' : {R : Type u} →
  [inst : Ring R] → {A : AddCommGrpCat} → (φ : R →+* CategoryTheory.End A) → Module R ↑(ModuleCat.mkOfSMul' φ)
-- Mathlib.Data.Tree.Basic
/-- The right child of the tree, or `nil` if the tree is `nil`  -/
BinaryTree.right : {α : Type u} → BinaryTree α → BinaryTree α
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.getOpId : Lean.Meta.Grind.AC.ACM ℕ
-- Init.Data.UInt.Lemmas
USize.ofFin_uint32ToFin : ∀ (n : UInt32), USize.ofFin (Fin.castLE UInt32.size_le_usizeSize n.toFin) = n.toUSize
-- Mathlib.Data.Multiset.ZeroCons
Multiset.singleton_inj : ∀ {α : Type u_1} {a b : α}, {a} = {b} ↔ a = b
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonWorkspaceClientCapabilities : Lean.ToJson Lean.Lsp.WorkspaceClientCapabilities
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.isBigO' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → f =O[⊤] fun p => ‖p‖ * ‖p‖
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.one_lt_re_one_add : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + Complex.I * ↑y).re ∧ 1 < (1 + ↑x + 2 * Complex.I * ↑y).re
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.hasNext.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.hasNext = decide (i.byteIdx < s.rawEndPos.byteIdx)
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If `R` is a ring with a separately continuous multiplication, then negation is continuous as
well since it is just multiplication with `-1`.  -/
IsSemitopologicalSemiring.continuousNeg_of_mul : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocRing R] [SeparatelyContinuousMul R], ContinuousNeg R
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coe_orderHom : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : NoZeroDivisors R] [inst_2 : Nontrivial R],
  ⇑PowerSeries.orderHom = PowerSeries.order
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Ico_sdiff_Ico_left`. -/
Finset.Ico_diff_Ico_left : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Finset.Ico a b \ Finset.Ico a c = Finset.Ico (max a c) b
-- Mathlib.Topology.Separation.Regular
/-- **Alias** of the reverse direction of `t5Space_iff_forall_isOpen_t4Space`.

---

A space is a `T5Space` iff all its open subspaces are `T4Space`.
 -/
T5Space.of_forall_isOpen_t4Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (s : Set X), IsOpen s → T4Space ↑s) → T5Space X
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_of_f_is_kernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) (hS : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
  [S.HasHomology], S.Exact
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.map_simple : ∀ {B : Type u_1} {W : Type u_3} {H : Type u_4} [inst : Group W] [inst_1 : Group H] {M : CoxeterMatrix B}
  (cs : CoxeterSystem M W) (e : W ≃* H) (i : B), (cs.map e).simple i = e (cs.simple i)
-- Mathlib.Control.Fold
Traversable.foldrm_toList : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {m : Type u → Type u}
  [inst_2 : Monad m] [LawfulMonad m] (f : α → β → m β) (x : β) (xs : t α),
  Traversable.foldrm f x xs = List.foldrM f x (Traversable.toList xs)
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_inv_le_one : ∀ (a : ENNReal), a * a⁻¹ ≤ 1
-- Mathlib.Data.BitVec
BitVec.toFin_injective : ∀ {n : ℕ}, Function.Injective BitVec.toFin
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView.induct : ∀ {α : Type u} {β : α → Type v}
  (motive :
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced → r.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Prop),
  (∀ (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced)
      (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced)
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size),
      motive k v Std.DTreeMap.Internal.Impl.leaf r hl hr hlr) →
    (∀ (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced) (size : ℕ) (k' : α) (v' : β k')
        (l' r' : Std.DTreeMap.Internal.Impl α β) (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
        (hlr :
          Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size)
        (dk : α) (dv : β dk) (dt : Std.DTreeMap.Internal.Impl α β) (hdt : dt.Balanced)
        (hdt' : dt.size = l'.size + r'.size),
        Std.DTreeMap.Internal.Impl.minView k' v' l' r' ⋯ ⋯ ⋯ =
            { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } →
          motive k' v' l' r' ⋯ ⋯ ⋯ → motive k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') r hl hr hlr) →
      ∀ (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced)
        (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size), motive k v l r hl hr hlr
-- Mathlib.FieldTheory.Normal.Closure
/-- A normal closure of `K/F` embeds into any `L/F`
where the minimal polynomials of `K/F` splits.  -/
IsNormalClosure.lift : {F : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F L] →
                [h : IsNormalClosure F K L] →
                  {L' : Type u_4} →
                    [inst_5 : Field L'] →
                      [inst_6 : Algebra F L'] →
                        (∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits) → L →ₐ[F] L'
-- Lean.Parser.Extension
/-- Called after a parser attribute is applied to a declaration.  -/
Lean.Parser.ParserAttributeHook.postAdd : Lean.Parser.ParserAttributeHook → Lean.Name → Lean.Name → Bool → Lean.AttrM Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α} {h : k ∈ Std.DHashMap.Raw.Const.unitOfList l},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.unitOfList l) k h = ()
-- Mathlib.MeasureTheory.Order.Lattice
AEMeasurable.const_sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → M} [inst_1 : Max M] [MeasurableSup M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => c ⊔ f x) μ
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftBindFunction.liftBind_bind : ∀ {m : Type u → Type v} {n : Type w → Type x} {inst : Monad m} {inst_1 : Monad n}
  {liftBind : (γ : Type u) → (δ : Type w) → (γ → n δ) → m γ → n δ}
  [self : Std.Internal.LawfulMonadLiftBindFunction liftBind] {β γ : Type u} {δ : Type w} (f : γ → n δ) (x : m β)
  (g : β → m γ), liftBind γ δ f (x >>= g) = liftBind β δ (fun b => liftBind γ δ f (g b)) x
-- Std.Async.Basic
/-- Creates a new `ETask` that will run after `x` has completed. If `x`:
- errors, return an `ETask` that resolves to the error.
- succeeds, run `f` on the result of `x` and return the `ETask` produced by `f`.
 -/
Std.Async.ETask.bind : {ε α β : Type} →
  Std.Async.ETask ε α →
    (α → Std.Async.ETask ε β) → optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.ETask ε β
-- Lean.LocalContext
Lean.LocalDecl.binderInfo : Lean.LocalDecl → Lean.BinderInfo
-- Mathlib.Order.Disjoint
Codisjoint.eq_top_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → b ≤ a → a = ⊤
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.hcomp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) [inst_6 : F₁.LaxMonoidal] [inst_7 : F₂.LaxMonoidal]
  {G₁ G₂ : CategoryTheory.Functor D E} [inst_8 : G₁.LaxMonoidal] [inst_9 : G₂.LaxMonoidal] (τ' : G₁ ⟶ G₂)
  [CategoryTheory.NatTrans.IsMonoidal τ] [CategoryTheory.NatTrans.IsMonoidal τ'],
  CategoryTheory.NatTrans.IsMonoidal (τ ◫ τ')
-- Mathlib.Analysis.SpecialFunctions.Pow.Integral
/-- A function that is dominated by `‖x‖ ^ (-d + ε)` is locally integrable  -/
MeasureTheory.locallyIntegrable_of_norm_le_rpow : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedAddCommGroup F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure],
  1 ≤ Module.finrank ℝ E →
    ∀ {f : E → F} {C α : ℝ},
      α < ↑(Module.finrank ℝ E) →
        (∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)) →
          MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.LocallyIntegrable f μ
-- Aesop.Script.Step
Aesop.Script.LazyStep.postGoals : Aesop.Script.LazyStep → Array Lean.MVarId
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSemigroupWithZeroOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : SemigroupWithZero β] → [ContinuousMul β] → SemigroupWithZero C(α, β)
-- Init.Data.Char.Lemmas
Char.notLTTrans : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasisOfPrimePow.eq_1 : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  hζ.integralPowerBasisOfPrimePow = (Algebra.adjoin.powerBasis' ⋯).map hζ.adjoinEquivRingOfIntegersOfPrimePow
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.id.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → Sort u_2) (a : C)
  (h_1 : (a : C) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of a with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_1 a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.allM_eq_forIn : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.allM p it =
    forIn it true fun x x_1 => do
      let __do_lift ← p x
      if __do_lift = true then pure (ForInStep.yield true) else pure (ForInStep.done false)
-- Mathlib.Analysis.Calculus.DSlope
DifferentiableWithinAt.of_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 (dslope f a) s b → DifferentiableWithinAt 𝕜 f s b
-- Mathlib.GroupTheory.Commutator.Basic
/-- The commutator of two subgroups `H₁` and `H₂`.  -/
Subgroup.commutator : {G : Type u_1} → [inst : Group G] → Bracket (Subgroup G) (Subgroup G)
-- Mathlib.Analysis.CStarAlgebra.Unitization
ContinuousLinearMap.opNNNorm_mul_flip_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E]
  [inst_2 : StarRing E] [NormedStarGroup E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E]
  [inst_6 : SMulCommClass 𝕜 E E] [RegularNormedAlgebra 𝕜 E] (a : E), ‖(ContinuousLinearMap.mul 𝕜 E).flip a‖₊ = ‖a‖₊
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_inv' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (k : ℕ),
  deriv^[k] Inv.inv = fun x => (-1) ^ k * ↑k.factorial * x ^ (-1 - ↑k)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.StructuralOfExpr_bicategoricalComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b}
  [inst_1 : CategoryTheory.BicategoricalCoherence g h] (η : f ⟶ g) (η' : f ≅ g),
  η'.hom = η →
    ∀ (θ : h ⟶ i) (θ' : h ≅ i),
      θ'.hom = θ → (CategoryTheory.bicategoricalIsoComp η' θ').hom = CategoryTheory.bicategoricalComp η θ
-- Mathlib.Data.Set.Function
Set.bijOn_empty_iff_right : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Set.BijOn f ∅ t ↔ t = ∅
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.monMonoidalStruct_tensorObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).X = CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.weylGroup.induction : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  {pred : (g : P.Aut) → g ∈ P.weylGroup → Prop},
  (∀ (i : ι), pred (RootPairing.Equiv.reflection P i) ⋯) →
    pred 1 ⋯ →
      (∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯) →
        ∀ {x : P.Aut} (hx : x ∈ P.weylGroup), pred x hx
-- Mathlib.NumberTheory.Dioph
Poly.instOne : {α : Type u_1} → One (Poly α)
-- Mathlib.Algebra.Quandle
Rack.toEnvelGroup.mapAux.eq_2 : ∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G)) (x_1 : R),
  Rack.toEnvelGroup.mapAux f (Rack.PreEnvelGroup.incl x_1) = f x_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      k' ∈ Std.DTreeMap.Raw.Const.alter t k f ↔
        if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true else k' ∈ t
-- Mathlib.Algebra.Quaternion
Quaternion.imK_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (star a).imK = -a.imK
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapAlgebra_self_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : CommRing.Pic R}, (CommRing.Pic.mapAlgebra R R) M = M
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getCaseGoals.showTagName : Lean.Name → Lean.MessageData
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E),
      ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ =
        ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.coe_weight_mk : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) (h : LieModule.genWeightSpace M χ ≠ ⊥),
  ⇑{ toFun := χ, genWeightSpace_ne_bot' := h } = χ
-- Mathlib.Computability.StateTransition
StateTransition.EvalsTo.mk : {σ : Type u_1} →
  {f : σ → Option σ} →
    {a : σ} → {b : Option σ} → (steps : ℕ) → (flip bind f)^[steps] (some a) = b → StateTransition.EvalsTo f a b
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- An algebraic extension of ℝ is isomorphic to either ℝ or ℂ as an ℝ-algebra.  -/
Real.nonempty_algEquiv_or : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Algebra ℝ F] [Algebra.IsAlgebraic ℝ F],
  Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_fun_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 d x → deriv (fun y => c y * d y) x = deriv c x * d x + c x * deriv d x
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) →
                (CategoryTheory.Functor.id
                        (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj
                    c ≅
                  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp
                        (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj
                    c
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `mul_inv_lt_iff₀` for a version with multiplication on the other side.  -/
mul_inv_lt_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (b * c⁻¹ < a ↔ b < c * a)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isLoopAt_congr : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  H ≤ G → e ∈ H.edgeSet → (H.IsLoopAt e x ↔ G.IsLoopAt e x)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
AddMonoidHom.coe_finsuppSum : ∀ {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [inst : Zero β] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : α →₀ β) (g : α → β → N →+ P), ⇑(f.sum g) = f.sum fun i fi => ⇑(g i fi)
-- Init.CbvSimproc
Lean.Parser.«command_Builtin_cbv_simproc_decl_(_):=_» : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_congr_set' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜} (y : 𝕜),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → derivWithin f s x = derivWithin f t x
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_toUSize : ∀ (n : UInt64), n.toUSize.toUInt8 = n.toUInt8
-- Mathlib.Data.Int.Bitwise
Int.natBitwise.eq_1 : ∀ (f : Bool → Bool → Bool) (m n : ℕ),
  Int.natBitwise f m n =
    bif f false false then Int.negSucc (Nat.bitwise (fun x y => !f x y) m n) else ↑(Nat.bitwise f m n)