mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Dual
/-- **Fréchet-Riesz representation**: any `ℓ` in the dual of a Hilbert space `E` is of the form
`fun u => ⟪y, u⟫` for some `y : E`, i.e. `toDualMap` is surjective.
 -/
InnerProductSpace.toDual : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_prod_filter : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s : Set α) [inst_1 : DecidablePred fun x => x ∈ s]
  (hf : Function.HasFiniteMulSupport f), ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ Set.Finite.toFinset hf with i ∈ s, f i
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.monotone_apply : ∀ {n i : ℕ} (x : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := i })), Monotone fun j => x j
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.id_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι),
  (CategoryTheory.CategoryStruct.id C).f i = CategoryTheory.CategoryStruct.id (C.X i)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.alts.injEq : ∀ (args args_1 : List Lean.Parser.Tactic.MCasesPat),
  (Lean.Parser.Tactic.MCasesPat.alts args = Lean.Parser.Tactic.MCasesPat.alts args_1) = (args = args_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [LawfulBEq α] {m₁ m₂ : Std.DHashMap α fun x => Unit},
  (∀ (k : α), m₁.contains k = m₂.contains k) → m₁.Equiv m₂
-- Mathlib.Topology.Separation.Basic
/-- For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`.  -/
IsCompact.finite_compact_cover : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {s : Set X},
  IsCompact s →
    ∀ {ι : Type u_3} (t : Finset ι) (U : ι → Set X),
      (∀ i ∈ t, IsOpen (U i)) →
        s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.h₀_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  CategoryTheory.CategoryStruct.comp self.h₀ S₂.f = 0
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuousOn.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  LowerSemicontinuousOn f s → LowerSemicontinuousOn g s → LowerSemicontinuousOn (fun x => min (f x) (g x)) s
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
OrthonormalBasis.measurePreserving_repr : ∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : MeasurableSpace F] [inst_3 : BorelSpace F] [inst_4 : Fintype ι] [inst_5 : FiniteDimensional ℝ F]
  (b : OrthonormalBasis ι ℝ F), MeasureTheory.MeasurePreserving (⇑b.repr) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C)
  {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).hom.left =
    CategoryTheory.CategoryStruct.id (X.right ⟹ W)
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_prod : ∀ {M : Type u_1} [inst : Add M] {N : Type u_2} [inst_1 : Add N] {S : Set M} {T : Set N},
  S.Nonempty → T.Nonempty → (S ×ˢ T).addCentralizer = S.addCentralizer ×ˢ T.addCentralizer
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.corootSpan_ne_bot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S N] [Nonempty ι] [NeZero 2], P.corootSpan S ≠ ⊥
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_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 : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X i ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h)
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.instBEqRelevantArg.beq : Mathlib.Tactic.Translate.RelevantArg → Mathlib.Tactic.Translate.RelevantArg → Bool
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_smul : ∀ {S : Type u_2} {R : Type u} {M : Type v} [inst : SMul S R] [inst_1 : SMul S M] (s : S) (x : TrivSqZeroExt R M),
  (s • x).snd = s • x.snd
-- Mathlib.Order.Filter.Map
Filter.NeBot.comap_of_range_mem : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, f.NeBot → Set.range m ∈ f → (Filter.comap m f).NeBot
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.smul_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α),
  g • MulAction.orbit G a = MulAction.orbit G a
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.insertIdxIfInBounds.eq_1 : ∀ {α : Type u} (as : Array α) (i : ℕ) (a : α),
  as.insertIdxIfInBounds i a = if h : i ≤ as.size then as.insertIdx i a h else as
-- Mathlib.NumberTheory.Chebyshev
/-- Simple bound on the integral from monotonicity.
We will bound the integral on 2..x by splitting into two intervals and using this result on both.  -/
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.integral_1_div_log_sq_le : ∀ {a b : ℝ}, a ≤ b → 1 < a → ∫ (x : ℝ) in a..b, 1 / Real.log x ^ 2 ≤ (b - a) / Real.log a ^ 2
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Ioc_sdiff_Ioo_self`. -/
Finset.Ioc_diff_Ioo_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a < b → Finset.Ioc a b \ Finset.Ioo a b = {b}
-- Mathlib.Topology.Basic
Set.Finite.isOpen_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, s.Finite → (∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s)
-- Mathlib.Analysis.Fourier.Notation
/-- `𝓕⁻ f` is the inverse Fourier transform of `f`. The meaning of this notation is
type-dependent.  -/
FourierTransform.«term𝓕⁻» : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Family
/-- `lt_ciSup_iff'` whenever the input type is small in the output universe.  -/
Ordinal.lt_iSup_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι], a < ⨆ i, f i ↔ ∃ i, a < f i
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.mk : Lean.FVarIdSet → Lean.MVarIdSet → Array Lean.Expr → Lean.Elab.Term.ToDepElimPattern.TopSort.State
-- Mathlib.Computability.TuringMachine.Tape
/-- The head of a `ListBlank` is well defined.  -/
Turing.ListBlank.head : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.ListBlank Γ → Γ
-- Mathlib.Analysis.PSeries
ENNReal.tsum_condensed_le : ∀ {f : ℕ → ENNReal},
  (∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) → ∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_eq_iInf : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : Decidable s.Nontrivial],
  s.infsep = if s.Nontrivial then ⨅ d, Function.uncurry dist ↑d else 0
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.IsOrtho.polar_eq_zero : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {Q : QuadraticMap R M N} {x y : M},
  Q.IsOrtho x y → QuadraticMap.polar (⇑Q) x y = 0
-- Std.Internal.Parsec.ByteArray
/-- `Parser α` is a parser that consumes a `ByteArray` input using a `ByteArray.Iterator` and returns a result of type `α`.
 -/
Std.Internal.Parsec.ByteArray.Parser : Type → Type
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.loop.eq_1 : ∀ {α : Type u} (x : Array α), Array.shrink.loop✝ 0 x = x
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.instRootCompTriple : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} [κ : φ.CompTriple ψ χ], CompTriple ⇑φ ⇑ψ ⇑χ
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instAlgebra : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      {S : Type u_3} →
        [inst_1 : CommRing R] → (v : Valuation R Γ₀) → [inst_2 : Semiring S] → [Algebra R S] → Algebra (WithVal v) S
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R}
  {a : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ},
  a ∈ (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).units ↔ Valued.v ↑a = 1
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_zero : ∀ {M : Type u_1} {A : Type u_7} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
IsGLB.ciInf_set_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : β → α},
  IsGLB (f '' s) a → s.Nonempty → ⨅ i, f ↑i = a
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) [inst_4 : DecidableEq σ]
  [inst_5 : Fintype σ], ∃ v, ∑ i, v i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1
-- Init.Data.Vector.InsertIdx
Vector.getElem?_insertIdx : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i k : ℕ} (h : i ≤ n),
  (xs.insertIdx i x h)[k]? = if k < i then xs[k]? else if k = i then if k ≤ n then some x else none else xs[k - 1]?
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_dite_of_false : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p]
  (h : ∀ i ∈ s, ¬p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M),
  (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, g ↑i ⋯
-- Init.Data.UInt.Bitwise
UInt32.not_zero : ~~~0 = -1
-- Init.Data.Slice.Array.Lemmas
Array.array_toSubarray : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (xs.toSubarray lo hi).array = xs
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_rii : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_rii._auto_1)
  {t : Std.TreeMap α β cmp}, Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.allowedMethods? : Lean.Lsp.LogConfig → Option (Std.HashSet String)
-- Lean.Meta.PProdN
/-- Given a value `e` of type `t = t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return the values of type `tᵢ`  -/
Lean.Meta.PProdN.projs : ℕ → Lean.Expr → Lean.Expr → Array Lean.Expr
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.comp_right_iff : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₂ → P₃},
  Isometry f → (Congruent v₁ (f ∘ v₂) ↔ Congruent v₁ v₂)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects colimits of shape `Jᵒᵖ`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits of
shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsLimitsOfShape J F.op
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.ext : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  {f g : R →ₑ+*[φ] S}, (∀ (x : R), f x = g x) → f = g
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprBinderInfo_mathlib : Lean.ToExpr Lean.BinderInfo
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.dropEndWhile_string_eq_dropEndWhile_toSlice : ∀ {pat : String} {s : String.Slice}, s.dropEndWhile pat = s.dropEndWhile pat.toSlice
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The pairing of a finite (Borel) measure `μ` with a nonnegative bounded continuous
function is obtained by (Lebesgue) integrating the (test) function against the measure.
This is `MeasureTheory.FiniteMeasure.testAgainstNN`.  -/
MeasureTheory.FiniteMeasure.testAgainstNN : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] → MeasureTheory.FiniteMeasure Ω → BoundedContinuousFunction Ω NNReal → NNReal
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.toStarAlgHom_restrictScalars : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  [inst_11 : Star A] [inst_12 : Star B] (e : A ≃⋆ₐ[S] B),
  (StarAlgEquiv.restrictScalars R e).toStarAlgHom = StarAlgHom.restrictScalars R e.toStarAlgHom
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_eq_bot_iff_of_injective : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {I : Ideal R} {f : F}, Function.Injective ⇑f → (Ideal.map f I = ⊥ ↔ I = ⊥)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_one_le_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, 1 ≤ a → b < c → b < a * c
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Taking sub-families preserves equicontinuity at a point.  -/
EquicontinuousAt.comp : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {F : ι → X → α} {x₀ : X}, EquicontinuousAt F x₀ → ∀ (u : κ → ι), EquicontinuousAt (F ∘ u) x₀
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_elim : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {Q R : l} {φ : Prop},
  Lean.Order.PartialOrder.rel Q (Lean.Order.CompleteLattice.ofProp φ) →
    (φ → Lean.Order.PartialOrder.rel Q R) → Lean.Order.PartialOrder.rel Q R
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt16 = OfNat.ofNat n
-- Mathlib.Algebra.Group.Defs
ZSMul.toSMul : {M : Type u_2} → [ZSMul M] → SMul ℤ M
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.range_mapIncl_mono : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid P]
  [inst_2 : AddCommMonoid Q] [inst_3 : Module R P] [inst_4 : Module R Q] {p p' : Submodule R P} {q q' : Submodule R Q},
  p ≤ p' → q ≤ q' → (TensorProduct.mapIncl p q).range ≤ (TensorProduct.mapIncl p' q').range
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_g₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).g₂ = CategoryTheory.SmallObject.ρFunctorObj f πX
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.integrable_llr_tilted_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
        MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
          MeasureTheory.Integrable (MeasureTheory.llr μ (ν.tilted f)) μ
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {s : Finset ι} {G : ι → 𝕜 → E},
  (∀ σ ∈ s, Meromorphic (G σ)) → Meromorphic (∑ n ∈ s, G n)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k fallback : α},
  (Std.DTreeMap.filter (fun k x => f k) t).getKeyD k fallback = (Option.filter f (t.getKey? k)).getD fallback
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (m.insertMany l).getKeyD k' fallback = k
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for `OneHypercoverDenseData.essSurj.presheafObjObjIso`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          (X₀ : C₀) →
                            G₀.obj.obj (Opposite.op X₀) ⟶
                              (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀).obj
                                (Opposite.op (F.obj X₀))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_subset_div_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.ext : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] {f g : A ≃A[R] B}, ⇑f = ⇑g → f = g
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.shrink : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [inst_4 : Small.{w, v} M], Module.Free R (Shrink.{w, v} M)
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instNonUnitalSeminormedRing : {α : Type u_2} → [NonUnitalSeminormedRing α] → NonUnitalSeminormedRing αᵐᵒᵖ
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.HasDetOne.det_eq : ∀ {n : Type u_1} {inst : Fintype n} {inst_1 : DecidableEq n} {R : Type u_2} {inst_2 : CommRing R}
  {Γ : Subgroup (GL n R)} [self : Γ.HasDetOne] {g : GL n R}, g ∈ Γ → Matrix.GeneralLinearGroup.det g = 1
-- Lean.Meta.Hint
Lean.Meta.Hint.Suggestion.mk : Lean.Meta.Tactic.TryThis.Suggestion →
  Option Lean.Syntax → Option Lean.Syntax → Lean.Meta.Hint.DiffGranularity → Lean.Meta.Hint.Suggestion
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (c c' : C) (d : D)
  {Z : D'}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' (F.obj d)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom h) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
            (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c' d))
          h))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, k ∈ Std.TreeMap.filterMap f t → k ∈ t
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons'.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} (u v w : V) (h : G.Adj u v) (p p_1 : G.Walk v w),
  p = p_1 → SimpleGraph.Walk.cons' u v w h p = SimpleGraph.Walk.cons' u v w h p_1
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.mk_nnratCast : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (q : ℚ≥0), ⟨↑q, ⋯⟩ = ↑q
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.add_left_inj : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the largest element of the tree set, panicking if the set is empty.
 -/
Std.ExtTreeSet.max! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α), s.drop 0 = s