mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Basic
/-- The Boolean less-than comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
 * `Nat.blt 2 5 = true`
 * `Nat.blt 5 2 = false`
 * `Nat.blt 5 5 = false`
 -/
Nat.blt : ℕ → ℕ → Bool
-- Init.Data.Array.Attach
/-- This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Array.foldl_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : β → { x // p x } → β} {g : β → α → β}
  {x : β}, (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) → Array.foldl f x xs = Array.foldl g x xs.unattach
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- Any action is `0`-preprimitive.  -/
MulAction.is_zero_preprimitive : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α], MulAction.IsMultiplyPreprimitive M α 0
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Given an additive group `α` acting on a type `β`, and a function `f : β → M`,
we automorphize `f` to a function `β ⧸ α → M` by summing over `α` orbits,
`b ↦ ∑' (a : α), f(a • b)`.  -/
AddAction.automorphize : {α : Type u_1} →
  {β : Type u_2} →
    {M : Type u_11} →
      [TopologicalSpace M] →
        [AddCommMonoid M] →
          [inst : AddGroup α] → [inst_1 : AddAction α β] → (β → M) → Quotient (AddAction.orbitRel α β) → M
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instHasFiniteCoproductsCostructuredArrowOppositeCommRingCatSchemeTopMorphismPropertySpec : ∀ {S : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.IsZariskiLocalAtSource P],
  CategoryTheory.Limits.HasFiniteCoproducts (P.CostructuredArrow ⊤ AlgebraicGeometry.Scheme.Spec S)
-- Std.Http.Data.Headers.Value
Std.Http.Header.Value.mk.sizeOf_spec : ∀ (value : String)
  (isValidHeaderValue :
    autoParam (Std.Http.Header.IsValidHeaderValue value) Std.Http.Header.Value.isValidHeaderValue._autoParam),
  sizeOf { value := value, isValidHeaderValue := isValidHeaderValue } = 1 + sizeOf value + sizeOf isValidHeaderValue
-- Mathlib.CategoryTheory.Equivalence
/-- The other triangle equality. The proof follows the following proof in Globular:
http://globular.science/1905.001  -/
CategoryTheory.Equivalence.unit_inverse_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D),
  CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) =
    CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
-- Init.Data.UInt.Basic
instComplementUInt8 : Complement UInt8
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective.  -/
AddSubmonoid.giMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} →
          [inst_2 : FunLike F M N] →
            [mc : AddMonoidHomClass F M N] →
              {f : F} → Function.Surjective ⇑f → GaloisInsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)
-- Mathlib.Data.Finset.Powerset
Finset.mem_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ∈ s.ssubsets ↔ t ⊂ s
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- **Alias** of `ContinuousOn.tendsto_domRestrict_iff_tendstoUniformlyOn`.

---

Given functions `F i, f` which are continuous on a compact set `s`, `F` tends to `f`
uniformly on `s` if and only if the restrictions (as elements of `C(s, β)`) converge.  -/
ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {s : Set α} [CompactSpace ↑s]
  {f : α → β} (hf : ContinuousOn f s) {ι : Type u_1} {p : Filter ι} {F : ι → α → β}
  (hF : ∀ (i : ι), ContinuousOn (F i) s),
  Filter.Tendsto (fun i => { toFun := s.domRestrict (F i), continuous_toFun := ⋯ }) p
      (nhds { toFun := s.domRestrict f, continuous_toFun := ⋯ }) ↔
    TendstoUniformlyOn F f p s
-- Mathlib.Order.Completion
/-- Any order embedding `β ↪o α` into a complete lattice `α` factors through `DedekindCut β`.

This map is defined so that `factorEmbedding f A = sSup (f '' A.left)`. Although the construction
`factorEmbedding f A = sInf (f '' A.right)` would also work, these do **not** in general give equal
embeddings.  -/
DedekindCut.factorEmbedding : {α : Type u_1} → {β : Type u_2} → [inst : CompleteLattice α] → [inst_1 : PartialOrder β] → β ↪o α → DedekindCut β ↪o α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel morphism of an epimorphism is a zero morphism  -/
CategoryTheory.Limits.cokernel.π_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasCokernel f]
  [CategoryTheory.Epi f], CategoryTheory.Limits.cokernel.π f = 0
-- Mathlib.GroupTheory.Congruence.Basic
/-- The first isomorphism theorem for `AddMonoid`s.  -/
AddCon.quotientKerEquivRange : {M : Type u_1} →
  {P : Type u_3} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass P] → (f : M →+ P) → (AddCon.ker f).Quotient ≃+ ↥(AddMonoidHom.mrange f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_self_of_one_lt : ∀ {x y : ℝ}, 1 < x → y < 1 → x ^ y < x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => a < b) r.toList
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.collectUsedAtExpr : Lean.FVarIdHashSet → Lean.Expr → Lean.FVarIdHashSet
-- Init.Data.UInt.Lemmas
UInt32.toFin.eq_1 : ∀ (x : UInt32), x.toFin = x.toBitVec.toFin
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_apply₁₁ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α) (i : n) (j : l), Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inl j) = A i j
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.inv f)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.one_add_ofNat : ∀ (m : ℕ) [inst : m.AtLeastTwo], 1 + OfNat.ofNat m = Order.succ (OfNat.ofNat m)
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- The points with `v.limRatioMeas hρ x = ∞` have measure `0` for `μ`.  -/
VitaliFamily.measure_limRatioMeas_top : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ), μ {x | v.limRatioMeas hρ x = ⊤} = 0
-- Init.Data.Range.Polymorphic.Basic
Std.Rii.mem : ∀ {α : Type u} {r : Std.Rii α} {a : α}, a ∈ r
-- Mathlib.RingTheory.Ideal.Over
/-- If `P` lies over `p`, then the stabilizer of `P` acts on the extension `(B ⧸ P) / (A ⧸ p)`.  -/
Ideal.Quotient.stabilizerHom : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (P : Ideal B) →
            (p : Ideal A) →
              [inst_3 : P.LiesOver p] →
                (G : Type u_6) →
                  [inst_4 : Group G] →
                    [inst_5 : MulSemiringAction G B] →
                      [SMulCommClass G A B] → ↥(MulAction.stabilizer G P) →* (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- If `R` is an artinian ring, and `S` is a finite type `R`-algebra `R`-quasi-finite at `p`,
then `{p}` is clopen in `Spec S`.  -/
Algebra.QuasiFiniteAt.isClopen_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum S)
  [IsArtinianRing R] [Algebra.FiniteType R S] [Algebra.QuasiFiniteAt R p.asIdeal], IsClopen {p}
-- Mathlib.Data.List.SplitLengths
_private.Mathlib.Data.List.SplitLengths.0.List.splitLengths.match_3.splitter : {α : Type u_1} →
  (motive : List ℕ → List α → Sort u_2) →
    (x : List ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive [] x) → ((n : ℕ) → (ns : List ℕ) → (x : List α) → motive (n :: ns) x) → motive x x_1
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instModularFormClass : ∀ (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ), ModularFormClass (ModularForm Γ k) Γ k
-- Mathlib.Logic.Basic
BEx.imp_right : ∀ {α : Sort u_1} {p : α → Prop} {P Q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), P x h → Q x h) → (∃ x, ∃ (h : p x), P x h) → ∃ x, ∃ (h : p x), Q x h
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α),
  κ.snd a = MeasureTheory.Measure.map Prod.snd (κ a)
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_Icc : ∀ {f : ℝ → ℝ} {y z : ℝ},
  ConcaveOn ℝ (Set.Icc y z) f →
    y < z → ContinuousWithinAt f (Set.Ici y) y → ContinuousWithinAt f (Set.Iic z) z → ContinuousOn f (Set.Icc y z)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `F` is a field of exponential characteristic `q`, `a : E` is separable over `F`, then
`F⟮a⟯ = F⟮a ^ q⟯`.  -/
IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {a : E},
  IsSeparable F a → ∀ (q : ℕ) [ExpChar F q], F⟮a⟯ = F⟮a ^ q⟯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.ofRepresentableBy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X),
  CategoryTheory.AddMonObj.ofRepresentableBy X F α =
    { zero := α.homEquiv'.symm 0,
      add :=
        α.homEquiv'.symm
          (α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) +
            α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.snd X X)),
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Mathlib.Data.List.Zip
List.forall_zipWith : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {p : γ → Prop} {l₁ : List α} {l₂ : List β},
  l₁.length = l₂.length → (List.Forall p (List.zipWith f l₁ l₂) ↔ List.Forall₂ (fun x y => p (f x y)) l₁ l₂)
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'},
  (k' == k) = false →
    (Std.Internal.List.insertEntry k v (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: Std.Internal.List.insertEntry k v l)
-- Mathlib.CategoryTheory.LocallyDirected
CategoryTheory.instIsLocallyDirectedDiscrete : ∀ {J : Type u_1} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (Type u_2)), F.IsLocallyDirected
-- Mathlib.Topology.Algebra.Group.Basic
nhds_neg : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] (a : G), nhds (-a) = -nhds a
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop_succ_cons : ∀ {α : Type u} {x : α} {s : Stream'.Seq α} {n : ℕ}, (Stream'.Seq.cons x s).drop (n + 1) = s.drop n
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.fderivCLM_apply_of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  (f : TestFunction Ω F n), k + 1 ≤ n → ⇑((TestFunction.fderivCLM 𝕜 n k) f) = fderiv ℝ ⇑f
-- Mathlib.Algebra.Group.Subgroup.Finite
AddMonoidHom.fintypeMrange.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : Fintype M]
  [inst_3 : DecidableEq N] (f : M →+ N), f.fintypeMrange = Set.fintypeRange ⇑f
-- Init.Data.Rat.Basic
/-- Division of rational numbers. Note: `div a 0 = 0`.  Written with a separate function `Rat.div`
as a wrapper so that the definition is not unfolded at `.instance` transparency.  -/
Rat.instDiv : Div ℚ
-- Mathlib.Algebra.FiveLemma
/-- One four lemma in terms of modules. For a diagram explaining the variables,
see the module docstring.  -/
LinearMap.injective_of_surjective_of_injective_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} {N₁ : Type u_7}
  {N₂ : Type u_8} {N₃ : Type u_9} {N₄ : Type u_10} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  [inst_7 : Module R M₃] [inst_8 : Module R M₄] [inst_9 : AddCommGroup N₁] [inst_10 : AddCommGroup N₂]
  [inst_11 : AddCommGroup N₃] [inst_12 : AddCommGroup N₄] [inst_13 : Module R N₁] [inst_14 : Module R N₂]
  [inst_15 : Module R N₃] [inst_16 : Module R N₄] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (f₃ : M₃ →ₗ[R] M₄)
  (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (g₃ : N₃ →ₗ[R] N₄) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃)
  (i₄ : M₄ →ₗ[R] N₄),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃ →
        Function.Exact ⇑f₁ ⇑f₂ →
          Function.Exact ⇑f₂ ⇑f₃ →
            Function.Exact ⇑g₁ ⇑g₂ →
              Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Injective ⇑i₄ → Function.Injective ⇑i₃
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkGroundPattern : Lean.Expr → Lean.Expr
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.combine.eq_def : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly),
  p₁.combine p₂ =
    match p₁, p₂ with
    | Lean.Grind.Linarith.Poly.nil, p₂ => p₂
    | p₁, Lean.Grind.Linarith.Poly.nil => p₁
    | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ =>
      bif Nat.beq x₁ x₂ then
        have a := a₁ + a₂;
        bif a == 0 then p₁.combine p₂ else Lean.Grind.Linarith.Poly.add a x₁ (p₁.combine p₂)
      else
        bif Nat.blt x₂ x₁ then Lean.Grind.Linarith.Poly.add a₁ x₁ (p₁.combine (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂))
        else Lean.Grind.Linarith.Poly.add a₂ x₂ ((Lean.Grind.Linarith.Poly.add a₁ x₁ p₁).combine p₂)
-- Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive
CategoryTheory.ObjectProperty.instAdditiveFullSubcategoryShiftFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [inst_3 : P.IsStableUnderShift A]
  [inst_4 : CategoryTheory.Preadditive C] (n : A) [(CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.shiftFunctor P.FullSubcategory n).Additive
-- Lean.Meta.AppBuilder
Lean.Meta.mkListLit : Lean.Expr → List Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
IsGδ.setOfPred_liouville : IsGδ {x | Liouville x}
-- Mathlib.Tactic.DepRewrite
/-- If `e : te` is a term whose type mentions `x`, `h` (the generalization variables)
or entries in `Δ`/`δ`,
return `h.symm ▸ e : te[p/x, rfl/h, …]`.
Otherwise return `none`.  -/
Mathlib.Tactic.DepRewrite.castBack? : Lean.Expr →
  Lean.Expr →
    Lean.Expr → Lean.Expr → Array (Lean.FVarId × Lean.Expr) → Std.HashSet Lean.FVarId → Lean.MetaM (Option Lean.Expr)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff' : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
  (a : A),
  a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔
    ∀ (i : ℕ),
      Localization.mk ((GradedRing.proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈
        ⇑(algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getElem!_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getElem!_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k : α},
  (Std.ExtTreeMap.filterMap f t)[k]! = (t[k]?.bind (f k)).get!
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonAssocRingWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [NonAssocRing α] → NonAssocRing (WithConv (Matrix m n α))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_a₆ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).a₆ = f W.a₆
-- Mathlib.Data.Tree.Basic
_private.Mathlib.Data.Tree.Basic.0.BinaryTree.traverse.match_1.splitter : {α : Type u_1} →
  (motive : BinaryTree α → Sort u_2) →
    (x : BinaryTree α) →
      (Unit → motive BinaryTree.nil) → ((a : α) → (l r : BinaryTree α) → motive (BinaryTree.node a l r)) → motive x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getD.eq_2 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (k : α) (fallback : δ) (size : ℕ) (k' : α) (v' : δ)
  (l r : Std.DTreeMap.Internal.Impl α fun x => δ),
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.inner size k' v' l r) k fallback =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getD l k fallback
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getD r k fallback
    | Ordering.eq => v'
-- Mathlib.Topology.Order.Monotone
MonotoneOn.tendsto_nhdsWithin_Ioo_right : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α},
  (Set.Ioo x y).Nonempty →
    MonotoneOn f (Set.Ioo x y) →
      BddBelow (f '' Set.Ioo x y) → Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioo x y)))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iSup_of_directed_le : ∀ {Ω : Type u_1} {ι : Type u_2} {m' m₁ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω},
  (∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ) →
    (∀ (i : ι), m i ≤ mΩ) →
      m₁ ≤ mΩ → Directed (fun x1 x2 => x1 ≤ x2) m → ProbabilityTheory.CondIndep m' (⨆ i, m i) m₁ hm' μ
-- Mathlib.Tactic.Simps.Basic
/-- projection expression  -/
Simps.ParsedProjectionData.expr? : Simps.ParsedProjectionData → Option Lean.Expr
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_range_inclusion_restrictScalars_eq_top : ∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M],
  Submodule.span S (Set.range ⇑(Submodule.inclusion ⋯)) = ⊤
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_zero : ∀ (x : ℕ), x ^^^ 0 = x
-- Mathlib.Algebra.WithConv
WithConv.congr_apply : ∀ {A : Type u_2} {B : Type u_3} (f : A ≃ B) (x : WithConv A), (WithConv.congr f) x = WithConv.toConv (f x.ofConv)
-- Mathlib.Order.Sublattice
/-- Binary product of sublattices as a sublattice.  -/
Sublattice.prod : {α : Type u_2} →
  {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → Sublattice α → Sublattice β → Sublattice (α × β)
-- Init.Data.List.Basic
List.extract_eq_take_drop : ∀ {α : Type u} {l : List α} {start stop : ℕ}, l.extract start stop = List.take (stop - start) (List.drop start l)
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.gid : Std.Internal.UV.System.PasswdInfo → Option UInt64
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(Iⁿ) = n*val_v(I)` for every `n ∈ ℤ`.  -/
FractionalIdeal.count_zpow : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ)
  (I : FractionalIdeal (nonZeroDivisors R) K), FractionalIdeal.count K v (I ^ n) = n * FractionalIdeal.count K v I
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.of_mem_adjoin_singleton : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  [FiniteDimensional K M], f.IsSemisimple → ∀ {a : Module.End K M}, a ∈ K[f] → a.IsSemisimple
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddGroup : {α : Type u_1} → [AddGroup α] → AddGroup αᵐᵒᵖ
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentRegistrationOptions.toJson : Lean.Lsp.TextDocumentRegistrationOptions → Lean.Json
-- Aesop.Tracing
Aesop.TraceOption.withEnabled : {m : Type → Type} → {α : Type} → [Lean.MonadWithOptions m] → Aesop.TraceOption → m α → m α
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endEquivAutGalois_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f g : CategoryTheory.End F),
  (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) (CategoryTheory.CategoryStruct.comp g f) =
    (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) g * (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f
-- Mathlib.Order.Types.Defs
OrderType.bot_eq_zero : ⊥ = 0
-- Mathlib.Algebra.DirectSum.Module
DirectSum.linearMap_ext_iff : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {N : Type u₁} [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] {ψ ψ' : (DirectSum ι fun i => M i) →ₗ[R] N},
  ψ = ψ' ↔ ∀ (i : ι), ψ ∘ₗ DirectSum.lof R ι M i = ψ' ∘ₗ DirectSum.lof R ι M i
-- Mathlib.Algebra.Group.Defs
ZPow.toPow : {M : Type u_2} → [ZPow M] → Pow M ℤ
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
homomorphism.
This is `Function.eval i` as a `MonoidHom`.  -/
Pi.evalMonoidHom : {I : Type u} → (f : I → Type v) → [inst : (i : I) → MulOneClass (f i)] → (i : I) → ((i : I) → f i) →* f i
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.brecOn.eq : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  {motive : (a a_1 : ι) → Monoid.CoprodI.NeWord M a a_1 → Sort u} {a a_1 : ι} (t : Monoid.CoprodI.NeWord M a a_1)
  (F_1 : (a a_2 : ι) → (t : Monoid.CoprodI.NeWord M a a_2) → Monoid.CoprodI.NeWord.below t → motive a a_2 t),
  Monoid.CoprodI.NeWord.brecOn t F_1 = F_1 a a_1 t (Monoid.CoprodI.NeWord.brecOn.go t F_1).2
-- Mathlib.GroupTheory.Nilpotent
/-- An additive group `G` is nilpotent if its upper central series is eventually `G`.  -/
AddGroup.IsNilpotent : (G : Type u_2) → [AddGroup G] → Prop