mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_map_mul : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] (a : α) (s : Multiset α),
  (Multiset.map (fun x => a * x) s).gcd = normalize a * s.gcd
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.map_pt : ∀ {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} (c : CategoryTheory.Limits.Multifork d)
  (F : CategoryTheory.Functor C D), (c.map F).pt = F.obj c.pt
-- Mathlib.CategoryTheory.Sites.Canonical
/-- If `J` is subcanonical, then any representable is a `J`-sheaf.  -/
CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical]
  (P : CategoryTheory.Functor Cᵒᵖ (Type w)) [P.IsRepresentable], CategoryTheory.Presieve.IsSheaf J P
-- Mathlib.GroupTheory.Coset.Basic
mem_rightCoset_iff : ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ MulOpposite.op a • s ↔ x * a⁻¹ ∈ s
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_comp : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) {K : ι → Type u_2}
  [inst_5 : (i : ι) → AddCommMonoid (K i)] [inst_6 : (i : ι) → Module R (K i)] (g : (i : ι) → N i →ₗ[R] K i),
  (DirectSum.lmap fun i => g i ∘ₗ f i) = DirectSum.lmap g ∘ₗ DirectSum.lmap f
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.natPow_zero_natMod_succ_succ : ∀ {a : ℕ} {m : ℕ}, (a.pow 0).mod m.succ.succ = 1
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.IsSetAlgebra.mk : ∀ {α : Type u_1} {𝒜 : Set (Set α)},
  ∅ ∈ 𝒜 → (∀ ⦃s : Set α⦄, s ∈ 𝒜 → sᶜ ∈ 𝒜) → (∀ ⦃s t : Set α⦄, s ∈ 𝒜 → t ∈ 𝒜 → s ∪ t ∈ 𝒜) → MeasureTheory.IsSetAlgebra 𝒜
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- The natural isomorphism from the dual of a subspace `W` to `W.dualLift.range`.  -/
Subspace.dualEquivDual : {K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (W : Subspace K V) → Module.Dual K ↥W ≃ₗ[K] ↥W.dualLift.range
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommAlgCat.Hom.Simps.hom : {R : Type u} → [inst : CommRing R] → (A B : CommAlgCat R) → A.Hom B → ↑A →ₐ[R] ↑B
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_alterₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β},
      Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.Const.alterₘ m a f)
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
/-- Given `P : ObjectProperty C`, we say that `P` is closed under quotients,
if for any epimorphism `X ⟶ Y`, `P X` implies `P Y`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderQuotients : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_natAdd : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (i : Fin n),
  (Polynomial.degreeLT.addLinearEquiv R m n) ((Polynomial.degreeLT.basis R (m + n)) (Fin.natAdd m i)) =
    (0, (Polynomial.degreeLT.basis R n) i)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNNNorm_diagonal : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (v : n → 𝕜),
  ‖Matrix.diagonal v‖₊ = ‖v‖₊
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma implies that a single function is uniformly integrable (in the probability sense).  -/
MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : α → β},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.StronglyMeasurable f →
      ∀ {ε : ℝ}, 0 < ε → ∃ M, 0 < M ∧ MeasureTheory.eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.inv_variableChange_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R)
  [inst_1 : W.IsElliptic], (C • W).Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivFunctorCompSndIso_inv_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (X_1 : A'),
  (CategoryTheory.Sum.functorEquivFunctorCompSndIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inr X_1))
-- Mathlib.Topology.Separation.GDelta
PerfectlyNormalSpace.toCompletelyNormalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PerfectlyNormalSpace X], CompletelyNormalSpace X
-- Mathlib.Order.Preorder.Chain
Monotone.isChain_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  Monotone f → IsChain (fun x1 x2 => x1 ≤ x2) s → IsChain (fun x1 x2 => x1 ≤ x2) (f '' s)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) =
    (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsGLB.exists_of_nonempty_of_not_isPredPrelimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α},
  IsGLB (Set.range f) x → ¬Order.IsPredPrelimit x → ∃ i, f i = x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.ne : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos → startPos ≠ endPos
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_smul_map : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure]
  [μ.Regular] (φ : G ≃ₜ* G), MeasureTheory.mulEquivHaarChar φ • MeasureTheory.Measure.map (⇑φ) μ = μ
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isConnected_setOfPred_sSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P},
  x ∉ s → (↑s).Nonempty → IsConnected {y | s.SSameSide x y}
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_sdiff : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).mulIndicator f = t.mulIndicator f * (s.mulIndicator f)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} {h : W'.Nonsingular x y}
  {p : W'.Point → Prop} (p0 : p WeierstrassCurve.Affine.Point.zero) (ph : p (WeierstrassCurve.Affine.Point.some x y h)),
  (WeierstrassCurve.Affine.nonsingularPointEquivSubtype p0).symm (some ⟨(x, y), ⋯⟩) =
    ⟨WeierstrassCurve.Affine.Point.some x y h, ph⟩
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_translationNumber_of_add_nat_le : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℕ}, x + ↑m ≤ f x → ↑m ≤ f.translationNumber
-- Std.Data.Internal.List.Associative
Std.Internal.List.beqModel_iff_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  [∀ (k : α), LawfulBEq (β k)] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ → (Std.Internal.List.beqModel l₁ l₂ = true ↔ l₁.Perm l₂)
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearMap.isBigOWith_comp : ∀ {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_5} {G : Type u_6} [inst : SeminormedAddCommGroup F]
  [inst_1 : SeminormedAddCommGroup G] [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NontriviallyNormedField 𝕜₃]
  [inst_4 : NormedSpace 𝕜₂ F] [inst_5 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃] {α : Type u_7}
  (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α), Asymptotics.IsBigOWith ‖g‖ l (fun x' => g (f x')) f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
_private.Mathlib.Algebra.Order.Monoid.Unbundled.Units.0.Units.mul_le_mul_iff_right : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a * ↑u ≤ b * ↑u ↔ a ≤ b
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
/-- The source (Zariski-)local closure of `P` is satisfied if there exists
an open cover of the source on which `P` is satisfied.  -/
AlgebraicGeometry.sourceLocalClosure : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Lean.Server.InfoUtils
/-- Construct a hover popup, if any, from an info node in a context. -/
Lean.Elab.Info.fmtHover? : Lean.Elab.ContextInfo → Lean.Elab.Info → IO (Option Lean.FormatWithInfos)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Set.algebraMap_mem_center : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R A) r ∈ Set.center A
-- Mathlib.RingTheory.Perfection
/-- Create a `PerfectionMap` from an isomorphism to the perfection.  -/
PerfectionMap.mk' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {f : P →+* R} (g : P ≃+* Perfection R p),
  (Perfection.lift p P R) f = ↑g → PerfectionMap p f
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchesAt_iff_revMatchesAt_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {base : s.Pos}
  {pos : (s.sliceTo base).Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔
    String.Slice.Pattern.Model.RevMatchesAt pat (String.Slice.Pos.ofSliceTo pos)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelCompIsIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.cokernelCompIsIso f g).hom =
    CategoryTheory.Limits.cokernel.desc (CategoryTheory.CategoryStruct.comp f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) (CategoryTheory.Limits.cokernel.π f)) ⋯
-- Mathlib.Algebra.Module.Equiv.Defs
RingEquiv.toSemilinearEquiv_apply : ∀ {R : Type u_1} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (a : R),
  f.toSemilinearEquiv a = f a
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedRing.toNorm : {α : Type u_5} → [self : NonUnitalSeminormedRing α] → Norm α
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.add.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_3 m n
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compPartialSumSource.eq_1 : ∀ (m M N : ℕ),
  FormalMultilinearSeries.compPartialSumSource m M N =
    (Finset.Ico m M).sigma fun n => Fintype.piFinset fun _i => Finset.Ico 1 N
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C),
  CategoryTheory.Limits.HasLimit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.inhabited : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → Inhabited ↥p
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasureTheory.AddContent.measure.congr_simp : ∀ {α : Type u_1} {C : Set (Set α)} [mα : MeasurableSpace α] (m m_1 : MeasureTheory.AddContent ENNReal C) (e_m : m = m_1)
  (hC : MeasureTheory.IsSetSemiring C) (hC_gen : mα ≤ MeasurableSpace.generateFrom C)
  (m_sigma_subadd : m.IsSigmaSubadditive), m.measure hC hC_gen m_sigma_subadd = m_1.measure hC hC_gen ⋯
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk.injEq : ∀ {R : Type u_1} {a b c : R} (re imI imJ imK re_1 imI_1 imJ_1 imK_1 : R),
  ({ re := re, imI := imI, imJ := imJ, imK := imK } = { re := re_1, imI := imI_1, imJ := imJ_1, imK := imK_1 }) =
    (re = re_1 ∧ imI = imI_1 ∧ imJ = imJ_1 ∧ imK = imK_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_mul : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r₁ r₂ : k),
  AffineMap.homothety c (r₁ * r₂) = (AffineMap.homothety c r₁).comp (AffineMap.homothety c r₂)
-- Mathlib.Data.List.Dedup
List.dedup_cons_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∈ l → (a :: l).dedup = l.dedup
-- Init.Data.Char.Lemmas
Char.le_def : ∀ {a b : Char}, a ≤ b ↔ a.val ≤ b.val
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.restrict_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {H : Type u_6} [inst_10 : Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G)
  (f : ContIntertwiningMap π π') (v : V), (ContIntertwiningMap.restrict φ f) v = f v
-- Aesop.Rule.Forward
/-- The rule's priority.  -/
Aesop.ForwardRule.prio : Aesop.ForwardRule → Aesop.ForwardRulePriority
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The morphism property in `Cᵒᵖ` associated to a morphism property in `C`  -/
CategoryTheory.MorphismProperty.op : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty Cᵒᵖ
-- Mathlib.Algebra.Algebra.Hom.Rat
/-- Reinterpret a `RingHom` as a `ℚ`-algebra homomorphism. This actually yields an equivalence,
see `RingHom.equivRatAlgHom`.  -/
RingHom.toRatAlgHom : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] → [inst_1 : Ring S] → [inst_2 : Algebra ℚ R] → [inst_3 : Algebra ℚ S] → (R →+* S) → R →ₐ[ℚ] S
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.instIteratorOfPure.match_3.splitter : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
        {m : Type → Type u_1} →
          {s : String.Slice} →
            (motive : Std.IterM m String.Slice → Sort u_2) →
              (x : Std.IterM m String.Slice) →
                ((currPos : s.Pos) →
                    (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                      motive { internalState := String.Slice.RevSplitIterator.operating currPos searcher }) →
                  (Unit → motive { internalState := String.Slice.RevSplitIterator.atEnd }) → motive x
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.instInhabitedChooseArg.default : Mathlib.Tactic.Choose.ChooseArg
-- Init.Data.Int.DivMod.Lemmas
Int.tmod.eq_1 : ∀ (m n : ℕ), (Int.ofNat m).tmod (Int.ofNat n) = Int.ofNat (m % n)
-- Mathlib.Algebra.Module.Submodule.Equiv
Submodule.equivSubtypeMap_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M}
  {q : Submodule R ↥p} (x : ↥q), ↑((p.equivSubtypeMap q) x) = (p.subtype.domRestrict q) x
-- Plausible.Arbitrary
Plausible.Fin.Arbitrary : {n : ℕ} → Plausible.Arbitrary (Fin n.succ)
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderPred_eq : ∀ {n : ℕ}, Order.pred = fun i => Fin.cases 0 Fin.castSucc i
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.apply_coe_mem_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (K : AddSubgroup G) (x : ↥K),
  f ↑x ∈ AddSubgroup.map f K
-- Init.Grind.Lemmas
Lean.Grind.eq_false_of_or_eq_false_right : ∀ {a b : Prop}, (a ∨ b) = False → b = False
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (n : ℤ) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGEδLT n).app X) = 0
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul_nc.match_1.splitter : (motive : Lean.Grind.CommRing.Mon → Sort u_1) →
  (m₁ : Lean.Grind.CommRing.Mon) →
    (Unit → motive Lean.Grind.CommRing.Mon.unit) →
      ((pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit)) →
        ((pw : Lean.Grind.CommRing.Power) →
            (m₁ : Lean.Grind.CommRing.Mon) →
              (m₁ = Lean.Grind.CommRing.Mon.unit → False) → motive (Lean.Grind.CommRing.Mon.mult pw m₁)) →
          motive m₁
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r : {n : ℕ} → ZMod n → DihedralGroup n
-- Lean.Expr
Lean.FVarId.mk.injEq : ∀ (name name_1 : Lean.Name), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.includeLeft_bijective : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B],
  Function.Bijective ⇑(algebraMap R B) → Function.Bijective ⇑Algebra.TensorProduct.includeLeft
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_neg : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Neg γ] (f : α → β) (g : α → γ) (e : β → γ),
  Function.extend f (-g) (-e) = -Function.extend f g e
-- Mathlib.Order.Preorder.Finsupp
Finsupp.orderEmbeddingToFun_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : LE M] (f : ι →₀ M) (a : ι),
  Finsupp.orderEmbeddingToFun f a = f a
-- Mathlib.Analysis.Calculus.FDeriv.Comp
fderiv_comp_fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G},
  DifferentiableAt 𝕜 g (f x) →
    DifferentiableWithinAt 𝕜 f s x →
      UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (g ∘ f) s x = fderiv 𝕜 g (f x) ∘SL fderivWithin 𝕜 f s x
-- Lean.Expr
Lean.Int.mkInstHMul : Lean.Expr
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Balanced C] (F : CategoryTheory.Functor C D)
  [F.ReflectsMonomorphisms] [F.ReflectsEpimorphisms], F.ReflectsIsomorphisms
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toArray_rco_eq : ∀ {m n i : ℕ}, ((m...n).toArray[i]?.isSome = true) = (i < n - m)
-- Mathlib.CategoryTheory.Action.Monoidal
Action.leftDual_v : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {H : Type u_3} [inst_2 : Group H] (X : Action V H) [inst_3 : CategoryTheory.LeftRigidCategory V], (ᘁX).V = ᘁX.V
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.cuspFunction_mul : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b),
        UpperHalfPlane.cuspFunction h ⇑(f.mul g) = UpperHalfPlane.cuspFunction h ⇑f * UpperHalfPlane.cuspFunction h ⇑g
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.mk : Lean.Elab.Structural.IndGroupInfo → List Lean.Level → Array Lean.Expr → Lean.Elab.Structural.IndGroupInst
-- Init.Data.String.Bootstrap
/-- Creates a string that contains the characters in a list, in order.

Examples:
* `['L', '∃', '∀', 'N'].asString = "L∃∀N"`
* `[].asString = ""`
* `['a', 'a', 'a'].asString = "aaa"`
 -/
List.asString : List Char → String
-- Mathlib.Condensed.Explicit
/-- The condensed object associated to a presheaf on `CompHaus` whose postcomposition with the
forgetful functor preserves finite products and satisfies the equalizer condition.
 -/
Condensed.ofSheafForgetCompHaus : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {FA : A → A → Type u_2} →
      {CA : A → Type u_3} →
        [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory A FA] →
            [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] →
              (F : CategoryTheory.Functor CompHausᵒᵖ A) →
                [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] →
                  CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A)) → Condensed A
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.zeta_mul_vonMangoldt : ↑ArithmeticFunction.zeta * ArithmeticFunction.vonMangoldt = ArithmeticFunction.log
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
/-- Given a multiequalizer diagram `I : MulticospanIndex (Type u)` in the category of
types and `c` a multifork for `I`, this is the canonical map `c.pt → I.sections`.  -/
CategoryTheory.Limits.Multifork.toSections : {J : CategoryTheory.Limits.MulticospanShape} →
  {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} → (c : CategoryTheory.Limits.Multifork I) → c.pt → I.sections