mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.sum_partition_boxes : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι}
  (f : BoxIntegral.BoxAdditiveMap ι M I₀),
  ↑I ≤ I₀ → ∀ {π : BoxIntegral.Prepartition I}, π.IsPartition → ∑ J ∈ π.boxes, f J = f I
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey? k = m₂.getKey? k
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.diagonal : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] {d : n → R}, (∀ (i : n), 0 < d i) → (Matrix.diagonal d).PosDef
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsQuotientMap f → Continuous f
-- Lean.Elab.BuiltinTerm
/-- Returns `true` if `stx` is a `by` expression with an empty tactic body
(not a parse error producing `.missing`).
The structure is: `node byTactic [atom "by", node tacticSeq [node tacticSeq1Indented [node null []]]]`  -/
Lean.Elab.Term.isEmptyByBlock : Lean.Syntax → Bool
-- Aesop.Forward.State
/-- Erase a `RawHyp` from the slot queue of the given slot.  -/
Aesop.ClusterState.eraseEnqueuedRawHyp : Aesop.RawHyp → Aesop.Slot → Aesop.ClusterState → Aesop.ClusterState
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.isScalarTower : ∀ {R : Type u} [inst : Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [inst_1 : SMul S₁ S₂] [inst_2 : SMulZeroClass S₁ R]
  [inst_3 : SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R], IsScalarTower S₁ S₂ (Polynomial R)
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.toMeasurable_iff : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasureTheory.pdf.IsUniform X (MeasureTheory.toMeasurable μ s) ℙ μ ↔ MeasureTheory.pdf.IsUniform X s ℙ μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_lt_add_right : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LT α] [AddRightStrictMono α], z ≠ ⊥ → x < y → x + z < y + z
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filter!_le_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  {f : (a : α) → β a → Bool}, t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).size ≤ t.size
-- Lean.Compiler.NameMangling
/-- Returns the demangled version of `s`, if it's the result of `Name.mangle _ ""`. Otherwise returns
`none`.
 -/
Lean.Name.demangle? : String → Option Lean.Name
-- Mathlib.Data.List.Permutation
List.mem_permutations : ∀ {α : Type u_1} {s t : List α}, s ∈ t.permutations ↔ s.Perm t
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D) (X : E) (X_1 : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)),
  (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).inv.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X_1)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
/-- In a category `C` equipped with a shift by an additive monoid,
this is the type of morphisms `X ⟶ (Y⟦m⟧)` for `m : M`.  -/
CategoryTheory.ShiftedHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {M : Type u_4} → [inst_1 : AddMonoid M] → [CategoryTheory.HasShift C M] → C → C → M → Type v_1
-- Init.Meta.Defs
/-- Converts a string to the Lean compiler's representation of names. The resulting name is
hierarchical, and the string is split at the dots (`'.'`).

`"a.b".toName` is the name `a.b`, not `«a.b»`. For the latter, use `Name.mkSimple`.
 -/
String.toName : String → Lean.Name
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- `HasFiniteIntegral f μ` means that the integral `∫⁻ a, ‖f a‖ ∂μ` is finite.
`HasFiniteIntegral f` means `HasFiniteIntegral f volume`.  -/
MeasureTheory.HasFiniteIntegral : {α : Type u_1} →
  {ε : Type u_4} →
    [ENorm ε] →
      {x : MeasurableSpace α} →
        (α → ε) → autoParam (MeasureTheory.Measure α) MeasureTheory.HasFiniteIntegral._auto_1 → Prop
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_sub : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S}
  (f : M →ₛₗ[σ] M₂) (x y : M), f (x - y) = f x - f y
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.preimage_image_mk : ∀ {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α),
  QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' s = ⋃ x, (fun x_1 => x_1 + ↑x) ⁻¹' s
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.congr_simp : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  {f f_1 : Module.Dual R V} (e_f : f = f_1) {v v_1 : V} (e_v : v = v_1) (h : f v = 0),
  LinearEquiv.transvection h = LinearEquiv.transvection ⋯
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.yes.injEq : ∀ (expectedType expectedType_1 : Lean.Expr),
  (Lean.Elab.Term.UseImplicitLambdaResult.yes expectedType =
      Lean.Elab.Term.UseImplicitLambdaResult.yes expectedType_1) =
    (expectedType = expectedType_1)
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofBitVec : ∀ (b : BitVec 64), { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- `capSyntax stx p` applies `capSourceInfo · s` to all `SourceInfo`s in all
`node`s, `atom`s and `ident`s contained in `stx`.

This is used to trim away all "fluff" that follows a command: comments and whitespace after
a command get removed with `capSyntax stx stx.getTailPos?.get!`.
 -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.capSyntax : Lean.Syntax → ℕ → Lean.Syntax
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_mono : ∀ {α : Type u} [inst : TopologicalSpace α] (x : α) {F G : Set α},
  F ⊆ G → connectedComponentIn F x ⊆ connectedComponentIn G x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).hom = X.right.hom
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_of : ∀ {α β : Type u} (f : α → β) (y : α), f <$> FreeAbelianGroup.of y = FreeAbelianGroup.of (f y)
-- Batteries.Data.Fin.Lemmas
Fin.exists_iff_exists_minimal : ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p], (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬p j
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- The general adjoint functor theorem says that if `G : D ⥤ C` preserves limits and `D` has them,
if `G` satisfies the solution set condition then `G` is a right adjoint.
 -/
CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (G : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasLimits D]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G],
  CategoryTheory.SolutionSetCondition G → G.IsRightAdjoint
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_comp_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e) U.ι =
    CategoryTheory.CategoryStruct.comp V.ι f
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.deriv_le_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f y → deriv f y ≤ slope f x y
-- Mathlib.Logic.Equiv.Basic
/-- Note: the "obvious" statement `(piCongrLeft P e) f b = f (e.symm b)` doesn't typecheck: the
LHS would have type `P b` while the RHS would have type `P (e (e.symm b))`. This lemma is a way
around it in the case where `b` is of the form `e a`, so we can use `f a` instead of
`f (e.symm (e a))`.  -/
Equiv.piCongrLeft_apply_apply : ∀ {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (a : α),
  (Equiv.piCongrLeft P e) f (e a) = f a
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPattern.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_im : ∀ (x : ℂ), (Complex.log x).im = x.arg
-- Mathlib.Tactic.Linter.DocString
/-- Lint module docs for Verso syntax errors.

Verso syntax in declaration docstrings is already handled by the `docStringLinter`.  -/
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.Style.moduleDocVersoLinter : Lean.Linter
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_domRestrict : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M),
  (f.domRestrict K).ker = f.ker.addSubgroupOf K
-- Mathlib.CategoryTheory.Shift.CommShift
/-- **Alias** of `CategoryTheory.Functor.CommShift.id_commShiftIso_hom_app`. -/
CategoryTheory.Functor.commShiftIso_id_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_4} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (x : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.id C) x).hom.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C x).obj X)
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Iterate over two lists, if the first element of the first list is `false`, insert `none` into the
result and continue with the tail of first list. Otherwise, wrap the first element of the second
list with `some` and continue with the tails of both lists. Return when either list is empty.

Example:
```
listBoolMerge [false, true, false, true] [0, 1, 2, 3, 4] = [none, (some 0), none, (some 1)]
```
 -/
Mathlib.Tactic.MkIff.listBoolMerge : {α : Type u_1} → List Bool → List α → List (Option α)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.algebraMap_eq : ∀ {R : Type u_5} [inst : CommRing R] (I : Ideal R), algebraMap R (R ⧸ I) = Ideal.Quotient.mk I
-- Mathlib.Data.FinEnum
/-- create a `FinEnum` instance using an injection  -/
FinEnum.ofInjective : {α : Type u_1} → {β : Type u_2} → (f : α → β) → [DecidableEq α] → [FinEnum β] → Function.Injective f → FinEnum α
-- Mathlib.Tactic.TacticAnalysis
_private.Mathlib.Tactic.TacticAnalysis.0.Mathlib.TacticAnalysis.Entry.import.unsafe_4 : Mathlib.TacticAnalysis.Entry → Lean.Environment → Lean.Options → Except String (Lean.Option Bool)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.comp.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P] (hnp : N →* P)
  (hmn : M →* N), hnp.comp hmn = { toFun := fun x => hnp (hmn x), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_comap : ∀ {α β : Type u} (M : Matroid β) (f : α → β) (X : Set α), (M.comap f).cRk X = M.cRk (f '' X)
-- Mathlib.GroupTheory.Commutator.Basic
conjugate_addCommutatorElement : ∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ g₃ : G), g₃ + ⁅g₁, g₂⁆ + -g₃ = ⁅g₃ + g₁ + -g₃, g₃ + g₂ + -g₃⁆
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.equivOfIsoObj_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (e : Y ≅ X) (R : F.RepresentableBy Y),
  (CategoryTheory.Functor.RepresentableBy.equivOfIsoObj e).symm R = R.ofIsoObj e.symm
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.nhdsWithin_extend_target_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M},
  y ∈ f.source → nhdsWithin (↑(f.extend I) y) (f.extend I).target = nhdsWithin (↑(f.extend I) y) (Set.range ↑I)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) {X : T} (Y : CategoryTheory.Over X) (Z : CategoryTheory.CostructuredArrow F Y.left),
  (CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse F Y).obj Z =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.Over.homMk Z.hom ⋯)
-- Aesop.Forward.State
Aesop.ClusterState.mk.injEq : ∀ (slots : Array Aesop.Slot) (conclusionDeps : Array Aesop.PremiseIndex) (variableMap : Aesop.VariableMap)
  (completeMatches : Lean.PHashSet Aesop.Match) (haveHypForEachSlot : Bool) (slotQueues : Array (Array Aesop.RawHyp))
  (slotQueues_size : slotQueues.size = slots.size) (slots_1 : Array Aesop.Slot)
  (conclusionDeps_1 : Array Aesop.PremiseIndex) (variableMap_1 : Aesop.VariableMap)
  (completeMatches_1 : Lean.PHashSet Aesop.Match) (haveHypForEachSlot_1 : Bool)
  (slotQueues_1 : Array (Array Aesop.RawHyp)) (slotQueues_size_1 : slotQueues_1.size = slots_1.size),
  ({ slots := slots, conclusionDeps := conclusionDeps, variableMap := variableMap, completeMatches := completeMatches,
        haveHypForEachSlot := haveHypForEachSlot, slotQueues := slotQueues, slotQueues_size := slotQueues_size } =
      { slots := slots_1, conclusionDeps := conclusionDeps_1, variableMap := variableMap_1,
        completeMatches := completeMatches_1, haveHypForEachSlot := haveHypForEachSlot_1, slotQueues := slotQueues_1,
        slotQueues_size := slotQueues_size_1 }) =
    (slots = slots_1 ∧
      conclusionDeps = conclusionDeps_1 ∧
        variableMap = variableMap_1 ∧
          completeMatches = completeMatches_1 ∧ haveHypForEachSlot = haveHypForEachSlot_1 ∧ slotQueues = slotQueues_1)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.mk.inj : ∀ {completion? : Option Lean.Lsp.CompletionClientCapabilities}
  {codeAction? : Option Lean.Lsp.CodeActionClientCapabilities}
  {inlayHint? : Option Lean.Lsp.InlayHintClientCapabilities}
  {completion?_1 : Option Lean.Lsp.CompletionClientCapabilities}
  {codeAction?_1 : Option Lean.Lsp.CodeActionClientCapabilities}
  {inlayHint?_1 : Option Lean.Lsp.InlayHintClientCapabilities},
  { completion? := completion?, codeAction? := codeAction?, inlayHint? := inlayHint? } =
      { completion? := completion?_1, codeAction? := codeAction?_1, inlayHint? := inlayHint?_1 } →
    completion? = completion?_1 ∧ codeAction? = codeAction?_1 ∧ inlayHint? = inlayHint?_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.mem_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {p : M × N},
  p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.function.injEq : ∀ (thm thm_1 : Mathlib.Meta.FunProp.FunctionTheorem),
  (Mathlib.Meta.FunProp.Theorem.function thm = Mathlib.Meta.FunProp.Theorem.function thm_1) = (thm = thm_1)
-- Mathlib.Topology.Instances.CantorSet
cantorSequence_mem_cantorSet : ∀ {x : ℝ}, x ∈ cantorSet → ∀ (n : ℕ), (cantorSequence x).get n ∈ cantorSet
-- Mathlib.Data.List.Triplewise
List.Triplewise.of_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {p : α → α → α → Prop} {f : α → β} {p' : β → β → β → Prop},
  (∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c) → List.Triplewise p' (List.map f l) → List.Triplewise p l
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.mulOppositeEquiv_apply : ∀ {M : Type u_2} [inst : Monoid M] (f : M →ₑ[id] M), MulActionHom.End.mulOppositeEquiv f = f 1
-- Mathlib.Topology.Metrizable.Basic
/-- The uniformity coming from `pseudoMetrizableSpaceUniformity` is countably generated..  -/
TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated : ∀ (X : Type u_5) [inst : TopologicalSpace X] [h : TopologicalSpace.PseudoMetrizableSpace X],
  (uniformity X).IsCountablyGenerated
-- Mathlib.RingTheory.WittVector.Basic
/-- Evaluates the `n`th Witt polynomial on the first `n` coefficients of `x`,
producing a value in `R`.  -/
WittVector.ghostComponent : {p : ℕ} → {R : Type u_1} → [inst : CommRing R] → [inst_1 : Fact (Nat.Prime p)] → ℕ → WittVector p R →+* R
-- Mathlib.RingTheory.FormalGroup.Basic
/-- The coefficient of $X$ in $F(X, Y)$ is 1.  -/
FormalGroup.lin_coeff_X : ∀ {R : Type u_1} [inst : CommRing R] (self : FormalGroup R), (MvPowerSeries.coeff fun₀ | 0 => 1) self.toPowerSeries = 1
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.mk_mem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, 0 < n → Function.IsPeriodicPt f n x → x ∈ Function.periodicPts f
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_cons_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l acc : List α},
  p a = true → List.splitOnPPrepend p (a :: l) acc = acc.reverse :: List.splitOnP p l
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.explicit.injEq : ∀ (ref : Lean.Syntax) (a : Lean.Elab.Tactic.RCases.RCasesPatt) (ref_1 : Lean.Syntax)
  (a_1 : Lean.Elab.Tactic.RCases.RCasesPatt),
  (Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref a = Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref_1 a_1) =
    (ref = ref_1 ∧ a = a_1)
-- Batteries.Data.String.Basic
instCoeStringRaw_batteries : Coe String Substring.Raw
-- Lean.Language.Basic
/-- Dynamic mutable slot usable by the language server for memorizing interactive diagnostics. If
`none`, interactive diagnostics are not remembered, which should only be used for messages not
containing any interactive elements as client-side state will be lost on recreating a diagnostic.

See also section "Communication" in Lean/Server/README.md.
 -/
Lean.Language.Snapshot.Diagnostics.interactiveDiagsRef? : Lean.Language.Snapshot.Diagnostics → Option (IO.Ref (Option Dynamic))
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSub_of_add_neg : ∀ (G : Type u_2) [inst : MeasurableSpace G] [inst_1 : SubNegMonoid G] [MeasurableAdd G] [MeasurableNeg G],
  MeasurableSub G
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [inst_1 : I.IsPrime]
  {r : (i : ι) → R i},
  (Localization.AtPrime.mapPiEvalRingHom I)
      ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) r) =
    (algebraMap (R i) (Localization.AtPrime I)) (r i)
-- Init.Data.Nat.Basic
Nat.pow_zero : ∀ (n : ℕ), n ^ 0 = 1
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
/-- Given `f : E₁ × E₂ → F` strictly differentiable at `u` with invertible partial derivative
`f₂u : E₂ →L[𝕜] F`, we may construct an `ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁` with `f` as its
`leftFun` and `Prod.fst : E₁ × E₂ → E₁` as its `rightFun` by proving that the kernels of the
associated `leftDeriv` and `rightDeriv` are complementary.  -/
HasStrictFDerivAt.implicitFunctionDataOfProdDomain : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E₁ : Type u_2} →
      [inst_1 : NormedAddCommGroup E₁] →
        [inst_2 : NormedSpace 𝕜 E₁] →
          [inst_3 : CompleteSpace E₁] →
            {E₂ : Type u_3} →
              [inst_4 : NormedAddCommGroup E₂] →
                [inst_5 : NormedSpace 𝕜 E₂] →
                  [inst_6 : CompleteSpace E₂] →
                    {F : Type u_4} →
                      [inst_7 : NormedAddCommGroup F] →
                        [inst_8 : NormedSpace 𝕜 F] →
                          [inst_9 : CompleteSpace F] →
                            {u : E₁ × E₂} →
                              {f : E₁ × E₂ → F} →
                                {f'u : E₁ × E₂ →L[𝕜] F} →
                                  HasStrictFDerivAt f f'u u →
                                    (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible →
                                      ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.nat_unpair_lt_2 : ∀ {n : ℕ}, (Nat.unpair n).1 ≠ 0 → (Nat.unpair n).2 < n
-- Std.Time.Format.Modifier
/-- `d`: Day of month (e.g., 10).
 -/
Std.Time.Modifier.d : Std.Time.Number → Std.Time.Modifier
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.CoherenceHom.mk.sizeOf_spec : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁) (inst unfold : Lean.Expr),
  sizeOf { e := e, src := src, tgt := tgt, inst := inst, unfold := unfold } =
    1 + sizeOf e + sizeOf src + sizeOf tgt + sizeOf inst + sizeOf unfold
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → ¬cmp k t.maxKey! = Ordering.eq → (t.erase k).maxKey! = t.maxKey!
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.Const.modify : {α : Type u} →
  [BEq α] →
    {β : Type v} →
      α → (β → β) → (Std.DHashMap.Internal.AssocList α fun x => β) → Std.DHashMap.Internal.AssocList α fun x => β
-- Mathlib.Data.Ordmap.Ordnode
/-- O(1). Construct a singleton set containing value `a`.

```
singleton 3 = {3}
```  -/
Ordnode.singleton : {α : Type u_1} → α → Ordnode α
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) thickening of the empty set is empty.  -/
Metric.thickening_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ), Metric.thickening δ ∅ = ∅
-- Mathlib.Topology.Order.LeftRight
nhdsGE_sup_nhdsLT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Ici a) ⊔ nhdsWithin a (Set.Iio a) = nhds a
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.prev_π₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) {c₂ : ComplexShape I₂}
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' → c₁₂.prev (c₁.π c₂ c₁₂ (i₁, i₂')) = c₁.π c₂ c₁₂ (i₁, i₂)
-- Mathlib.Order.Bounds.Basic
/-- An alternative constructor for `SemilatticeInf` using `IsGLB`.  -/
SemilatticeInf.ofIsGLB : {α : Type u_1} → [inst : PartialOrder α] → (inf : α → α → α) → (∀ (a b : α), IsGLB {a, b} (inf a b)) → SemilatticeInf α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
Filter.EventuallyEq.congr_contDiffWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → (ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff m₂ ⋯).get! k = default