mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →* N`, the surjection sending `(x, y) : M × S` to
`f x * (f y)⁻¹`.  -/
Submonoid.LocalizationMap.mk' : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → S.LocalizationMap N → M → ↥S → N
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH =
    CategoryTheory.Limits.Cofork.π c
-- Init.Data.String.Lemmas.Iterate
String.Slice.toList_revPositions : ∀ {s : String.Slice}, s.revPositions.toList = String.Slice.Model.revPositionsFrom s.endPos
-- Lean.Attributes
Lean.instBEqAttributeKind.beq : Lean.AttributeKind → Lean.AttributeKind → Bool
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (arrows : (c d : C) → Set (c ⟶ d))
  (inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows c d → CategoryTheory.Groupoid.inv p ∈ arrows d c)
  (mul :
    ∀ {c d e : C} {p : c ⟶ d},
      p ∈ arrows c d → ∀ {q : d ⟶ e}, q ∈ arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows c e)
  (arrows_1 : (c d : C) → Set (c ⟶ d))
  (inv_1 : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows_1 c d → CategoryTheory.Groupoid.inv p ∈ arrows_1 d c)
  (mul_1 :
    ∀ {c d e : C} {p : c ⟶ d},
      p ∈ arrows_1 c d → ∀ {q : d ⟶ e}, q ∈ arrows_1 d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows_1 c e),
  ({ arrows := arrows, inv := inv, mul := mul } = { arrows := arrows_1, inv := inv_1, mul := mul_1 }) =
    (arrows = arrows_1)
-- Mathlib.RingTheory.Nilpotent.Defs
/-- An element `y` in a monoid is radical if for any element `x`, `y` divides `x` whenever it
divides a power of `x`.  -/
IsRadical : {R : Type u_1} → [Dvd R] → [Pow R ℕ] → R → Prop
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_forall_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {α : Type u_1} {Φ : α → Prop},
  Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp (∀ (x : α), Φ x))
    (Lean.Order.iInf fun x => Lean.Order.CompleteLattice.ofProp (Φ x))
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (h_1 : Unit → motive Turing.ToPartrec.Code.zero')
  (h_2 : Unit → motive Turing.ToPartrec.Code.succ) (h_3 : Unit → motive Turing.ToPartrec.Code.tail)
  (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs)) (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g))
  (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g)) (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match Turing.ToPartrec.Code.zero' with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_1 ()
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.DefEqCacheKey.mk.inj : ∀ {lhs rhs : Lean.Expr} {configKey : UInt64} {lhs_1 rhs_1 : Lean.Expr} {configKey_1 : UInt64},
  { lhs := lhs, rhs := rhs, configKey := configKey } = { lhs := lhs_1, rhs := rhs_1, configKey := configKey_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ configKey = configKey_1
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Choose `N` sufficiently large such that a particular quantity is small.  -/
_private.Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real.0.RealRMK.exists_nat_large : ∀ (a' b' : ℝ) {ε : ℝ}, 0 < ε → ∃ N, 0 < N ∧ a' / ↑N * (b' + a' / ↑N) ≤ ε
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.LocallyQuasiFinite f ↔
    ∀ (x : ↥Y), AlgebraicGeometry.IsFinite (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f x)
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.add_of_tendstoInMeasure_const : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'}
  {μ' : MeasureTheory.Measure Ω'} [inst : MeasureTheory.IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''}
  {μ'' : MeasureTheory.Measure Ω''} [inst_1 : MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E}
  {Z : Ω' → E} {l : Filter ι} [inst_2 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_4 : BorelSpace E]
  {X Y : ι → Ω'' → E} [l.IsCountablyGenerated] {c : E},
  MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ' →
    (MeasureTheory.TendstoInMeasure μ'' Y l fun x => c) →
      (∀ (i : ι), AEMeasurable (Y i) μ'') →
        MeasureTheory.TendstoInDistribution (fun n => X n + Y n) l (fun ω => Z ω + c) (fun x => μ'') μ'
-- Init.Data.BitVec.Lemmas
/-- Accessing bits in `x.rotateLeft r` the range `[0, r)` is equal to
accessing bits `x` in the range `[w - r, w)`.

Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>

(x.rotateLeft 2).getLsbD ⟨i, i < 2⟩
= <3 2 1 0 | 6 5>.getLsbD ⟨i, i < 2⟩
= <6 5>[i]
= <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)]
= <6 5 | 4 3 2 1 0>[i + 7 - 2]
 -/
BitVec.getLsbD_rotateLeftAux_of_lt : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ}, i < r → (x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i)
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.mOfFn.match_1.splitter : {m : Type u_3 → Type u_2} →
  {α : Type u_3} →
    (motive : (x : ℕ) → (Fin x → m α) → Sort u_1) →
      (x : ℕ) →
        (x_1 : Fin x → m α) →
          ((x : Fin 0 → m α) → motive 0 x) → ((n : ℕ) → (f : Fin (n + 1) → m α) → motive n.succ f) → motive x x_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constInsertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ (l : List (α × β)), (Std.DTreeMap.Raw.Const.insertMany t₁ l).Equiv (Std.DTreeMap.Raw.Const.insertMany t₂ l)
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.evalTryTrace : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.UniformSpace.Cauchy
cauchySeq_of_controlled : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [Nonempty β] (U : β → SetRel α α),
  (∀ s ∈ uniformity α, ∃ n, U n ⊆ s) → ∀ {f : β → α}, (∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) → CauchySeq f
-- Init.Data.List.MapIdx
List.length_mapFinIdx_go : ∀ {α : Type u_1} {as : List α} {α_1 : Type u_2} {f : (i : ℕ) → α → i < as.length → α_1} {bs : List α} {acc : Array α_1}
  {h : bs.length + acc.size = as.length}, (List.mapFinIdx.go as f bs acc h).length = as.length
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_eq_zero_of_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  V x = 0 → W x = 0 → VectorField.mlieBracketWithin I V W s x = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial] {Z : ModuleCat k}
  (h : ModuleCat.of k (Additive G →+ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.H1π A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H1IsoOfIsTrivial A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocycles₁IsoOfIsTrivial A).hom h
-- Init.Data.UInt.Bitwise
USize.zero_or : ∀ {a : USize}, 0 ||| a = a
-- Init.Grind.AC
Lean.Grind.AC.eq_erase_dup_cert : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Turn a bilinear map into a homomorphism.  -/
SemimoduleCat.ofHom₂ : {R : Type u_1} →
  [inst : CommSemiring R] → {M N P : SemimoduleCat R} → (↑M →ₗ[R] ↑N →ₗ[R] ↑P) → (M ⟶ SemimoduleCat.of R (N ⟶ P))
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.eq_of_eq_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f g : E →ₗ.[R] F}, f.graph = g.graph → f = g
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.homotopicRel_empty : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)},
  f₀.HomotopicRel f₁ ∅ ↔ f₀.Homotopic f₁
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.riemannianEDist_comm : ∀ {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 : (x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y : M},
  Manifold.riemannianEDist I x y = Manifold.riemannianEDist I y x
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- Closed balls in `StrongDual 𝕜 E` pull back to closed sets in `WeakDual 𝕜 E`.  -/
WeakDual.isClosed_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x' : StrongDual 𝕜 E) (r : ℝ), IsClosed (⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall x' r)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_ball : ∀ {a r : ℝ}, 0 ≤ r → MeasureTheory.volume.real (Metric.ball a r) = 2 * r
-- Mathlib.CategoryTheory.MorphismProperty.CommaSites
CategoryTheory.MorphismProperty.exists_map_eq_of_presieve : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition],
  ∀ K ≤ P.precoverage,
    ∀ {X : P.Over ⊤ S} {R : CategoryTheory.Presieve ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).obj X)},
      R ∈
          (CategoryTheory.Precoverage.comap (CategoryTheory.Over.forget S) K).coverings
            ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).obj X) →
        ∃ T, CategoryTheory.Presieve.map (CategoryTheory.MorphismProperty.Over.forget P ⊤ S) T = R
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_quotient_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] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M], LieModule.IsNilpotent L (M ⧸ N) ↔ ∃ k, LieModule.lowerCentralSeries R L M k ≤ N
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.semireducible.sizeOf_spec : sizeOf Lean.ReducibilityStatus.semireducible = 1
-- Init.Internal.Order.Basic
Lean.Order.PProd.chain.snd : {α : Sort u} → {β : Sort v} → [Lean.Order.CCPO α] → [Lean.Order.CCPO β] → (α ×' β → Prop) → β → Prop
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.continuous : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), Continuous ⇑e
-- Batteries.Data.Vector.Lemmas
Vector.scanlM_pure : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : β → α → β} {as : Vector α n}, Vector.scanlM (fun x1 x2 => pure (f x1 x2)) init as = pure (Vector.scanl f init as)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.cokernelBiprodInlIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.cokernelBiprodInlIso.inv =
    (CategoryTheory.Limits.biprod.isCokernelInlCokernelFork X Y).desc
      (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inl 0))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.diff_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ \ m₃).Equiv (m₂ \ m₃)
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- An induction principle for additive closure membership. If `p` holds for `0` and all
elements of `s`, and is preserved under addition, then `p` holds for all elements of the
additive closure of `s`.  -/
AddSubmonoid.closure_induction : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {motive : (x : M) → x ∈ AddSubmonoid.closure s → Prop},
  (∀ (x : M) (h : x ∈ s), motive x ⋯) →
    motive 0 ⋯ →
      (∀ (x y : M) (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s),
          motive x hx → motive y hy → motive (x + y) ⋯) →
        ∀ {x : M} (hx : x ∈ AddSubmonoid.closure s), motive x hx
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_le_ofNat : ∀ {m : ℕ∞} {n : ℕ} [inst : n.AtLeastTwo], ↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n
-- Init.Data.Float.Model.Float
Float.Model.instDiv : Div Float.Model
-- Mathlib.Data.Int.Bitwise
Int.testBit_lnot : ∀ (n : ℤ) (k : ℕ), n.lnot.testBit k = !n.testBit k
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_strictMono : ∀ (α : Type u_1) [inst : Preorder α], StrictMono UpperSet.Ici
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.instFaithfulKaroubiFunctorKaroubiFunctorCategoryEmbedding : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C],
  (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).Faithful
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h'' : (P out).Property { down := false })
  (h_1 : (h'' : (P out).Property { down := true }) → motive ⟨{ down := true }, h''⟩)
  (h_2 : (h'' : (P out).Property { down := false }) → motive ⟨{ down := false }, h''⟩),
  (match ⟨{ down := false }, h''⟩ with
    | ⟨{ down := true }, h''⟩ => h_1 h''
    | ⟨{ down := false }, h''⟩ => h_2 h'') =
    h_2 h''
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(α →₁ₛ[μ] ℝ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.L1.SimpleFunc.negPart f)) =ᵐ[μ]
    ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f).negPart
-- Mathlib.Order.PiLex
Pi.lex_lt_of_lt : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : (i : ι) → PartialOrder (β i)] {r : ι → ι → Prop},
  WellFounded r → ∀ {x y : (i : ι) → β i}, x < y → Pi.Lex r (fun {i} x1 x2 => x1 < x2) x y
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupportValueSet : Type
-- Mathlib.Topology.Order.NhdsSet
hasBasis_nhdsSet_Ici_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a : α) [Nonempty ↑(Set.Iio a)],
  (nhdsSet (Set.Ici a)).HasBasis (fun x => x < a) Set.Ioi
-- Aesop.Tree.Data
Aesop.MVarCluster.state : Aesop.MVarCluster → Aesop.NodeState
-- Mathlib.Computability.Primrec.Basic
Primrec.eq : ∀ {α : Type u_1} [inst : Primcodable α], PrimrecRel Eq
-- Mathlib.Algebra.Quandle
Rack.toEnvelGroup.mapAux.eq_3 : ∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
  (a b : Rack.PreEnvelGroup R),
  Rack.toEnvelGroup.mapAux f (a.mul b) = Rack.toEnvelGroup.mapAux f a * Rack.toEnvelGroup.mapAux f b
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulLeftMono : ∀ {α : Type u} [inst : LE α] [inst_1 : Mul α] [c : MulLeftMono α], MulLeftMono αᵒᵈ
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.frequently_atTop : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] {p : α → Prop} [Nonempty α],
  (∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b, a ≤ b ∧ p b
-- Mathlib.Topology.Neighborhoods
eventually_mem_nhds_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, (∀ᶠ (x' : X) in nhds x, s ∈ nhds x') ↔ s ∈ nhds x
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_subset_balancedCoreAux : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, balancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientiInfSubgroupOfEmbedding_apply : ∀ {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α)
  (q : ↥H ⧸ (⨅ i, f i).subgroupOf H) (i : ι),
  (Subgroup.quotientiInfSubgroupOfEmbedding f H) q i = Subgroup.quotientSubgroupOfMapOfLE H ⋯ q
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (self : F ⊣₂ G) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁)
  {Z : CategoryTheory.Functor C₂ C₂} (h : (F.obj Y₁).comp (G.obj (Opposite.op X₁)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.adj X₁).unit
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) h) =
    CategoryTheory.CategoryStruct.comp (self.adj Y₁).unit
      (CategoryTheory.CategoryStruct.comp ((F.obj Y₁).whiskerLeft (G.map f.op)) h)
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- This alias for `Functor.CommShift₂.comm` allows to use the dot notation.  -/
CategoryTheory.Functor.commShift₂_comm_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  (h : CategoryTheory.CommShift₂Setup D M) [self : G.CommShift₂ h] (X₁ : C₁) (X₂ : C₂) (m n : M) {Z : D}
  (h_1 : (CategoryTheory.shiftFunctor D n).obj ((CategoryTheory.shiftFunctor D m).obj ((G.flip.obj X₂).obj X₁)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso (G.obj ((CategoryTheory.shiftFunctor C₁ m).obj X₁)) n).hom.app X₂)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso (G.flip.obj X₂) m).hom.app X₁))
        h_1) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso (G.flip.obj ((CategoryTheory.shiftFunctor C₂ n).obj X₂)) m).hom.app X₁)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D m).map ((CategoryTheory.Functor.commShiftIso (G.obj X₁) n).hom.app X₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm ((G.obj X₁).obj X₂) m n).inv
          (CategoryTheory.CategoryStruct.comp
            ((↑(h.ε m n)).app
              ((CategoryTheory.shiftFunctor D n).obj ((CategoryTheory.shiftFunctor D m).obj ((G.obj X₁).obj X₂))))
            h_1)))
-- Mathlib.LinearAlgebra.Matrix.DotProduct
/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`.  -/
dotProduct_star_self_nonneg : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] (v : n → R), 0 ≤ star v ⬝ᵥ v
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_add : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f g : M →ₗ[R] N),
  LinearMap.baseChange A (f + g) = LinearMap.baseChange A f + LinearMap.baseChange A g
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.homRel.σ_comp_σ : ∀ {n : ℕ} {i j : Fin (n + 1)},
  i ≤ j →
    FreeSimplexQuiver.homRel
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i.castSucc))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j)))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.succ))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i)))
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), nndist x y = nndist y x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List ((a : α) × β a)}
  {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).get k h' = t.get k ⋯
-- Lean.Meta.Tactic.Grind.Internalize
/-- Applies `addSplitCandidatesForExt` if `funext` is enabled.  -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addSplitCandidatesForFunext : Lean.Expr → ℕ → optParam (Option Lean.Expr) none → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Logic.Equiv.Defs
Equiv.cast_eq_iff_heq : ∀ {α β : Sort u_1} (h : α = β) {a : α} {b : β}, (Equiv.cast h) a = b ↔ a ≍ b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
StarAlgebra.elemental.instNormedCommRingSubtypeMemStarSubalgebraOfIsStarNormal : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : NormedRing A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] →
              [inst_5 : ContinuousStar A] →
                [inst_6 : StarModule R A] → (a : A) → [IsStarNormal a] → NormedCommRing ↥(StarAlgebra.elemental R a)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData) {Z : C} (h_1 : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.CategoryStruct.comp h.homologyIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.inv (CategoryTheory.CategoryStruct.comp S.homologyπ h_1)
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_vecAlt1 : ∀ {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α),
  Matrix.vecAlt1 h (Matrix.vecCons x (Matrix.vecCons y u)) = Matrix.vecCons y (Matrix.vecAlt1 ⋯ u)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.coe_pow : ∀ (M : Type u_4) [inst : AddZero M] (f : AddMonoid.End M) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]