mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
and `f'` is antitone on the interior, then `f` is concave on `D`.  -/
AntitoneOn.concaveOn_of_deriv : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D → DifferentiableOn ℝ f (interior D) → AntitoneOn (deriv f) (interior D) → ConcaveOn ℝ D f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X : C}
  {mon : CategoryTheory.MonObj X} {X_1 : C} {mon_1 : CategoryTheory.MonObj X_1},
  { X := X, mon := mon } = { X := X_1, mon := mon_1 } → X = X_1 ∧ mon ≍ mon_1
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotIdx.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P P_1 : RootPairing ι R M N} (e_P : P = P_1) [inst_8 : P.IsCrystallographic] (i i_1 : ι),
  i = i_1 → ∀ (j j_1 : ι), j = j_1 → RootPairing.chainBotIdx i j = RootPairing.chainBotIdx i_1 j_1
-- Mathlib.Algebra.Order.Quantale
AddQuantale.sup_add_distrib : ∀ {α : Type u_1} {x y z : α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α],
  x ⊔ y + z = (x + z) ⊔ (y + z)
-- Lean.Elab.DeclModifiers
Lean.Elab.instToStringModifiers : ToString Lean.Elab.Modifiers
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.signedInfDist.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.signedInfDist i = s_1.signedInfDist i_1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.hom_ext_iff : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] {g₁ g₂ : DirectLimit G f →ₗ[R] P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁ ∘ₗ DirectLimit.Module.of R ι G f i = g₂ ∘ₗ DirectLimit.Module.of R ι G f i
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation.module : Lean.Elab.InlayHintLinkLocation → Lean.Name
-- Mathlib.Probability.Distributions.Pareto
/-- The pdf of the Pareto distribution depending on its scale `t` and rate `r`.  -/
ProbabilityTheory.paretoPDFReal : ℝ → ℝ → ℝ → ℝ
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.isPullback_of_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z)
  [inst_2 : F.Full] [F.Faithful], CategoryTheory.IsPullback (hf.fst' (F.map g)) (hf.snd (F.map g)) f g
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.algebraMap_apply : ∀ {ι : Type u_1} {R' : Type u_2} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R'] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → Semiring (A i)] [inst_3 : Algebra R' R] [inst_4 : (i : ι) → Algebra R (A i)]
  [inst_5 : (i : ι) → Algebra R' (A i)] [∀ (i : ι), IsScalarTower R' R (A i)] (r : R') (i : ι) [inst_7 : DecidableEq ι],
  (algebraMap R' (PiTensorProduct R fun i => A i)) r =
    (PiTensorProduct.tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {km kmi : α}, t.maxKey? = some km → (t.insert k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.support_sub : ∀ {R : Type u} (σ : Type u_1) [inst : CommRing R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R),
  (p - q).support ⊆ p.support ∪ q.support
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkCongr : Lean.Meta.Simp.Result → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Testing.Plausible.Functions
/-- Interpret a list of pairs as a total function, defaulting to
the identity function when no entries are found for a given function  -/
Plausible.InjectiveFunction.List.applyId : {α : Type u} → [DecidableEq α] → List (α × α) → α → α
-- Init.Data.Ord.Basic
Ordering.eq_eq_of_isGE_of_isGE_swap : ∀ {o : Ordering}, o.isGE = true → o.swap.isGE = true → o = Ordering.eq
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidates.mk.inj : ∀ {candidates : Array Lean.Elab.Structural.RecArgCandidate} {report : Lean.MessageData}
  {candidates_1 : Array Lean.Elab.Structural.RecArgCandidate} {report_1 : Lean.MessageData},
  { candidates := candidates, report := report } = { candidates := candidates_1, report := report_1 } →
    candidates = candidates_1 ∧ report = report_1
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_injective : ∀ {α : Type u_1} [inst : PartialOrder α], Function.Injective LowerSet.Iic
-- Mathlib.Data.Finset.Basic
Finset.isDirected_le : ∀ {α : Type u_1}, IsDirectedOrder (Finset α)
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg.eq_1 : ∀ (i : ISize), i.toNatClampNeg = i.toInt.toNat
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.vadd_left_injective : ∀ (z : UpperHalfPlane), Function.Injective fun x => x +ᵥ z
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.isCokernelEpiComp_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) {W : C} (g : W ⟶ X)
  [hg : CategoryTheory.Epi g] {h : W ⟶ Y} (hh : h = CategoryTheory.CategoryStruct.comp g f)
  (s : CategoryTheory.Limits.CokernelCofork h),
  (CategoryTheory.Limits.isCokernelEpiComp i g hh).desc s =
    i.desc (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofork.π s) ⋯)
-- Mathlib.Algebra.Group.Action.Sum
Sum.instVAdd.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β],
  Sum.instVAdd = { vadd := fun a => Sum.map (fun x => a +ᵥ x) fun x => a +ᵥ x }
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.parentDeclCtx.sizeOf_spec : ∀ (parentDecl : Lean.Name), sizeOf (Lean.Elab.PartialContextInfo.parentDeclCtx parentDecl) = 1 + sizeOf parentDecl
-- Mathlib.Data.Int.ModEq
Int.modEq_iff_add_fac : ∀ {a b n : ℤ}, a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.isUnit_toLin'_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {M : Matrix n n R}, IsUnit (Matrix.toLin' M) ↔ IsUnit M
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_ne_endPos : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h ≠ s.endPos
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_dite_eq' : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M]
  [inst_3 : DecidableEq ι] (i : ι) (f : (j : ι) → j = i → M),
  (Finset.univ.expect fun j => if h : j = i then f j h else 0) = (↑(Fintype.card ι))⁻¹ • f i ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.nonempty_sup_right : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P) [Nonempty ↥s₂], Nonempty ↥(s₁ ⊔ s₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Constructor for natural isomorphisms between spans.  -/
CategoryTheory.Limits.spanIsoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} →
      (z : F.obj CategoryTheory.Limits.WalkingSpan.zero ≅ G.obj CategoryTheory.Limits.WalkingSpan.zero) →
        (l : F.obj CategoryTheory.Limits.WalkingSpan.left ≅ G.obj CategoryTheory.Limits.WalkingSpan.left) →
          (r : F.obj CategoryTheory.Limits.WalkingSpan.right ≅ G.obj CategoryTheory.Limits.WalkingSpan.right) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) l.hom =
                  CategoryTheory.CategoryStruct.comp z.hom (G.map CategoryTheory.Limits.WalkingSpan.Hom.fst))
                CategoryTheory.Limits.spanIsoMk._auto_1 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd) r.hom =
                    CategoryTheory.CategoryStruct.comp z.hom (G.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
                  CategoryTheory.Limits.spanIsoMk._auto_3 →
                (F ≅ G)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.id : Lean.Meta.Grind.Arith.CommRing.Ring → ℕ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.doLetElseToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_sup_eq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} {K₁ K₂ : TopologicalSpace.Compacts G},
  (interior U).Nonempty →
    Disjoint (K₁.carrier + -U) (K₂.carrier + -U) →
      MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (K₁ ⊔ K₂) =
        MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂
-- Mathlib.GroupTheory.ResiduallyFinite
Group.residuallyFinite_iff_exists_finiteIndex : ∀ {G : Type u_1} [inst : Group G], Group.ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (hV : AlgebraicGeometry.IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V i))
      (CategoryTheory.CategoryStruct.comp hU.fromSpec h) =
    CategoryTheory.CategoryStruct.comp hV.fromSpec (CategoryTheory.CategoryStruct.comp f h)
-- Init.Data.Array.Lemmas
Array.filter_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {xs : Array α},
  Array.filter p (Array.filterMap f xs) = Array.filterMap (fun x => Option.filter p (f x)) xs
-- Lean.Parser.Term
Lean.Parser.Term.tuple.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.Lemmas
Int32.ofInt_bitVecToInt : ∀ (n : BitVec 32), Int32.ofInt n.toInt = Int32.ofBitVec n
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- If `f` is real-meromorphic on a compact interval, then `log ‖f ·‖` is interval integrable on this
interval.
 -/
MeromorphicOn.intervalIntegrable_posLog_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  MeromorphicOn f (Set.uIcc a b) → IntervalIntegrable (fun x => ‖f x‖.posLog) MeasureTheory.volume a b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
AddAction.fixingAddSubgroup_le_stabilizer : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (s : Set α),
  fixingAddSubgroup G s ≤ AddAction.stabilizer G s
-- Mathlib.Logic.Equiv.Set
Equiv.Set.rangeInl_apply_inl : ∀ {α : Type u_3} (β : Type u_4) (x : α), (Equiv.Set.rangeInl α β) ⟨Sum.inl x, ⋯⟩ = x
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_three_mul : ∀ (x : ℝ), Real.cos (3 * x) = 4 * Real.cos x ^ 3 - 3 * Real.cos x
-- Mathlib.CategoryTheory.Groupoid
/-- Promote (noncomputably) an `IsGroupoid` to a `Groupoid` structure.  -/
CategoryTheory.Groupoid.ofIsGroupoid : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.IsGroupoid C] → CategoryTheory.Groupoid C
-- Std.Time.Date.PlainDate
/-- `PlainDate` represents a date in the Year-Month-Day (YMD) format. It encapsulates the year, month,
and day components, with validation to ensure the date is valid.
 -/
Std.Time.PlainDate : Type
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.comm : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_6)
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'],
  Algebra.IsPushout R S R' S' ↔ Algebra.IsPushout R R' S S'
-- Lean.Elab.ConfigEval.Basic
/-- Like `evalTermWithInfo`, but uses an existing `ToExpr` instance
for `expectedType?` and for constructing the expression.  -/
Lean.Elab.ConfigEval.EvalTerm.evalTermWithInfo' : {α : Type} → [Lean.ToExpr α] → (Lean.Term → Lean.Elab.TermElabM α) → Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.mk.injEq : ∀ {V : Type u_1} {G : SimpleGraph V} {E : Type u_3} [inst : MetricSpace E] (p : V ↪ E)
  (unit_dist : ∀ {u v : V}, G.Adj u v → dist (p u) (p v) = 1) (p_1 : V ↪ E)
  (unit_dist_1 : ∀ {u v : V}, G.Adj u v → dist (p_1 u) (p_1 v) = 1),
  ({ p := p, unit_dist := unit_dist } = { p := p_1, unit_dist := unit_dist_1 }) = (p = p_1)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_cons_mk : ∀ {α : Type u} {β : Type v} {l : Std.DHashMap.Raw α fun x => β} {acc : List (α × β)},
  Std.DHashMap.Raw.Internal.foldRev (fun acc k v => (k, v) :: acc) acc l =
    List.map
        (fun x =>
          match x with
          | ⟨k, v⟩ => (k, v))
        (Std.DHashMap.Internal.toListModel l.buckets) ++
      acc
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.Extension.frob_apply : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n] {x : FiniteField.Extension k p n}, (FiniteField.Extension.frob k p n) x = x ^ Nat.card k
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A subsemigroup is closed under multiplication.  -/
Subsemigroup.mul_mem : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLED_eq_getD_getKeyLE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k fallback : α},
  Std.DTreeMap.Internal.Impl.getKeyLED k t fallback = (Std.DTreeMap.Internal.Impl.getKeyLE? k t).getD fallback
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Add parentheses if `paren == true`.  -/
Lean.Meta.RefinedDiscrTree.keysAsPattern.parenthesize : Lean.MessageData → Bool → Lean.MessageData
-- Mathlib.Algebra.Order.Archimedean.Basic
archimedean_iff_nat_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  Archimedean K ↔ ∀ (x : K), ∃ n, x < ↑n
-- Mathlib.Probability.Independence.Process.Basic
/-- If `X` is a process independent from `Y` and for all `i`, `X' i` is almost everywhere equal
to `X i`, then `X'` is also independent from `Y`. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.Kernel.IndepFun.process_congr_left : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) Y κ P →
    (∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) → ProbabilityTheory.Kernel.IndepFun (fun ω i => X' i ω) Y κ P
-- Mathlib.Algebra.Order.Group.Cone
AddGroupConeClass.toAddSubmonoidClass : ∀ {S : Type u_1} {G : outParam (Type u_2)} {inst : AddCommGroup G} {inst_1 : SetLike S G}
  [self : AddGroupConeClass S G], AddSubmonoidClass S G
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The auxiliary function is continuous away from the zeros of the L-functions of the Dirichlet
characters mod `q` (including at `s = 1`).  -/
ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux' : ∀ {q : ℕ} (a : ZMod q) [inst : NeZero q],
  ContinuousOn (ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), DirichletCharacter.LFunction χ s ≠ 0}
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instUniqueOfIsEmpty.eq_1 : ∀ {α : Type u} [inst : IsEmpty α],
  FreeAddGroup.instUniqueOfIsEmpty = { toInhabited := FreeAddGroup.instInhabited, uniq := ⋯ }
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_toUInt32 : ∀ (n : USize) (h : System.Platform.numBits = 64), n.toUInt32.toBitVec = BitVec.setWidth 32 (n.toBitVec64 h)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.of_f : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] {i j : ι}
  (hij : i ≤ j) (x : G i), (DirectLimit.NonUnitalRing.of G f j) ((f i j hij) x) = (DirectLimit.NonUnitalRing.of G f i) x
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift : ∀ {X : AlgebraicGeometry.Scheme},
  X.IsSeparated ↔
    AlgebraicGeometry.IsClosedImmersion
      (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Plausible.Functions
Plausible.TotalFunction.withDefault : {α : Type u} → {β : Type v} → List ((_ : α) × β) → β → Plausible.TotalFunction α β
-- Std.Do.WP.SimpLemmas
Std.Do.WP.set_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u}
  {Q : Std.Do.PostCond PUnit.{u + 1} (Std.Do.PostShape.arg σ ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (x : σ), (Std.Do.wp (set x)).apply Q = fun x_1 => Q.1 PUnit.unit x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` reflects
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsLimit_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimit K.op F],
  CategoryTheory.Limits.ReflectsLimit K F.unop
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.ref.inj : ∀ {α : Type u} {β : Type v} {σ : Type w} {node node_1 : σ},
  Lean.PersistentHashMap.Entry.ref node = Lean.PersistentHashMap.Entry.ref node_1 → node = node_1
-- Init.Data.BitVec.Basic
/-- Shifts a bitvector to the right. This is an arithmetic right shift - the high bits are filled with
most significant bit's value.

As a numeric operation, this is equivalent to `a.toInt >>> s.toNat`.

SMT-LIB name: `bvashr`.
 -/
BitVec.sshiftRight' : {n m : ℕ} → BitVec n → BitVec m → BitVec n
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_of_castSucc_lt : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i), p.predAbove i = i.pred ⋯
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.compMultilinearMap_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] {β : ι → Type u_1} {N : (i : ι) → β i → Type u_2}
  [inst_5 : (i : ι) → (b : β i) → AddCommMonoid (N i b)] [inst_6 : (i : ι) → (b : β i) → Module R (N i b)]
  (g : MultilinearMap R M₁ M₂) (f : (i : ι) → MultilinearMap R (N i) (M₁ i)) (m : (i : (i : ι) × β i) → N i.fst i.snd),
  (g.compMultilinearMap f) m = g fun i => (f i) (Sigma.curry m i)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_mul : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : CommMonoid β]
  [inst_3 : Preorder β] [inst_4 : IsOrderedMonoid β] (f g : α →*o β), ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.ι_ofι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y P : C}
  (f : X ⟶ Y) (ι : P ⟶ X) (w : CategoryTheory.CategoryStruct.comp ι f = 0),
  CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι ι w) = ι
-- Lean.DocString.Parser
/-- Parses an argument value, which may be a string literal, identifier, or numeric literal.  -/
Lean.Doc.Parser.val : Lean.Parser.ParserFn
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.ExtHashMap.ofList l)[k']? = some v
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_re : ∀ (x : ℂ), (Complex.exp x).re = Real.exp x.re * Real.cos x.im
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.reuse.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (var : Lean.FVarId) (i : Lean.Compiler.LCNF.CtorInfo) (updateHeader : Bool)
  (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_19),
  sizeOf (Lean.Compiler.LCNF.LetValue.reuse var i updateHeader args h) =
    1 + sizeOf var + sizeOf i + sizeOf updateHeader + sizeOf args + sizeOf h
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.inr.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.inr M N = { toFun := fun y => (0, y), map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.support_pow_subset_closure : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] (x : HahnSeries Γ R) (n : ℕ), (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
-- Mathlib.Order.Category.BddLat
BddLat.coe_forget_to_bddOrd : ∀ (X : BddLat), ↑((CategoryTheory.forget₂ BddLat BddOrd).obj X).toPartOrd = ↑X.toLat
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
ModuleCat.Derivation.d_mul : ∀ {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b b' : ↑B),
  D.d (b * b') = b • D.d b' + b' • D.d b
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.zoom_fill' : ∀ {α : Type u_1} (cut : α → Ordering) (t : RBTree.RBNode α) (path : RBTree.RBNode.Path α),
  RBTree.RBNode.Path.fill' (RBTree.RBNode.zoom cut t path) = path.fill t