mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
linear in both variables.  -/
CategoryTheory.Preadditive.homGroup : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.Preadditive C] → (P Q : C) → AddCommGroup (P ⟶ Q)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_surjective : ∀ {α : Type u_1} [Nonempty α], Function.Surjective FreeMonoid.length
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.isSimplyLaced_E₆ : CartanMatrix.E₆.IsSimplyLaced
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- The Galois coinsertion from sets of isotypic components to fully invariant submodules.  -/
GaloisCoinsertion.setIsotypicComponents : (R : Type u_2) →
  (M : Type u) →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → GaloisCoinsertion (fun s => ⨆ c ∈ s, ⟨↑c, ⋯⟩) fun m => {c | ↑c ≤ ↑m}
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_eval_dom : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  [inst_1 : Inhabited Λ] [inst_2 : Inhabited σ] (k : K) (L : List (Γ k)),
  (Turing.TM1.eval (Turing.TM2to1.tr M) (Turing.TM2to1.trInit k L)).Dom ↔ (Turing.TM2.eval M k L).Dom
-- Mathlib.MeasureTheory.Measure.Haar.Basic
_private.Mathlib.MeasureTheory.Measure.Haar.Basic.0.MeasureTheory.Measure.steinhaus_mul_aux : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ.InnerRegularCompactLTTop] [LocallyCompactSpace G]
  (E : Set G), MeasurableSet E → (∃ K ⊆ E, IsCompact K ∧ 0 < μ K) → E / E ∈ nhds 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Hölder's inequality for integrable functions: the scalar multiplication of an integrable
scalar-valued function by a vector-value function with finite essential supremum is integrable.  -/
MeasureTheory.Integrable.smul_essSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → 𝕜},
  MeasureTheory.Integrable f μ →
    ∀ {g : α → β},
      MeasureTheory.AEStronglyMeasurable g μ →
        essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤ → MeasureTheory.Integrable (fun x => f x • g x) μ
-- Mathlib.LinearAlgebra.Eigenspace.Pi
/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a
submodule `p` which is invariant w.r.t. every `f i`, the intersection of `p` with the simultaneous
maximal generalised eigenspace (taken over all `i`), is the same as the simultaneous maximal
generalised eigenspace of the `f i` restricted to `p`.  -/
Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) {μ : ι → R} (p : Submodule R M) (hfp : ∀ (i : ι), Set.MapsTo ⇑(f i) ↑p ↑p),
  p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, Module.End.maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
-- Lean.Util.ParamMinimizer
/-- Status of the parameter minimizer procedure.  -/
Lean.Util.ParamMinimizer.Status : Type
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Given a coloring `α` of `G`, and a clique of size at least the number of colors, the clique
contains a vertex of each color.
 -/
SimpleGraph.Coloring.surjOn_of_card_le_isClique : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} [inst : Fintype α] {s : Finset V},
  G.IsClique ↑s → Fintype.card α ≤ s.card → ∀ (C : G.Coloring α), Set.SurjOn (⇑C) (↑s) Set.univ
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- `HasConicalLimit F` represents the mere existence of a conical limit for `F`.
 -/
CategoryTheory.Enriched.HasConicalLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (V : outParam (Type u')) →
      [inst_1 : CategoryTheory.Category.{v', u'} V] →
        [inst_2 : CategoryTheory.MonoidalCategory V] →
          {C : Type u} →
            [inst_3 : CategoryTheory.Category.{v, u} C] →
              [CategoryTheory.EnrichedOrdinaryCategory V C] → CategoryTheory.Functor J C → Prop
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- [Stacks Tag 00F8](https://stacks.math.columbia.edu/tag/00F8) (without the finite presentation part) -/
PrimeSpectrum.exists_range_eq_of_isConstructible : ∀ {R : Type u} [inst : CommRing R] {s : Set (PrimeSpectrum R)},
  Topology.IsConstructible s → ∃ S x f, Set.range (PrimeSpectrum.comap f) = s
-- Mathlib.Data.TypeVec
TypeVec.ofSubtype.eq_1 : ∀ (n_2 : ℕ) (α_2 : TypeVec.{u} (n_2 + 1)) (p_2 : α_2.Arrow (TypeVec.repeat (n_2 + 1) Prop)) (i : Fin2 n_2)
  (x_2 : TypeVec.Subtype_ p_2 i.fs), TypeVec.ofSubtype p_2 i.fs x_2 = TypeVec.ofSubtype (TypeVec.dropFun p_2) i x_2
-- Mathlib.CategoryTheory.Types.Basic
/-- `TypeCat.Hom.hom` bundled as an `Equiv`.  -/
TypeCat.homEquiv : {X Y : Type u} → (X ⟶ Y) ≃ (X → Y)
-- Init.Data.Option.Instances
/-- Given an optional value and a function that can be applied when the value is `some`, returns the
result of applying the function if this is possible, or a fallback value otherwise.

The function `f` is _partial_ because it is only defined for the values `a : α` such that
`o = some a`. This restriction allows the function to use the fact that it can only be called when
`o` is not `none`: it can relate its argument to the optional value `o`. Its runtime behavior is
equivalent to that of `Option.elim`.

Examples:
```lean example
def attach (v : Option α) : Option { y : α // v = some y } :=
  v.pelim none fun x h => some ⟨x, h⟩
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
 -/
Option.pelim : {α : Type u_1} → {β : Sort u_2} → (o : Option α) → β → ((a : α) → o = some a → β) → β
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_mono_right : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
  {s₁ s₂ : Set α}, s₁ ⊆ s₂ → omegaLimit f ϕ s₁ ⊆ omegaLimit f ϕ s₂
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.fun_id : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (q : Q),
  RegularWreathProduct.rightHom (RegularWreathProduct.inl q) = q
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k fallback : α}, m₁.contains k = false → (m₁.diff m₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.Homology.Localization
instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : AddRightCancelSemigroup ι] [inst_3 : One ι] [CategoryTheory.Limits.HasBinaryBiproducts C],
  (HomotopyCategory.quotient C (ComplexShape.down ι)).IsLocalization
    (HomologicalComplex.homotopyEquivalences C (ComplexShape.down ι))
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.instTrans : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Trans Std.HashSet.Equiv Std.HashSet.Equiv Std.HashSet.Equiv
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.eq_2 : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (n : ℕ),
  MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n.succ =
    max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1))
      (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) (val : ℤ) (x n : Lean.Grind.Linarith.Var),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen c val x n) =
    1 + sizeOf c + sizeOf val + sizeOf x + sizeOf n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.mk.sizeOf_spec : ∀ (mctx : Lean.MetavarContext) (paramNames : Array Lean.Name) (nextParamIdx : ℕ)
  (cache : Std.HashMap Lean.ExprStructEq Lean.Expr),
  sizeOf { mctx := mctx, paramNames := paramNames, nextParamIdx := nextParamIdx, cache := cache } =
    1 + sizeOf mctx + sizeOf paramNames + sizeOf nextParamIdx + sizeOf cache
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.finite_fiber : ∀ {R : Type u_1} {S : Type u_2} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.QuasiFinite R S] (P : Ideal R) [inst_3 : P.IsPrime], Module.Finite P.ResidueField (P.Fiber S)
-- Lean.Parser.Term
/-- `+nondep` elaborates as a nondependent `let`, a `have` expression.
 -/
Lean.Parser.Term.letOptNondep : Lean.Parser.Parser
-- Mathlib.Order.Cover
WithBot.covBy_bot_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : WithBot α}, ⊥ ⋖ a ↔ ∃ b, IsMin b ∧ a = ↑b
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Identifying the tangent space at a normed space with the normed space itself.
This canonical identification (which, in mathlib, is implemented using an abuse of definitional
equality) is very prevalent in a number of places: this device allows making it explicit.  -/
NormedSpace.fromTangentSpace : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] → (v : E) → TangentSpace (modelWithCornersSelf 𝕜 E) v ≃L[𝕜] E
-- Init.Data.Vector.Count
Vector.countP_replicate : ∀ {α : Type u_1} {p : α → Bool} {a : α} {n : ℕ}, Vector.countP p (Vector.replicate n a) = if p a = true then n else 0
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.infsep : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : Decidable s.Nontrivial] (hsf : s.Finite),
  s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (Function.uncurry dist) else 0
-- Init.Core
true_iff_false : (True ↔ False) ↔ False
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α},
  t.WF → (Std.DTreeMap.Raw.map f t).get? k = Option.map (f k) (t.get? k)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- The defining property of `OverArrows.val`.  -/
CategoryTheory.OverPresheafAux.OverArrows.app_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} (p : CategoryTheory.OverPresheafAux.OverArrows η s),
  (CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op X))) p.val = CategoryTheory.yonedaEquiv s
-- Lean.DocString.Extension
Lean.VersoModuleDocs.canAdd : Lean.VersoModuleDocs → Lean.VersoModuleDocs.Snippet → Bool
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_eq_det_mul_det : ∀ {R : Type u_6} {V : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] [Module.Finite R V]
  (W : Submodule R V) [Module.Free R ↥W] [Module.Finite R ↥W] [Module.Free R (V ⧸ W)] (e : V →ₗ[R] V)
  (he : W ≤ Submodule.comap e W), LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- The closure (as a submodule) of the graph is equal to the graph of the closure
(as a `LinearPMap`).  -/
LinearPMap.IsClosable.graph_closure_eq_closure_graph : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, f.IsClosable → f.graph.topologicalClosure = f.closure.graph
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.conv_withDensity_eq_mlconvolution₀ : ∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ → (μ.withDensity f).conv (μ.withDensity g) = μ.withDensity (MeasureTheory.lconvolution f g μ)
-- Mathlib.Tactic.Simps.Basic
/-- syntax that might have provided `strName`  -/
Simps.ParsedProjectionData.strStx : Simps.ParsedProjectionData → Lean.Syntax
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The morphism `ιFunctorObj f πX : X ⟶ functorObj f πX` is obtained by
attaching `f`-cells, and the index type can be chosen to be in `Type t`
if the category is `t`-locally small and the index type for `f`
is `t`-small.  -/
CategoryTheory.SmallObject.attachCellsιFunctorObjOfSmall : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [inst_2 :
                    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  [CategoryTheory.LocallySmall.{t, v, u} C] →
                    [Small.{t, w} I] → HomotopicalAlgebra.AttachCells f (CategoryTheory.SmallObject.ιFunctorObj f πX)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_monoLM_le : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n₁ K₁),
  (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((ContDiffMapSupportedIn.monoLM 𝕜) f) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
-- Mathlib.Algebra.Ring.Defs
RightDistribClass.mk : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R], (∀ (a b c : R), (a + b) * c = a * c + b * c) → RightDistribClass R
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  Set.EqOn V₁ V s →
    V₁ x = V x →
      Set.EqOn W₁ W s → W₁ x = W x → VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MulticospanIndex J C`, `c : Multifork d` and `F : C ⥤ D`,
this is the induced multifork of `d.map F`.  -/
CategoryTheory.Limits.Multifork.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.Limits.MulticospanShape} →
          {d : CategoryTheory.Limits.MulticospanIndex J C} →
            CategoryTheory.Limits.Multifork d →
              (F : CategoryTheory.Functor C D) → CategoryTheory.Limits.Multifork (d.map F)
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullback_obj_obj_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {Z : C} {f : X ⟶ Y} {F : TopCat.Presheaf C Y} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ}
  {φ ψ : ((TopCat.Presheaf.pullback C f).obj F).obj U ⟶ Z},
  φ = ψ ↔
    ∀ (V : TopologicalSpace.Opens ↑Y) (hV : Opposite.unop U ≤ (TopologicalSpace.Opens.map f).obj V),
      CategoryTheory.CategoryStruct.comp
          (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
          (CategoryTheory.CategoryStruct.comp
            (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) φ) =
        CategoryTheory.CategoryStruct.comp
          (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
          (CategoryTheory.CategoryStruct.comp
            (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) ψ)
-- Lean.Elab.Binders
/-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name.  -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandBinderIdent : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A variant of `eqToIso` that lifts terms to the discrete category.  -/
CategoryTheory.Discrete.eqToIso' : {α : Type u₁} → {a b : α} → a = b → ({ as := a } ≅ { as := b })
-- Init.Data.Array.Subarray
/-- A subarray with the provided bounds. -/
Array.«term__[_:_]» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_of_isEmpty_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {ρ : Type w}
  [inst_2 : ForIn Id ρ α] [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : ρ}, (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).isEmpty = true → (↑m).isEmpty = true
-- Mathlib.Algebra.Lie.Basic
LieRingModule.compLieHom_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : AddCommGroup M]
  [inst_6 : LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) (m : M), ⁅x, m⁆ = ⁅f x, m⁆
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α} (h' : a ∈ m), m.get? a = some (m.get a h')
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.instRing : {R : Type u_1} → [inst : Ring R] → [MulSemiringAction (Multiplicative ℕ) R] → Ring (SkewPolynomial R)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.smul.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {α : Type u_3} [inst_1 : SMul α Y],
  LocallyConstant.smul = { smul := fun n f => LocallyConstant.map (fun x => n • x) f }
-- Std.Async.System
Std.Async.System.instInhabitedEnvironment : Inhabited Std.Async.System.Environment
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.Data.Fintype.Fin
Fin.card_filter_univ_succ' : ∀ {n : ℕ} (p : Fin (n + 1) → Prop) [inst : DecidablePred p],
  {x | p x}.card = (if p 0 then 1 else 0) + {x | p x.succ}.card
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_subgroup_op : ∀ {G : Type u_1} [inst : Group G] (s : Subgroup Gᵐᵒᵖ), MulAction.stabilizer G ↑s = s.unop
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map `Hₙ(G, A) ⟶ Hₙ(H, B)` sending `∑ aᵢ·gᵢ : Gⁿ →₀ A` to
`∑ φ(aᵢ)·(f ∘ gᵢ) : Hⁿ →₀ B`.  -/
groupHomology.map : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} → (f : G →* H) → (A ⟶ Rep.res f B) → (n : ℕ) → groupHomology A n ⟶ groupHomology B n
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.quotientBotIsometryEquiv.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M],
  QuotientGroup.quotientBotIsometryEquiv = { toEquiv := QuotientGroup.quotientBot.toEquiv, isometry_toFun := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.isStableUnderProductsOfShape_trivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] (J : Type w),
  (HomotopicalAlgebra.trivialFibrations C).IsStableUnderProductsOfShape J
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_app : ∀ {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) (a b : ℤ) (h : a + 1 = b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).inv.app X) ((t.truncLEι a).app X) =
    (t.truncLTι b).app X
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
/-- The functors `homologyFunctor C n : DerivedCategory C ⥤ C` for all `n : ℤ` are part
of a "shift sequence", i.e. they satisfy compatibilities with shifts.  -/
DerivedCategory.instShiftSequenceHomologyFunctorOfNatInt : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → (DerivedCategory.homologyFunctor C 0).ShiftSequence ℤ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff : ∀ {X Y : AlgebraicGeometry.Scheme} {f g : X.PartialMap Y}, f.toRationalMap = g.toRationalMap ↔ f.equiv g
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (a : α), mulRothNumber {a} = 1
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasStrictDerivAt.pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasStrictDerivAt f f' x →
    ∀ (n : ℕ), HasStrictDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
-- Mathlib.FieldTheory.KummerExtension
IsUnit.unit'.congr_simp : ∀ {α : Type u} [inst : DivisionMonoid α] {a a_1 : α} (e_a : a = a_1) (h : IsUnit a), h.unit' = ⋯.unit'
-- Mathlib.GroupTheory.OrderOfElement
nsmulCoprime_neg : ∀ {n : ℕ} {G : Type u_6} [inst : AddGroup G] (h : (Nat.card G).Coprime n) {g : G},
  (nsmulCoprime h) (-g) = -(nsmulCoprime h) g
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_ric_eq_some_iff : ∀ {k n i : ℕ}, (*...=n).toList[i]? = some k ↔ i ≤ n ∧ i = k
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instVAdd.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : VAdd M G],
  Filter.Germ.instVAdd = { vadd := fun n f => Filter.Germ.map (fun x => n +ᵥ x) f }
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_blockDiag : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] {A : X → Matrix (m × p) (n × p) R}, Continuous A → Continuous fun x => (A x).blockDiag