mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
/-- If we fix a background affine basis `b`, then for any other basis `b₂`, we can characterise
the barycentric coordinates provided by `b₂` in terms of determinants relative to `b`.  -/
AffineBasis.det_smul_coords_eq_cramer_coords : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : CommRing k] [inst_3 : Module k V] [inst_4 : DecidableEq ι] [inst_5 : Fintype ι] (b b₂ : AffineBasis ι k P)
  (x : P), (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂).transpose.cramer (b.coords x)
-- Mathlib.RepresentationTheory.Equiv
Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single : ∀ {G : Type v} [inst : Monoid G] {k : Type u} [inst_1 : CommSemiring k] {α : Type w'} (i : α) (g : G) (r : k),
  ((Representation.leftRegularTensorTrivialIsoFree α).symm fun₀ | i => MonoidAlgebra.single g r) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single i r
-- Mathlib.Algebra.Group.Hom.Instances
/-- The expression `fun m n ↦ g (f m n)` as an `AddMonoidHom`.

This also exists as a `LinearMap` version, `LinearMap.compr₂`  -/
AddMonoidHom.compr₂ : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      {Q : Type uQ} →
        [inst : AddZeroClass M] →
          [inst_1 : AddZeroClass N] →
            [inst_2 : AddCommMonoid P] → [inst_3 : AddCommMonoid Q] → (M →+ N →+ P) → (P →+ Q) → M →+ N →+ Q
-- Aesop.RuleTac.Forward.Basic
Aesop.isForwardImplDetailHyp : Lean.LocalDecl → Bool
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the inclusion of the (right) homology in the chosen cokernel of `S.f`  -/
CategoryTheory.ShortComplex.RightHomologyData.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (self : S.RightHomologyData) → self.H ⟶ self.Q
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 → (W.Equation P ↔ W.toAffine.Equation (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3))
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryFin0_apply : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G'),
  (continuousMultilinearCurryFin0 𝕜 G G') f = f 0
-- Mathlib.Data.Set.Image
Set.mem_compl_image : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (t : α) (s : Set α), t ∈ compl '' s ↔ tᶜ ∈ s
-- Mathlib.Analysis.Matrix.Spectrum
/-- **Diagonalization theorem**, **spectral theorem** for matrices; A Hermitian matrix can be
diagonalized by a change of basis. For the spectral theorem on linear maps, see
`LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply`.  -/
Matrix.IsHermitian.spectral_theorem : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian),
  A =
    ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues))
-- Mathlib.Data.ENNReal.Basic
ENNReal.exists_ne_top : ∀ {p : ENNReal → Prop}, (∃ x, x ≠ ⊤ ∧ p x) ↔ ∃ x, p ↑x
-- Mathlib.Data.ZMod.Basic
ZMod.val_unit' : ∀ {n : ZMod 0}, IsUnit n ↔ n.val = 1
-- Mathlib.Analysis.Complex.Poisson
/-- The Herglotz–Riesz kernel integral of a circle-integrable function is analytic in the pole
parameter, throughout the open ball.
 -/
analyticOnNhd_circleAverage_herglotzRieszKernel_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} [CompleteSpace E],
  CircleIntegrable f 0 R →
    AnalyticOnNhd ℂ (fun w => Real.circleAverage (fun ζ => herglotzRieszKernel 0 w ζ • f ζ) 0 R) (Metric.ball 0 R)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.method.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.method = 1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.sub_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂), (f - g).hom₂ = f.hom₂ - g.hom₂
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.descOfTruncation_comp : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C] {X' : SSet.Truncated 2} (ψ : X ⟶ X')
  (φ : X' ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C)),
  SSet.Truncated.HomotopyCategory.descOfTruncation (CategoryTheory.CategoryStruct.comp ψ φ) =
    (SSet.Truncated.mapHomotopyCategory ψ).comp (SSet.Truncated.HomotopyCategory.descOfTruncation φ)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.eq_2 : ∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C CategoryTheory.FreeMonoidalCategory.unit x =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
-- Mathlib.Order.Fin.InsertNth
Fin.strictMono_insertNth_zero : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  StrictMono f → ∀ x < f 0, StrictMono (Fin.insertNth 0 x f)
-- Mathlib.Order.Ideal
/-- Every proper ideal is contained in some maximal ideal.  -/
Order.Ideal.IsProper.exists_le_maximal : ∀ {P : Type u_1} [inst : LE P] [OrderTop P] {I : Order.Ideal P}, I.IsProper → ∃ J, I ≤ J ∧ J.IsMaximal
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.decidableZero : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] →
      [(i : ι) → (x : β i) → Decidable (x = 0)] → (f : Π₀ (i : ι), β i) → Decidable (f = 0)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.lift_leftSMul_eq_lift_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] (Z : C) (x y : Z ⟶ X) (m : Z ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x)
        (CategoryTheory.ModObj.leftSMul M X) =
      CategoryTheory.CartesianMonoidalCategory.lift y x ↔
    m • x = y
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Continuous linear maps form a normed ring with respect to the operator norm.  -/
ContinuousLinearMap.toNormedRing : {𝕜 : Type u_1} →
  {E : Type u_5} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NontriviallyNormedField 𝕜] → [inst_2 : NormedSpace 𝕜 E] → NormedRing (E →L[𝕜] E)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.succ.match_1.splitter : (motive : PosNum → Sort u_1) →
  (x : PosNum) → (Unit → motive PosNum.one) → ((n : PosNum) → motive n.bit1) → ((n : PosNum) → motive n.bit0) → motive x
-- Init.Prelude
Lean.instInhabitedParserDescr : Inhabited Lean.ParserDescr
-- Init.Data.Order.FactoriesExtra
/-- Creates a `DecidableLT α` instance using a well-behaved `Ord α` instance.
 -/
DecidableLT.ofOrd : (α : Type u) →
  [inst : LE α] → [inst_1 : LT α] → [inst_2 : Ord α] → [Std.LawfulOrderOrd α] → [Std.LawfulOrderLT α] → DecidableLT α
-- Mathlib.Algebra.Lie.Ideal
/-- An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself.  -/
LieIdeal : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type v
-- Mathlib.CategoryTheory.Yoneda
/-- Version of the Yoneda lemma where the presheaf is fixed but the argument varies.  -/
CategoryTheory.yonedaOpCompYonedaObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) →
      CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj P) ≅ P.comp CategoryTheory.uliftFunctor.{u₁, v₁}
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The number of solutions to `x^2 = a` is determined by the quadratic character.  -/
quadraticChar_card_sqrts : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∀ (a : F), ↑{x | x ^ 2 = a}.toFinset.card = (quadraticChar F) a + 1
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.top_toSubmonoid : ∀ {G : Type u_1} [inst : Group G], ⊤.toSubmonoid = ⊤
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
/-- `(∫ ‖f a‖^q ∂μ) ^ (1/q)`, which is a seminorm on the space of measurable functions for which
this quantity is finite.

Note: this is a purely auxiliary quantity; lemmas about `eLpNorm'` should only be used to
prove results about `eLpNorm`; every `eLpNorm'` lemma should have a `eLpNorm` version.  -/
MeasureTheory.eLpNorm' : {α : Type u_1} → {ε : Type u_2} → [ENorm ε] → {x : MeasurableSpace α} → (α → ε) → ℝ → MeasureTheory.Measure α → ENNReal
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {k : α} {v : β}, (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
-- Mathlib.RingTheory.Coalgebra.GroupLike
IsGroupLikeElem.mk : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A},
  CoalgebraStruct.counit a = 1 → CoalgebraStruct.comul a = a ⊗ₜ[R] a → IsGroupLikeElem R a
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_dite_neg_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} (p : β → Prop)
  [inst_2 : DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β},
  b ∈ s → ∀ (h₁ : ¬p b), (s.inf fun i => if h : p i then f i h else g i h) ≤ g b h₁
-- Mathlib.Topology.GDelta.Basic
/-- The union of finitely many Gδ sets is a Gδ set, bounded indexed union version.  -/
IsGδ.iUnion : ∀ {X : Type u_1} {ι' : Sort u_4} [inst : TopologicalSpace X] [Finite ι'] {f : ι' → Set X},
  (∀ (i : ι'), IsGδ (f i)) → IsGδ (⋃ i, f i)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copy_E : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E)
  (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I),
  (M.copy E IsBase Indep hE hB hI).E = E
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- Turn a Legendre symbol into a Jacobi symbol.  -/
Mathlib.Meta.NormNum.LegendreSym.to_jacobiSym : ∀ (p : ℕ) (pp : Fact (Nat.Prime p)) (a r : ℤ),
  Mathlib.Meta.NormNum.IsInt (jacobiSym a p) r → Mathlib.Meta.NormNum.IsInt (legendreSym p a) r
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_ofReal_re : ∀ (x : ℝ), (Complex.sinh ↑x).re = Real.sinh x
-- Lean.Elab.DocString
/-- Environment extension for docstring roles  -/
Lean.Doc.docRoleExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap (Array Lean.Name))
-- Init.Data.UInt.Lemmas
UInt8.neg_sub : ∀ {a b : UInt8}, -(a - b) = b - a
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.IsEmbedding.inl : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Zero M],
  Topology.IsEmbedding TrivSqZeroExt.inl
-- Mathlib.RingTheory.AdicCompletion.Topology
RingFilterBasis.mk.congr_simp : ∀ {R : Type u} [inst : Ring R] [toAddGroupFilterBasis : AddGroupFilterBasis R]
  [toAddGroupFilterBasis_1 : AddGroupFilterBasis R]
  (e_toAddGroupFilterBasis : toAddGroupFilterBasis = toAddGroupFilterBasis_1)
  (mul' : ∀ {U : Set R}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V * V ⊆ U)
  (mul_left' :
    ∀ (x₀ : R) {U : Set R},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ * x) ⁻¹' U)
  (mul_right' :
    ∀ (x₀ : R) {U : Set R},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x * x₀) ⁻¹' U),
  { toAddGroupFilterBasis := toAddGroupFilterBasis, mul' := mul', mul_left' := mul_left', mul_right' := mul_right' } =
    { toAddGroupFilterBasis := toAddGroupFilterBasis_1, mul' := ⋯, mul_left' := ⋯, mul_right' := ⋯ }
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C''),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT'') f =
        (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f + (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {f : α → E} {g : α → F}
  {p q r : ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (b : E → F → G) (c : NNReal),
        (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
          0 < r →
            r < p →
              1 / r = 1 / p + 1 / q →
                MeasureTheory.eLpNorm' (fun x => b (f x) (g x)) r μ ≤
                  ↑c * MeasureTheory.eLpNorm' f p μ * MeasureTheory.eLpNorm' g q μ
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- The equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of `Additive`  -/
MonoidAlgebra.toAdditive : (R : Type u_3) →
  (M : Type u_6) → [inst : Semiring R] → [inst_1 : Mul M] → MonoidAlgebra R M ≃+* AddMonoidAlgebra R (Additive M)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.sndHom_comp_map : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N),
  TrivSqZeroExt.sndHom R' N ∘ₗ (TrivSqZeroExt.map f).toLinearMap = f ∘ₗ TrivSqZeroExt.sndHom R' M
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_toEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), ⇑h.toEquiv = ⇑h
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.Quotient.addGroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal],
  QuotientAddGroup.Quotient.addGroup N =
    { add := Quotient.map₂ (fun x1 x2 => x1 + x2) ⋯, add_assoc := ⋯, zero := Quotient.mk'' 0, zero_add := ⋯,
      add_zero := ⋯, nsmul := QuotientAddGroup.Quotient.addGroup._aux_4 N, nsmul_zero := ⋯, nsmul_succ := ⋯,
      neg := Quotient.map' Neg.neg ⋯, sub := Quotient.map₂ (fun x1 x2 => x1 - x2) ⋯,
      zsmul := QuotientAddGroup.Quotient.addGroup._aux_8 N, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯,
      zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
instAddCommMonoidSymmetricPower : (R ι : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_2) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → AddCommMonoid (SymmetricPower R ι M)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.coe_ereal_ennreal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => ↑(f x)) μ
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimit_iff_of_orderTop : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : OrderTop α],
  Order.IsPredLimit a ↔ a ≠ ⊤ ∧ Order.IsPredPrelimit a
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The "unlifted" version of negation in the colimit.  -/
AddGrpCat.FilteredColimits.colimitNegAux : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) → (j : J) × ↑(F.obj j) → ↑(AddGrpCat.FilteredColimits.G F)
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.mkSubProof.eq_def : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) (iM : Q(AddCommGroup «$M»))
  (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : Mathlib.Tactic.Module.qNF R M),
  Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM l₁ l₂ =
    match l₁, l₂ with
    | [], l =>
      have a := l.toNF;
      q(⋯)
    | l, [] =>
      have a := l.toNF;
      q(⋯)
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ < k₂ then
        have pf := Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM t₁ (((a₂, x₂), k₂) ::ᵣ t₂);
        q(⋯)
      else
        if k₁ = k₂ then
          have pf := Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM t₁ t₂;
          q(⋯)
        else
          have pf := Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM (((a₁, x₁), k₁) ::ᵣ t₁) t₂;
          q(⋯)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.comp_pow : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp h (f ^ n) = CategoryTheory.CategoryStruct.comp h f ^ n
-- Mathlib.Analysis.Complex.Periodic
/-- Parameter for q-expansions, `qParam h z = exp (2 * π * I * z / h)`  -/
Function.Periodic.qParam : ℝ → ℂ → ℂ
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_mul : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 ≤ ArchimedeanClass.mk x →
    0 ≤ ArchimedeanClass.mk y →
      ArchimedeanClass.stdPart (x * y) = ArchimedeanClass.stdPart x * ArchimedeanClass.stdPart y
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_ric_eq_self : ∀ {n i fallback : ℕ}, i ≤ n → (*...=n).toList.getD i fallback = i
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Matrix.map.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : Matrix m n α) (f : α → β),
  M.map f = Matrix.of fun i j => f (M i j)
-- Mathlib.Order.Filter.Lift
Filter.mem_lift : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β} {s : Set β} {t : Set α},
  t ∈ f → s ∈ g t → s ∈ f.lift g
-- Mathlib.Topology.Homeomorph.Defs
/-- Change the homeomorphism `f` to make the inverse function definitionally equal to `g`.  -/
Homeomorph.changeInv : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (f : X ≃ₜ Y) → (g : Y → X) → Function.RightInverse g ⇑f → X ≃ₜ Y
-- Mathlib.Order.RelIso.Basic
RelIso.relIsoCongr_apply_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ≃r s₁) (a : α₂),
  ((e₁.relIsoCongr e₂) f₁) a = e₂ (f₁ (e₁.symm a))
-- Mathlib.Analysis.Normed.Operator.Prod
Continuous.prod_mapL : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {M₄ : Type u_8}
  [inst_1 : SeminormedAddCommGroup M₁] [inst_2 : NormedSpace 𝕜 M₁] [inst_3 : SeminormedAddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜 M₂] [inst_5 : SeminormedAddCommGroup M₃] [inst_6 : NormedSpace 𝕜 M₃]
  [inst_7 : SeminormedAddCommGroup M₄] [inst_8 : NormedSpace 𝕜 M₄] {X : Type u_9} [inst_9 : TopologicalSpace X]
  {f : X → M₁ →L[𝕜] M₂} {g : X → M₃ →L[𝕜] M₄}, Continuous f → Continuous g → Continuous fun x => (f x).prodMap (g x)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.map_measureReal_apply : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
  {f : α → β}, Measurable f → ∀ {s : Set β}, MeasurableSet s → (MeasureTheory.Measure.map f μ).real s = μ.real (f ⁻¹' s)
-- Lean.Meta.Reduce
Lean.Meta.reduce : Lean.Expr → optParam Bool true → optParam Bool true → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).inv.app X_1).left.right =
    CategoryTheory.CategoryStruct.id X_1.left.right
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.cones_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : Cᵒᵖ} (f : X ⟶ Y),
  F.cones.map f =
    TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.unop) g
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- The stabilizer of a set acts on that set  -/
instMulActionSubtypeMemSubgroupStabilizerSetElem : (G : Type u_1) →
  [inst : Group G] → (α : Type u_2) → [inst_1 : MulAction G α] → (s : Set α) → MulAction ↥(MulAction.stabilizer G s) ↑s
-- Init.Control.Lawful.Instances
StateT.run_modifyGet : ∀ {m : Type u_1 → Type u_2} {σ α : Type u_1} [inst : Monad m] (f : σ → α × σ) (s : σ),
  (modifyGet f).run s = pure ((f s).1, (f s).2)
-- Init.Data.Fin.Lemmas
Fin.val_add_one : ∀ {n : ℕ} (i : Fin (n + 1)), ↑(i + 1) = if i = Fin.last n then 0 else ↑i + 1
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherianSpace_iff_of_homeomorph : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  TopologicalSpace.NoetherianSpace α ↔ TopologicalSpace.NoetherianSpace β