mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of an integrable function is smaller than its mean, while
avoiding a null set.  -/
MeasureTheory.exists_notMem_null_le_average : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
  [MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → MeasureTheory.Integrable f μ → μ N = 0 → ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
-- Mathlib.Topology.Compactness.Lindelof
SecondCountableTopology.toHereditarilyLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] [SecondCountableTopology X], HereditarilyLindelofSpace X
-- Mathlib.Topology.MetricSpace.Defs
instDistAdditive : {X : Type u_1} → [Dist X] → Dist (Additive X)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_right_cancel : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, IsUnit b → a * b = c * b → a = c
-- Lean.Meta.Tactic.Replace
/-- Convert the given goal `Ctx |- target` into `Ctx |- targetNew` using an equality proof `eqProof : target = targetNew`.
It assumes `eqProof` has type `target = targetNew`  -/
Lean.MVarId.replaceTargetEq : Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MVarId
-- Mathlib.Topology.Order.LeftRightNhds
/-- If `S` is order-connected and contains two points `x < y`, then `S` is a left neighbourhood
of `y`.  -/
Set.OrdConnected.mem_nhdsLE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {S : Set α} {x y : α},
  S.OrdConnected → x ∈ S → y ∈ S → x < y → S ∈ nhdsWithin y (Set.Iic y)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Characterization of `C^n` functions into a vector bundle. Version at a point.  -/
Bundle.contMDiffAt_totalSpace : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7}
  [inst_5 : NormedAddCommGroup EB] [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM]
  {HM : Type u_11} [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  {f : M → Bundle.TotalSpace F E} {x₀ : M},
  ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f x₀ ↔
    ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧
      ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_bif_eq_bif : ∀ (d a b c : Bool), ((!bif d then a else b) == bif d then a else c) = (!d && (!b) == c)
-- Batteries.Util.ProofWanted
DerivedWanted.ofVal.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α] (val : α), sizeOf { val := val } = 1 + sizeOf val
-- Init.Prelude
Monad.mk : {m : Type u → Type v} → [toApplicative : Applicative m] → [toBind : Bind m] → Monad m
-- Mathlib.Order.Interval.Set.Basic
Set.isEmpty_Iio_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], IsEmpty ↑(Set.Iio 1)
-- Mathlib.Topology.Algebra.ConstMulAction
interior_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G) (s : Set α), interior (c • s) = c • interior s
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.comp_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {x x_1 x_2 : CategoryTheory.Dial C} (F : x.Hom x_1) (G : x_1.Hom x_2),
  (CategoryTheory.CategoryStruct.comp F G).F =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id x_2.tgt)) G.F))
      F.F
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.le_val_assemble₄ : ∀ {w x y z : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c → 65535 < c.val
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.exi_rat_seq_conv_cauchy : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE), IsCauSeq (padicNorm p) (Padic.limSeq f)
-- Init.Data.List.Sublist
List.IsSuffix.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₂.length ≤ l₁.length → l₁ = l₂
-- Mathlib.Topology.Instances.Rat
Rat.continuous_coe_real : Continuous Rat.cast
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Subsemiring.isLocalRing_of_unit : ∀ {R : Type u_1} [inst : Semiring R] [IsLocalRing R] (S : Subsemiring R),
  (∀ (x : R) (hx : x ∈ S), IsUnit x → IsUnit ⟨x, hx⟩) → IsLocalRing ↥S
-- Mathlib.Algebra.Ring.Parity
Nat.not_odd_iff_even : ∀ {n : ℕ}, ¬Odd n ↔ Even n
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.instDecidableMem : {α : Type u} → {β : α → Type v} → [inst : Ord α] → {m : Std.DTreeMap.Internal.Impl α β} → {a : α} → Decidable (a ∈ m)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_def : ∀ {x : ℝ*}, x.InfinitePos ↔ ∀ (r : ℝ), ↑r < x
-- Mathlib.Analysis.Normed.Group.Uniform
dist_add_self_left : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a b : E), dist (b + a) a = ‖b‖
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.keep.injEq : ∀ (basis_hd : ℝ → ℝ) {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ex ex_1 : Tactic.ComputeAsymptotics.BasisExtension basis_tl),
  (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex =
      Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex_1) =
    (ex = ex_1)
-- Mathlib.Data.Finset.Sum
Finset.toLeft_cons_inl : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} (ha : Sum.inl a ∉ u),
  (Finset.cons (Sum.inl a) u ha).toLeft = Finset.cons a u.toLeft ⋯
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_repr_inr_of_mem : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)),
  ∀ v ∈ W, ∀ (j : n), ((bW.sumQuot bQ).repr v) (Sum.inr j) = 0
-- Mathlib.Analysis.CStarAlgebra.Classes
StarSubalgebra.cstarAlgebra : {S : Type u_1} →
  {A : Type u_2} →
    [inst : CStarAlgebra A] →
      [inst_1 : SetLike S A] →
        [SubringClass S A] →
          [SMulMemClass S ℂ A] → [StarMemClass S A] → (s : S) → [h_closed : IsClosed ↑s] → CStarAlgebra ↥s
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Associates.ufm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α], UniqueFactorizationMonoid (Associates α)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- For a multiply pretransitive action,
computes the index of the `fixingSubgroup` of a subset
of adequate cardinality.  -/
MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α] (s : Set α),
  MulAction.IsMultiplyPretransitive G α s.ncard →
    (fixingSubgroup G s).index = (Nat.card α).choose s.ncard * s.ncard.factorial
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initial.subsingleton_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {A : C}, Subsingleton (A ⟶ ⊥_ C)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.not_commutative : ∀ {n : ℕ}, n ≠ 1 → n ≠ 2 → ¬IsMulCommutative (DihedralGroup n)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instInhabited : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Inhabited (SpecialLinearGroup R V)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X k ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f k))
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f k))
        h)
-- Mathlib.Algebra.GCDMonoid.Nat
Int.associated_natAbs : ∀ (k : ℤ), Associated k ↑k.natAbs
-- Init.Data.UInt.Basic
instAndOpUInt16 : AndOp UInt16
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X} {C : ℝ},
  μ s < ⊤ → (∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C) → ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_tsum_le : ∀ {α : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] (f : ↥(lp (fun x => E) 1)), ‖∑' (i : α), ↑f i‖ ≤ ‖f‖
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.mk.injEq : ∀ {α : Type u_6} [inst : MeasurableSpace α] (toOuterMeasure : MeasureTheory.OuterMeasure α)
  (m_iUnion :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure (f i))
  (trim_le : toOuterMeasure.trim ≤ toOuterMeasure) (toOuterMeasure_1 : MeasureTheory.OuterMeasure α)
  (m_iUnion_1 :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → toOuterMeasure_1 (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure_1 (f i))
  (trim_le_1 : toOuterMeasure_1.trim ≤ toOuterMeasure_1),
  ({ toOuterMeasure := toOuterMeasure, m_iUnion := m_iUnion, trim_le := trim_le } =
      { toOuterMeasure := toOuterMeasure_1, m_iUnion := m_iUnion_1, trim_le := trim_le_1 }) =
    (toOuterMeasure = toOuterMeasure_1)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.eraseListₘ.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (hd : α) → (tl : List α) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.coe_symm_linearEquiv : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ⇑(WithLp.linearEquiv p K V).symm = WithLp.toLp p
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotToQuotSupₐ_toRingHom : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ↑(DoubleQuot.quotQuotToQuotSupₐ R I J) = DoubleQuot.quotQuotToQuotSup I J
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `assoc_comp_map` that only fires when `f₃ ≠ id`.  -/
CoassocSimps.assoc_comp_map_simproc : Lean.Meta.Simp.Simproc
-- Init.Data.AC
Lean.Data.AC.instInhabitedExpr.default : Lean.Data.AC.Expr
-- Mathlib.Topology.Sheaves.Sheafify
/-- The morphism from a presheaf to its sheafification,
sending each section to its germs.
(This forms the unit of the adjunction.)
 -/
TopCat.Presheaf.toSheafify : {X : TopCat} → (F : TopCat.Presheaf (Type v) X) → F ⟶ F.sheafify.obj
-- Mathlib.Data.ENNReal.Real
ENNReal.natCast_le_ofReal : ∀ {n : ℕ} {p : ℝ}, n ≠ 0 → (↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p)
-- Init.Data.Ord.Basic
/-- Uses decidable less-than and equality relations to find an `Ordering`.

In particular, if `x < y` then the result is `Ordering.lt`. If `x = y` then the result is
`Ordering.eq`. Otherwise, it is `Ordering.gt`.

`compareOfLessAndBEq` uses `BEq` instead of `DecidableEq`.
 -/
compareOfLessAndEq : {α : Type u_1} → (x y : α) → [inst : LT α] → [Decidable (x < y)] → [DecidableEq α] → Ordering
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- Conditional expectation commutes with affine functions. Note that `IsFiniteMeasure μ` is a
necessary assumption because we want constant functions to be integrable.  -/
ContinuousLinearMap.comp_condExp_add_const_comm : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {F : Type u_5}
  [inst_3 : NormedAddCommGroup F] [CompleteSpace F] [inst_5 : NormedSpace ℝ F] [MeasureTheory.IsFiniteMeasure μ],
  m ≤ m₀ →
    MeasureTheory.Integrable f μ →
      ∀ (T : E →L[ℝ] F) (a : F), (fun x => T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y => T (f y) + a | m]
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R`
factors in `S` as `∏ i, P i ^ e i`,
then `S ⧸ I` factors `R ⧸ I`-linearly as `Π i, R ⧸ (P i ^ e i)`.  -/
Ideal.Factors.piQuotientLinearEquiv : {R : Type u} →
  [inst : CommRing R] →
    (S : Type v) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [inst_3 : IsDedekindDomain S] →
            (p : Ideal R) →
              Ideal.map (algebraMap R S) p ≠ ⊥ →
                (S ⧸ Ideal.map (algebraMap R S) p) ≃ₗ[R ⧸ p]
                  (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset) →
                    S ⧸ ↑P ^ p.ramificationIdx' ↑P
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.dvd_mul : ∀ {p m n : ℕ}, Nat.Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.instIsSplitEpiApp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (f : F ⟶ G) [CategoryTheory.IsSplitEpi f] (X : C),
  CategoryTheory.IsSplitEpi (f.app X)
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.algebraMap_def : ∀ (A : Type u_2) [inst : Ring A] [inst_1 : UniformSpace A] [inst_2 : IsUniformAddGroup A] [inst_3 : IsTopologicalRing A]
  (R : Type u_3) [inst_4 : CommSemiring R] [inst_5 : Algebra R A] [inst_6 : UniformContinuousConstSMul R A] (r : R),
  (algebraMap R (UniformSpace.Completion A)) r = ↑((algebraMap R A) r)
-- Mathlib.Algebra.Quandle
Rack.EnvelGroup.inhabited : (R : Type u_1) → [inst : Rack R] → Inhabited (Rack.EnvelGroup R)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_add_subset : ∀ {α : Type u_2} [inst : Add α] (S : Set (Set α)) (t : Set α), ⋂₀ S + t ⊆ ⋂ s ∈ S, s + t
-- Std.Data.HashMap.Raw
/-- The notation `m[a]!` is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
 -/
Std.HashMap.Raw.get! : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [Inhabited β] → Std.HashMap.Raw α β → α → β
-- Mathlib.Data.DFinsupp.BigOperators
/-- The sum over two dfinsupps agree if the functions agree and are well-behaved within the
shared support.  -/
DFinsupp.sum_congr_of_eq_on_union : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {f1 f2 : Π₀ (i : ι), β i}
  {g1 g2 : (i : ι) → β i → γ},
  (∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)) →
    (∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 0) → (∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 0) → f1.sum g1 = f2.sum g2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α] {k : α}, t.contains k = true → t.getKey! k = k
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `add_apply`. -/
Seminorm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Computability.Primrec.List
Primrec.fin_curry₁ : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ},
  Primrec₂ f ↔ ∀ (i : Fin n), Primrec (f i)
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative groups is fully faithful.
 -/
CommGrpCat.uliftFunctorFullyFaithful : CommGrpCat.uliftFunctor.FullyFaithful
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The weight `k` slash action of `GL(2, ℝ)⁺` preserves holomorphic functions. This is private,
since it is a step towards the proof of `MDifferentiable.slash` which is more general.  -/
_private.Mathlib.NumberTheory.ModularForms.Basic.0.MDifferentiable.slash_of_pos : ∀ {f : UpperHalfPlane → ℂ},
  MDiff f → ∀ (k : ℤ) {g : GL (Fin 2) ℝ}, 0 < ↑(Matrix.GeneralLinearGroup.det g) → MDiff (SlashAction.map k g f)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) (γ : CochainComplex.HomComplex.Cochain K L n),
  (CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn') γ = γ.rightShift a n' hn'
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parsePortNumber : Std.Internal.Parsec.ByteArray.Parser UInt16
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_pos : ∀ {r : ℝ}, 0 < r.toNNReal ↔ 0 < r
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_orderIso : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), ⇑↑f = ⇑f
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.isClosed_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {U : Set Y}, IsClosed U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed (⇑f ⁻¹' U)
-- Mathlib.Data.Multiset.AddSub
Multiset.card_erase_add_one : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → (s.erase a).card + 1 = s.card
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.deriv_sin : deriv Complex.sin = Complex.cos
-- Mathlib.GroupTheory.Nilpotent
/-- The lower central series of `H : Subgroup G` computed in the ambient group `G` coincides with
the lower central series of `H` viewed as its own group, mapped back to `G`.  -/
Subgroup.top_subtype_lowerCentralSeries : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (n : ℕ),
  Subgroup.map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k fallback : α}, k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKeyD k fallback = fallback
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Ioi_comp_mul_right_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℝ → E) (c : ℝ) {a : ℝ},
  0 < a →
    (MeasureTheory.IntegrableOn (fun x => f (x * a)) (Set.Ioi c) MeasureTheory.volume ↔
      MeasureTheory.IntegrableOn f (Set.Ioi (c * a)) MeasureTheory.volume)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
/-- `K.truncLE'ToRestriction e` is a quasi-isomorphism in degrees that are not at the boundary.  -/
HomologicalComplex.truncLE'.quasiIsoAt_truncLE'ToRestriction : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (j : ι),
  ¬e.BoundaryLE j →
    ∀ [inst_4 : (K.restriction e).HasHomology j] [inst_5 : (K.truncLE' e).HasHomology j],
      QuasiIsoAt (K.truncLE'ToRestriction e) j
-- Mathlib.Data.PFunctor.Univariate.M
/-- `truncate a` turns `a` into a more limited approximation  -/
PFunctor.Approx.truncate : {F : PFunctor.{uA, uB}} → {n : ℕ} → PFunctor.Approx.CofixA F (n + 1) → PFunctor.Approx.CofixA F n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → ∀ {h' : k' ∈ Std.DTreeMap.ofList l cmp}, (Std.DTreeMap.ofList l cmp).getKey k' h' = k
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
/-- The complex power function with any exponent is not integrable on `(0, +∞)`.  -/
not_integrableOn_Ioi_cpow : ∀ (s : ℂ), ¬MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioi 0) MeasureTheory.volume
-- Std.Time.DateTime.Timestamp
Std.Time.instReprTimestamp_1 : Repr Std.Time.Timestamp
-- Mathlib.RingTheory.Int.Basic
Int.span_natAbs : ∀ (a : ℤ), Ideal.span {↑a.natAbs} = Ideal.span {a}
-- Lean.Environment
Lean.ConstantVal.instantiateTypeLevelParams : Lean.ConstantVal → List Lean.Level → Lean.Expr
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.toOver_map_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} S]
  (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
  (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) {X_1 Y : S} (g : X_1 ⟶ Y),
  ((F.toOver X f h).map g).left = F.map g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct an isomorphism between whiskered lifts.  -/
CategoryTheory.Bicategory.RightLift.whiskerIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {s t : CategoryTheory.Bicategory.RightLift f g} → (s ≅ t) → {x : B} → (h : x ⟶ c) → s.whisker h ≅ t.whisker h
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mem_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F}, x ∈ e.target ↔ x.1 ∈ e.baseSet
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.toFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : LocallyConstant X Y), f.toFun = ⇑f
-- Init.Data.List.Basic
List.reverse_nil : ∀ {α : Type u}, [].reverse = []