mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.glue.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (sz : ℕ) →
      (k : α) →
        (v : β k) →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                (r : Std.DTreeMap.Internal.Impl α β) →
                  r.Balanced →
                    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                        r.size →
                      Sort u_3) →
              (r : Std.DTreeMap.Internal.Impl α β) →
                (hr : r.Balanced) →
                  (hlr :
                      Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                        r.size) →
                    ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalancedAtRoot
                              (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                              Std.DTreeMap.Internal.Impl.leaf.size) →
                          motive Std.DTreeMap.Internal.Impl.leaf hr hlr) →
                      ((sz' : ℕ) →
                          (k' : α) →
                            (v' : β k') →
                              (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                                (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalancedAtRoot
                                        (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                                        (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size) →
                                    motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') hr hlr) →
                        motive r hr hlr
-- Mathlib.NumberTheory.MulChar.Basic
/-- Multiplication of multiplicative characters. (This needs the target to be commutative.)  -/
MulChar.mul : {R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → MulChar R R' → MulChar R R' → MulChar R R'
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α)
  (motive : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth → Sort u_1) (lw rw : ℕ) (lhs : aig.RefVec lw)
  (rhs : aig.RefVec rw) (h : newWidth = rw + lw)
  (h_1 :
    (lw rw : ℕ) →
      (lhs : aig.RefVec lw) →
        (rhs : aig.RefVec rw) →
          (h : newWidth = rw + lw) → motive { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h }),
  (match { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } with
    | { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } => h_1 lw rw lhs rhs h) =
    h_1 lw rw lhs rhs h
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.replayConsts.replayKernel.unsafe_impl_2 : Lean.Kernel.Environment →
  Lean.Kernel.Environment →
    List Lean.AsyncConst✝ →
      Lean.EnvExtension Lean.EnvExtensionState →
        Lean.Kernel.Environment → Lean.ReplayFn Lean.EnvExtensionState → Array Lean.EnvExtensionState
-- Lean.Meta.Tactic.Grind.Types
/-- Number of times E-match theorem has been instantiated.  -/
Lean.Meta.Grind.Counters.thm : Lean.Meta.Grind.Counters → Lean.PHashMap Lean.Meta.Grind.Origin ℕ
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.forall : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {P : PolynomialModule R M → Prop}, (∀ (p : PolynomialModule R M), P p) ↔ ∀ (q : ℕ →₀ M), P { coeff := q }
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instIsCentralScalar : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {S : Type u_5} [inst_8 : Semiring S]
  [inst_9 : Module S F] [inst_10 : SMulCommClass 𝕜₂ S F] [inst_11 : ContinuousConstSMul S F] [inst_12 : Module Sᵐᵒᵖ F]
  [inst_13 : IsCentralScalar S F], IsCentralScalar S (E →SWOT[σ] F)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Translating a `CuspForm` by `SL(2, ℤ)`, to obtain a new `CuspForm`.  -/
CuspForm.translate : {k : ℤ} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {F : Type u_1} →
      [inst : FunLike F UpperHalfPlane ℂ] →
        F → [CuspFormClass F Γ k] → (g : GL (Fin 2) ℝ) → CuspForm (ConjAct.toConjAct g⁻¹ • Γ) k
-- Mathlib.CategoryTheory.Galois.Basic
/-- Along a mono that is not an iso, the cardinality of the fiber strictly increases.  -/
CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Mono f], ¬CategoryTheory.IsIso f → Nat.card (F.obj X).obj < Nat.card (F.obj Y).obj
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.natCast_apply : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (n : ℕ) (x : F), ↑n x = n • x
-- Mathlib.Tactic.DefEqAbuse
/-- Only applies `f` to `Meta.isDefEq` trace nodes. Skips `Meta.isDefEq.onFailure` nodes.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.onlyOnDefEqNodes : {m : Type u_1 → Type u_2} →
  [Monad m] →
    {α : Type u_1} →
      (Lean.TraceData → Lean.MessageData → Array Lean.MessageData → m (Lean.MessageData.VisitStep✝ α)) →
        Lean.TraceData → Lean.MessageData → Array Lean.MessageData → m (Lean.MessageData.VisitStep✝ α)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_neg : ∀ {G : Type u_2} [inst : AddGroup G] (s : Set G), AddSubgroup.closure (-s) = AddSubgroup.closure s
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isModule : {R : Type u} → [inst : Ring R] → (self : ModuleCat R) → Module R ↑self
-- Init.Data.Bool
Bool.le_of_lt_or_eq : ∀ {x y : Bool}, x < y ∨ x = y → x ≤ y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_ofList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.DHashMap.Const.ofList l).size ≤ l.length
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlMFast.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α)
  (start stop : USize) (h_stop : stop.toNat ≤ as.size) (acc : Array β),
  Array.scanlMFast.loop✝ f init as start stop h_stop acc =
    if h_lt : start < stop then do
      let next ← f init (as.uget start ⋯)
      Array.scanlMFast.loop✝ f next as (start + 1) stop h_stop (acc.push init)
    else pure (acc.push init)
-- Init.Data.UInt.Lemmas
USize.toUInt16_sub : ∀ (a b : USize), (a - b).toUInt16 = a.toUInt16 - b.toUInt16
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
  (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂), (γ.add γ').φK = γ.φK + γ'.φK
-- Mathlib.CategoryTheory.GradedObject
/-- This is the morphism `X.mapObj p j ⟶ A` constructed from a family of
morphisms `X i ⟶ A` for all `i : I` such that `p i = j`.  -/
CategoryTheory.GradedObject.descMapObj : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) →
          (p : I → J) → [inst_1 : X.HasMap p] → {A : C} → {j : J} → ((i : I) → p i = j → (X i ⟶ A)) → (X.mapObj p j ⟶ A)
-- Mathlib.Order.Bounds.Basic
bddBelow_bddAbove_iff_subset_Icc : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.Icc a b
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_π_subtype_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C}
  (h : f ↑j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f ↑j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObj_obj_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G] (X : Cᵒᵖ), ↑((CategoryTheory.yonedaGrpObj G).obj X) = (Opposite.unop X ⟶ G)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatDiseq_k.eq_1 : ∀ (p : Int.Internal.Linear.Poly),
  p.isUnsatDiseq_k = Int.Internal.Linear.Poly.rec (fun k => k.beq' 0) (fun x x_1 x_2 x_3 => false) p
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
/-- An auxiliary definition which is used to define the adjunction between the star functor
and the sections functor. See `starSectionsAdjunction`.  -/
CategoryTheory.Over.coreHomEquivToOverSections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (I : C) →
        [inst_2 : CategoryTheory.Closed I] →
          [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)] →
            [CategoryTheory.BraidedCategory C] →
              CategoryTheory.Adjunction.CoreHomEquiv (CategoryTheory.toOver I) (CategoryTheory.Over.sections I)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.forget_preservesColimits : CategoryTheory.Limits.PreservesColimits (CategoryTheory.forget TopCat)
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart.congr_simp : ∀ (x y : ℝ) [h : Fact (x < y)], IccLeftChart x y = IccLeftChart x y
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_eq_zero_iff : ∀ {n m : ℕ}, n ||| m = 0 ↔ n = 0 ∧ m = 0
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- Existence of local integral curves for a $C^1$ vector field at interior points of a `C^1`
manifold.  -/
exists_isMIntegralCurveAt_of_contMDiffAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ℝ) {x₀ : M} [CompleteSpace E],
  ContMDiffAt I I.tangent 1 (fun x => ⟨x, v x⟩) x₀ → I.IsInteriorPoint x₀ → ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
-- Std.Sync.Mutex
/-- `mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex.

Calling `mutex.atomically` while already holding the underlying `BaseMutex` in the same thread
is undefined behavior. If this is unavoidable in your code, consider using `RecursiveMutex`.
 -/
Std.Mutex.atomically : {m : Type → Type} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.Mutex α → Std.AtomicT α m β → m β
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.sum_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  (t : Finset α) (B : α → LinearMap.BilinForm R M) (v w : M), ((∑ i ∈ t, B i) v) w = ∑ i ∈ t, ((B i) v) w
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftOn'_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : Sort v} (p q : Polynomial K)
  (f : Polynomial K → Polynomial K → P),
  (∀ (p : Polynomial K), f p 0 = f 0 1) →
    ∀ (H : ∀ {p q a : Polynomial K}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q),
      ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn' f H = f p q
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
_private.Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.splitter : {n : ℕ} →
  (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) →
    (x x_1 : Fin (n + 1 + 1)) →
      (x_2 : x ≤ x_1) →
        ((isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x) →
          ((isLt : 0 < n + 1 + 1) →
              (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x) →
            ((isLt : 0 < n + 1 + 1) →
                (j : ℕ) →
                  (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x) →
              ((i : ℕ) →
                  (hi : i + 1 < n + 1 + 1) →
                    (j : ℕ) →
                      (hj : j + 1 < n + 1 + 1) →
                        (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij) →
                motive x x_1 x_2
-- Init.Data.UInt.Lemmas
Nat.toUSize_eq : ∀ {n : ℕ}, n.toUSize = USize.ofNat n
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_comp_subset : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] {g : M → N},
  g 1 = 1 → ∀ (f : ι → M), Function.mulSupport (g ∘ f) ⊆ Function.mulSupport f
-- Aesop.Frontend.Saturate
Aesop.Frontend.tacticForward____ : Lean.ParserDescr
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- Type synonym for a preorder equipped with the lower set topology.  -/
Topology.WithLowerSet : Type u_4 → Type u_4
-- Mathlib.ModelTheory.LanguageMap
/-- Extends a language with a constant for each element of a parameter set in `M`.  -/
FirstOrder.Language.withConstants : FirstOrder.Language → Type w' → FirstOrder.Language
-- Mathlib.Condensed.Light.Small
LightCondensed.forget.eq_1 : ∀ (R : Type u) [inst : Ring R],
  LightCondensed.forget R =
    CategoryTheory.sheafCompose (CategoryTheory.coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- **Alias** of the reverse direction of `AbsoluteValue.pos_iff`. -/
AbsoluteValue.pos : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) {x : R}, x ≠ 0 → 0 < abv x
-- Mathlib.Analysis.Analytic.Constructions
analyticOn_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_8} [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝], AnalyticOn 𝕜 (fun z => z⁻¹) {z | z ≠ 0}
-- Init.Data.Int.Order
Int.negSucc_max_zero : ∀ (n : ℕ), max (Int.negSucc n) 0 = 0
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAt_apply : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (p : Z.TotalSpace), ↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.CtorIdx
/-- This simproc reduces `T.ctorIdx (T.con …)` to the constructor index.
It does not take part in simp's discrimination tree index, so can be costly on large goals.
 -/
reduceCtorIdx : Lean.Meta.Simp.DSimproc
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {v : β},
  List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.ExtDTreeMap.Const.toList t) = some (k', v) ↔
    t.getKey? k = some k' ∧ Std.ExtDTreeMap.Const.get? t k = some v
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsGE_neg : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ici (-a))) (nhdsWithin a (Set.Iic a))
-- Mathlib.Data.PNat.Defs
instLinearOrderPNat : LinearOrder ℕ+
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLEιOfIsLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsLE X n],
  CategoryTheory.IsIso ((t.truncLEι n).app X)
-- Mathlib.Data.Finset.NAry
Finset.image₂_congr : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f f' : α → β → γ} {s : Finset α} {t : Finset β},
  (∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) → Finset.image₂ f s t = Finset.image₂ f' s t
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure β),
  MeasureTheory.Measure.comap f μ =
    if hf : Function.Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ then
      ((MeasureTheory.OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯
    else 0
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.filter_boxes_val : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop),
  (π.filter p).boxes.val = Multiset.filter (fun J => p J) π.boxes.val
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsPreimmersion g]
  [AlgebraicGeometry.IsPreimmersion (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.IsPreimmersion f
-- Mathlib.Geometry.Convex.Cone.Face.Basic
Submodule.map.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M),
  Submodule.map f p = { carrier := ⇑f '' ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.RingTheory.Multiplicity
le_emultiplicity_of_le_multiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, n ≤ multiplicity a b → ↑n ≤ emultiplicity a b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_2 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (val : BitVec w)
  (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.const val with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_2 w val
-- Mathlib.Algebra.Lie.Abelian
/-- The center of a Lie algebra is the set of elements that commute with everything. It can
be viewed as the maximal trivial submodule of the Lie algebra as a Lie module over itself via the
adjoint representation.  -/
LieAlgebra.center : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toCStarAlgebra : {A : Type u_1} → [self : CommCStarAlgebra A] → CStarAlgebra A
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.positive.congr_simp : ∀ (R : Type u_2) (E : Type u_3) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : PartialOrder E]
  [inst_7 : IsOrderedAddMonoid E] [inst_8 : PosSMulMono R E] [inst_9 : OrderClosedTopology E],
  ProperCone.positive R E = ProperCone.positive R E
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_erase : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : M →₀ R),
  AddMonoidAlgebra.ofCoeff (Finsupp.erase m x) = AddMonoidAlgebra.erase m (AddMonoidAlgebra.ofCoeff x)
-- Init.Data.LawfulHashable
instLawfulHashableOfLawfulBEq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α], LawfulHashable α
-- Mathlib.Algebra.Lie.Nilpotent
Function.Injective.lieAlgebra_isNilpotent : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [h₁ : LieRing.IsNilpotent L'] {f : L →ₗ⁅R⁆ L'},
  Function.Injective ⇑f → LieRing.IsNilpotent L
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instSemilatticeInf.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instSemilatticeInf = Function.Injective.semilatticeInf AddGroupTopology.toTopologicalSpace ⋯ ⋯ ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.isNClique_fst_left : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsNClique (r + 1) (insert w₁ s)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
MulActionWithZero.nontrivial : ∀ (M₀ : Type u_2) (A : Type u_7) [inst : MonoidWithZero M₀] [inst_1 : Zero A] [MulActionWithZero M₀ A] [Nontrivial A],
  Nontrivial M₀