mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Torsion
AddEquiv.comap_torsion : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] (e : G ≃+ H),
  AddSubgroup.comap (↑e) (AddCommGroup.torsion H) = AddCommGroup.torsion G
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_pos_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] (k : ℤ) {x : M}, 0 < x → (0 < k • x ↔ 0 < k)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.lintegral_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ),
  ∫⁻ (b : β), ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    (κ a) (Set.univ ×ˢ Set.Iic x)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₈'_int_eq_χ₄_mul_χ₈ : ∀ (a : ℤ), ZMod.χ₈' ↑a = ZMod.χ₄ ↑a * ZMod.χ₈ ↑a
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- An open subgroup of a nonarchimedean ring contains the square of another one.  -/
NonarchimedeanRing.mul_subset : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R),
  ∃ V, ↑V * ↑V ⊆ ↑U
-- Mathlib.Logic.Nontrivial.Basic
nontrivial_of_lt : ∀ {α : Type u_1} [inst : Preorder α] (x y : α), x < y → Nontrivial α
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ.eq_2 : ∀ {m₁ m₂ : ℕ} (a : ℕ) (t : List ℕ) (h_2 : m₂ + (a :: t).length = m₁),
  SimplexCategoryGenRel.standardσ (a :: t) h_2 =
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ t ⋯)
      (SimplexCategoryGenRel.σ (Fin.ofNat (m₂ + 1) a))
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.iInf_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {ι : Sort u_5} (S : ι → StarSubalgebra R A),
  (⨅ i, S i).toSubalgebra = ⨅ i, (S i).toSubalgebra
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α}
  {t₁ t₂ : Finset β},
  s₂ ⊆ s₁ →
    t₂ ⊆ t₁ →
      s₂.Nonempty →
        t₂.Nonempty →
          Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁ ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.map_join : ∀ {α : Type u} {β : Type v} (f : α → β) (S : Stream'.Seq1 (Stream'.Seq1 α)),
  Stream'.Seq1.map f S.join = (Stream'.Seq1.map (Stream'.Seq1.map f) S).join
-- Mathlib.NumberTheory.NumberField.ClassNumber
RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  (∀ ⦃I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))⦄,
      ↑(Ideal.absNorm ↑I) ≤
          (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
            (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|) →
        Submodule.IsPrincipal ↑I) →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub : {α : Type u_2} → {β : Type u_3} → [VSub α β] → VSub (Set α) (Set β)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The limit cone for the product with a zero object.  -/
CategoryTheory.Limits.binaryFanZeroLeft : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → CategoryTheory.Limits.BinaryFan 0 X
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D), (P.map F).RespectsIso
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between the zero vector and a vector.  -/
InnerProductGeometry.angle_zero_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V),
  InnerProductGeometry.angle 0 x = Real.pi / 2
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.root_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₂} (self : P.Hom Q),
  ⇑self.weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑self.indexEquiv
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.of_isNonZero : ∀ (ctx : Nat.Internal.Linear.Context) {p : Nat.Internal.Linear.Poly},
  p.isNonZero = true → Nat.Internal.Linear.Poly.denote ctx p > 0
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instSub : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] → [inst_3 : SubNegZeroMonoid R] → [ContinuousSub R] → Sub (ContinuousMapZero X R)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.dirac_withDensity' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {f : α → ENNReal},
  Measurable f → ∀ (a : α), (MeasureTheory.Measure.dirac a).withDensity f = f a • MeasureTheory.Measure.dirac a
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isIso_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact → ∀ (h : S.LeftHomologyData) [CategoryTheory.Mono S.f], CategoryTheory.IsIso h.f'
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.find? : {α : Type u_1} → {β : Type u_2} → (cmp : α → α → Ordering) → Lean.PrefixTreeNode α β cmp → List α → Option β
-- Mathlib.Data.List.Cycle
Cycle.nil_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α], Cycle.nil.toFinset = ∅
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set.  -/
IsCompact.exists_isMinOn : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] {s : Set β}, IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, IsMinOn f s x
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.finsupp_R : ∀ {A : Type u} [inst : Ring A] {N : Type v} [inst_1 : AddCommGroup N] [inst_2 : Module A N]
  (pres : Module.Presentation A N) (ι : Type w) [inst_3 : DecidableEq ι] [inst_4 : DecidableEq N],
  (pres.finsupp ι).R = ((i : ι) × pres.R)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.mk.injEq : ∀ {T : Type u_1} {N : Type u_2} (input : N) (output : List (Symbol T N)) (input_1 : N) (output_1 : List (Symbol T N)),
  ({ input := input, output := output } = { input := input_1, output := output_1 }) =
    (input = input_1 ∧ output = output_1)
-- Mathlib.Topology.Homotopy.Product
/-- Abbreviation for projection onto the right coordinate of a path class.  -/
Path.Homotopic.projRight : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {c₁ c₂ : α × β} → Path.Homotopic.Quotient c₁ c₂ → Path.Homotopic.Quotient c₁.2 c₂.2
-- Mathlib.CategoryTheory.Action
/-- Any subgroup of `G` is a vertex group in its action groupoid.  -/
CategoryTheory.ActionCategory.endMulEquivSubgroup : {G : Type u_2} →
  [inst : Group G] → (H : Subgroup G) → CategoryTheory.End ((CategoryTheory.ActionCategory.objEquiv G (G ⧸ H)) ↑1) ≃* ↥H
-- Mathlib.SetTheory.Ordinal.Notation
/-- Convert a `Nat` into an ordinal  -/
ONote.ofNat : ℕ → ONote
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.mk : {β : Type u_1} →
  {G : Type u_2} →
    {α : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : AddMonoid α] →
          (map : β → G → α → α) →
            (∀ (k : β) (g : G), map k g 0 = 0) →
              (∀ (k : β) (a : α), map k 1 a = a) →
                (∀ (k : β) (g h : G) (a : α), map k (g * h) a = map k h (map k g a)) →
                  (∀ (k : β) (g : G) (a b : α), map k g (a + b) = map k g a + map k g b) → SlashAction β G α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr →
  Lean.FVarId → Lean.Meta.Grind.Arith.Cutsat.UnsatProof → Array Lean.FVarId → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiable_inv_denom : ∀ (g : GL (Fin 2) ℝ), MDiff fun τ => (UpperHalfPlane.denom g ↑τ)⁻¹
-- Mathlib.RingTheory.Adjoin.Dimension
/-- If `A` and `B` are subalgebras of a commutative `R`-algebra `S`, both of them are
free `R`-algebras, then the rank of the rank of the subalgebra generated by `A` and `B`
over `R` is less than or equal to the product of that of `A` and `B`.  -/
Subalgebra.rank_sup_le_of_free : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [StrongRankCondition R] [inst_2 : CommRing S] [inst_3 : Algebra R S]
  (A B : Subalgebra R S) [Module.Free R ↥A] [Module.Free R ↥B],
  Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_ne_zero_of_natDegree_lt : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  f.Monic → ∀ {g : Polynomial R}, g ≠ 0 → g.natDegree < f.natDegree → (AdjoinRoot.mk f) g ≠ 0
-- Mathlib.Algebra.Group.Indicator
/-- On non-dependent functions, `Set.mulIndicator` on a singleton set equals `Pi.mulSingle`.  -/
Set.mulIndicator_singleton : ∀ {ι : Type u_6} [inst : DecidableEq ι] {M : Type u_7} [inst_1 : One M] (i : ι) (f : ι → M),
  {i}.mulIndicator f = Pi.mulSingle i (f i)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app : ∀ {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),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X) ((t.eTruncGE.map f).app X) = (t.eTruncGEπ j).app X
-- Init.WFExtrinsicFix
/-- A fixpoint combinator that allows for deferred proofs of termination.

`extrinsicFix R F` is function implemented as the loop
`extrinsicFix R F a = F a (fun a _ => extrinsicFix R F a)`.

If the loop can be shown to be well-founded, `extrinsicFix_eq_apply` proves that it satisfies the
fixpoint equation. Otherwise, `extrinsicFix R F` is opaque, i.e., it is impossible to prove
nontrivial properties about it.
 -/
WellFounded.extrinsicFix : {α : Sort u_1} →
  {C : α → Sort u_2} →
    [∀ (a : α), Nonempty (C a)] → (R : α → α → Prop) → ((a : α) → ((a' : α) → R a' a → C a') → C a) → (a : α) → C a
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.baseChange_obj_obj_carrier : ∀ (R : Type u) [inst : CommRing R] (S : Type w) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (A : CommAlgCat.FiniteEtale R), ↑((CommAlgCat.FiniteEtale.baseChange R S).obj A).obj = TensorProduct R S ↑A.obj
-- Mathlib.Analysis.Normed.Algebra.Exponential
Commute.exp : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸] {x y : 𝔸},
  Commute x y → Commute (NormedSpace.exp x) (NormedSpace.exp y)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- Some information about the rewrite position.  -/
Mathlib.Tactic.ClickSuggestions.RwInfo.rwKind : Mathlib.Tactic.ClickSuggestions.RwInfo → Mathlib.Tactic.ClickSuggestions.RwKind
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The pointwise opposite of a bounded continuous function is again bounded continuous.  -/
BoundedContinuousFunction.instNeg : {α : Type u} →
  {β : Type v} → [inst : TopologicalSpace α] → [inst_1 : SeminormedAddCommGroup β] → Neg (BoundedContinuousFunction α β)
-- Mathlib.Data.Nat.Init
Nat.decidableLoHiLe : (lo hi : ℕ) → (P : ℕ → Prop) → [DecidablePred P] → Decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.comp_rankOne : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {G : Type u_8}
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (x : E) (y : F) (f : E →L[𝕜] G),
  f ∘SL ((InnerProductSpace.rankOne 𝕜) x) y = ((InnerProductSpace.rankOne 𝕜) (f x)) y
-- Init.Data.Array.Basic
Array.reverse.loop.eq_def : ∀ {α : Type u} (as : Array α) (i : ℕ) (j : Fin as.size),
  Array.reverse.loop as i j =
    if h : i < ↑j then
      have this := ⋯;
      let as_1 := as.swap i ↑j ⋯ ⋯;
      have this := ⋯;
      Array.reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩
    else as
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_inv : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → Group (G i)] [inst_7 : Group C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h x⁻¹ = (DirectLimit.lift f (fun x => ⇑(g x)) h x)⁻¹
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.proj.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {typeName : Lean.Name} {idx : ℕ} {struct : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_1} {typeName_1 : Lean.Name}
  {idx_1 : ℕ} {struct_1 : Lean.FVarId}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_1},
  Lean.Compiler.LCNF.LetValue.proj typeName idx struct h =
      Lean.Compiler.LCNF.LetValue.proj typeName_1 idx_1 struct_1 h_1 →
    typeName = typeName_1 ∧ idx = idx_1 ∧ struct = struct_1
-- Batteries.Data.Fin.Coding
/-- Encode `Fin m → Fin n` into `Fin (n ^ m)`.  -/
Fin.encodeFun : {n m : ℕ} → (Fin m → Fin n) → Fin (n ^ m)
-- Init.Data.Vector.Nat
Vector.prod_reverse_nat : ∀ {n : ℕ} (xs : Vector ℕ n), xs.reverse.prod = xs.prod
-- Mathlib.Data.Finset.Fold
Finset.fold_disjUnion : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
  {s₁ s₂ : Finset α} {b₁ b₂ : β} (h : Disjoint s₁ s₂),
  Finset.fold op (op b₁ b₂) f (s₁.disjUnion s₂ h) = op (Finset.fold op b₁ f s₁) (Finset.fold op b₂ f s₂)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : L'.Structure M] {k : ℕ} {ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))}
  {fr : (n : ℕ) → L.Relations n → L'.Relations n} {n : ℕ} {φ : L.BoundedFormula α n}
  (v : {n : ℕ} → (Fin (k + n) → M) → α → M) {v' : β → M} (xs : Fin (k + n) → M),
  (∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
      FirstOrder.Language.Term.realize (Sum.elim v' xs') (ft n t) =
        FirstOrder.Language.Term.realize (Sum.elim (v xs') (xs' ∘ Fin.natAdd k)) t) →
    (∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) →
      (∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (Fin.snoc xs x) = v xs) →
        ((FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => FirstOrder.Language.BoundedFormula.castLE ⋯)
                φ).Realize
            v' xs ↔
          φ.Realize (v xs) (xs ∘ Fin.natAdd k))
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.unop_nonneg : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : αᵐᵒᵖ}, 0 ≤ MulOpposite.unop a ↔ 0 ≤ a
-- Aesop.Constants
Aesop.postponedSafeRuleSuccessProbability : Aesop.Percent
-- Init.Data.BitVec.Bitblast
/-- Given flattened bitvector `x : BitVec w` and a length `l : Nat`,
construct a parallel prefix sum circuit adding each available `l`-long word in `x`.
 -/
BitVec.cpopRec : {w : ℕ} → BitVec w → BitVec w
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_le_of_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N}
  {f : M →ₙ+ N}, S ≤ AddSubsemigroup.comap f T → AddSubsemigroup.map f S ≤ T
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) μ
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_iff_isLindelof_univ : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s ↔ IsLindelof Set.univ
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec.eq_1 : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S],
  AlgebraicGeometry.coprodSpec R S =
    CategoryTheory.Limits.coprod.desc (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S)))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S)))
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableConstVAdd.mk : ∀ {M : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : MeasurableSpace α],
  (∀ (c : M), Measurable fun x => c +ᵥ x) → MeasurableConstVAdd M α
-- Std.Sat.AIG.Basic
/-- If `Cache.get? decl` returns `some i` then `decls[i] = decl` holds.
 -/
Std.Sat.AIG.Cache.get?_property : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  (c : Std.Sat.AIG.Cache α decls) (decl : Std.Sat.AIG.Decl α) (hfound : (↑c)[decl]? = some idx), decls[idx] = decl
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_associator_hom_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).hom.1 = (CategoryTheory.Bicategory.associator f.1 g.1 h.1).hom
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.ext : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B D : LinearMap.BilinForm R M}, (∀ (x y : M), (B x) y = (D x) y) → B = D
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves limits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F],
  CategoryTheory.Limits.PreservesColimits F.leftOp
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₃ : CategoryTheory.MorphismProperty C₃} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₃) [Φ.IsLocalizedFullyFaithful] [Ψ.IsLocalizedFullyFaithful],
  (Φ.comp Ψ).IsLocalizedFullyFaithful
-- Mathlib.Order.WithBot
/-- `WithTop.toDual` is the equivalence sending `⊤` to `⊥` and any `a : α` to `toDual a : αᵒᵈ`.
See `WithTop.toDualBotEquiv` for the related order-iso.  -/
WithTop.toDual : {α : Type u_1} → WithTop α ≃ WithBot αᵒᵈ
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
contMDiffOn_continuousLinearMapCoordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {n : WithTop ℕ∞} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B]
  [inst_18 : FiberBundle F₁ E₁] [inst_19 : VectorBundle 𝕜 F₁ E₁] [inst_20 : FiberBundle F₂ E₂]
  [inst_21 : VectorBundle 𝕜 F₂ E₂] {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [ContMDiffVectorBundle n F₁ E₁ IB]
  [ContMDiffVectorBundle n F₂ E₂ IB] [inst_24 : MemTrivializationAtlas e₁] [inst_25 : MemTrivializationAtlas e₁']
  [inst_26 : MemTrivializationAtlas e₂] [inst_27 : MemTrivializationAtlas e₂'],
  ContMDiffOn IB (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂)) n
    (Bundle.Pretrivialization.continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_nil_equiv_symm_apply : ∀ (τ : Type u) (a : Function.FromTypes ![] τ), (Function.fromTypes_nil_equiv τ).symm a = a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {β : Type u_5} [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s + t).sup f = s.sup fun x => t.sup fun x_1 => f (x + x_1)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy),
  ed.section_ =
    {
      app := fun n =>
        CategoryTheory.CategoryStruct.comp ed.s'
          (X.left.map (SimplexCategory.isTerminalZero.from (Opposite.unop n)).op),
      naturality := ⋯ }
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.instInhabitedState : Inhabited Lean.Meta.Grind.Clean.State
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by applying the multiplication operation with a positive number.
 -/
Std.Time.Internal.Bounded.LE.mul_neg : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → num ≤ 0 → Std.Time.Internal.Bounded.LE (m * num) (n * num)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDerivWithin_mul_const` without differentiability assumption when
the scalar multiplication is by division ring elements.  -/
iteratedDerivWithin_mul_const_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_6}
  [inst_1 : NormedDivisionRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (d : 𝕜'),
  iteratedDerivWithin n (fun z => f z * d) s x = iteratedDerivWithin n f s x * d