mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Continuity
/-- See `tendsto_norm_one` for a version with pointed neighborhoods.  -/
tendsto_norm_one : ∀ {E : Type u_4} [inst : SeminormedGroup E], Filter.Tendsto (fun a => ‖a‖) (nhds 1) (nhds 0)
-- Mathlib.Data.Seq.Computation
Computation.ret_terminates : ∀ {α : Type u} (a : α), (Computation.pure a).Terminates
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.mk.sizeOf_spec : ∀ (cache : Lean.Meta.Simp.Cache) (congrCache : Lean.Meta.Simp.CongrCache) (dsimpCache : Lean.ExprStructMap Lean.Expr)
  (usedTheorems : Lean.Meta.Simp.UsedSimps) (numSteps : ℕ) (diag : Lean.Meta.Simp.Diagnostics),
  sizeOf
      { cache := cache, congrCache := congrCache, dsimpCache := dsimpCache, usedTheorems := usedTheorems,
        numSteps := numSteps, diag := diag } =
    1 + sizeOf cache + sizeOf congrCache + sizeOf dsimpCache + sizeOf usedTheorems + sizeOf numSteps + sizeOf diag
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀`.

---

For any subobject `x`, the pullback of `h.Ω₀` along the characteristic map of `x`
given by `h.homEquiv` is `x` itself.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {X : C} (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism.  -/
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y},
  f = g → ∀ {c : CategoryTheory.Limits.Fork f g} (h : CategoryTheory.Limits.IsLimit c), CategoryTheory.IsIso c.ι
-- Mathlib.Data.List.ReduceOption
List.reduceOption_eq_nil_iff : ∀ {α : Type u_1} (l : List (Option α)), l.reduceOption = [] ↔ ∃ n, l = List.replicate n none
-- Std.Do.PostCond
/-- The assertions and postconditions in this monad use neither state nor exceptions.  -/
Std.Do.PostShape.pure : Std.Do.PostShape
-- Mathlib.Algebra.CharP.Defs
CharP.char_ne_one : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [Nontrivial R] (p : ℕ) [hc : CharP R p], p ≠ 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_sub_pi : ∀ (θ : Real.Angle), (θ - ↑Real.pi).sin = -θ.sin
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- A variant of `Submodule.mem_span_finset` using `s` as the index type.  -/
Submodule.mem_span_finset' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Finset M}
  {x : M}, x ∈ Submodule.span R ↑s ↔ ∃ f, ∑ a, f a • ↑a = x
-- Init.Data.List.Sublist
List.subset_cons_self : ∀ {α : Type u_1} (a : α) (l : List α), l ⊆ a :: l
-- Mathlib.Combinatorics.HalesJewett
/-- Consider a line as a one-dimensional subspace.  -/
Combinatorics.Line.toSubspaceUnit : {α : Type u_2} → {ι : Type u_3} → Combinatorics.Line α ι → Combinatorics.Subspace Unit α ι
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getLtFn : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.Meta.Grind.Arith.Linear.MonadGetStruct m] → m Lean.Expr
-- Init.Data.List.Zip
List.head_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ}
  (h : List.zipWithAll f as bs ≠ []), (List.zipWithAll f as bs).head h = f as.head? bs.head?
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.IsConnected.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {X : C},
  (∀ (a : CategoryTheory.Limits.IsInitial X), False) →
    (∀ (Y : C) (i : Y ⟶ X) [CategoryTheory.Mono i],
        (∀ (a : CategoryTheory.Limits.IsInitial Y), False) → CategoryTheory.IsIso i) →
      CategoryTheory.PreGaloisCategory.IsConnected X
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get?.eq_2 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a k : α) (v : β) (es : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.get? a (Std.DHashMap.Internal.AssocList.cons k v es) =
    bif k == a then some v else Std.DHashMap.Internal.AssocList.get? a es
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.isReduced_toWord : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeGroup α}, FreeGroup.IsReduced x.toWord
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.Slice.Pos.prevn.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.NumberTheory.LSeries.Nonvanishing
DirichletCharacter.zetaMul_prime_pow_nonneg : ∀ {N : ℕ} {χ : DirichletCharacter ℂ N}, χ ^ 2 = 1 → ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), 0 ≤ χ.zetaMul (p ^ k)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain_comp_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n),
  (CochainComplex.mappingCocone.liftCochain φ α β h).comp (CochainComplex.mappingCocone.snd φ) ⋯ = β
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit.sizeOf_spec : ∀ (c₁ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) (decVar : Lean.FVarId) (h : Lean.Meta.Grind.Arith.Linear.UnsatProof)
  (decVars : Array Lean.FVarId),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁ decVar h decVars) =
    1 + sizeOf c₁ + sizeOf decVar + sizeOf h + sizeOf decVars
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_biInf_principal : ∀ {α : Type u_1} {β : Type u_2} {s : β → Set α} {S : Set β},
  DirectedOn (s ⁻¹'o fun x1 x2 => x1 ⊇ x2) S →
    S.Nonempty → (⨅ i ∈ S, Filter.principal (s i)).HasBasis (fun i => i ∈ S) s
-- Mathlib.Analysis.Convex.Body
/-- The convex bodies in a fixed space $V$ form a module over the nonnegative reals.  -/
ConvexBody.instModuleNNReal : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] →
      [inst_2 : Module ℝ V] → [ContinuousSMul ℝ V] → [inst_4 : ContinuousAdd V] → Module NNReal (ConvexBody V)
-- Mathlib.Data.Finset.Fold
Finset.lt_fold_min : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  c < Finset.fold min b f s ↔ c < b ∧ ∀ x ∈ s, c < f x
-- Lean.DocString.Parser
/-- Parenthesizer for `withoutVersoSyntax`—parenthesizes according to the underlying parenthesizer.
 -/
Lean.Doc.Parser.withoutVersoSyntax.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A} {x : NNReal}, CFC.sqrt a ^ x = a ^ (x / 2)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_apply_eq : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α) (i : m) (j : n) (k : o), Matrix.blockDiagonal M (i, k) (j, k) = M k i j
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The simple (aka pure) elements span the tensor product.  -/
TensorProduct.span_tmul_eq_top : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.spanning_iff_ground_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {S : Set α},
  autoParam (S ⊆ M.E) Matroid.spanning_iff_ground_subset_closure._auto_1 → (M.Spanning S ↔ M.E ⊆ M.closure S)
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- For a locally finite preconnected graph, the number of components outside of any finite set
is finite.  -/
SimpleGraph.componentCompl_finite : ∀ {V : Type u} {G : SimpleGraph V} [G.LocallyFinite] [Gpc : Fact G.Preconnected] (K : Finset V),
  Finite (G.ComponentCompl ↑K)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_mapM : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {o : Type u₁ → Type u_2} {β₂ γ : Type u₁} {m : Type u₁ → Type u_3}
  {β : Type u₁} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n]
  [inst_4 : Monad o] [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_11 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [inst_13 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_15 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        g __do_lift acc ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.mapM f it) init g ⦃Q⦄
-- Init.Data.SInt.Lemmas
Int32.toISize_neg_of_ne : ∀ {x : Int32}, x ≠ -2147483648 → (-x).toISize = -x.toISize
-- Lean.Declaration
Lean.ConstantInfo.quotInfo.sizeOf_spec : ∀ (val : Lean.QuotVal), sizeOf (Lean.ConstantInfo.quotInfo val) = 1 + sizeOf val
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The middle right map in the forward hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' C
-- Mathlib.Topology.Sheaves.Module
TopologicalSpace.Opens.overPullbackSheafEquivOver.eq_1 : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {X : TopCat} (U : TopologicalSpace.Opens ↑X),
  U.overPullbackSheafEquivOver =
    CategoryTheory.Iso.refl (((Opens.grothendieckTopology ↑X).overPullback A U).comp U.sheafEquivOver.functor)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the chain map sending `∑ aᵢ·gᵢ : Gⁿ →₀ A` to `∑ φ(aᵢ)·(f ∘ gᵢ) : Hⁿ →₀ B`.  -/
groupHomology.chainsMap : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) →
              (A ⟶ Rep.res f B) → (groupHomology.inhomogeneousChains A ⟶ groupHomology.inhomogeneousChains B)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U)
  (y : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) y)
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight_neg : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.addETransformRight (-e) x = (Finset.addETransformLeft e x.swap).swap
-- Lean.Parser.Term
/-- Strip leading `paren` wrappers from `stx`.  -/
Lean.Parser.Term.dropParens : Lean.Syntax → Lean.Syntax
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow : ∀ {p a m n : ℕ}, Nat.Prime p → p ^ m = a ^ n → m = n * a.factorization p
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.glue.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (sz : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced →
        Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size r.size →
          Sort u_3)
  (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
      (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
            Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hr hlr)
  (h_2 :
    (sz' : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                    (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size) →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') hr hlr),
  (match Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => h_1 hr hlr
    | Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr => h_2 sz' k' v' l'' r'' hr hlr) =
    h_2 sz' k' v' l'' r'' hr hlr
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of `ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem`. -/
ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∏ j ∈ s, f j) (f i) μ
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_map_hom : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R),
  (MvPolynomial.eval₂Hom φ g) ((MvPolynomial.map f) p) = (MvPolynomial.eval₂Hom (φ.comp f) g) p
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.argPartialEquiv_source : Circle.argPartialEquiv.source = Set.univ
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑X.isoSpec.inv '' PrimeSpectrum.zeroLocus s = X.zeroLocus s
-- Init.Prelude
/-- `id x = x`, as a `@[simp]` lemma.  -/
id_eq : ∀ {α : Sort u_1} (a : α), id a = a
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.prod_mk : ∀ {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕜 β) (a₁ a₂ : α) (b₁ b₂ : β),
  (f.prod g) (a₁, b₁) (a₂, b₂) = f a₁ a₂ * g b₁ b₂
-- Mathlib.Data.List.Basic
List.dropLast_append_getLast : ∀ {α : Type u} {l : List α} (h : l ≠ []), l.dropLast ++ [l.getLast h] = l
-- Mathlib.Data.Holor
Holor.instNeg : {α : Type} → {ds : List ℕ} → [Neg α] → Neg (Holor α ds)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.toSubtype_eq_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p],
  CategoryTheory.Limits.biproduct.toSubtype f p =
    CategoryTheory.Limits.biproduct.desc fun j =>
      if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0
-- Aesop.Options.Internal
Aesop.Options.toOptions' : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Aesop.Options → optParam (Option ℕ) none → m Aesop.Options'
-- Batteries.Lean.HashSet
/-- `O(n)`. Returns `true` if `f` returns `true` for any element of the set.
 -/
Std.HashSet.anyM : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → {m : Type → Type u_2} → [Monad m] → Std.HashSet α → (α → m Bool) → m Bool
-- Init.Data.SInt.Bitwise
ISize.ofBitVec_intMin : ISize.ofBitVec (BitVec.intMin System.Platform.numBits) = ISize.minValue
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNNNorm_def : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m n 𝕜), ‖A‖₊ = ‖(Matrix.toEuclideanLin ≪≫ₗ LinearMap.toContinuousLinearMap) A‖₊
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsConj.comp : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ →
    ∀ (ν : Gal(K/k)), NumberField.ComplexEmbedding.IsConj (φ.comp ↑ν) (ν⁻¹ * σ * ν)
-- Mathlib.RingTheory.Localization.Defs
/-- The typeclass `IsLocalization (M : Submonoid R) S` where `S` is an `R`-algebra
expresses that `S` is isomorphic to the localization of `R` at `M`.  -/
IsLocalization : {R : Type u_4} →
  [inst : CommSemiring R] → Submonoid R → (S : Type u_5) → [inst_1 : CommSemiring S] → [Algebra R S] → Prop
-- Mathlib.Algebra.CharP.Invertible
invertibleOfPos : {K : Type u_2} → [inst : Semifield K] → [CharZero K] → (n : ℕ) → [NeZero n] → Invertible ↑n
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.basis_repr_apply : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (x : ↥(⋀[R]^n M)) (s : ↑(Set.powersetCard I n)),
  ((Module.Basis.exteriorPower n b).repr x) s = (exteriorPower.ιMultiDual R n b s) x
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mkMulProof.match_1.splitter : {v : Lean.Level} →
  {M : Q(Type v)} →
    (motive : Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M → Sort u_1) →
      (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M) →
        ((l : Mathlib.Tactic.FieldSimp.qNF M) → motive [] l) →
          ((l : Mathlib.Tactic.FieldSimp.qNF M) → (l = [] → False) → motive l []) →
            ((a₁ : ℤ) →
                (x₁ : Q(«$M»)) →
                  (k₁ : ℕ) →
                    (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
                      (a₂ : ℤ) →
                        (x₂ : Q(«$M»)) →
                          (k₂ : ℕ) →
                            (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)) →
              motive l₁ l₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.map f m) k fallback =
      (Option.map (f k') (Std.ExtDHashMap.Const.get? m k)).getD fallback
-- Init.Data.String.Pattern.Basic
/-- A lawful backward pattern is one where the three functions `BackwardPattern.skipSuffix?`,
`BackwardPattern.skipSuffixOfNonempty?` and `BackwardPattern.endsWith` agree for any
given input slice.

Note that this is a relatively weak condition. It is non-uniform in the sense that the functions
can still return completely different results on different slices, even if they represent the same
string.

There is a stronger lawfulness typeclass `LawfulBackwardPatternModel` that asserts that the
`BackwardPattern.skipSuffix?` function behaves like a function that skips the longest prefix
according to some notion of matching.
 -/
String.Slice.Pattern.LawfulBackwardPattern : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Prop
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.eraseMax_aux : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂ →
    Ordnode.Valid' o₁ (l.node' x r).eraseMax ↑(Ordnode.findMax' x r) ∧
      (l.node' x r).size = (l.node' x r).eraseMax.size + 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRooSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Roo.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RooSlice α)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.subset_singleton_zero_compl : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsUnit a → spectrum R a ⊆ {0}ᶜ
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.prod_mul_reverse_inv_prod : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (L : List (Matrix.TransvectionStruct n R)),
  (List.map Matrix.TransvectionStruct.toMatrix L).prod *
      (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L.reverse).prod =
    1
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂Measurable_eq_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : MeasurableSpace γ]
  [inst_8 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_9 : BorelSpace γ]
  [inst_10 : SecondCountableTopologyEither β γ] [inst_11 : MeasurableSpace δ]
  [inst_12 : TopologicalSpace.PseudoMetrizableSpace δ] [inst_13 : OpensMeasurableSpace δ]
  [inst_14 : SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β)
  (f₂ : α →ₘ[μ] γ),
  MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂ =
    MeasureTheory.AEEqFun.compMeasurable (Function.uncurry g) hg (f₁.pair f₂)
-- Mathlib.Data.Finset.Sort
Finset.sort_singleton : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r] (a : α), {a}.sort r = [a]
-- Std.Time.Duration
/-- Normalizes `Second.Offset` and `NanoSecond.span` in order to build a new `Duration` out of it.
 -/
Std.Time.Duration.fromComponents : Std.Time.Second.Offset → Std.Time.Nanosecond.Span → Std.Time.Duration
-- Lean.Parser.Attr
Lean.Parser.Attr.specialize.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMinOn.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsMinOn f s a → HasLineDerivAt ℝ f f' a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_pi : ∀ {α : Type u_1} {F' : Type u_7} [inst : SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17}
  [inst_1 : Fintype ι] {E' : ι → Type u_18} [inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i},
  f =O[l] g' ↔ ∀ (i : ι), (fun x => f x i) =O[l] g'