mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMax.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.insertMax k v Std.DTreeMap.Internal.Impl.leaf hr_1 =
    { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
      balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- An affine equivalence, denoted `P₁ ≃ᵃ[k] P₂`, is an equivalence between affine spaces
such that both forward and inverse maps are affine.

We define it using an `Equiv` for the map and a `LinearEquiv` for the linear part in order
to allow affine equivalences with good definitional equalities.  -/
«term_≃ᵃ[_]_» : Lean.TrailingParserDescr
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitEntry.mk : {α : Type} → Lean.Meta.LazyDiscrTree.Key → Lean.Meta.LazyDiscrTree.LazyEntry α → Lean.Meta.LazyDiscrTree.InitEntry α
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function `f` is strongly measurable at a filter `l` w.r.t. a measure `μ` if it is
ae strongly measurable w.r.t. `μ.restrict s` for some `s ∈ l`.  -/
StronglyMeasurableAtFilter : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      [TopologicalSpace β] →
        (α → β) → Filter α → autoParam (MeasureTheory.Measure α) StronglyMeasurableAtFilter._auto_1 → Prop
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_one_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 < a → (a ^ n ≤ 1 ↔ n ≤ 0)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_lt_iff_of_pos : ∀ {z : ℝ} {y : NNReal}, 0 ≤ y → 0 < z → ∀ (x : NNReal), x ^ z⁻¹ < y ↔ x < y ^ z
-- Init.Data.Array.Attach
/-- Variant of `foldl_subtype` with side condition to check `stop = l.size`.  -/
Array.foldl_subtype' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {p : α → Prop} {xs : Array { x // p x }} {f : β → { x // p x } → β}
  {g : β → α → β} {x : β},
  (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) →
    stop = xs.size → Array.foldl f x xs 0 stop = Array.foldl g x xs.unattach
-- Init.Data.Option.Lemmas
Option.isSome_or : ∀ {α : Type u_1} {o o' : Option α}, (o.or o').isSome = (o.isSome || o'.isSome)
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_coe : ∀ {α : Type u_1} [inst : Zero α] (a : α), (↑a).untop₀ = a
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.indep : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndep m κ μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.Kernel.Indep (m i) (m j) κ μ
-- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
/-- **Alias** of `AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty`.

---

The `G`-action on `X` is proper iff, for each pair of compacts `U, V` in `X`,
the set of `g` such that `U` intersects `g +ᵥ V` is compact.

See `ProperVAdd.isCompact_setOfPred_inter_nonempty`
for a one-way implication with fewer conditions.

**Note**: We assume `CompactlyCoherentSpace (X × X)`
as this is the minimal assumption needed to make the proof work;
but this follows from various more familiar conditions,
such as `FirstCountableTopology X`.
Importing `Mathlib.Topology.Sequences` makes this implication available.
 -/
AddAction.properVAdd_iff_isCompact_setOf_inter_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  [inst_3 : AddAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [ContinuousVAdd G X],
  ProperVAdd G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | ((g +ᵥ U) ∩ V).Nonempty}
-- Init.Data.SInt.Lemmas
Int16.neg_nonpos_iff : ∀ (n : Int16), -n ≤ 0 ↔ n = Int16.minValue ∨ 0 ≤ n
-- Mathlib.Algebra.Group.Nat.Even
Nat.one_lt_of_ne_zero_of_even : ∀ {n : ℕ}, n ≠ 0 → Even n → 1 < n
-- Init.Data.Vector.FinRange
Vector.finRange_succ : ∀ {n : ℕ}, Vector.finRange (n + 1) = Vector.cast ⋯ (#v[0] ++ Vector.map Fin.succ (Vector.finRange n))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_eq_of_two_zsmul_eq : ∀ {θ ψ : Real.Angle}, 2 • θ = 2 • ψ → θ.tan = ψ.tan
-- Init.Data.String.Basic
String.Pos.ofSliceTo_le_ofSliceTo_iff : ∀ {s : String} {p : s.Pos} {q r : (s.sliceTo p).Pos}, String.Pos.ofSliceTo q ≤ String.Pos.ofSliceTo r ↔ q ≤ r
-- Init.Guard
/-- Alpha-eq matching for `guard_hyp` values  -/
Lean.Parser.colonEqA : Lean.ParserDescr
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.sub_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y Z : C}
  (f g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f - g) h =
    CategoryTheory.CategoryStruct.comp f h - CategoryTheory.CategoryStruct.comp g h
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
Associated.moebius_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  Associated a b → UniqueFactorizationMonoid.moebius a = UniqueFactorizationMonoid.moebius b
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_ext_iff : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {f g : M ⟶ N}, f = g ↔ ModuleCat.Hom.hom f = ModuleCat.Hom.hom g
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformEquiv.inv.eq_1 : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  UniformEquiv.inv G = { toEquiv := Equiv.inv G, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
-- Init.Data.Int.LemmasAux
Int.natCast_ne_zero_iff_pos : ∀ {n : ℕ}, ↑n ≠ 0 ↔ 0 < n
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart.  -/
mdifferentiableWithinAt_iff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Data.Fintype.EquivFin
_private.Mathlib.Data.Fintype.EquivFin.0.Infinite.natEmbeddingAux : (α : Type u_4) → [Infinite α] → ℕ → α
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.exteriorPower.eq_1 : ∀ (R : Type u1) [inst : CommRing R] (n : ℕ) (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ⋀[R]^n M = (ExteriorAlgebra.ι R).range ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The witness of the universal property for the chosen factorisation of `f` through
a monomorphism.  -/
CategoryTheory.Limits.Image.isImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          CategoryTheory.Limits.IsImage (CategoryTheory.Limits.Image.monoFactorisation f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y)
  (eq :
    autoParam (CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
      CategoryTheory.Limits.PullbackCone.mk._auto_1),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).pt = W
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iAlls.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (β : Type v') [inst : Finite β] (φ : L.Formula (α ⊕ β)),
  FirstOrder.Language.Formula.iAlls β φ =
    (FirstOrder.Language.BoundedFormula.relabel (fun a => Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCover_f : ∀ (X : AlgebraicGeometry.Scheme) (i : X.affineCover.I₀), X.affineOpenCover.f i = X.affineCover.f i
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The homotopy cofiber of a morphism of homological complexes,
also known as the mapping cone.  -/
HomologicalComplex.homotopyCofiber : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) → [HomologicalComplex.HasHomotopyCofiber φ] → [DecidableRel c.Rel] → HomologicalComplex C c
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- Convert a bundled function to a morphism of `C`.  -/
CategoryTheory.ConcreteCategory.ofHom : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {FC : outParam (C → C → Type u_1)} →
      {CC : outParam (C → Type w)} →
        {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} →
          [self : CategoryTheory.ConcreteCategory C FC] → {X Y : C} → FC X Y → (X ⟶ Y)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T T' : Set α → β}
  [inst : AddCommMonoid β],
  MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive μ T' → MeasureTheory.FinMeasAdditive μ (T + T')
-- Mathlib.Data.PNat.Basic
/-- An induction principle for `ℕ+`: it takes values in `Sort*`, so it applies also to Types,
not only to `Prop`.  -/
PNat.recOn : (n : ℕ+) → {p : ℕ+ → Sort u_1} → p 1 → ((n : ℕ+) → p n → p (n + 1)) → p n
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsLittleOIsEquivalent : {α : Type u_1} →
  {β : Type u_2} →
    {β₂ : Type u_3} →
      [inst : NormedAddCommGroup β] →
        [inst_1 : Norm β₂] →
          {l : Filter α} → Trans (Asymptotics.IsLittleO l) (Asymptotics.IsEquivalent l) (Asymptotics.IsLittleO l)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates finite limits, then `F : C ⥤ D` creates finite colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsOfOp : {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.CreatesFiniteLimits F.op] → CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverEntropyInfEntourage_image_le : ∀ {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) (V : SetRel Y Y),
      Dynamics.coverEntropyInfEntourage T (φ '' F) V ≤ Dynamics.coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V)
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffVAddOfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M] {n : WithTop ℕ∞}
  [ContMDiffVAdd I I' (↑⊤) G M] [ENat.LEInfty n], ContMDiffVAdd I I' n G M
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `MonoidAlgebra.mapRangeAlgEquiv` as a `MonoidHom` from `A ≃ₐ[R] A`.  -/
MonoidAlgebra.mapRangeAlgAut : (R : Type u_1) →
  {A : Type u_4} →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Monoid M] → (A ≃ₐ[R] A) →* MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A M
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.id_eq : ∀ (X : CategoryTheory.Limits.WalkingReflexivePair),
  CategoryTheory.Limits.WalkingReflexivePair.Hom.id X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearEquiv.leftInverse_hasLeftInverse : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] (f : E ≃L[R] F), ⋯.leftInverse = ↑f.symm
-- Init.Data.List.Nat.Sum
List.sum_append_nat : ∀ {l₁ l₂ : List ℕ}, (l₁ ++ l₂).sum = l₁.sum + l₂.sum
-- Mathlib.Algebra.Quandle
/-- A *Shelf* is a structure with a self-distributive binary operation.
The binary operation is regarded as a left action of the type on itself.
 -/
Shelf : Type u → Type u
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : MulOneClass γ]
  (f : α →* β) (g : β →* γ) (x : WithZero α), (WithZero.map' g) ((WithZero.map' f) x) = (WithZero.map' (g.comp f)) x
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying type.  -/
AddMonCat.carrier : AddMonCat → Type u
-- Mathlib.Order.ModularLattice
IsModularLattice.inf_sup_inf_assoc : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
-- Mathlib.Analysis.Normed.Module.Basic
SeparationQuotient.instNormedSpace : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [NormedSpace 𝕜 E] → NormedSpace 𝕜 (SeparationQuotient E)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor_toNat_sum_le : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ),
  ∑ i, (IsProperLinearSet.floor✝ hs x i).toNat • ↑i ≤ x + ∑ i, (-IsProperLinearSet.floor✝ hs x i).toNat • ↑i
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (n : WithTop ℕ∞)
  (f : E → F) (s : Set E), ContDiffOn 𝕜 n f s = ∀ x ∈ s, ContDiffWithinAt 𝕜 n f s x
-- Std.Async.Process
/-- CPU time spent in user mode (milliseconds)
 -/
Std.IO.Process.ResourceUsageStats.cpuUserTime : Std.IO.Process.ResourceUsageStats → Std.Time.Millisecond.Offset
-- Mathlib.Logic.Equiv.Option
Equiv.removeNoneAux_none : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α}, e (some x) = none → some (e.removeNoneAux x) = e none
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_eq_Ico_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo b a = Set.Ico b a ↔ ¬b < a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
/-- Given a partition `P` of `s`, as well as a proof that `a * m + b * (m + 1) = #s`, we can
find a new partition `Q` of `s` where each part has size `m` or `m + 1`, every part of `P` is the
union of parts of `Q` plus at most `m` extra elements, there are `b` parts of size `m + 1` and
(provided `m > 0`, because a partition does not have parts of size `0`) there are `a` parts of size
`m` and hence `a + b` parts in total.  -/
Finpartition.equitabilise_aux : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m a b : ℕ} {P : Finpartition s},
  a * m + b * (m + 1) = s.card →
    ∃ Q,
      (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧
        (∀ x ∈ P.parts, (x \ {y ∈ Q.parts | y ⊆ x}.biUnion id).card ≤ m) ∧ {i ∈ Q.parts | i.card = m + 1}.card = b
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra : {A : Type u_1} → [self : NonUnitalCommCStarAlgebra A] → NonUnitalCStarAlgebra A
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (c : CategoryTheory.Limits.Cone F) (α : F ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c) (CategoryTheory.Limits.limMap α) =
    CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cone.postcompose α).obj c)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.filter_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop), π.filter p ≤ π
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.instMonoidHomClass : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G), MonoidHomClass S.Splitting G E
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f f_1 : A →+* B} (e_f : f = f_1)
  {K : Type u_3} {M : Submonoid A} [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K]
  (L : Type u_4) {N : Submonoid B} [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L]
  (hf : M ≤ Submonoid.comap f N) (I I_1 : FractionalIdeal M K),
  I = I_1 → FractionalIdeal.extended L hf I = FractionalIdeal.extended L ⋯ I_1
-- Mathlib.Topology.Baire.Lemmas
/-- In a nonempty Baire space, any dense `Gδ` set is not meagre.  -/
not_isMeagre_of_isGδ_of_dense : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] [Nonempty X] {s : Set X}, IsGδ s → Dense s → ¬IsMeagre s
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Asymptotics.IsTheta.summable_iff : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : ι → E}
  {g : ι → F}, f =Θ[Filter.cofinite] g → (Summable f ↔ Summable g)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.re_toComplex : ∀ (x y : ℤ), (GaussianInt.toComplex { re := x, im := y }).re = ↑x
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- At the SL level: when `Fintype.card ι = 2`, the supremum over all projective points of
the `lineStab` subgroups equals `⊤` in `SL ι F`.  -/
PSL.iSup_lineStab_eq_top : ∀ {F : Type u_2} [inst : Field F], ⨆ p, Matrix.SpecialLinearGroup.lineStab p.submodule = ⊤
-- Mathlib.Algebra.Order.SuccPred
Order.le_sub_one_iff : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α] [NoMinOrder α],
  x ≤ y - 1 ↔ x < y
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- On a finite-dimensional space, a linear map is injective if and only if it is surjective.  -/
LinearMap.injective_iff_surjective : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {f : V →ₗ[K] V}, Function.Injective ⇑f ↔ Function.Surjective ⇑f
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toCoweightBasis_apply : ∀ {ι : 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] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsRootSystem] (i : ↥b.support), b.toCoweightBasis i = P.coroot ↑i
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, then we
can push forward a continuous compactly supported function on `B` to a continuous compactly
supported function on `C` by integrating over `A`.  -/
TopologicalGroup.IsSES.pushforward : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {E : Type u_4} →
        [inst : Group A] →
          [inst_1 : Group B] →
            [inst_2 : Group C] →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : TopologicalSpace C] →
                    {φ : A →* B} →
                      {ψ : B →* C} →
                        TopologicalGroup.IsSES φ ψ →
                          [IsTopologicalGroup A] →
                            [IsTopologicalGroup B] →
                              [inst_8 : NormedAddCommGroup E] →
                                [inst_9 : MeasurableSpace A] →
                                  [BorelSpace A] →
                                    (μA : MeasureTheory.Measure A) →
                                      [hμA : μA.IsHaarMeasure] →
                                        [inst : NormedSpace ℝ E] →
                                          [IsTopologicalGroup C] →
                                            [LocallyCompactSpace B] →
                                              CompactlySupportedContinuousMap B E →ₗ[ℝ]
                                                CompactlySupportedContinuousMap C E
-- Mathlib.Data.Nat.Basic
Nat.instPreorder : Preorder ℕ
-- Mathlib.Order.Bounds.Image
IsCofinalFor.image_of_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s t : Set α} {f : α → β},
  IsCofinalFor s t → Antitone f → IsCoinitialFor (f '' s) (f '' t)
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.eq_iff : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {L₁ L₂ : IntermediateField.Lifts F E K},
  L₁ = L₂ ↔ ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (IntermediateField.inclusion ⋯) = L₁.emb
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instDecidableEqOfLawfulBEq : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] →
          [inst_3 : (k : α) → BEq (β k)] → [∀ (k : α), LawfulBEq (β k)] → DecidableEq (Std.ExtDHashMap α β)
-- Lean.Elab.PreDefinition.WF.Eqns
/-- This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `foo`
in a module would cause `foo.eq_def` to be defined eagerly and privately,
but it should still be visible from non-module files.

So we create a unfold equation generator that aliases an existing private `eq_def` to
wherever the current module expects it.
 -/
_private.Lean.Elab.PreDefinition.WF.Eqns.0.Lean.Elab.WF.copyPrivateUnfoldTheorem : Lean.Meta.GetUnfoldEqnFn
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.some_eq_natCast`.

---

Lemmas about `WithTop` expect (and can output) `WithTop.some` but the normal form for coercion
`ℕ → ℕ∞` is `Nat.cast`.  -/
ENat.some_eq_coe : WithTop.some = Nat.cast
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α} {k : α},
  k ∈ t → (t.insertMany l).get? k = t.get? k
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.instModuleSelf : {n : Type u_1} → {R : Type u_2} → [inst : CommRing R] → Module R (MvPolynomial n R)
-- Init.Data.SInt.Lemmas
ISize.toInt_bmod_size : ∀ (a : ISize), a.toInt.bmod ISize.size = a.toInt
-- Mathlib.Algebra.CubicDiscriminant
/-- The degree-0 coefficient  -/
Cubic.d : {R : Type u_1} → Cubic R → R
-- Init.Data.String.Defs
String.Slice.offset_endPos : ∀ {s : String.Slice}, s.endPos.offset = s.rawEndPos
-- Mathlib.Algebra.BigOperators.Finprod
finsum_apply_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (a : α), ∑ᶠ (_ : f a ≠ 0), f a = f a