mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Verifies an ordering relation on the nodes of the tree.  -/
RBTree.RBNode.isOrdered : {α : Type u_1} → (α → α → Ordering) → RBTree.RBNode α → optParam (Option α) none → optParam (Option α) none → Bool
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.find?_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Bool}, List.find? f it.toList = it.find? f
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk_proj_snd : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, x ∈ e.source → (proj x, (↑e x).2) = ↑e x
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toIntertwiningMap_injective : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W}, Function.Injective fun f => f.toIntertwiningMap
-- Mathlib.Data.FP.Basic
FP.Float.add : [C : FP.FloatCfg] → FP.RMode → FP.Float → FP.Float → FP.Float
-- Mathlib.Order.SymmDiff
bihimp_left_surjective : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), Function.Surjective fun x => bihimp x a
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The forgetful functor from `𝒪_{Spec R}` modules to sheaves of `R`-modules is fully faithful.  -/
AlgebraicGeometry.SpecModulesToSheafFullyFaithful : {R : CommRingCat} → AlgebraicGeometry.modulesSpecToSheaf.FullyFaithful
-- Mathlib.Data.Set.Card
Set.tsub_encard_le_encard_sdiff : ∀ {α : Type u_1} (s t : Set α), s.encard - t.encard ≤ (s \ t).encard
-- Init.Data.BitVec.Bitblast
/-- Construct a layer of the parallel-prefix-sum tree by summing two-by-two all the
`w`-long words in `oldLayer`, returning a bitvector containing `(oldLen + 1) / 2`
flattened `w`-long words, each resulting from an addition.
 -/
BitVec.cpopLayer : {len w iterNum : ℕ} → BitVec (len * w) → BitVec (iterNum * w) → 2 * (iterNum - 1) < len → BitVec ((len + 1) / 2 * w)
-- Init.Data.Array.Lemmas
/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array.  -/
Array.getElem_append_right' : ∀ {α : Type u_1} (xs : Array α) {ys : Array α} {i : ℕ} (hi : i < ys.size), ys[i] = (xs ++ ys)[i + xs.size]
-- Mathlib.Data.Sum.Order
/-- `WithTop α` is order-isomorphic to `α ⊕ₗ PUnit`, by sending `⊤` to `Unit` and `↑a` to
`a`.  -/
WithTop.orderIsoSumLexPUnit : {α : Type u_1} → [inst : LE α] → WithTop α ≃o α ⊕ₗ PUnit.{u_4 + 1}
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_map_le_sum_map : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [AddLeftMono α] {s : Multiset ι}
  (f g : ι → α), (∀ i ∈ s, f i ≤ g i) → (Multiset.map f s).sum ≤ (Multiset.map g s).sum
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Composition of morphisms of `SimplexCategory`.  -/
SimplexCategory.Hom.comp : {a b c : SimplexCategory} → b.Hom c → a.Hom b → a.Hom c
-- Mathlib.Algebra.Ring.IsFormallyReal
isSumNonzeroSq_iff : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] (a : R),
  IsSumNonzeroSq a ↔ (∃ a_1, a_1 ≠ 0 ∧ a = a_1 * a_1) ∨ ∃ a_1 s, a_1 ≠ 0 ∧ IsSumNonzeroSq s ∧ a = a_1 * a_1 + s
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.sub : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [inst_2 : (i : ι) → Sub (β i)]
  [∀ (i : ι), MeasurableSub₂ (β i)],
  MeasureTheory.Adapted f u → MeasureTheory.Adapted f v → MeasureTheory.Adapted f (u - v)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The equivalence between representations induced from iso between objects in `Rep k G`.  -/
Representation.equivOfIso : {k : Type u} →
  {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → (A ≅ B) → A.ρ.Equiv B.ρ
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  ↑(TensorProduct.tensorQuotEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (TensorProduct.mk R M (R ⧸ I)).flip 1
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearEquiv.analyticOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃L[𝕜] F)
  (s : Set E), AnalyticOn 𝕜 (⇑f) s
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
OrthonormalBasis.tensorProduct_repr_tmul_apply' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁ × ι₂),
  ((b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y)).ofLp i = (b₂.repr y).ofLp i.2 * (b₁.repr x).ofLp i.1
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.toByteArray_eq_right : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → t₂.toByteArray = s.toByteArray.extract p.offset.byteIdx s.toByteArray.size
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_comp_le_tsum_of_inj : ∀ {α : Type u_1} {β : Type u_4} {f : α → NNReal},
  Summable f → ∀ {i : β → α}, Function.Injective i → ∑' (x : β), f (i x) ≤ ∑' (x : α), f x
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.zero_mul_subset : ∀ {α : Type u_1} [inst : MulZeroClass α] (s : Set α), 0 * s ⊆ 0
-- Mathlib.Analysis.Analytic.CPolynomial
hasFiniteFPowerSeriesOnBall_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {c : F} {e : E},
  HasFiniteFPowerSeriesOnBall (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e 1 ⊤
-- Mathlib.Tactic.Check
/-- The `#check' t` tactic elaborates the term `t` and then pretty prints it with its type as `e : ty`.
In contrast to `#check t`, we only pretty-print explicit arguments, and omit implicit or type class
arguments. Currently this only works when `t` is the name of a declaration.

If `t` is an identifier, then it pretty prints a type declaration form
for the global constant `t` instead.
Use `#check' (t)` to pretty print it as an elaborated expression.

Like other `#check` commands, the `#check'` tactic allows stuck typeclass instance problems.
These become metavariables in the output.
 -/
Mathlib.Tactic.«tactic#check'__» : Lean.ParserDescr
-- Mathlib.Order.Category.Semilat
SemilatInfCat.instLargeCategory : CategoryTheory.LargeCategory SemilatInfCat
-- Mathlib.Order.Interval.Set.Basic
/-- In an order without minimal elements, the intervals `Iio` are nonempty.  -/
Set.nonempty_Iio_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMinOrder α], Nonempty ↑(Set.Iio a)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- To construct an isomorphism between cotridents,
it suffices to give an isomorphism between the cocone points
and check that it commutes with the `π` morphisms.
 -/
CategoryTheory.Limits.Cotrident.ext : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {s t : CategoryTheory.Limits.Cotrident f} →
              (i : s.pt ≅ t.pt) →
                autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π)
                    CategoryTheory.Limits.Cotrident.ext._auto_1 →
                  (s ≅ t)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_min : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddLeftMono α] (a b c : α), a + min b c = min (a + b) (a + c)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_symmDiff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  a • symmDiff s t = symmDiff (a • s) (a • t)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The map that sends an element of `a : integerSet K` to the associates class
of its preimage in `(𝓞 K)⁰`. By quotienting by the kernel of the map, which is equal to the
subgroup of torsion, we get the equivalence `integerSetQuotEquivAssociates`.  -/
NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K) →
        Associates ↥(nonZeroDivisors (NumberField.RingOfIntegers K))
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q P ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.inv) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr) h
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey_cons_perm.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    {k : α} →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((v : β k) → motive (some v)) → motive x
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_iff_succ_ne : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α],
  Order.IsSuccPrelimit a ↔ ∀ (b : α), Order.succ b ≠ a
-- Lean.Elab.Do.Legacy
/-- Given a term `term` produced by `ToTerm.run`, pattern match on its result.
See comment at the beginning of the `ToTerm` namespace.

- `a` is true if the code block has a `Code.action _` exit point
- `r` is true if the code block has a `Code.return _ _` exit point
- `bc` is true if the code block has a `Code.break _` or `Code.continue _` exit point

The result is a sequence of `doElem`  -/
Lean.Elab.Term.Do.ToTerm.matchNestedTermResult : Lean.Syntax → Array Lean.Elab.Term.Do.Var → Bool → Bool → Bool → Lean.MacroM (List Lean.Syntax)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.trivial.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.trivial C =
    { X := (CategoryTheory.AddMon.trivial C).X, addGrp := CategoryTheory.AddGrpObj.instTensorAddUnit }
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- Given a nonarchimedean function `α → R`, a function `g : β → α` and a nonempty finset
`t : Finset β`, we can always find `b : β` belonging to `t` such that `f (t.sum g) ≤ f (g b)` .  -/
IsNonarchimedean.finset_image_add_of_nonempty : ∀ {R : Type u_1} [inst : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_1 : AddCommMonoid α] {f : α → R},
  IsNonarchimedean f → ∀ (g : β → α) {t : Finset β}, t.Nonempty → ∃ b ∈ t, f (t.sum g) ≤ f (g b)
-- Mathlib.Data.Nat.Factors
/-- **Fundamental theorem of arithmetic**  -/
Nat.primeFactorsList_unique : ∀ {n : ℕ} {l : List ℕ}, l.prod = n → (∀ p ∈ l, Nat.Prime p) → l.Perm n.primeFactorsList
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.halt with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_7 ()
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The natural inclusion from multivariate polynomials into multivariate formal power series.  -/
MvPolynomial.coeToMvPowerSeries : {σ : Type u_1} → {R : Type u_2} → [inst : CommSemiring R] → Coe (MvPolynomial σ R) (MvPowerSeries σ R)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- An element `x` lies in the span of `v` iff it can be written as sum `∑ cᵢ • vᵢ = x`.
 -/
Submodule.mem_span_range_iff_exists_fun : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {v : α → M} {x : M}, x ∈ Submodule.span R (Set.range v) ↔ ∃ c, ∑ i, c i • v i = x
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.counit_single : ∀ (R : Type u) (ι : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (i : ι) (a : A), (CoalgebraStruct.counit fun₀ | i => a) = CoalgebraStruct.counit a
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The infinite sum of strongly measurable functions is measurable.  -/
MeasureTheory.StronglyMeasurable.tsum : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [ContinuousAdd E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [Countable ι] {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable fun x => ∑'[L] (i : ι), f i x
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Complex.isTheta_cpow_const_rpow : ∀ {α : Type u_1} {l : Filter α} {f : α → ℂ} {b : ℂ},
  (b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0) → (fun x => f x ^ b) =Θ[l] fun x => ‖f x‖ ^ b.re
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax right unity.  -/
CategoryTheory.OplaxFunctor.map₂_rightUnitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b))
        (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : β →+o γ) (g : α →+o β),
  ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_getElem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} (h' : a ∈ t), t[a]? = some t[a]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Decomp.0.SimpleGraph.Walk.takeUntil.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V}
  (motive : (w : V) → (x : G.Walk v w) → (x_1 : V) → x_1 ∈ x.support → Sort u_2) (w v_1 : V) (r : G.Adj v v_1)
  (p : G.Walk v_1 w) (u : V) (h : u ∈ (SimpleGraph.Walk.cons r p).support)
  (h_1 : (u : V) → (h : u ∈ SimpleGraph.Walk.nil.support) → motive v SimpleGraph.Walk.nil u h)
  (h_2 :
    (w v_2 : V) →
      (r : G.Adj v v_2) →
        (p : G.Walk v_2 w) →
          (u : V) → (h : u ∈ (SimpleGraph.Walk.cons r p).support) → motive w (SimpleGraph.Walk.cons r p) u h),
  (match w, SimpleGraph.Walk.cons r p, u, h with
    | .(v), SimpleGraph.Walk.nil, u, h => h_1 u h
    | w, SimpleGraph.Walk.cons r p, u, h => h_2 w v_2 r p u h) =
    h_2 w v_1 r p u h
-- Lean.Server.AsyncList
Lean.AsyncList.instInhabited : {ε : Type u_1} → {α : Type u_2} → Inhabited (Lean.AsyncList ε α)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A predicate on arrows with codomain `X`.  -/
CategoryTheory.Presieve : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max u₁ v₁)
-- Init.Data.List.Lemmas
List.any_eq_not_all_not : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, l.any p = !l.all fun x => !p x
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key in the tree map, panicking if the map is empty.
 -/
Std.DTreeMap.Raw.minKey! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α
-- Mathlib.RingTheory.Binomial
Ring.smeval_ascPochhammer_neg_add : ∀ (n k : ℕ), (ascPochhammer ℕ (n + k + 1)).smeval (-↑n) = 0
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.tensorDistrib_tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  [inst_10 : Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂),
  ((QuadraticForm.tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₂ m₂ • Q₁ m₁
-- Mathlib.Data.List.Nodup
/-- **Alias** of `List.Nodup.sdiff_eq_filter`. -/
List.Nodup.diff_eq_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List α},
  l₁.Nodup → l₁.diff l₂ = List.filter (fun x => decide (x ∉ l₂)) l₁
-- Mathlib.Algebra.Lie.Solvable
/-- The radical of a Noetherian Lie algebra is solvable.  -/
LieAlgebra.radicalIsSolvable : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  LieAlgebra.IsSolvable ↥(LieAlgebra.radical R L)
-- Batteries.Data.String.Lemmas
String.utf8Len.eq_2 : ∀ (c : Char) (cs : List Char), String.utf8Len (c :: cs) = String.utf8Len cs + c.utf8Size
-- Std.Time.Internal.Bounded
/-- Creates a new `Bounded.LE` using the Truncating modulus of a number.
 -/
Std.Time.Internal.Bounded.LE.byMod : ℤ → (i : ℤ) → 0 < i → Std.Time.Internal.Bounded.LE (-(i - 1)) (i - 1)
-- Aesop.RuleSet
/-- The set of rules that were erased from `normRules`, `unsafeRules`, `safeRules`
and `forwardRules`. When we erase a rule which is present in any of these four
indices, the rule is not removed from the indices but just added to this set.
By contrast, when we erase a rule from `unfoldRules`, we actually delete it.
 -/
Aesop.BaseRuleSet.erased : Aesop.BaseRuleSet → Lean.PHashSet Aesop.RuleName
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.conjAlgEquiv_apply : ∀ {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₁]
  [inst_7 : Module S M₂] [inst_8 : SMulCommClass S R M₁] [inst_9 : SMulCommClass S R M₂] [inst_10 : SMul R S]
  [inst_11 : IsScalarTower R S M₁] [inst_12 : IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : Module.End S M₁),
  (LinearEquiv.conjAlgEquiv R e) f = ↑e ∘ₗ f ∘ₗ ↑e.symm
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFree_induce_iff : ∀ {α : Type u_1} (G : SimpleGraph α) (s : Set α) (n : ℕ), (SimpleGraph.induce s G).CliqueFree n ↔ G.CliqueFreeOn s n
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.smul_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  {𝕜 : Type u_3} [inst_2 : SeminormedRing 𝕜] [inst_3 : Module 𝕜 Y] [NormSMulClass 𝕜 Y] {c : 𝕜},
  ‖c‖₊ ≠ 0 → (MemHolder r (c • f) ↔ MemHolder r f)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_g₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).g₁ = c.g₁
-- Init.Control.Lawful.Lemmas
map_inj_right_of_nonempty : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β},
  (∀ {x y : α}, f x = f y → x = y) → ∀ {x y : m α}, f <$> x = f <$> y ↔ x = y
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.inf_def : ∀ (x x_1 : ℝ),
  Real.inf✝ x x_1 =
    match x, x_1 with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 => x1 ⊓ x2) ⋯ x y }
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_1.eq_2 : ∀ {β γ : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option γ)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (out' : γ) (h' : (f out).Property (some out'))
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨some out', h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_2 out' h'
-- Mathlib.Algebra.Group.Defs
mul_pow_mul : ∀ {M : Type u_2} [inst : Monoid M] (a b : M) (n : ℕ), (a * b) ^ n * a = a * (b * a) ^ n
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext : Type
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors of equal norm is equal to 0, then the vectors are equal.  -/
InnerProductGeometry.eq_of_angle_eq_zero_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = 0 → ‖x‖ = ‖y‖ → x = y
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_iff_eq_mul_left : ∀ {a b c : ℤ}, b ≠ 0 → b ∣ a → (a.fdiv b = c ↔ a = c * b)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkNumParams : Array Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.TermElabM ℕ
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- **Alias** of the reverse direction of `ArchimedeanClass.stdPart_eq_zero`. -/
ArchimedeanClass.stdPart_of_mk_ne_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K},
  ArchimedeanClass.mk x ≠ 0 → ArchimedeanClass.stdPart x = 0
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.hasSubst_iff : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a ↔ MvPowerSeries.HasSubst (Function.const Unit a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Antitone.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [MulLeftMono α],
  Antitone f → ∀ (a : α), Antitone fun x => a * f x