mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.unitCoeff.congr_simp : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x x_1 : ℤ_[p]} (e_x : x = x_1) (hx : x ≠ 0),
  PadicInt.unitCoeff hx = PadicInt.unitCoeff ⋯
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- The set of functions which are 1-Lipschitz on a metric space separates points.  -/
Set.separatesPoints_lipschitzWith_one : ∀ (E : Type u_1) [inst : MetricSpace E], {f | LipschitzWith 1 f}.SeparatesPoints
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.id_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), LinearIsometry.id.comp f = f
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Run a computation in such a way that we can keep track of it.  -/
Mathlib.Tactic.ClickSuggestions.trackingComputation : {α : Type} →
  String → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM α → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM α
-- Init.Grind.Ring.ToInt
/-- A `ToInt` instance on a semiring preserves powers if it preserves numerals and multiplication.  -/
Lean.Grind.ToInt.pow_of_semiring : ∀ {α : Type u_1} {I : Lean.Grind.IntInterval} [inst : Lean.Grind.Semiring α] [inst_1 : Lean.Grind.ToInt α I]
  [Lean.Grind.ToInt.OfNat α I] [Lean.Grind.ToInt.Mul α I], I.isFinite = true → Lean.Grind.ToInt.Pow α I
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- If `P` respects isos, also `affineAnd P` respects isomorphisms.  -/
AlgebraicGeometry.affineAnd_respectsIso : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
-- Mathlib.Logic.Basic
/-- **Alias** of `Xor`.

---

`Xor a b` is the exclusive-or of propositions.  -/
Xor' : Prop → Prop → Prop
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
/-- The structure `MorphComponents` is an ad hoc structure that is used in
the proof that `N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ))`
reflects isomorphisms. The fields are the data that are needed in order to
construct a morphism `X _⦋n+1⦌ ⟶ Z` (see `φ`) using the decomposition of the
identity given by `decomposition_Q n (n+1)`.  -/
AlgebraicTopology.DoldKan.MorphComponents : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.SimplicialObject C → ℕ → C → Type v_1
-- Mathlib.LinearAlgebra.Basis.MulOpposite
MulOpposite.finrank : ∀ {R : Type u_1} {H : Type u_2} [inst : DivisionRing R] [inst_1 : AddCommGroup H] [inst_2 : Module R H],
  Module.finrank R Hᵐᵒᵖ = Module.finrank R H
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Raw.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insertIfNew a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a b) else m
-- Mathlib.RingTheory.MatrixAlgebra
/-- `Matrix.kroneckerTMul` as a ⋆-algebra equivalence, when the two arguments are tensored.  -/
Matrix.kroneckerTMulStarAlgEquiv : (m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_5) →
      (S : Type u_6) →
        (A : Type u_7) →
          (B : Type u_8) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : Fintype n] →
                        [inst_6 : DecidableEq n] →
                          [inst_7 : CommSemiring S] →
                            [inst_8 : Algebra R S] →
                              [inst_9 : Algebra S A] →
                                [inst_10 : IsScalarTower R S A] →
                                  [inst_11 : Fintype m] →
                                    [inst_12 : DecidableEq m] →
                                      [inst_13 : StarRing R] →
                                        [inst_14 : StarAddMonoid A] →
                                          [inst_15 : StarAddMonoid B] →
                                            [inst_16 : StarModule R A] →
                                              [inst_17 : StarModule R B] →
                                                TensorProduct R (Matrix m m A) (Matrix n n B) ≃⋆ₐ[S]
                                                  Matrix (m × n) (m × n) (TensorProduct R A B)
-- Init.Data.String.Lemmas.Intercalate
String.join_append : ∀ {l m : List String}, String.join (l ++ m) = String.join l ++ String.join m
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSigmaSubtypeEq.eq_1 : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : α) (b : β),
  Equiv.sigmaSigmaSubtypeEq a b =
    Equiv.sigmaSigmaSubtype
      (fun x =>
        match x with
        | ⟨a', b'⟩ => a' = a ∧ b' = b)
      ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.isCofibrant_iff_of_isInitial : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).RespectsIso] {A X : C} (i : A ⟶ X)
  (hA : CategoryTheory.Limits.IsInitial A), HomotopicalAlgebra.IsCofibrant X ↔ HomotopicalAlgebra.Cofibration i
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_self_le_prod_self : ∀ {α : Type u_1} [inst : Preorder α] {s₁ s₂ : LowerSet α}, s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalence_unitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂),
  (HomologicalComplex₂.flipEquivalence C c₁ c₂).unitIso = HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂
-- Mathlib.Probability.Process.HittingTime
/-- `hittingBtwn` is monotone with respect to the maximal time.  -/
MeasureTheory.hittingBtwn_mono_right : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {ω : Ω} (u : ι → Ω → β)
  (s : Set β) (n : ι), Monotone fun x => MeasureTheory.hittingBtwn u s n x ω
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f : (α →𝒄 β) × α), OmegaCompletePartialOrder.ContinuousHom.Prod.apply f = f.1 f.2
-- Init.Data.Iterators.Consumers.Loop
Std.instForMIterOfIteratorLoopIdOfMonad : {m : Type x → Type x'} →
  {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → [Monad m] → ForM m (Std.Iter β) β
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Creates the canonical packed `NaN` for the given specification.  -/
Float.Model.UnpackedFloat.packedNaN : (spec : Float.Model.Format) → BitVec spec.numBits
-- Lean.Data.Lsp.CodeActions
/-- A code action represents a change that can be performed in code, e.g. to fix a problem or to refactor code.

A CodeAction should set either `edit` and/or a `command`.
If both are supplied, the `edit` is applied first, then the `command` is executed.
If none are supplied, the client makes a `codeAction/resolve` JSON-RPC request to compute the edit.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction)  -/
Lean.Lsp.CodeAction : Type
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite : ∀ (G : GrpCat), Function.Injective (ProfiniteGrp.ProfiniteCompletion.etaFn G) ↔ Group.ResiduallyFinite ↑G
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.image_vsub_image : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {s t : Set P1} (f : P1 →ᵃ[k] P2),
  ⇑f '' s -ᵥ ⇑f '' t = ⇑f.linear '' (s -ᵥ t)
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.instInhabited_self : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Inhabited (L.PartialEquiv M M)
-- Mathlib.Tactic.ModCases
/-- The first theorem we apply says that `∃ m, 0 ≤ m < n ∧ a ≡ m (mod n)`.
The actual mathematical content of the proof is here.
 -/
Mathlib.Tactic.ModCases.NatMod.onModCases_start : (p : Sort u_1) → (a n : ℕ) → Nat.ble 1 n = true → Mathlib.Tactic.ModCases.NatMod.OnModCases n a 0 p → p
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
frestrictLe₂_comp_IicProdIoc : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] {a b : ι} (hab : a ≤ b), Preorder.frestrictLe₂ hab ∘ IicProdIoc a b = Prod.fst
-- Mathlib.CategoryTheory.Sums.Products
/-- The equivalence between functors from a sum and the product of the functor categories.  -/
CategoryTheory.Sum.functorEquiv : (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] →
            CategoryTheory.Functor (A ⊕ A') B ≌ CategoryTheory.Functor A B × CategoryTheory.Functor A' B
-- Mathlib.Data.Nat.MaxPowDiv
/-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p n` defaults to `0`.  -/
padicValNat : ℕ → ℕ → ℕ
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.projective_kaehlerDifferential : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.FormallySmooth R A], Module.Projective A Ω[A⁄R]
-- Mathlib.RingTheory.MvPolynomial.Localization
IsLocalization.Away.mvPolynomialQuotientEquiv_apply : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (p : MvPolynomial Unit R),
  (IsLocalization.Away.mvPolynomialQuotientEquiv S r)
      ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})) p) =
    (MvPolynomial.aeval fun x => IsLocalization.Away.invSelf r) p
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousWithinAt.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α} {s t : Set α},
  LowerSemicontinuousWithinAt f s x → t ⊆ s → LowerSemicontinuousWithinAt f t x
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.

`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.

This variant requires terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.findM?`.

Example:
```lean example
#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Std.IterM.Total.findM? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] →
          [Std.Iterators.Finite α m] → Std.IterM.Total m β → (β → m (ULift.{w, 0} Bool)) → m (Option β)
-- Lean.PrettyPrinter.Parenthesizer
/-- Whether to add parentheses regardless of any other conditions. This is cached from the `pp.parens` option.  -/
Lean.PrettyPrinter.Parenthesizer.Context.forceParens : Lean.PrettyPrinter.Parenthesizer.Context → Bool
-- Aesop.Frontend.Extension
Aesop.Frontend.extensionDescr : Aesop.RuleSetName → Lean.SimpleScopedEnvExtension.Descr Aesop.BaseRuleSetMember Aesop.BaseRuleSet
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Sigma.fst l).contains k = true
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.instEmptyCollection : EmptyCollection Std.Http.Internal.ChunkedBuffer
-- Mathlib.Data.Nat.Cast.Basic
map_natCast' : ∀ {B : Type u_4} {F : Type u_5} [inst : AddMonoidWithOne B] {A : Type u_6} [inst_1 : AddMonoidWithOne A]
  [inst_2 : FunLike F A B] [AddMonoidHomClass F A B] (f : F), f 1 = 1 → ∀ (n : ℕ), f ↑n = ↑n
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Algebra.Order.AddGroupWithTop
/-- **Alias** of the reverse direction of `LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_iff_ne_top`. -/
LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a ≠ ⊤ → a - a = 0
-- Mathlib.Topology.MetricSpace.Antilipschitz
LipschitzWith.to_rightInverse : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {g : β → α}, Function.RightInverse g f → AntilipschitzWith K g
-- Mathlib.Order.Extension.Linear
/-- A type alias for `α`, intended to extend a partial order on `α` to a linear order.  -/
LinearExtension : Type u → Type u
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- The unconditional filter is preserved by comaps.  -/
SummationFilter.comap_unconditional : ∀ {γ : Type u_3} {β : Type u_4} (f : γ ↪ β), (SummationFilter.unconditional β).comap f = SummationFilter.unconditional γ
-- Mathlib.Algebra.Group.Commute.Defs
addCommute_iff_eq : ∀ {S : Type u_3} [inst : Add S] (a b : S), AddCommute a b ↔ a + b = b + a
-- Mathlib.Algebra.DirectSum.Finsupp
finsuppLEquivDirectSum_apply : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Type u_1)
  [inst_3 : DecidableEq ι] (m : ι →₀ M) (i : ι), ((finsuppLEquivDirectSum R M ι) m) i = m i
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Option.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (x : α) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match some x, none with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_2 x
-- Mathlib.Order.Filter.Pointwise
Filter.add_top_of_nonneg : ∀ {α : Type u_2} [inst : AddMonoid α] {f : Filter α}, 0 ≤ f → f + ⊤ = ⊤
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel (ProbabilityTheory.Kernel.prodMkRight γ κ)
-- Mathlib.RingTheory.FractionalIdeal.Extended
_private.Mathlib.RingTheory.FractionalIdeal.Extended.0.FractionalIdeal.termMap_f : Lean.ParserDescr
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.findAsyncConst? : Lean.Environment → Lean.Name → optParam Bool false → Option Lean.AsyncConst✝
-- Mathlib.Data.Fintype.EquivFin
/-- There is (computably) an equivalence between `α` and `Fin (card α)`.

Since it is not unique and depends on which permutation
of the universe list is used, the equivalence is wrapped in `Trunc` to
preserve computability.

See `Fintype.equivFin` for the noncomputable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq`
for an equiv `α ≃ Fin n` given `Fintype.card α = n`.

See `Fintype.truncFinBijection` for a version without `[DecidableEq α]`.
 -/
Fintype.truncEquivFin : (α : Type u_4) → [DecidableEq α] → [inst : Fintype α] → Trunc (α ≃ Fin (Fintype.card α))
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C}
  (h : (t.eTruncLT.obj j).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι j).app X))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map f).app X) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)) h
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_lt_encard_iff_encard_sdiff_lt_encard_sdiff`. -/
Set.encard_lt_encard_iff_encard_diff_lt_encard_diff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ t).Finite → (s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard)
-- Mathlib.Algebra.Group.Action.End
/-- The monoid hom representing a monoid action.

When `M` is a group, see `MulAction.toPermHom`.  -/
MulAction.toEndHom : {M : Type u_2} → {α : Type u_5} → [inst : Monoid M] → [MulAction M α] → M →* Function.End α
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.zero_mem_polar : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] (s : Set E), 0 ∈ StrongDual.polar 𝕜 s
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_mul_left : ∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal}, ∑' (i : α), a * f i = a * ∑' (i : α), f i
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel_zero : ∀ (x : ℝ), HurwitzZeta.oddKernel 0 x = 0
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Given a list `l : List α` and a permutation `f : Perm α` whose nonfixed points are all in `l`,
recursively factors `f` into cycles.  -/
Equiv.Perm.cycleFactorsAux : {α : Type u_2} →
  [DecidableEq α] →
    [Fintype α] →
      (l : List α) →
        (f : Equiv.Perm α) →
          (∀ {x : α}, f x ≠ x → x ∈ l) →
            { pl // pl.prod = f ∧ (∀ g ∈ pl, g.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint pl }
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
multipliable_norm_one_add_of_summable_norm : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R},
  (Summable fun i => ‖f i‖) → Multipliable fun i => ‖1 + f i‖
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` is in the equivalence class of `False`.  -/
Lean.Meta.Grind.isEqFalse : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Order.Lattice
inf_right_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ c ⊓ b
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.lineDifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E}, HasLineDerivAt 𝕜 f f' x v → LineDifferentiableAt 𝕜 f x v
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.instMembershipOfLE : {α : Type u} → [LE α] → Membership α (Std.Rcc α)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `ContinuousLinearMap.prod` as an `Equiv`.  -/
ContinuousLinearMap.prodEquiv : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            {M₂ : Type u_3} →
              [inst_4 : TopologicalSpace M₂] →
                [inst_5 : AddCommMonoid M₂] →
                  [inst_6 : Module R M₂] →
                    {M₃ : Type u_4} →
                      [inst_7 : TopologicalSpace M₃] →
                        [inst_8 : AddCommMonoid M₃] →
                          [inst_9 : Module R M₃] → (M →L[R] M₂) × (M →L[R] M₃) ≃ (M →L[R] M₂ × M₃)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_eq_iff_eq_add_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable b → b ≤ a → (a - b = c ↔ a = c + b)
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.mk_lt_mk : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a₁ a₂ b₁ b₂ : α},
  Lean.Grind.IntModule.OfNatModule.Q.mk (a₁, a₂) < Lean.Grind.IntModule.OfNatModule.Q.mk (b₁, b₂) ↔ a₁ + b₂ < a₂ + b₁
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_union_of_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_mul : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly)
  (k : ℕ), p.NonnegCoeffs → Lean.Grind.Linarith.Poly.denoteN ctx (p.mul ↑k) = k • Lean.Grind.Linarith.Poly.denoteN ctx p
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams.contentChanges : Lean.Lsp.DidChangeTextDocumentParams → Array Lean.Lsp.TextDocumentContentChangeEvent
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A literal.  -/
Lean.Meta.RefinedDiscrTree.Key.lit : Lean.Literal → Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightEquiv_symm_weightMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (m : M),
  (RootPairing.Equiv.weightEquiv P Q e).symm ((↑e).weightMap m) = m
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (i : ℕ),
  1 ≤ p.natDegree →
    p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.mk.injEq : ∀ (term : Lean.Term) (options : Aesop.RuleBuilderOptions) (phase : Aesop.PhaseSpec) (term_1 : Lean.Term)
  (options_1 : Aesop.RuleBuilderOptions) (phase_1 : Aesop.PhaseSpec),
  ({ term := term, options := options, phase := phase } = { term := term_1, options := options_1, phase := phase_1 }) =
    (term = term_1 ∧ options = options_1 ∧ phase = phase_1)
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mk : {H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] →
      [inst_2 : CompleteSpace H] →
        (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)) →
          toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier → VonNeumannAlgebra H
-- Mathlib.Order.Grade
grade_le_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : LinearOrder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  grade 𝕆 a ≤ grade 𝕆 b ↔ a ≤ b