mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_of_top_iff' : ∀ {R : Type u} {L : Type v} {M : Type w} [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] [LieModule R L M],
  LieModule.IsNilpotent L ↥⊤ ↔ LieModule.IsNilpotent L M
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrder.toInfSet : {α : Type u_3} → [self : ConditionallyCompletePartialOrder α] → InfSet α
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.re_inner_nonneg_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 x (T x))
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp g.hom f.hom
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Naturality of the oplax naturality constraint.  -/
CategoryTheory.Lax.OplaxTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.OplaxTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (self.naturality g) =
    CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
-- Mathlib.Order.UpperLower.Hom
/-- `LowerSet.Iic` as an `InfHom`.  -/
LowerSet.iicInfHom : {α : Type u_1} → [inst : SemilatticeInf α] → InfHom α (LowerSet α)
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.baseChange : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [h : Algebra.EssFiniteType R S],
  Algebra.EssFiniteType T (TensorProduct R T S)
-- Batteries.Data.List.Interleave
List.interleave_nil : ∀ {α : Type u_1} (l₁ : List α), l₁.interleave [] = l₁
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRcc : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Rcc α)
-- Mathlib.Algebra.Group.Action.Defs
SemiconjBy.smul_right_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Mul H] [inst_2 : MulAction G H] [SMulCommClass G H H]
  [IsScalarTower G H H] {a b x : H} {r : G}, SemiconjBy x (r • a) (r • b) ↔ SemiconjBy x a b
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Γ_map : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyRingedSpace.Γ.map f = f.unop.c.app (Opposite.op ⊤)
-- Mathlib.Order.Filter.Basic
Filter.not_eventually : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x
-- Std.Internal.Do.WP.Basic
_private.Std.Internal.Do.WP.Basic.0.Std.Internal.Do.EStateM.wpInst.match_1.splitter : {ε σ α : Type} →
  (motive : EStateM.Result ε σ α → Sort u_1) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((el : ε) → (s' : σ) → motive (EStateM.Result.error el s')) → motive x
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_le : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I J : LieIdeal R L}
  {k l : ℕ}, I ≤ J → l ≤ k → LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l J
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
`Π i, E →L[𝕜] F i` and `E →L[𝕜] Π i, F i`.  -/
ContinuousLinearMap.piEquivL : (𝕜 : Type u_1) →
  [inst : NormedField 𝕜] →
    (E : Type u_2) →
      {ι : Type u_3} →
        (F : ι → Type u_4) →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : (i : ι) → AddCommGroup (F i)] →
                  [inst_5 : (i : ι) → Module 𝕜 (F i)] →
                    [inst_6 : (i : ι) → TopologicalSpace (F i)] →
                      [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] →
                        [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] →
                          ((i : ι) → E →L[𝕜] F i) ≃L[𝕜] E →L[𝕜] (i : ι) → F i
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.extendScalarsOfIsLocalizationEquiv.congr_simp : ∀ {R : Type u_3} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N],
  LinearMap.extendScalarsOfIsLocalizationEquiv S A = LinearMap.extendScalarsOfIsLocalizationEquiv S_1 A
-- Mathlib.LinearAlgebra.Projection
LinearMap.coe_equivProdOfSurjectiveOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommGroup G] [inst_6 : Module R G]
  {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : f.range = ⊤) (hg : g.range = ⊤) (hfg : IsCompl f.ker g.ker),
  ↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = f.prod g
-- Init.Data.Array.Attach
Array.attachWith_push : ∀ {α : Type u_1} {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x},
  (xs.push a).attachWith P H = (xs.attachWith P ⋯).push ⟨a, ⋯⟩
-- Lean.Level
Lean.Level.PP.Context.mk : Bool → (Lean.LMVarId → Option ℕ) → Lean.Level.PP.Context
-- Init.Prelude
ReaderT.instMonadFunctor : (ρ : Type u_1) → (m : Type u_1 → Type u_2) → MonadFunctor m (ReaderT ρ m)
-- Mathlib.Tactic.NormNum.IsSquare
/-- `norm_num` extension for `IsSquare` on `ℤ`.  -/
Mathlib.Meta.NormNum.evalIsSquareInt : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C} (h : CategoryTheory.Limits.pushout f g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h
-- Lean.Language.Basic
Lean.Language.instToSnapshotTreeSnapshotTree : Lean.Language.ToSnapshotTree Lean.Language.SnapshotTree
-- Std.Sync.Mutex
/-- Mutual exclusion primitive (lock) guarding shared state of type `α`.

The type `Mutex α` is similar to `IO.Ref α`, except that concurrent accesses are guarded by a mutex
instead of atomic pointer operations and busy-waiting.
 -/
Std.Mutex : Type → Type
-- Mathlib.Topology.Algebra.Monoid.Defs
continuous_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], Continuous fun p => p.1 + p.2
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.mk.sizeOf_spec : ∀ (toProfinite : Profinite) [group : Group ↑toProfinite.toTop]
  [topologicalGroup : IsTopologicalGroup ↑toProfinite.toTop],
  sizeOf { toProfinite := toProfinite, group := group, topologicalGroup := topologicalGroup } =
    1 + sizeOf toProfinite + sizeOf group + sizeOf topologicalGroup
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ}, (List.map f l)[i]? = Option.map f l[i]?
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_bot : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α], ⊥.length = 0
-- Std.Async.Basic
Std.Async.EAsync.instMonadAwaitETask : {ε : Type} → Std.Async.MonadAwait (Std.Async.ETask ε) (Std.Async.EAsync ε)
-- Mathlib.RingTheory.Noetherian.Orzech
/-- If `M ⊕ N` embeds into `M`, for `M` Noetherian over `R`, then `N` is trivial.  -/
IsNoetherian.equivPUnitOfProdInjective : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type w} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                [IsNoetherian R M] → (f : M × N →ₗ[R] M) → Function.Injective ⇑f → N ≃ₗ[R] PUnit.{w + 1}
-- Mathlib.LinearAlgebra.Complex.Module
Complex.adjoin_I : ℝ[Complex.I] = ⊤
-- Mathlib.Topology.Sequences
/-- A set is sequentially closed iff it is equal to its sequential closure.  -/
isSeqClosed_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSeqClosed s ↔ seqClosure s = s
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.id_separatingLeft : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V],
  LinearMap.id.SeparatingLeft
-- Init.Data.Vector.MapIdx
/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction.  -/
Vector.mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {xs : Vector α n}, x ∈ xs.zipIdx ↔ xs[x.2]? = some x.1
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.ofLowerSet_le_ofLowerSet : ∀ {α : Type u_1} [inst : Preorder α] {a b : Topology.WithLowerSet α},
  Topology.WithLowerSet.ofLowerSet a ≤ Topology.WithLowerSet.ofLowerSet b ↔ a ⤳ b
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nndist_tmul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x x' : E)
  (y y' : F), nndist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊
-- Mathlib.Probability.Density
MeasureTheory.map_eq_setLIntegral_pdf : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.map_eq_setLIntegral_pdf._auto_1)
  [hX : MeasureTheory.HasPDF X ℙ μ] {s : Set E},
  MeasurableSet s → (MeasureTheory.Measure.map X ℙ) s = ∫⁻ (x : E) in s, MeasureTheory.pdf X ℙ μ x ∂μ
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of the forward direction of `Set.pairwise_iff_of_refl`. -/
Set.Pairwise.of_refl : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Pairwise r → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.coeSeq : {α : Type u} → Coe (Stream'.Seq α) (Stream'.WSeq α)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toSubalgebra_eq_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S : StarSubalgebra R A},
  S.toSubalgebra = ⊤ ↔ S = ⊤
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasureTheory.Measure.instSMulCommClassDomMulActNNReal : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : MulAction G A] [inst_2 : MeasurableSpace A]
  [inst_3 : MeasurableConstSMul G A], SMulCommClass Gᵈᵐᵃ NNReal (MeasureTheory.Measure A)
-- Mathlib.Algebra.WithConv
WithConv.instMulAction : {R : Type u_1} → {A : Type u_2} → [inst : Monoid R] → [MulAction R A] → MulAction R (WithConv A)
-- Mathlib.Logic.Equiv.Set
Equiv.coe_ofInjective_symm : ∀ {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f),
  ⇑(Equiv.ofInjective f hf).symm = Set.rangeSplitting f
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.linearCombination_dualBasis : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (f : ι →₀ R) (i : ι),
  ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i
-- Std.Http.Protocol.H1.Writer
/-- Initial state before any outgoing message has been prepared.
 -/
Std.Http.Protocol.H1.Writer.State.pending : Std.Http.Protocol.H1.Writer.State
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_bij_ne_zero : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → f a ≠ 0 → κ),
  (∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t) →
    (∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0),
        i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) →
      (∀ b ∈ t, g b ≠ 0 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ = b) →
        (∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) → ∑ x ∈ s, f x = ∑ x ∈ t, g x
-- Mathlib.Tactic.NormNum.Basic
/-- The result of adding two `norm_num` results.  -/
Mathlib.Meta.NormNum.Result.add : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : autoParam Q(Add «$α») Mathlib.Meta.NormNum.Result.add._auto_1) →
            Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» + «$b»))
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_neg : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : AddGroup α]
  (M : o → Matrix m n α), Matrix.blockDiagonal (-M) = -Matrix.blockDiagonal M
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.of_hComp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  [B₁.EssSurj] [w.GuitartExact] [(w.hComp w').GuitartExact], w'.GuitartExact
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageMulHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : FunLike F α β] [inst_4 : MulHomClass F α β] (f : F) [inst_5 : DecidableEq β],
  Finset.imageMulHom f = { toFun := Finset.image ⇑f, map_mul' := ⋯ }
-- Mathlib.Order.Hom.Basic
OrderHom.instInhabited : {α : Type u_2} → [inst : Preorder α] → Inhabited (α →o α)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_coe : ∀ {α : Type u_1} {n : ℕ} {s : ↑(Set.powersetCard α n)}, ↑↑s = ↑s
-- Init.Data.List.Basic
List.elem_cons : ∀ {α : Type u} {b : α} {bs : List α} [inst : BEq α] {a : α},
  List.elem a (b :: bs) =
    match a == b with
    | true => true
    | false => List.elem a bs
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsPath.below : {F : PFunctor.{uA, uB}} →
  {motive : (a : PFunctor.Approx.Path F) → (a_1 : F.M) → PFunctor.M.IsPath a a_1 → Prop} →
    {a : PFunctor.Approx.Path F} → {a_1 : F.M} → PFunctor.M.IsPath a a_1 → Prop
-- Mathlib.Data.Countable.Basic
untopD_coe_enat : ∀ (d n : ℕ), WithTop.untopD d ↑n = n
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.step : Lean.Meta.SynthInstance.SynthM Bool
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.isEmpty : Lean.Meta.Match.Overlaps → Bool
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxChild_ : Lean.ParserDescr
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.convMul_algHom_single_one : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] (f g : WithConv (AddMonoidAlgebra R M →ₐ[R] A)) (x : M),
  (f * g).ofConv (AddMonoidAlgebra.single x 1) =
    f.ofConv (AddMonoidAlgebra.single x 1) * g.ofConv (AddMonoidAlgebra.single x 1)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
  (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  m₁ = Lean.Grind.CommRing.Mon.unit →
    m₂ = Lean.Grind.CommRing.Mon.mult p m →
      (match m₁, m₂ with
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
        | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
        | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) ≍
        h_2 p m
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.lengthParity_comp_simple : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W),
  ⇑cs.lengthParity ∘ cs.simple = fun x => Multiplicative.ofAdd 1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The second projection from the chosen pullback along `g` of `f` to the domain of `g`.  -/
CategoryTheory.ChosenPullbacksAlong.snd : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] → CategoryTheory.ChosenPullbacksAlong.pullbackObj f g ⟶ Z
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedLetRecToLift.default : Lean.Elab.Term.LetRecToLift
-- Mathlib.Algebra.Order.GroupWithZero.Basic
strictMonoOn_mul_self : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] [PosMulStrictMono M₀] [MulPosMono M₀],
  StrictMonoOn (fun x => x * x) {x | 0 ≤ x}
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The determinant of `rotation` (as a linear map) is equal to `1`.  -/
Orientation.det_rotation : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle), LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.univ.sizeOf_spec : sizeOf BigOperators.FinsetResult.univ✝ = 1
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_single : ∀ {ι : Type u_9} [inst : Fintype ι] [inst_1 : DecidableEq ι] (𝕜 : Type u_10) [inst_2 : NontriviallyNormedField 𝕜]
  (E : ι → Type u_11) [inst_3 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] (i : ι)
  [NontrivialTopology (E i)], ‖ContinuousLinearMap.single 𝕜 E i‖ = 1
-- Mathlib.Data.EReal.Operations
EReal.sub_nonpos : ∀ {x y : EReal}, x - y ≤ 0 ↔ x ≤ y
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_fromCols_eq_fromBlocks : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R)
  (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R),
  (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- Given an orthonormal set `v` of vectors in `E`, there exists a maximal orthonormal set
containing it.  -/
exists_maximal_orthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {s : Set E},
  Orthonormal 𝕜 Subtype.val → ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.center_eq_iInf : ∀ {G : Type u_1} [inst : Group G] {s : Set G},
  Subgroup.closure s = ⊤ → Subgroup.center G = ⨅ g ∈ s, Subgroup.centralizer {g}
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.continuousLinearMapOfBilin_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) (v w : E),
  inner 𝕜 ((InnerProductSpace.continuousLinearMapOfBilin B) v) w = (B v) w
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.msgRecv : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.mk.inj : ∀ {R : Type u_1} {M : Type u_2} {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {Q : QuadraticForm R M} {A : Type u_3} {inst_3 : Ring A} {inst_4 : Algebra R A} {bilin : M →ₗ[R] M →ₗ[R] A}
  {contract : ∀ (m : M), (bilin m) m = (algebraMap R A) (Q m)}
  {contract_mid : ∀ (m₁ m₂ m₃ : M), (bilin m₁) m₂ * (bilin m₂) m₃ = Q m₂ • (bilin m₁) m₃} {bilin_1 : M →ₗ[R] M →ₗ[R] A}
  {contract_1 : ∀ (m : M), (bilin_1 m) m = (algebraMap R A) (Q m)}
  {contract_mid_1 : ∀ (m₁ m₂ m₃ : M), (bilin_1 m₁) m₂ * (bilin_1 m₂) m₃ = Q m₂ • (bilin_1 m₁) m₃},
  { bilin := bilin, contract := contract, contract_mid := contract_mid } =
      { bilin := bilin_1, contract := contract_1, contract_mid := contract_mid_1 } →
    bilin = bilin_1
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instSMulNat : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddMonoid Y] → SMul ℕ (Function.locallyFinsuppWithin U Y)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.comp_add : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β}, (μ + ν).bind ⇑κ = μ.bind ⇑κ + ν.bind ⇑κ
-- Mathlib.Tactic.Core
/-- Extract the arguments from a `withArgs` syntax as an array of syntaxes  -/
Mathlib.Tactic.getWithArgs : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Syntax)
-- Mathlib.RingTheory.Valuation.RankOne
/-- Convert between the rank one statement on valuative relation's induced valuation.  -/
Valuation.RankOne.rankLeOneStruct : {R : Type u_3} →
  [inst : Ring R] → [inst_1 : ValuativeRel R] → (ValuativeRel.valuation R).RankOne → ValuativeRel.RankLeOneStruct R
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.isNumeral : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Bool
-- Mathlib.Data.Finset.NoncommProd
Multiset.map_noncommProd : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : FunLike F α β]
  [inst_3 : MonoidHomClass F α β] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (f : F),
  f (s.noncommProd comm) = (Multiset.map (⇑f) s).noncommProd ⋯