mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_enorm : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  {f : α → ε}, MeasureTheory.eLpNorm' (fun a => ‖f a‖ₑ) q μ = MeasureTheory.eLpNorm' f q μ
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled additive semigroup homomorphism `M₁ →ₙ+ M₂` from a function `f`
and a proof that it belongs to the closure of the range of the coercion from `M₁ →ₙ+ M₂` (or another
type of bundled homomorphisms that has an `AddHomClass` instance) to `M₁ → M₂`.  -/
addHomOfMemClosureRangeCoe : {M₁ : Type u_6} →
  {M₂ : Type u_7} →
    [inst : TopologicalSpace M₂] →
      [T2Space M₂] →
        [inst_2 : Add M₁] →
          [inst_3 : Add M₂] →
            [ContinuousAdd M₂] →
              {F : Type u_8} →
                [inst_5 : FunLike F M₁ M₂] →
                  [AddHomClass F M₁ M₂] → (f : M₁ → M₂) → f ∈ closure (Set.range fun f x => f x) → M₁ →ₙ+ M₂
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_alterKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey a (Std.Internal.List.alterKey a f l) =
      (f (Std.Internal.List.getValueCast? a l)).isSome
-- Mathlib.Analysis.Normed.Group.Hom
/-- If a normed space is non-trivial, then the norm of the identity equals `1`.  -/
NormedAddGroupHom.norm_id : ∀ (V : Type u_1) [inst : SeminormedAddCommGroup V] [NontrivialTopology V], ‖NormedAddGroupHom.id V‖ = 1
-- Std.Time.Date.Unit.Weekday
/-- `Ordinal` represents a bounded value for weekdays, which ranges between 1 and 7.
 -/
Std.Time.Weekday.Ordinal : Type
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom._auto_3) {Z : C}
  (h : X.opcycles f₂ f₃ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles
      (CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom h) =
    CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) h
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given a regular cardinal `κ` and `x : X`, this is the singleton `{x}`,
considered as a subset of `X` of cardinality `< κ`.  -/
CategoryTheory.CardinalDirectedPoset.SetCardinalLT.singleton : (κ : Cardinal.{u}) → [Fact κ.IsRegular] → {X : Type u} → X → CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ X
-- Mathlib.Tactic.Simps.Basic
/-- Linter to check that no unused custom declarations are declared for simps.  -/
Lean.Parser.linter.simpsUnusedCustomDeclarations : Lean.Option Bool
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
Coe.coe : {α : semiOutParam (Sort u)} → {β : Sort v} → [self : Coe α β] → α → β
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_transpose : ∀ {μ : YoungDiagram} {c : ℕ × ℕ}, c ∈ μ.transpose ↔ c.swap ∈ μ
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.natAbs_valMinAbs_add_le : ∀ {n : ℕ} (a b : ZMod n), (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.rightUnitor_inv_apply : ∀ {X : TopCat} {x : ↑X},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) x = (x, PUnit.unit)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_idem : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] (A : Matrix m n α) (i : m) (x y : n → α),
  (A.updateRow i x).updateRow i y = A.updateRow i y
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Sleep.ofNative.inj : ∀ {native native_1 : Std.Internal.UV.Timer}, { native := native } = { native := native_1 } → native = native_1
-- Mathlib.Tactic.Widget.Conv
/-- Traverses into the body of a forall, let, or lambda.
Corresponds to the `conv` tactics `intro` or `ext`.
 -/
Mathlib.Tactic.Conv.Path.body : Lean.Name → Mathlib.Tactic.Conv.Path → Mathlib.Tactic.Conv.Path
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_lt_omega : ∀ {o₁ o₂ : Ordinal.{u_1}}, Ordinal.omega o₁ < Ordinal.omega o₂ ↔ o₁ < o₂
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_eq_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ {f : MvPolynomial σ R}, (MvPolynomial.expand p) f = 0 ↔ f = 0
-- Mathlib.Data.Finset.Insert
Finset.instNontrivial : ∀ {α : Type u_1} [Nonempty α], Nontrivial (Finset α)
-- Std.Data.DTreeMap.Internal.Balancing
/-- Slower version of `balanceL` with weaker balancing assumptions that hold after erasing from
the right side of the tree.
 -/
Std.DTreeMap.Internal.Impl.balanceLErase : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_finsetSum_index : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : CommMonoid N]
  {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N},
  (∀ (a : α), h a 0 = 1) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) → ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
-- Mathlib.Analysis.LConvolution
/-- The definition of multiplicative convolution of functions.  -/
MeasureTheory.mlconvolution_def : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Mul G] [inst_1 : Inv G] {f g : G → ENNReal}
  {μ : MeasureTheory.Measure G} {x : G}, MeasureTheory.mlconvolution f g μ x = ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- If `t` is a colimit pushout cocone over `f` and `g` and `h : Y ⟶ W` and `k : Z ⟶ W` are
morphisms satisfying `f ≫ h = g ≫ k`, then we have a factorization `l : t.pt ⟶ W` such that
`inl t ≫ l = h` and `inr t ≫ l = k`.  -/
CategoryTheory.Limits.PushoutCocone.IsColimit.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {t : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit t →
              {W : C} →
                (h : Y ⟶ W) →
                  (k : Z ⟶ W) →
                    CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k →
                      { l //
                        CategoryTheory.CategoryStruct.comp t.inl l = h ∧
                          CategoryTheory.CategoryStruct.comp t.inr l = k }
-- Mathlib.CategoryTheory.Skeletal
/-- The isomorphism between `⟦X⟧.out` and `X`.  -/
CategoryTheory.fromSkeletonToSkeletonIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) → (CategoryTheory.fromSkeleton C).obj (CategoryTheory.toSkeleton X) ≅ X
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapObj_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {p : I₁ × I₂ × I₃ → J} {X₁ : CategoryTheory.GradedObject I₁ C₁}
  {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y : C₄} {j : J}
  [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  {φ φ' : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y},
  φ = φ' ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
          φ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
          φ'
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.rfind'.injEq : ∀ (a a_1 : Nat.Partrec.Code), (a.rfind' = a_1.rfind') = (a = a_1)
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- The identity `WithGeneratedByTopology.equiv.symm : Y → WithGeneratedByTopology X Y`
as a `X`-continuous map.  -/
Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBy : {ι : Type t} →
  (X : ι → Type u) →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (Y : Type v) →
        [inst_1 : TopologicalSpace Y] → Topology.ContinuousMapGeneratedBy X Y (Topology.WithGeneratedByTopology X Y)
-- Mathlib.Logic.Relation
Relation.comp_eq_fun : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} (f : γ → β),
  (Relation.Comp r fun x1 x2 => x1 = f x2) = fun x1 x2 => r x1 (f x2)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) → P.IsStableUnderBaseChange
-- Mathlib.Analysis.SpecialFunctions.Log.Base
_private.Mathlib.Analysis.SpecialFunctions.Log.Base.0.Real.b_pos : ∀ {b : ℝ}, 1 < b → 0 < b
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The equivalence between functions on the generators and additive group homomorphisms from an
additive free group given by those generators.  -/
IsFreeAddGroup.lift : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : IsFreeAddGroup G] → {H : Type u_2} → [inst_2 : AddGroup H] → (IsFreeAddGroup.Generators G → H) ≃ (G →+ H)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n},
  φ.IsQF →
    P ⊥ →
      (∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) →
        (∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) →
          (∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) →
            (∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ
-- Mathlib.Combinatorics.Hindman
Hindman.FS.below.head' : ∀ {M : Type u_1} [inst : AddSemigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FS a a_1 → Prop}
  (a : Stream' M), Hindman.FS.below ⋯
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.isZero_extend_X : ∀ {ι : 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.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero ((K.extend e).X i')
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.antitone_chain_condition_of_isArtinianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.IsArtinianObject X]
  (f : ℕ →o (CategoryTheory.Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instInhabitedConfig : Inhabited Mathlib.Tactic.RingNF.Config
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState.mk.sizeOf_spec : ∀ (seen : Lean.ExprSet) (consts : Lean.NameSet),
  sizeOf { seen := seen, consts := consts } = 1 + sizeOf seen + sizeOf consts
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_atBot_atBot : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Ico Filter.atBot Filter.atBot
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `X`-coordinate of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Projective.dblX : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → R
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.instIsRightAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A], (CategoryTheory.ihom A).IsRightAdjoint
-- Lean.Syntax
/-- A position range inside a string. This type is mostly used in combination with syntax trees,
as there might not be a single underlying string in this case that could be used for a `Substring`.
 -/
Lean.Syntax.Range : Type
-- Mathlib.Order.SuccPred.Limit
/-- A value can be built by building it on successors and successor pre-limits.  -/
Order.isSuccPrelimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : SuccOrder α] →
          ((a : α) → ¬IsMax a → motive (Order.succ a)) → ((a : α) → Order.IsSuccPrelimit a → motive a) → motive b
-- Mathlib.Topology.UniformSpace.Cauchy
/-- **Alias** of `Filter.TotallyBounded.isCompact_setOfPred_clusterPt`. -/
Filter.TotallyBounded.isCompact_setOf_clusterPt : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α},
  f.TotallyBounded → IsCompact {x | ClusterPt x f}
-- Lean.Meta.Closure
Lean.Meta.Closure.instInhabitedToProcessElement.default : Lean.Meta.Closure.ToProcessElement
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_cons_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → (a ::ₘ s).dedup = a ::ₘ s.dedup
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.mem_closed_iff_bsup : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}},
  IsClosed s → (a ∈ s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a)
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.mk : {R : Type u} → [inst : Ring R] → (n : ℕ) → Submodule R (Fin n → R) → FGModuleRepr R
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.image_sphere : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ), ⇑e '' Metric.sphere x r = Metric.sphere (e x) r
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_cons : ∀ {w : ℕ} {a : Bool} {x : BitVec w}, BitVec.setWidth w (BitVec.cons a x) = x
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] {δ : α → Sort u_2} (m : Multiset α) (a : α)
  (b b_1 : δ a),
  b = b_1 →
    ∀ (f f_1 : (a : α) → a ∈ m → δ a),
      f = f_1 → ∀ (a' : α) (a_1 : a' ∈ a ::ₘ m), Multiset.Pi.cons m a b f a' a_1 = Multiset.Pi.cons m a b_1 f_1 a' a_1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv : {C : Type u} → (X : CategoryTheory.FreeMonoidalCategory C) → X.Hom (X.tensor CategoryTheory.FreeMonoidalCategory.unit)
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.ker_mapRange : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N) (I : Type u_6),
  (Finsupp.mapRange.linearMap f).ker = Finsupp.submodule fun x => f.ker
-- Lean.Environment
/-- Module data for all imported modules.  -/
Lean.EnvironmentHeader.moduleData : Lean.EnvironmentHeader → Array Lean.ModuleData
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_le : ∀ {a b : UInt16}, a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.instIsLocalOfOfIsZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P],
  (AlgebraicGeometry.AffineTargetMorphismProperty.of P).IsLocal
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_pow : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (m : σ →₀ ℕ) (a : R) (n : ℕ),
  (MvPowerSeries.monomial m) a ^ n = (MvPowerSeries.monomial (n • m)) (a ^ n)
-- Mathlib.Topology.MetricSpace.Similarity
Similar.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 : Type u_6}
  [inst_3 : FunLike F P₂ P₃] [DilationClass F P₂ P₃] (f : F), Similar v₁ (⇑f ∘ v₂) ↔ Similar v₁ v₂
-- Init.Data.UInt.Bitwise
UInt8.ofNatLT_or : ∀ (a b : ℕ) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8), UInt8.ofNatLT (a ||| b) ⋯ = UInt8.ofNatLT a ha ||| UInt8.ofNatLT b hb
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.instUniqueSingleObj : (x : Type u_1) → Unique (Quiver.SingleObj x)
-- Init.Data.List.Lex
List.le_nil : ∀ {α : Type u_1} [inst : LT α] {l : List α}, l ≤ [] ↔ l = []
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mk.injEq : ∀ (toOrderHom : ℝ →o ℝ) (map_add_one' : ∀ (x : ℝ), toOrderHom.toFun (x + 1) = toOrderHom.toFun x + 1)
  (toOrderHom_1 : ℝ →o ℝ) (map_add_one'_1 : ∀ (x : ℝ), toOrderHom_1.toFun (x + 1) = toOrderHom_1.toFun x + 1),
  ({ toOrderHom := toOrderHom, map_add_one' := map_add_one' } =
      { toOrderHom := toOrderHom_1, map_add_one' := map_add_one'_1 }) =
    (toOrderHom = toOrderHom_1)
-- Mathlib.LinearAlgebra.Basis.Bilinear
/-- Two bilinear maps are equal when they are equal on all basis vectors.  -/
LinearMap.ext_basis : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring R₂] [inst_3 : Semiring S₂]
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M]
  [inst_8 : Module S N] [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P]
  {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Module.Basis ι₁ R M) (b₂ : Module.Basis ι₂ S N)
  {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, (∀ (i : ι₁) (j : ι₂), (B (b₁ i)) (b₂ j) = (B' (b₁ i)) (b₂ j)) → B = B'
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_coe : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a → ∀ (p : Polynomial R), PowerSeries.subst a ↑p = (Polynomial.aeval a) p
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- The linear equivalence between cusp forms of weight `k` and modular forms of weight `k - 12`,
given by division by the discriminant.  -/
CuspForm.discriminantEquiv : {k : ℤ} →
  CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k ≃ₗ[ℂ]
    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An `affineCombination` equals a point if that point is in the set
and has weight 1 and the other points in the set have weight 0.  -/
Finset.affineCombination_of_eq_one_of_eq_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {i : ι},
  i ∈ s → w i = 1 → (∀ i2 ∈ s, i2 ≠ i → w i2 = 0) → (Finset.affineCombination k s p) w = p i
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_mk : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (hf : ∀ (x : E), ‖f x‖ = ‖x‖), ⇑{ toLinearMap := f, norm_map' := hf } = ⇑f
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasCountableBasis.isCountablyGenerated : ∀ {α : Type u_1} {ι : Type u_4} {f : Filter α} {p : ι → Prop} {s : ι → Set α},
  f.HasCountableBasis p s → f.IsCountablyGenerated
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The canonical projection into the colimit, as a quotient type.  -/
MonCat.FilteredColimits.M.mk : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → (j : J) × ↑(F.obj j) → MonCat.FilteredColimits.M F
-- Mathlib.Topology.Order
nhds_true : nhds True = pure True
-- Mathlib.Data.Sigma.Basic
Prod.snd_toSigma : ∀ {α : Type u_7} {β : Type u_8} (x : α × β), x.toSigma.snd = x.2
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree.eq_1 : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x.intDegree = ↑x.num.natDegree - ↑x.denom.natDegree
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList'_nil : ∀ {α : Type u} (l : List α),
  Computation.corec
      (fun x =>
        match x with
        | (l, s) =>
          match Stream'.Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, Stream'.WSeq.nil) =
    Computation.pure l.reverse
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_apply_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B) (x : A), e.symm (e x) = x
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.ext : ∀ {X : Type u} {inst : PartialOrder X} {x y : PartialOrder.NonemptyFiniteChains X}, x.finset = y.finset → x = y
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasFDerivAt (g i) (g' i) x) →
    HasFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {a : α} [inst : Inhabited α], ∅.getKey! a = default
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivLM_apply_of_le : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  k + 1 ≤ n → ⇑((ContDiffMapSupportedIn.fderivLM 𝕜 n k) f) = fderiv ℝ ⇑f
-- Mathlib.LinearAlgebra.Ray
Module.Ray.map_apply : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  (e : M ≃ₗ[R] N) (v : M) (hv : v ≠ 0), (Module.Ray.map e) (rayOfNeZero R v hv) = rayOfNeZero R (e v) ⋯
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.instBind : Bind Ultrafilter
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.pair_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C),
  (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } = Y
-- Mathlib.Order.InitialSeg
_private.Mathlib.Order.InitialSeg.0.collapseF_not_lt : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ↪r s) (a : α)
  {b : β}, (∀ (a' : α), r a' a → s (↑(collapseF✝ f a')) b) → ¬s b ↑(collapseF✝ f a)