mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.bientails.of_eq : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P = Q → P ⊣⊢ₛ Q
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.toTopCat_map : ∀ (X : TopCat) {U V : TopologicalSpace.Opens ↑X} {f : U ⟶ V} {x : ↑X} {h : x ∈ U},
  (CategoryTheory.ConcreteCategory.hom ((TopologicalSpace.Opens.toTopCat X).map f)) ⟨x, h⟩ = ⟨x, ⋯⟩
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.natCast_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {b₁ b₃ : R} {a₁ a₃ : ℕ} (a₂ : ℕ),
  ↑a₁ = b₁ → ↑a₃ = b₃ → ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart_add_ae_eq : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E]
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f g : ℕ → Ω → E},
  MeasureTheory.Martingale f ℱ μ →
    (MeasureTheory.StronglyAdapted ℱ fun n => g (n + 1)) →
      g 0 = 0 →
        (∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) → ∀ (n : ℕ), MeasureTheory.predictablePart (f + g) ℱ μ n =ᵐ[μ] g n
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Right homotopy is closed under composition (on the right).  -/
CategoryTheory.Arrow.RightHomotopy.compRight : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v w : CategoryTheory.Arrow V} →
        {e f : u ⟶ v} →
          CategoryTheory.Arrow.RightHomotopy e f →
            (g : v ⟶ w) →
              CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp e g)
                (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.erase0 c = Lean.Meta.Grind.AC.EqCnstrProof.erase0 c_1) = (c = c_1)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j : 𝒰.I₀}
  (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))),
  ∃ k hki hkj y, (CategoryTheory.Limits.pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) y = x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitIsoSwapCompColim_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.colimitIsoSwapCompColim G).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).hom
      (CategoryTheory.Limits.colimMap (G.flipIsoCurrySwapUncurry.hom.app X))
-- Init.Data.Array.Lemmas
Array.mem_map : ∀ {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {xs : Array α}, b ∈ Array.map f xs ↔ ∃ a ∈ xs, f a = b
-- Mathlib.Topology.Category.LightProfinite.Sequence
/-- The one point compactification of the natural numbers as a light profinite set.  -/
LightProfinite.«termℕ∪{∞}» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Action.Basic
/-- Actions/representations of the trivial monoid are just objects in the ambient category.  -/
Action.actionPUnitEquivalence : {V : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} V] → Action V PUnit.{u_3 + 1} ≌ V
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (e : F ≅ F') (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  [inst_4 : F'.IsContinuous J K],
  (CategoryTheory.Functor.sheafPushforwardContinuousIso e A J K).hom =
    CategoryTheory.Functor.sheafPushforwardContinuousNatTrans e.inv A J K
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, t.getKey! a = (t.getKey? a).get!
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.mk.injEq : ∀ (mvarId : Lean.MVarId) (newHs : Array Lean.FVarId) (subst : Lean.Meta.FVarSubst) (mvarId_1 : Lean.MVarId)
  (newHs_1 : Array Lean.FVarId) (subst_1 : Lean.Meta.FVarSubst),
  ({ mvarId := mvarId, newHs := newHs, subst := subst } = { mvarId := mvarId_1, newHs := newHs_1, subst := subst_1 }) =
    (mvarId = mvarId_1 ∧ newHs = newHs_1 ∧ subst = subst_1)
-- Mathlib.MeasureTheory.Function.Egorov
/-- **Alias** of `MeasureTheory.Egorov.tendstoUniformlyOn_sdiff_iUnionNotConvergentSeq`. -/
MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  TendstoUniformlyOn f g Filter.atTop (s \ MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg)
-- Lean.Parser.Term
Lean.Parser.Term.logNamedWarningAtMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftStar_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x),
  (CategoryTheory.WithTerminal.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z
-- Mathlib.Data.Num.Lemmas
PosNum.cmp_swap : ∀ (m n : PosNum), (m.cmp n).swap = n.cmp m
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.counit_app : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] (c : C),
  (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app c = (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom
-- Mathlib.Data.Int.Cast.Lemmas
/-- Two additive monoid isomorphisms `f`, `g` from `ℤ` to an additive monoid are equal
if `f 1 = g 1`.  -/
AddEquiv.ext_int : ∀ {A : Type u_5} [inst : AddMonoid A] {f g : ℤ ≃+ A}, f 1 = g 1 → f = g
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_of_omega0_sq_le : ∀ {o : Ordinal.{u_1}}, Ordinal.omega0 ^ 2 ≤ o → Cardinal.preAleph o = Cardinal.aleph o
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorOptions.mk.inj : ∀ {toWorkDoneProgressOptions toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions},
  { toWorkDoneProgressOptions := toWorkDoneProgressOptions } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1 } →
    toWorkDoneProgressOptions = toWorkDoneProgressOptions_1
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.localDeclsEqualUpToIdsCore : Lean.LocalDecl → Lean.LocalDecl → ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM Bool
-- Mathlib.Geometry.Polygon.Basic
/-- Polygons with nondegenerate vertices also have nondegenerate edges.  -/
Polygon.HasNondegenerateVertices.hasNondegenerateEdges : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {n : ℕ} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] [inst_4 : NeZero n] [Nontrivial R] {poly : Polygon P n},
  Polygon.HasNondegenerateVertices R poly → poly.HasNondegenerateEdges
-- Init.Data.Array.Subarray
/-- Folds a monadic operation from right to left over the elements in a subarray.

An accumulator of type `β` is constructed by starting with `init` and monadically combining each
element of the subarray with the current accumulator value in turn, moving from the end to the
start. The monad in question may permit early termination or repetition.

Examples:
```lean example
#eval #["red", "green", "blue"].toSubarray.foldrM (init := "") fun x acc => do
  let l ← Option.guard (· ≠ 0) x.length
  return s!"{acc}({l}){x} "
```
```output
some "(4)blue (5)green (3)red "
```
```lean example
#eval #["red", "green", "blue"].toSubarray.foldrM (init := 0) fun x acc => do
  let l ← Option.guard (· ≠ 5) x.length
  return s!"{acc}({l}){x} "
```
```output
none
```
 -/
Subarray.foldrM : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → β → m β) → β → Subarray α → m β
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {cc : CategoryTheory.Limits.CokernelCofork S.f}
  (hcc : CategoryTheory.Limits.IsColimit cc),
  hcc.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯) =
    CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom S.fromOpcycles
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instStar : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] → [inst_3 : StarAddMonoid β] → [ContinuousStar β] → Star (ZeroAtInftyContinuousMap α β)
-- Init.Data.Fin.Lemmas
Fin.lt_of_lt_of_le : ∀ {n : ℕ} {a b c : Fin n}, a < b → b ≤ c → a < c
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.star : ∀ {α : Type u} {R : Type u_2} [inst : Star R] {f g : α → R} {l : Filter α}, f =ᶠ[l] g → star f =ᶠ[l] star g
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting.eq_1 : ∀ (n : ℕ), n.primeCounting = (n + 1).primeCounting'
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instTransOrdOrdinal : Std.TransOrd Std.Time.Weekday.Ordinal
-- Mathlib.Topology.Compactness.LocallyCompact
/-- In a weakly locally compact space,
every compact set is contained in the interior of a compact set.  -/
exists_compact_superset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] {K : Set X},
  IsCompact K → ∃ K', IsCompact K' ∧ K ⊆ interior K'
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq : {M : Type u_1} →
  {α : Type u_3} →
    [inst : Monoid M] →
      [inst_1 : MulAction M α] →
        [DecidableEq α] → (a : α) → DecidablePred fun x => x ∈ MulAction.stabilizerSubmonoid M a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Var : Type
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.compContinuousLinearMap_apply : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F)
  (n : ℕ) (v : Fin n → E), (p.compContinuousLinearMap u n) v = (p n) (⇑u ∘ v)
-- Mathlib.Analysis.Convex.BetweenList
AffineEquiv.list_sbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {l : List P} (f : P ≃ᵃ[R] P'),
  List.Sbtw R (List.map (⇑f) l) ↔ List.Sbtw R l
-- Mathlib.GroupTheory.IsSubnormal
AddSubgroup.IsSubnormal.brecOn : ∀ {G : Type u_2} [inst : AddGroup G] {motive : (a : AddSubgroup G) → a.IsSubnormal → Prop} {a : AddSubgroup G}
  (t : a.IsSubnormal),
  (∀ (a : AddSubgroup G) (t : a.IsSubnormal), AddSubgroup.IsSubnormal.below t → motive a t) → motive a t
-- Mathlib.Algebra.DirectSum.Basic
/-- `DirectSum ι β` is the direct sum of a family of additive commutative monoids `β i`.

Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum ι β`.  -/
DirectSum : (ι : Type v) → (β : ι → Type w) → [(i : ι) → AddCommMonoid (β i)] → Type (max w v)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The right arrow of the walking span.  -/
CategoryTheory.Limits.WalkingSpan.Hom.snd : CategoryTheory.Limits.WalkingSpan.zero ⟶ CategoryTheory.Limits.WalkingSpan.right
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobeniusAlgEquiv_symm_apply : ∀ (K : Type u_1) (R : Type u_2) [inst : Field K] [inst_1 : Fintype K] [inst_2 : CommRing R] [inst_3 : Algebra K R]
  (p : ℕ) [inst_4 : ExpChar R p] [inst_5 : PerfectRing R p] (b : R),
  (FiniteField.frobeniusAlgEquiv K R p).symm b = Function.surjInv ⋯ b
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z Y X : C} {g : Z ⟶ Y} {f : Y ⟶ X}
  (seg : CategoryTheory.SplitMono g) (sef : CategoryTheory.SplitMono f),
  seg.comp sef = { retraction := CategoryTheory.CategoryStruct.comp sef.retraction seg.retraction, id := ⋯ }
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The abbreviation for the limit of `ProfiniteGrp`s.  -/
ProfiniteGrp.limit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J ProfiniteGrp.{max v u} → ProfiniteGrp.{max v u}
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_commute_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} [inst_1 : Add M],
  AddCommute m₁ m₂ → Commute r₁ r₂ → Commute (AddMonoidAlgebra.single m₁ r₁) (AddMonoidAlgebra.single m₂ r₂)
-- Mathlib.Topology.Connected.PathConnected
AddSubgroup.Normal.pathComponentZero : ∀ (G : Type u_4) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  (AddSubgroup.pathComponentZero G).Normal
-- Mathlib.Tactic.Linter.DocString
/-- Try to parse `docComment` as a Verso docstring, and report any parse errors,
ignoring those that should be silenced by linters.

`fileName` is the file where this docstring is defined (default: the file currently being
elaborated).
 -/
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.lintVersoSyntax : String →
  optParam (Option String) none →
    Lean.Elab.Command.CommandElabM (Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error))
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_apply_left`. -/
Submodule.IsCompl.projection_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : ↥p), (p.projection q hpq) ↑x = ↑x
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_neg_right`. -/
AntivaryOn.neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g s → MonovaryOn f (-g) s
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.mem_supported : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s : Set α} (p : α →₀ M), p ∈ Finsupp.supported M R s ↔ ↑p.support ⊆ s
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_eq' : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x >>> y = x >>> y.toNat
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_symm_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P) (m : M) (p : P), (LinearEquiv.rTensor M f).symm (p ⊗ₜ[R] m) = f.symm p ⊗ₜ[R] m
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM : MonadReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.DelabM
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.disjoint_def' : ∀ {M : Type u_1} [inst : MulOneClass M] {p₁ p₂ : Submonoid M},
  Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.coe_toPermHom : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) (k : ↥(Subgroup.centralizer {g}))
  (c : ↥g.cycleFactorsFinset), ↑(((Equiv.Perm.OnCycleFactors.toPermHom g) k) c) = ↑k * ↑c * (↑k)⁻¹
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_def : ∀ (x : Turing.ToPartrec.Code),
  Turing.ToPartrec.stepNormal x =
    match (motive := Turing.ToPartrec.Code → Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg) x with
    | Turing.ToPartrec.Code.zero' => fun k v => Turing.ToPartrec.Cfg.ret k (0 :: v)
    | Turing.ToPartrec.Code.succ => fun k v => Turing.ToPartrec.Cfg.ret k [v.headI.succ]
    | Turing.ToPartrec.Code.tail => fun k v => Turing.ToPartrec.Cfg.ret k v.tail
    | f.cons fs => fun k v => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.cons₁ fs v k) v
    | f.comp g => fun k v => Turing.ToPartrec.stepNormal g (Turing.ToPartrec.Cont.comp f k) v
    | f.case g => fun k v =>
      Nat.rec (Turing.ToPartrec.stepNormal f k v.tail) (fun y x => Turing.ToPartrec.stepNormal g k (y :: v.tail))
        v.headI
    | f.fix => fun k v => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitialIso_symm_apply_coe : ∀ (x : Cardinal.{u_1}), ↑((RelIso.symm Ordinal.isInitialIso) x) = x.ord
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_toUInt8 : ∀ (n : UInt16), n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec
-- Mathlib.Data.Sum.Order
OrderIso.sumLexAssoc_symm_apply_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (a : α),
  (OrderIso.sumLexAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_eq_delete_iff : ∀ {α : Type u_1} {M : Matroid α} {D₁ D₂ : Set α}, M.delete D₁ = M.delete D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E
-- Mathlib.RingTheory.Support
/-- The support of a module, defined as the set of primes `p` such that `Mₚ ≠ 0`.  -/
Module.support : (R : Type u_1) → (M : Type u_2) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Set (PrimeSpectrum R)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- This instance is here for convenience, but is literally the same as the coercion from
`hasCoeToMatrix`.  -/
Matrix.SpecialLinearGroup.instCoeFun : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → CoeFun (Matrix.SpecialLinearGroup n R) fun x => n → n → R
-- Mathlib.NumberTheory.ModularForms.NormTrace
/-- For `f` invariant under `𝒢`, this is a function on `(ℋ ⧸ 𝒢 ⊓ ℋ) × ℍ → ℂ` which packages up the
translates of `f` by `ℋ`.  -/
SlashInvariantForm.quotientFunc : {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} →
  {F : Type u_1} →
    F →
      [inst : FunLike F UpperHalfPlane ℂ] →
        {k : ℤ} → [SlashInvariantFormClass F 𝒢 k] → ↥ℋ ⧸ 𝒢.subgroupOf ℋ → UpperHalfPlane → ℂ
-- Lean.Server.FileWorker.InlayHints
Lean.Elab.InlayHintTextEdit.toLspTextEdit : Lean.FileMap → Lean.Elab.InlayHintTextEdit → Lean.Lsp.TextEdit
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as : ∀ {C₁ : Type u₁} {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₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ),
  ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).left.left.as = PUnit.unit
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_neg : ∀ {R : Type u_1} {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {f : α → α} {g : α → M}, birkhoffAverage R f (-g) = -birkhoffAverage R f g
-- Mathlib.Algebra.Polynomial.Laurent
/-- **Alias** of `LaurentPolynomial.support_coeff_toLaurent`.

---

The support of a polynomial `f` is a finset in `ℕ`.  The lemma `toLaurent_support f`
shows that the support of `f.toLaurent` is the same finset, but viewed in `ℤ` under the natural
inclusion `ℕ ↪ ℤ`.  -/
LaurentPolynomial.toLaurent_support : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  (Polynomial.toLaurent f).coeff.support = Finset.map Nat.castEmbedding f.support
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.revAll_bool_eq : ∀ {p : Char → Bool} {s : String.Slice}, s.revAll p = s.copy.toList.all p
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.lift'_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] (f : α →* β),
  (WithZero.lift' f) 0 = 0
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Array.mapM.map.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β),
  Array.mapM.map✝ f as i bs =
    if hlt : i < as.size then do
      let __do_lift ← f as[i]
      Array.mapM.map✝ f as (i + 1) (bs.push __do_lift)
    else pure bs
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_const_smul : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NormedField 𝕜] [inst_2 : Module 𝕜 E] [NormSMulClass 𝕜 E] (c : 𝕜) (f : α → E) (μ : MeasureTheory.Measure α),
  MeasureTheory.lpNorm (c • f) p μ = ↑‖c‖₊ * MeasureTheory.lpNorm f p μ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) (T : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) T ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) T)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) T) h) =
    h
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ringEquivOfRingEquiv_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T : Submonoid P}
  {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q] {j : R ≃+* P}
  (H : Submonoid.map j M = T),
  (IsLocalization.ringEquivOfRingEquiv S Q j H).symm = IsLocalization.ringEquivOfRingEquiv Q S j.symm ⋯
-- Mathlib.Order.Hom.Set
compl_strictAnti : ∀ (α : Type u_1) [inst : BooleanAlgebra α], StrictAnti compl