mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The moment-generating function of a random variable with Gaussian distribution
with mean `μ` and variance `v` is given by `t ↦ exp (μ * t + v * t ^ 2 / 2)`.  -/
ProbabilityTheory.mgf_gaussianReal : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {p : MeasureTheory.Measure Ω} {μ : ℝ} {v : NNReal} {X : Ω → ℝ},
  MeasureTheory.Measure.map X p = ProbabilityTheory.gaussianReal μ v →
    ∀ (t : ℝ), ProbabilityTheory.mgf X p t = Real.exp (μ * t + ↑v * t ^ 2 / 2)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.instIsComonHomInvOfHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.ComonObj N] (f : M ≅ N)
  [CategoryTheory.IsComonHom f.hom], CategoryTheory.IsComonHom f.inv
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Set.prod_self_eq_iUnion_perm : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f.IsCycleOn s → s ×ˢ s = ⋃ n, (fun a => (a, (f ^ n) a)) '' s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getEntry? k (Std.Internal.List.eraseKey k l) = none
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.norm_smul_le : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)), ‖f • g‖ ≤ ‖f‖ * ‖g‖
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.instGroupZeroCochain : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor Cᵒᵖ GrpCat) →
      {I : Type w'} → (U : I → C) → Group (CategoryTheory.PresheafOfGroups.ZeroCochain G U)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : Dᵒᵖ) {d d' : Cᵒᵖ} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight c f =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (Opposite.unop c) f.unop).op
-- Mathlib.Combinatorics.SimpleGraph.Trails
/-- An *Eulerian trail* (also known as an "Eulerian path") is a walk
`p` that visits every edge exactly once.  The lemma `SimpleGraph.Walk.IsEulerian.IsTrail` shows
that these are trails.

Combine with `p.IsCircuit` to get an Eulerian circuit (also known as an "Eulerian cycle").  -/
SimpleGraph.Walk.IsEulerian : {V : Type u_1} → {G : SimpleGraph V} → [DecidableEq V] → {u v : V} → G.Walk u v → Prop
-- Mathlib.ModelTheory.Topology.Types
CompleteType.isClosed_typesWith : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} (φ : (L.withConstants α).Sentence), IsClosed (T.typesWith φ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k h' =
    Std.DTreeMap.Internal.Impl.Const.get t k ⋯
-- Mathlib.Analysis.Meromorphic.Divisor
MeromorphicOn.divisor.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜),
  MeromorphicOn.divisor f U =
    { toFun := fun z => if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0,
      supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }
-- Lean.Elab.Tactic.Omega.Core
/-- Construct the proof term associated to a `combine` step.  -/
Lean.Elab.Tactic.Omega.Justification.combineProof : Lean.Omega.Constraint → Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.endsWith_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.endsWith pat = true ↔ String.Slice.Pattern.Model.RevMatchesAt pat s.endPos
-- Mathlib.Algebra.Prime.Defs
Prime.isPrimal : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → IsPrimal p
-- Mathlib.Order.Filter.Extr
isMaxOn_const : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMaxOn (fun x => b) s a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a b : α}
  {fallback : β}, cmp a b = Ordering.eq → t.getD a fallback = t.getD b fallback
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne_lt_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H : Subgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H], LinearOrderedCommGroup.Subgroup.genLTOne H < 1
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U →
    Continuous f → (Topology.IsEmbedding f ↔ ∀ (i : ι), Topology.IsEmbedding ((U i).carrier.restrictPreimage f))
-- Mathlib.LinearAlgebra.SModEq.Basic
sub_smodEq_zero : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then
`CommGrpCat(F) : CommGrpCat C ⥤ CommGrpCat D` is fully faithful too.  -/
CategoryTheory.Functor.FullyFaithful.mapCommGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} → [inst_6 : F.Braided] → F.FullyFaithful → F.mapCommGrp.FullyFaithful
-- Mathlib.Order.Partition.Basic
/-- The function is the identity outside the support.  -/
Partition.IsRepFun.apply_of_notMem : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α}, P.IsRepFun f → ∀ ⦃a : α⦄, a ∉ u → f a = a
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r r' : α → β → Prop},
  Semicontinuous r → Semicontinuous r' → Semicontinuous (r ⊓ r')
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux_ker : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ),
  RingHom.ker (Algebra.Presentation.aux✝ Q P) =
    Ideal.map (MvPolynomial.rename Sum.inr) (RingHom.ker (MvPolynomial.aeval P.val))
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.epi_homologyMap_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i j k : ι),
  c.prev j = i →
    c.next j = k →
      (CategoryTheory.Epi (HomologicalComplex.homologyMap φ j) ↔
        ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
          CategoryTheory.CategoryStruct.comp y₂ (L.d j k) = 0 →
            ∃ A' π,
              ∃ (_ : CategoryTheory.Epi π),
                ∃ x₂,
                  ∃ (_ : CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0),
                    ∃ y₁,
                      CategoryTheory.CategoryStruct.comp π y₂ =
                        CategoryTheory.CategoryStruct.comp x₂ (φ.f j) + CategoryTheory.CategoryStruct.comp y₁ (L.d i j))
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- If one controls the norm of every `A x`, then one controls the norm of `A`.  -/
ContinuousLinearMap.opNNNorm_le_bound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) (M : NNReal), (∀ (x : E), ‖f x‖₊ ≤ M * ‖x‖₊) → ‖f‖₊ ≤ M
-- Mathlib.Data.EReal.Operations
/-- The product of two positive extended real numbers is positive.  -/
EReal.mul_pos : ∀ {a b : EReal}, 0 < a → 0 < b → 0 < a * b
-- Lean.Parser.Syntax
Lean.Parser.Command.identPrec.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.PowerSeries.Ideal
PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)} [I.IsPrime],
  PowerSeries.X ∉ I → I.FG → Submodule.spanFinrank I = Submodule.spanFinrank (Ideal.map PowerSeries.constantCoeff I)
-- Mathlib.Analysis.Convex.Star
StarConvex.linear_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {x : E} {s : Set E},
  StarConvex 𝕜 x s → ∀ (f : E →ₗ[𝕜] F), StarConvex 𝕜 (f x) (⇑f '' s)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.zero : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S], MvPowerSeries.HasSubst fun x => 0
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_eq_extractLsb' : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getLsbD i = (BitVec.extractLsb' i 1 x == 1#1)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a (p + b) = toIocDiv hp a b + 1
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the forward direction of `norm_sub_eq_zero_iff`. -/
eq_of_norm_sub_eq_zero : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a b : E}, ‖a - b‖ = 0 → a = b
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.codRestrict_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c ∈ p} (x : M),
  ↑((FirstOrder.Language.Embedding.codRestrict p f h) x) = f x
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instAlgebra : (K : Type u_1) →
  [inst : Field K] → {L : Type u_3} → [inst_1 : Ring L] → [Algebra K L] → Algebra (NumberField.RingOfIntegers K) L
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given two distinct paths with same endpoints, we can extract a cycle whose length is less than or
equal to the sum of their lengths.
 -/
SimpleGraph.Walk.IsPath.exists_isCycle_length_le_add_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v},
  p.IsPath → q.IsPath → p ≠ q → ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.length ≤ p.length + q.length
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- Pointwise form of `toSignedMeasure_toJordanDecomposition`.  -/
MeasureTheory.SignedMeasure.apply_eq_posPart_real_sub_negPart_real : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) {i : Set α},
  MeasurableSet i → s i = s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i
-- Init.Data.Bool
Bool.and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z || y && z)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side, version subtracting vectors.  -/
Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.instMod : {R : Type u} → [EuclideanDomain R] → Mod R
-- Lean.LocalContext
Lean.LocalContext.findFVar? : Lean.LocalContext → Lean.Expr → Option Lean.LocalDecl
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ τ₁_1 : S₁.X₁ ⟶ S₂.X₁) (e_τ₁ : τ₁ = τ₁_1) (τ₂ τ₂_1 : S₁.X₂ ⟶ S₂.X₂)
  (e_τ₂ : τ₂ = τ₂_1) (τ₃ τ₃_1 : S₁.X₃ ⟶ S₂.X₃) (e_τ₃ : τ₃ = τ₃_1)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃),
  { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
    { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, comm₁₂ := ⋯, comm₂₃ := ⋯ }
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Ioc : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.Ioc x y = Set.Ioc ↑x ↑y
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.mk.injEq : ∀ (filePath : System.FilePath) (size : USize) (isMemoryMapped : Bool) (baseAddr bufferOffset : USize) (root : NonScalar)
  (filePath_1 : System.FilePath) (size_1 : USize) (isMemoryMapped_1 : Bool) (baseAddr_1 bufferOffset_1 : USize)
  (root_1 : NonScalar),
  ({ filePath := filePath, size := size, isMemoryMapped := isMemoryMapped, baseAddr := baseAddr,
        bufferOffset := bufferOffset, root := root } =
      { filePath := filePath_1, size := size_1, isMemoryMapped := isMemoryMapped_1, baseAddr := baseAddr_1,
        bufferOffset := bufferOffset_1, root := root_1 }) =
    (filePath = filePath_1 ∧
      size = size_1 ∧
        isMemoryMapped = isMemoryMapped_1 ∧ baseAddr = baseAddr_1 ∧ bufferOffset = bufferOffset_1 ∧ root = root_1)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings.  -/
two_mul_le_add_of_sq_le_mul : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] {a b r : R}, 0 ≤ a → 0 ≤ b → r ^ 2 ≤ a * b → 2 * r ≤ a + b
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Composition by a fixed right argument as a group homomorphism  -/
CategoryTheory.Preadditive.rightComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (P : C) → {Q R : C} → (Q ⟶ R) → (P ⟶ Q) →+ (P ⟶ R)
-- Init.Core
instInhabitedPNonScalar : Inhabited PNonScalar
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)}
  (h : (F.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.mapId b₁).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_const_add_Ioo : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => a + x) '' Set.Ioo b c = Set.Ioo (a + b) (a + c)
-- Lean.Server.Requests
Lean.Server.isStatefulLspRequestMethod : String → BaseIO Bool
-- Init.Data.Option.List
Option.toList_bind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β},
  (o.bind f).toList = List.flatMap (Option.toList ∘ f) o.toList
-- Batteries.Data.DList.Basic
/-- `O(apply())`. Convert a `DList α` into a `List α` by running the `apply` function.  -/
Batteries.DList.toList : {α : Type u} → Batteries.DList α → List α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL)
      (CategoryTheory.CategoryStruct.comp (L.map s) h) =
    h
-- Init.Data.List.Basic
/-- Reverses a list.

`O(|as|)`.

Because of the “functional but in place” optimization implemented by Lean's compiler, this function
does not allocate a new list when its reference to the input list is unshared: it simply walks the
linked list and reverses all the node pointers.

Examples:
* `[1, 2, 3, 4].reverse = [4, 3, 2, 1]`
* `[].reverse = []`
 -/
List.reverse : {α : Type u} → List α → List α
-- Mathlib.Order.Partition.Basic
Partition.instSetLike : {α : Type u_1} → [inst : CompleteLattice α] → {s : α} → SetLike (Partition s) α
-- Mathlib.Data.Fin.Tuple.Basic
/-- Updating a tuple and adding an element at the end commute.  -/
Fin.snoc_update : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n)
  (y : α i.castSucc), Fin.snoc (Function.update p i y) x = Function.update (Fin.snoc p x) i.castSucc y
-- Mathlib.RingTheory.WittVector.TeichmullerSeries
_private.Mathlib.RingTheory.WittVector.TeichmullerSeries.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.RingTheory.Artinian.Module
LinearEquiv.isArtinian_iff : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid P]
  [inst_3 : Module R M] [inst_4 : Module R P] (f : M ≃ₗ[R] P), IsArtinian R M ↔ IsArtinian R P
-- ImportGraph.Tools.FindHome
instRpcEncodableGoToModuleLinkProps : Lean.Server.RpcEncodable GoToModuleLinkProps
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
/-- [Stacks Tag 0310](https://stacks.math.columbia.edu/tag/0310) ((2)) -/
Module.associatedPrimes.comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {R' : Type u_2} [inst_1 : CommRing R'] [inst_2 : Algebra R R']
  [hSR' : IsLocalization S R'] {M : Type u_3} {M' : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  [inst_5 : AddCommGroup M'] [inst_6 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [inst_8 : Module R' M']
  [IsScalarTower R R' M'],
  ∀ p ∈ associatedPrimes R' M',
    (Ideal.comap (algebraMap R R') p).FG → Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M
-- Std.Internal.Parsec.ByteArray
/-- Parses while a predicate is satisfied, up to a given limit, requiring at least one byte.
Fails with `.eof` if input ends before stopping or reaching the limit.
 -/
Std.Internal.Parsec.ByteArray.takeWhileUpTo1 : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.uniqueOfSubsingleton : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] →
                            [Subsingleton R] → [Subsingleton R₂] → Unique (M ≃ₛₗ[σ₁₂] M₂)
-- Mathlib.CategoryTheory.UnivLE
instFaithfulWitness : ∀ [inst : UnivLE.{max u v, v}], UnivLE.witness.Faithful
-- Init.Data.SInt.Lemmas
UInt32.toInt32_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt32 = OfNat.ofNat n
-- Lean.Declaration
Lean.RecursorVal.getMajorIdx : Lean.RecursorVal → ℕ
-- Init.Data.Array.Lemmas
Array.filterMap_replicate_of_isSome : ∀ {α : Type u_1} {β : Type u_2} {a : α} {n : ℕ} {f : α → Option β} (h : (f a).isSome = true),
  Array.filterMap f (Array.replicate n a) = Array.replicate n ((f a).get h)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.Sign.toBitVec_ofBitVec : ∀ (b : BitVec 1), (Float.Model.UnpackedFloat.Sign.ofBitVec b).toBitVec = b
-- Mathlib.RingTheory.Ideal.Maximal
/-- If P is not properly contained in any maximal ideal then it is not properly contained
in any proper ideal  -/
Ideal.maximal_of_no_maximal : ∀ {α : Type u} [inst : Semiring α] {P : Ideal α},
  (∀ (m : Ideal α), P < m → ¬m.IsMaximal) → ∀ (J : Ideal α), P < J → J = ⊤
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Iic : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α) [inst_2 : Fintype ↑(Set.Iic a)],
  Fintype.card ↑(Set.Iic a) = (Finset.Iic a).card
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_add : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} (x y : ↥S), ↑(x + y) = ↑x + ↑y
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  {P Q : CategoryTheory.Functor Cᵒᵖ A}
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallyInjective J f],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f))
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_neg : ∀ {b x : ℝ}, 1 < b → 0 < x → x < 1 → Real.logb b x < 0
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_iInf : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] {ι : Sort u_3} (K : ι → Ideal S), Ideal.comap f (iInf K) = ⨅ i, Ideal.comap f (K i)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The inclusion functor is a final functor  -/
CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_final : CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.Final