mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holderL.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (p q r : ENNReal) [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B B_1 : E →L[𝕜] F →L[𝕜] G),
  B = B_1 →
    ∀ [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)] [inst_9 : Fact (1 ≤ r)],
      ContinuousLinearMap.holderL μ p q r B = ContinuousLinearMap.holderL μ p q r B_1
-- Mathlib.Analysis.InnerProductSpace.Defs
Inner.mk : {𝕜 : Type u_4} → {E : Type u_5} → (E → E → 𝕜) → Inner 𝕜 E
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_sub_center_inv : ∀ (c : ℂ) {R : ℝ}, R ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ = 2 * ↑Real.pi * Complex.I
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.sigmaCurryEquiv` as a linear equivalence.

This is the `DFinsupp` version of `Finsupp.curryLinearEquiv`.  -/
DFinsupp.sigmaCurryLEquiv : {ι : Type u_1} →
  {R : Type u_3} →
    [inst : Semiring R] →
      [DecidableEq ι] →
        {α : ι → Type u_7} →
          {M : (i : ι) → α i → Type u_8} →
            [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (M i j)] →
              [inst_3 : (i : ι) → (j : α i) → Module R (M i j)] →
                (Π₀ (i : (x : ι) × α x), M i.fst i.snd) ≃ₗ[R] Π₀ (i : ι) (j : α i), M i j
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Auxiliary lemma for `condExp_bilin_of_stronglyMeasurable_left`.  -/
MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G)
  [CompleteSpace E],
  m ≤ mΩ →
    ∀ (f : MeasureTheory.SimpleFunc Ω F) {g : Ω → E},
      MeasureTheory.Integrable g μ → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)
-- Aesop.Tree.RunMetaM
Aesop.Goal.runMetaMInPostNormState : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadFinally m] →
        {α : Type} → [Lean.MonadError m] → (Lean.MVarId → m α) → Aesop.Goal → m (α × Lean.Meta.SavedState)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_or : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ} (h : i < w), (x ||| y)[i] = (x[i] || y[i])
-- Mathlib.Topology.Algebra.Group.OpenMapping
/-- Consider a sigma-compact additive group acting continuously and transitively on a
Baire space. Then the orbit map is open around zero. It follows in
`isOpenMap_vadd_of_sigmaCompact` that it is open around any point.  -/
vadd_singleton_mem_nhds_of_sigmaCompact : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup G]
  [IsTopologicalAddGroup G] [inst_4 : AddAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X]
  [ContinuousVAdd G X] [AddAction.IsPretransitive G X] {U : Set G}, U ∈ nhds 0 → ∀ (x : X), U +ᵥ {x} ∈ nhds x
-- Mathlib.Topology.MetricSpace.Bounded
/-- In a compact space, all sets are bounded  -/
Metric.isBounded_of_compactSpace : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] [CompactSpace α], Bornology.IsBounded s
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Status.noConfusionType : Sort v✝ → Mathlib.Explode.Status → Mathlib.Explode.Status → Sort v✝
-- Mathlib.Analysis.Complex.Circle
Circle.coe_inj : ∀ {x y : Circle}, ↑x = ↑y ↔ x = y
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.mk : ∀ {A : Type u} [inst : CommRing A] [inst_1 : IsDomain A] [toPreValuationRing : PreValuationRing A], ValuationRing A
-- Mathlib.Algebra.Azumaya.Defs
/-- An Azumaya algebra is a finitely generated, projective and faithful R-algebra where
`AlgHom.mulLeftRight R A : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A` is an isomorphism.  -/
IsAzumaya : (R : Type u_1) → (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α}, m.WF → (Array.find? (fun x => x.fst == k) m.toArray = none ↔ m.contains k = false)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- A manifold decomposes into interior and boundary.  -/
ModelWithCorners.interior_union_boundary_eq_univ : ∀ {𝕜 : 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],
  ModelWithCorners.interior M ∪ ModelWithCorners.boundary M = Set.univ
-- Std.Sync.StreamMap
/-- Check if the StreamMap is empty
 -/
Std.StreamMap.isEmpty : {α β : Type} → Std.StreamMap α β → Bool
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- One entry of one Matrix/Fin Bird recurrence step.  -/
BirdDet.Spec.stepEntry : {R : Type u_1} → [CommRing R] → {n : ℕ} → Matrix (Fin n) (Fin n) R → Matrix (Fin n) (Fin n) R → Matrix (Fin n) (Fin n) R
-- Mathlib.Order.Defs.Unbundled
IsStrictWeakOrder.toIsStrictOrder : ∀ {α : Sort u_1} {lt : α → α → Prop} [self : IsStrictWeakOrder α lt], IsStrictOrder α lt
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The unit of the multiplication is `single 1 1`,
i.e. the function that is `1` at `1` and `0` elsewhere.  -/
AddMonoidAlgebra.zero : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Zero M] → One (AddMonoidAlgebra R M)
-- Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Valued.exists_pow_lt_of_le_exp_neg_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Valued R (WithZero (Multiplicative ℤ))] {x : R},
  Valued.v x ≤ WithZero.exp (-1) → ∀ (γ : (WithZero (Multiplicative ℤ))ˣ), ∃ n, Valued.v x ^ n < ↑γ
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.head_desc_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B ⟶ X)
  (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) {Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.desc f fs w) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Data.List.InsertIdx
List.get_insertIdx_add_succ : ∀ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length)
  (hk : optParam (n + k + 1 < (l.insertIdx n x).length) ⋯), (l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
_private.Mathlib.NumberTheory.Zsqrtd.GaussianInt.0.«termℤ[i]» : Lean.ParserDescr
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_get_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k v : α} {w : k ∈ m}, m.get k w = v → k ∈ m
-- Mathlib.Data.Set.Finite.Basic
Set.not_injOn_infinite_finite_image : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α}, s.Infinite → (f '' s).Finite → ¬Set.InjOn f s
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
/-- A property of objects satisfies `P.IsClosedUnderCokernels` if whenever `X` and `Y`
satisfy `P`, all kernels of morphisms from `X` to `Y` satisfy `P`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderCokernels : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.zero_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (b : R), 0 * b = 0
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eq : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R n = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) - Polynomial.Chebyshev.T R (n - 2)
-- Lean.Elab.DeclNameGen
/-- Generate a name, while naming the top-level foralls using "Of".
The provided expression should be a winnowed expression.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameAux : Lean.Expr → Lean.Elab.Command.NameGen.MkNameM✝ String
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- The projection from the weak limit object to a value of the functor.  -/
CategoryTheory.Limits.weakLimit.π : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasWeakLimit F] → (j : J) → CategoryTheory.Limits.weakLimit F ⟶ F.obj j
-- Mathlib.Data.List.Defs
/-- Ternary version of `List.zipWith`.  -/
List.zipWith3 : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α → β → γ → δ) → List α → List β → List γ → List δ
-- Mathlib.RingTheory.Polynomial.Quotient
/-- If `P` is a prime ideal of `R`, then `R[x]/(P)` is an integral domain.  -/
Ideal.isDomain_map_C_quotient : ∀ {R : Type u_1} [inst : CommRing R] {P : Ideal R}, P.IsPrime → IsDomain (Polynomial R ⧸ Ideal.map Polynomial.C P)
-- Mathlib.ModelTheory.Definability
/-- A singleton `{a}` is definable over any set `A` that contains `a`.  -/
Set.Definable.singleton_of_mem : ∀ {M : Type w} (L : FirstOrder.Language) [inst : L.Structure M] {a : M} {A : Set M}, a ∈ A → A.Definable₁ L {a}
-- Mathlib.Control.Monad.Cont
instMonadContExceptT : {m : Type u → Type v} → [Monad m] → {ε : Type u} → [MonadCont m] → MonadCont (ExceptT ε m)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (X : CategoryTheory.Endofunctor.Coalgebra F),
  (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.inv.app X).f = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Helper function for typechecking.  -/
CategoryTheory.WithInitial.down : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y) → (X ⟶ Y)
-- Mathlib.Logic.Hydra
Relation.not_cutExpand_zero : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] (s : Multiset α), ¬Relation.CutExpand r s 0
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.map_units_smul : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {X Y : C} (r : Rˣ) (f : X ⟶ Y),
  F.map (r • f) = r • F.map f
-- Aesop.RuleTac.Basic
Aesop.SingleRuleTac.toRuleTac : Aesop.SingleRuleTac → Aesop.RuleTac
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_unique : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {ι : Type u_7} [inst_2 : Unique ι]
  (x : HahnSeries.SummableFamily Γ R ι), x.hsum = x default
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.forIn'.loop.match_3.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The counit of the adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet`  -/
LightCondSet.topCatAdjunctionCounit : (X : TopCat) → X.toLightCondSet.toTopCat ⟶ X
-- Mathlib.Data.NNReal.Defs
NNReal.coe_sub_def : ∀ {r p : NNReal}, ↑(r - p) = max (↑r - ↑p) 0
-- Mathlib.Data.Int.ModEq
Int.modulus_mul_add_modEq_iff : ∀ {n a b c : ℤ}, n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.Data.Sigma.Interval
Sigma.Iio_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)]
  (i : ι) (a : α i), Finset.Iio ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Iio a)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
/-- The absolute value defined via the non-unital continuous functional calculus.  -/
CFC.abs : {A : Type u_2} →
  [inst : NonUnitalRing A] →
    [inst_1 : StarRing A] →
      [inst_2 : TopologicalSpace A] →
        [inst_3 : Module ℝ A] →
          [inst_4 : SMulCommClass ℝ A A] →
            [inst_5 : IsScalarTower ℝ A A] →
              [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] →
                [inst_7 : PartialOrder A] → [StarOrderedRing A] → [NonnegSpectrumClass ℝ A] → A → A
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.comp : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M} {g : Module.End R M},
  p ∈ f.invtSubmodule → p ∈ g.invtSubmodule → p ∈ Module.End.invtSubmodule (f ∘ₗ g)
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRocSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRocSlice._auto_1) →
      Std.Roc.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RocSlice α β)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.mem_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] {m : E},
  m ∈ ZSpan.fundamentalDomain b ↔ ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- If the monoid equiv `f : α ≃* β` commutes with `normalize` then, for `a : α`, it yields a
bijection between the `normalizedFactors` of `a` and of `f a`.
 -/
UniqueFactorizationMonoid.normalizedFactorsEquiv : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [inst_1 : NormalizationMonoid α] →
      [inst_2 : UniqueFactorizationMonoid α] →
        {β : Type u_2} →
          [inst_3 : CommMonoidWithZero β] →
            [inst_4 : NormalizationMonoid β] →
              [inst_5 : UniqueFactorizationMonoid β] →
                {F : Type u_3} →
                  [inst_6 : EquivLike F α β] →
                    [MulEquivClass F α β] →
                      {f : F} →
                        (∀ (x : α), normalize (f x) = f (normalize x)) →
                          (a : α) →
                            { x // x ∈ UniqueFactorizationMonoid.normalizedFactors a } ≃
                              { y // y ∈ UniqueFactorizationMonoid.normalizedFactors (f a) }
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.x_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) =
    (hζ.toInteger - 1) ^ (3 * FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 2) *
      FermatLastTheoremForThreeGen.Solution.x✝ S
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- If `p ∤ a`, then `legendreSym p a` is `1` or `-1`.  -/
legendreSym.eq_one_or_neg_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ}, ↑a ≠ 0 → legendreSym p a = 1 ∨ legendreSym p a = -1
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_mul_leadingCoeff_self_inv : ∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K), (p * Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
-- Std.Http.Data.Chunk
/-- Gets the number of trailer headers.
 -/
Std.Http.Trailer.size : Std.Http.Trailer → ℕ
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- Dependent product of an `n`-ary functor. The sum can range over
data types like `ℕ` or over `Type.{u-1}`  -/
MvQPF.Pi : {n : ℕ} → {A : Type u} → (A → TypeVec.{u} n → Type u) → TypeVec.{u} n → Type u
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.comp_over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (S : C)
  [inst_1 : CategoryTheory.OverClass X S] [inst_2 : CategoryTheory.OverClass Y S] [CategoryTheory.HomIsOver f S],
  CategoryTheory.CategoryStruct.comp f (Y ↘ S) = X ↘ S
-- Init.Data.Array.Find
Array.idxOf_lt_size_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, Array.idxOf a xs < xs.size ↔ a ∈ xs
-- Mathlib.LinearAlgebra.Matrix.ZMatrix
Matrix.diag_pos_of_mul_diagonal_posDef : ∀ {ι : Type u_1} {R : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : CommRing R]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] [inst_5 : StarRing R] [TrivialStar R] (A : Matrix ι ι R) (d : ι → R),
  (Matrix.diagonal d * A).PosDef → (∀ (i : ι), 0 < d i) → ∀ (i : ι), 0 < A i i
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_mono_right : ∀ {G : Type uG} {x : G} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] {f g g' : G → ℝ},
  MeasureTheory.ConvolutionExistsAt f g x (ContinuousLinearMap.lsmul ℝ ℝ) μ →
    MeasureTheory.ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ) μ →
      (∀ (x : G), 0 ≤ f x) →
        (∀ (x : G), g x ≤ g' x) →
          MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x ≤
            MeasureTheory.convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) μ x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyι_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (L.homologyι i) =
    CategoryTheory.CategoryStruct.comp (K.homologyι i) (HomologicalComplex.opcyclesMap φ i)
-- Init.Data.List.Attach
List.filterMap_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : List (Subtype P)} {f : α → Option β},
  List.filterMap f xs.unattach =
    List.filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.disjoint_def : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M}, Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = 0
-- Init.Data.SInt.Basic
/-- Constructs an `Int32` from an `Int` that is known to be in bounds.  -/
Int32.ofIntLE : (i : ℤ) → Int32.minValue.toInt ≤ i → i ≤ Int32.maxValue.toInt → Int32
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.hom_ext : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (f g : F ⟶ G),
  f.hom = g.hom → f = g
-- Mathlib.Topology.Covering.Basic
/-- **Alias** of `IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn`.

---

If `f : E → X` is a closed map between topological spaces with `E` Hausdorff, and `s` is
a subset of `X` on which `f` has finite fibers, such that `f` restricts to a homeomorphism on
a neighborhood of every point of `f ⁻¹' s`, then `f` is a covering map on `s`.  -/
IsClosedMap.isCoveringMapOn_of_openPartialHomeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  [T2Space E], IsClosedMap f → (∀ x ∈ s, (f ⁻¹' {x}).Finite) → IsLocalHomeomorphOn f (f ⁻¹' s) → IsCoveringMapOn f s
-- Mathlib.Order.KrullDimension
Order.bot_lt_krullDim : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], ⊥ < Order.krullDim α
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_id : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.map (AddMonoidHom.id M) S = S
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourier_neg : ∀ {d : Type u_1} [inst : Fintype d] {n : d → ℤ} {x : UnitAddTorus d},
  (UnitAddTorus.mFourier (-n)) x = (starRingEnd ℂ) ((UnitAddTorus.mFourier n) x)
-- Init.Data.SInt.Lemmas
Int64.le_rfl : ∀ {a : Int64}, a ≤ a
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- A coalgebra morphism with an underlying isomorphism hom in `C` is a coalgebra isomorphism.  -/
CategoryTheory.Endofunctor.Coalgebra.iso_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (f : V₀ ⟶ V₁) [CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filter!_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).Equiv t ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), f (t.getKey a h) = true)
-- Mathlib.Order.Bounds.Defs
upperBounds.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), upperBounds s = {x | ∀ ⦃a : α⦄, a ∈ s → a ≤ x}
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.Barrier.cvar : Std.Barrier → Std.Condvar
-- Lean.Elab.Tactic.RCases
/-- This function is used for producing rcases patterns based on a case tree. Here we are given
the list of patterns to apply to each argument of each constructor after the main case, and must
produce a list of alternatives with the same effect. This function calls `tuple₁` to make the
individual alternatives, and handles merging `[a, b, c | d]` to `a | b | c | d` instead of
`a | b | (c | d)`.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.alts₁Core : List (List Lean.Elab.Tactic.RCases.RCasesPatt) → List Lean.Elab.Tactic.RCases.RCasesPatt
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instCode : List Lean.Name →
  List Lean.Level →
    Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure → Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Constructs a `ContinuousHom` from a function `f` and a proof of `ωScottContinuous f`.
By default, the proof is inferred by `fun_prop`, which makes it ideal for simple cases.
 -/
OmegaCompletePartialOrder.ContinuousHom.ofFun : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] →
        (f : α → β) →
          autoParam (OmegaCompletePartialOrder.ωScottContinuous f)
              OmegaCompletePartialOrder.ContinuousHom.ofFun._auto_1 →
            α →𝒄 β
-- Mathlib.Order.Antisymmetrization
/-- See if the term is `AntisymmRel r a b` and the goal is `r a b`.  -/
Mathlib.Tactic.GCongr.exactAntisymmRelLeft : Mathlib.Tactic.GCongr.ForwardExt
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabMutualDef.go : Array Lean.Expr → Lean.Elab.Command.Scope → Array Lean.Elab.DefView → Lean.Elab.TermElabM Unit
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
IsOpen.uniqueMDiffOn : ∀ {𝕜 : 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] {s : Set M}, IsOpen s → UniqueMDiff[s]