mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.Simps.symm_apply.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), MulEquiv.Simps.symm_apply e = ⇑e.symm
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  Neg.neg '' Set.Ioi a = Set.Iio (-a)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
HasFDerivAtFilter.of_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {L : Filter (E × E)},
  ((fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; L] fun p => p.1 - p.2) → HasFDerivAtFilter f f' L
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.IsPrimitive.exists_pos_pow : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Fintype n] [inst_3 : DecidableEq n]
  {A : Matrix n n R}, A.IsPrimitive → ∃ k > 0, ∀ (i j : n), 0 < (A ^ k) i j
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.submartingale_nat : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedAddMonoid E] [ClosedIciTopology E] [IsOrderedModule ℝ E] [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]) → MeasureTheory.Submartingale f 𝒢 μ
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_simple_mul : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- We say that a functor creates finite colimits if it creates all colimits of shape `J` where
`J : Type` is a finite category.  -/
CategoryTheory.Limits.CreatesFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.below : {c₀ : RBTree.RBColor} →
  {n₀ : ℕ} →
    {α : Type u_1} →
      {motive :
          (a : RBTree.RBNode.Path α) →
            (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop} →
        {a : RBTree.RBNode.Path α} →
          {a_1 : RBTree.RBColor} → {a_2 : ℕ} → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instDistribMulAction : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {S : Type u_10} →
                    [inst_5 : Monoid S] →
                      [inst_6 : DistribMulAction S N] → [SMulCommClass R S N] → DistribMulAction S (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {z : M} {F' : Type u_21} [inst_6 : NormedDivisionRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'}, MDiffAt p z → p z ≠ 0 → MDiffAt p⁻¹ z
-- Init.Data.AC
Lean.Data.AC.Variable.neutral : {α : Sort u} → {op : α → α → α} → (self : Lean.Data.AC.Variable op) → Option (PLift (Std.LawfulIdentity op self.value))
-- Mathlib.Data.Fintype.Sum
/-- Any injection from a set `s` in a fintype `α` to a finset `t` of the same cardinality as `α`
can be extended to a bijection between `α` and `t`.  -/
Set.MapsTo.exists_equiv_extend_of_card_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {t : Finset β},
  Fintype.card α = t.card → ∀ {s : Set α} {f : α → β}, Set.MapsTo f s ↑t → Set.InjOn f s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_map_right : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {M₃ : Type u_7}
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module R M₃] (f : M₁ →ₗ[R] M₃) (g : M₂ ≃ₗ[R] M₃),
  (LinearMap.toMatrix v₁ (v₂.map g)) f = (LinearMap.toMatrix v₁ v₂) (↑g.symm ∘ₗ f)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.default.sizeOf_spec : sizeOf Lean.Elab.Tactic.Simp.DischargeWrapper.default = 1
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_nsmul : ∀ (n : ℕ) (x : NNReal), ↑(n • x) = n • ↑x
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Iio_add_one : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∏ i < a + 1, f i = (∏ i < a, f i) * f a
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.instPartialOrder : {G : Type u_1} → [inst : AddGroup G] → PartialOrder (AddSubgroup G)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If for every cell either `A ∩ openCell n j` or `A ∩ closedCell n j` is closed then
`A` is closed.  -/
Topology.CWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] [T2Space X] {A : Set X},
  A ⊆ C →
    (∀ (n : ℕ),
        0 < n →
          ∀ (j : Topology.RelCWComplex.cell C n),
            IsClosed (A ∩ Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) →
      IsClosed A
-- Mathlib.RingTheory.DedekindDomain.Dvr
IsDedekindDomainDvr.toIsNoetherian : ∀ {A : Type u_1} {inst : CommRing A} {inst_1 : IsDomain A} [self : IsDedekindDomainDvr A], IsNoetherian A A
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.contains.match_1.eq_2 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (x : String.Slice.Pattern.SearchStep s)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (x : String.Slice.Pattern.SearchStep s) → motive x),
  (∀ (startPos endPos : s.Pos), x = String.Slice.Pattern.SearchStep.matched startPos endPos → False) →
    (match x with
      | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
      | x => h_2 x) =
      h_2 x
-- Mathlib.RingTheory.FormalGroup.Basic
_private.Mathlib.RingTheory.FormalGroup.Basic.0.termX₁ : Lean.ParserDescr
-- Init.Data.Int.Order
Int.le_natAbs : ∀ {a : ℤ}, a ≤ ↑a.natAbs
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- A satellite configuration is a configuration of `N+1` points that shows up in the inductive
construction for the Besicovitch covering theorem. It depends on some parameter `τ ≥ 1`.

This is a family of balls (indexed by `i : Fin N.succ`, with center `c i` and radius `r i`) such
that the last ball intersects all the other balls (condition `inter`),
and given any two balls there is an order between them, ensuring that the first ball does not
contain the center of the other one, and the radius of the second ball cannot be larger than
the radius of the first ball (up to a factor `τ`). This order corresponds to the order of choice
in the inductive construction: otherwise, the second ball would have been chosen before.
This is the condition `h`.

Finally, the last ball is chosen after all the other ones, meaning that `h` can be strengthened
by keeping only one side of the alternative in `hlast`.
 -/
Besicovitch.SatelliteConfig : (α : Type u_1) → [MetricSpace α] → ℕ → ℝ → Type u_1
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) {D : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} D],
  ((CategoryTheory.Functor.whiskeringLeft (HomologicalComplex V c) (HomotopyCategory V c) D).obj
      (HomotopyCategory.quotient V c)).Full
-- Mathlib.Logic.Hydra
Relation.cutExpand_pair_left : ∀ {α : Type u_1} {r : α → α → Prop} {a' a b : α}, r a' a → Relation.CutExpand r {a', b} {a, b}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_minKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).minKey?.isSome = !t.isEmpty
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_smul_closedEBall`. -/
EMetric.preimage_smul_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal),
  (fun x => c • x) ⁻¹' Metric.closedEBall x r = Metric.closedEBall (c⁻¹ • x) r
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- The universal property of `AdicCompletion` for rings.
The lift ring map `R →+* AdicCompletion I S` of a compatible family of
ring maps `R →+* S ⧸ I ^ n`.
 -/
AdicCompletion.liftRingHom : {R : Type u_4} →
  {S : Type u_5} →
    [inst : NonAssocSemiring R] →
      [inst_1 : CommRing S] →
        (I : Ideal S) →
          (f : (n : ℕ) → R →+* S ⧸ I ^ n) →
            (∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) → R →+* AdicCompletion I S
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).leadingExp = ↑exp
-- Batteries.Data.AssocList
Batteries.AssocList.find?_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  Batteries.AssocList.find? a l = Option.map (fun x => x.2) (List.find? (fun x => x.1 == a) l.toList)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.id_comp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), (AlgHom.id R B).comp φ = φ
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.instHtmlEvalTermElabMHtml : ProofWidgets.HtmlEval (Lean.Elab.TermElabM ProofWidgets.Html)
-- Mathlib.Topology.Inseparable
/-- **Alias** of the forward direction of `specializes_iff_closure_subset`. -/
Specializes.closure_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → closure {y} ⊆ closure {x}
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
/-- The t-structure induced on the full subcategory of `t`-bounded above objects.  -/
CategoryTheory.Triangulated.TStructure.onPlus : {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) →
                [CategoryTheory.IsTriangulated C] → CategoryTheory.Triangulated.TStructure t.plus.FullSubcategory
-- Mathlib.Topology.Separation.Regular
IsCompact.closure_eq_nhdsKer : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {s : Set X}, IsCompact s → closure s = nhdsKer s
-- Mathlib.RingTheory.DividedPowers.Basic
/-- A "multinomial" theorem for divided powers — without multinomial coefficients — for finitely
supported functions.  -/
DividedPowers.dpow_finsupp_sum : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {ι : Type u_2} [inst_1 : DecidableEq ι]
  {x : ι →₀ A},
  (∀ (i : ι), x i ∈ I) →
    ∀ {n : ℕ}, hI.dpow n (x.sum fun x r => r) = ∑ k ∈ x.support.sym n, x.prod fun i r => hI.dpow (Multiset.count i ↑k) r
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2_indicator_of_measurable : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E),
  ↑((MeasureTheory.condExpL2 E 𝕜 hm) (MeasureTheory.indicatorConstLp 2 ⋯ hμs c)) =
    MeasureTheory.indicatorConstLp 2 ⋯ hμs c
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- On a sphere of nonzero radius, the central angle `∠ p₁ s.center p₂` equals zero iff
`p₁ = p₂`.  -/
EuclideanGeometry.Sphere.angle_center_eq_zero_iff_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → s.radius ≠ 0 → (EuclideanGeometry.angle p₁ s.center p₂ = 0 ↔ p₁ = p₂)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_same_index_anti : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} [inst : LinearOrder ι] {p : ι → Prop}
  {sa : ι → Set α} {sb : ι → Set β},
  la.HasBasis p sa →
    lb.HasBasis p sb → AntitoneOn sa {i | p i} → AntitoneOn sb {i | p i} → (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
-- Batteries.Util.LibraryNote
Batteries.Util.instInhabitedLibraryNote : Inhabited Batteries.Util.LibraryNote
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A shorthand for the natural transformation of functors out of PUnit defined by
the canonical morphism `𝟙_ V ⟶ U.obj (𝟙_ C)` when `U` is a unit for Day convolution.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (U : CategoryTheory.Functor C V) →
              [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] →
                CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V) ⟶
                  (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp U
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
ContinuousLinearMap.integrable_comp : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜' E]
  [inst_5 : NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] {φ : α → H} (L : H →SL[σ] E),
  MeasureTheory.Integrable φ μ → MeasureTheory.Integrable (fun a => L (φ a)) μ
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one : Asymptotics.IsEquivalent Filter.atTop (fun x => 1 + AkraBazziRecurrence.smoothingFn x) fun x => 1
-- Mathlib.Analysis.Complex.Norm
Complex.norm_prod : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℂ), ‖s.prod f‖ = ∏ i ∈ s, ‖f i‖
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- We define `PreLp E` to be a type synonym for `∀ i, E i` which, importantly, does not inherit
the `pi` topology on `∀ i, E i` (otherwise this topology would descend to `lp E p` and conflict
with the normed group topology we will later equip it with.)

We choose to deal with this issue by making a type synonym for `∀ i, E i` rather than for the `lp`
subgroup itself, because this allows all the spaces `lp E p` (for varying `p`) to be subgroups of
the same ambient group, which permits lemma statements like `lp.monotone` (below).  -/
PreLp : {α : Type u_3} → (E : α → Type u_5) → [(i : α) → NormedAddCommGroup (E i)] → Type (max u_3 u_5)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {f : β k → β k},
  t.WF → (Std.DTreeMap.Internal.Impl.modify k f t).minKey? = t.minKey?
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Functor.objEquiv_symm_apply_apply : ∀ {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] (F : CategoryTheory.Functor C D) [inst_2 : F.IsIso] (X : C),
  F.objEquiv.symm (F.obj X) = X
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T : Set α → β} {C : ℝ} {μ' : MeasureTheory.Measure α} {c : ENNReal},
  c ≠ ⊤ →
    μ ≤ c • μ' →
      MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive μ' T (c.toReal * C)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.insert : ∀ {left right : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  Tactic.ComputeAsymptotics.WellFormedBasis (left ++ right) →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[Filter.atTop] (Real.log ∘ g)) →
        (∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[Filter.atTop] (Real.log ∘ f)) →
          Tactic.ComputeAsymptotics.WellFormedBasis (left ++ f :: right)
-- Init.Notation
/-- Addition of precedences. This is normally used only for offsetting, e.g. `max + 1`.  -/
Lean.Parser.Syntax.addPrec : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
/-- A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `AlgHom` on the LHS.  -/
Matrix.mvPolynomialX_mapMatrix_aeval : ∀ {m : Type u_1} (R : Type u_3) {S : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (A : Matrix m m S),
  (MvPolynomial.aeval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (a : ι → ↥A),
  (Submodule.mulLeftMap (Subalgebra.toSubmodule B) a).ker = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
-- Init.Data.Int.Basic
Int.ofNat_zero : ↑0 = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_zero_left : ∀ {x : ℝ}, Real.logb 0 x = 0
-- Mathlib.Order.Monotone.Monovary
Subsingleton.antivaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton ι] (f : ι → α)
  (g : ι → β) (s : Set ι), AntivaryOn f g s
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.insert : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X},
  Metric.IsSeparated ε s → (∀ y ∈ s, x ≠ y → ε < edist x y) → Metric.IsSeparated ε (insert x s)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.algebraMap_eq_coe : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} {L : Type u_2} [inst_1 : Field L]
  [inst_2 : Algebra K L] (w : NumberField.InfinitePlace L) (x : WithAbs ↑v),
  (algebraMap (WithAbs ↑v) w.Completion) x = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instLattice : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Lattice β] → Lattice (MeasureTheory.SimpleFunc α β)
-- Mathlib.Lean.Elab.InfoTree
/-- Get the `parentDecl`s of every elaborated body.

This includes `let rec`/`where` definitions, but excludes decls without "bodies" (such as
`alias`es, `structure`s, declarations generated by attributes like `@[ext]`, and so on) as we
might find by considering every `parentDeclCtx` throughout the infotree.

Assumes that every body elaboration proceeds through `Lean.Elab.Term.BodyInfo`.
 -/
Lean.Elab.InfoTree.getDeclsByBody : Lean.Elab.InfoTree → List Lean.Name
-- Aesop.Search.Queue
Aesop.BestFirstQueue.addGoals : Aesop.BestFirstQueue → Array Aesop.GoalRef → BaseIO Aesop.BestFirstQueue
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.size_eq_match_rcc : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.HasSize α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some next => (next...r.upper).size
-- Mathlib.Order.Bounds.Basic
bbdBelow_range_left_of_inf : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeInf α] {f g : ι → α},
  BddBelow (Set.range fun x => f x ⊓ g x) → BddBelow (Set.range f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w : ℕ} (aig : Std.Sat.AIG α)
  (oldLayer : aig.RefVec (len * w)) (h : 0 < len) (idx : ℕ)
  (h1 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go oldLayer h).aig.decls.size)
  (h2 : idx < aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go oldLayer h).aig.decls[idx] = aig.decls[idx]
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) (x : ↑(⇑f ⁻¹' {y})),
  (AlgebraicGeometry.Scheme.Hom.fiberι f y) ((AlgebraicGeometry.Scheme.Hom.fiberHomeo f y).symm x) = ↑x
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.ext : ∀ {C : Type u} {inst : CategoryTheory.Groupoid C} {x y : CategoryTheory.Subgroupoid C}, x.arrows = y.arrows → x = y
-- Mathlib.Analysis.Complex.Basic
Complex.continuous_re : Continuous Complex.re
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasurableEmbedding.isProbabilityMeasure_comap : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ] {f : β → α},
  MeasurableEmbedding f →
    (∀ᵐ (a : α) ∂μ, a ∈ Set.range f) → MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.explicit : Lean.Option Bool
-- Mathlib.LinearAlgebra.Ray
/-- If `y` and `z` are on the same ray as `x`, then so is `y + z`.  -/
SameRay.add_right : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y z : M}, SameRay R x y → SameRay R x z → SameRay R x (y + z)
-- Init.Data.Array.Basic
/-- Returns a new array that contains the longest prefix of elements that satisfy the predicate `p` from
an array.

Examples:
 * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 2) = #[0, 1]`
 * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 20) = #[0, 1, 2, 3, 2, 1]`
 * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
Array.takeWhile : {α : Type u} → (α → Bool) → Array α → Array α