mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_restrict_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent (ι := ↑s) R (s.domRestrict v) ↔ LinearIndepOn R v s
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.ringEquiv_algebraMap : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_4) [inst : Semiring A] [inst_1 : CommSemiring S] [inst_2 : Algebra S A]
  [inst_3 : CommSemiring R] [inst_4 : Algebra R S] (r : R),
  (RestrictScalars.ringEquiv R S A) ((algebraMap R (RestrictScalars R S A)) r) = (algebraMap S A) ((algebraMap R S) r)
-- Mathlib.Analysis.Complex.Conformal
/-- A real linear map `ℓ : ℂ →ₗ[ℝ] E` respects complex scalar multiplication if it maps `I` to
`I • ℓ 1`.
 -/
real_linearMap_map_smul_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ℓ : ℂ →ₗ[ℝ] E},
  ℓ Complex.I = Complex.I • ℓ 1 → ∀ (a b : ℂ), ℓ (a • b) = a • ℓ b
-- Mathlib.Topology.Compactness.Compact
finite_cover_nhds_interior : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {U : X → Set X},
  (∀ (x : X), U x ∈ nhds x) → ∃ t, ⋃ x ∈ t, interior (U x) = Set.univ
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
/-- If `w : TwoSquare T L R B` is a Guitart exact square, with `B` essentially surjective,
and `E` is a left extension of `F` along `R`, then `E` is a pointwise left Kan extension
of `F` along `R` iff `E.compTwoSquare w` is a pointwise left Kan extension
of `T ⋙ F` along `L`.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfGuitartExact : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            {F : CategoryTheory.Functor C₂ D} →
                              (E : R.LeftExtension F) →
                                (w : CategoryTheory.TwoSquare T L R B) →
                                  [w.GuitartExact] →
                                    [B.EssSurj] →
                                      (E.compTwoSquare w).IsPointwiseLeftKanExtension ≃ E.IsPointwiseLeftKanExtension
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.eq_1 : ∀ {α : Type u_1} (ys : List α) (le : α → α → Bool), [].merge ys le = ys
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.part_iff : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ}, Nat.Partrec' f ↔ Partrec f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_dropWhile_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, ((s.takeWhile pat).dropWhile pat).isEmpty = true
-- Mathlib.Topology.Inseparable
specializingMap_iff_stableUnderSpecialization_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f ↔ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.isNone = t.isEmpty
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.algEquivOfTranscendental.congr_simp : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S)
  (h : Transcendental R s), Polynomial.algEquivOfTranscendental R s h = Polynomial.algEquivOfTranscendental R s h
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) (Y : T),
  (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.obj Y = CategoryTheory.Over.mk (hX.from Y)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_eq_match_rci : ∀ {α : Type u} {r : Std.Rii α} [inst : LE α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_7 : Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    match Std.PRange.least? with
    | none => pure init
    | some next => forIn' next...* init fun a x acc => f a ⋯ acc
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_D₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') =
    HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
-- Mathlib.RingTheory.RootsOfUnity.Basic
card_rootsOfUnity : ∀ (R : Type u_4) (k : ℕ) [NeZero k] [inst : CommRing R] [IsDomain R], Nat.card ↥(rootsOfUnity k R) ≤ k
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The arithmetic function `zetaMul χ` is multiplicative.  -/
DirichletCharacter.isMultiplicative_zetaMul : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N), χ.zetaMul.IsMultiplicative
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_obj_injective : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] {F₁ F₂ : CategoryTheory.Functor (C × D) E},
  CategoryTheory.Functor.curry.obj F₁ = CategoryTheory.Functor.curry.obj F₂ → F₁ = F₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_neg_natCast : ∀ (x : ℝ) (n : ℕ), x ^ (-↑n) = x ^ (-↑n)
-- Mathlib.Data.List.Sigma
List.mem_lookupAll : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)},
  b ∈ List.lookupAll a l ↔ ⟨a, b⟩ ∈ l
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.comap_mker : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (g : N →* P) (f : M →* N), Submonoid.comap f (MonoidHom.mker g) = MonoidHom.mker (g.comp f)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.map_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C}, Function.Surjective F.map
-- Mathlib.CategoryTheory.Monoidal.Linear
/-- A category is `MonoidalLinear R` if tensoring is `R`-linear in both factors.
 -/
CategoryTheory.MonoidalLinear : (R : Type u_1) →
  [inst : Semiring R] →
    (C : Type u_2) →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] →
            [inst : CategoryTheory.MonoidalCategory C] → [CategoryTheory.MonoidalPreadditive C] → Prop
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.component.eq_1 : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) (M : ι → Type w) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] (i : ι), DirectSum.component R ι M i = DFinsupp.lapply i
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWithTR.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : List α) (a_1 : List β) (a_2 : Array γ),
  List.zipWithTR.go✝ f a a_1 a_2 =
    match a, a_1, a_2 with
    | a :: as, b :: bs, acc => List.zipWithTR.go✝ f as bs (acc.push (f a b))
    | x, x_1, acc => acc.toList
-- Mathlib.Topology.MetricSpace.Infsep
Set.nontrivial_of_einfsep_lt_top : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep < ⊤ → s.Nontrivial
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.ne_mem_support_of_support_of_adj_of_isPath : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic →
    ∀ {u v w : V} {p : G.Walk u v} {q : G.Walk u w}, p.IsPath → q.IsPath → G.Adj v w → w ∈ p.support → v ∉ q.support
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.getModify_bind_modify : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  (f : σ → σ) (g : σ → σ → σ),
  (do
      let s ← getModify f
      modify (g s)) =
    do
    let s ← get
    modify (g s ∘ f)
-- Mathlib.Topology.Algebra.MulAction
VAddMemClass.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X] {S : Type u_5} [inst_4 : SetLike S X] [inst_5 : VAddMemClass S M X] (s : S), ContinuousVAdd M ↥s
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_add : ∀ {R : Type u_3} {A : Type u_4} [inst : Add R] [inst_1 : Add A] (x₁ x₂ : Unitization R A),
  (x₁ + x₂).toProd = x₁.toProd + x₂.toProd
-- Lean.Declaration
Lean.ReducibilityHints.compare : Lean.ReducibilityHints → Lean.ReducibilityHints → Ordering
-- Mathlib.Algebra.Ring.Periodic
/-- A function `f` is said to be `antiperiodic` with antiperiod `c` if for all `x`,
`f (x + c) = -f x`.  -/
Function.Antiperiodic : {α : Type u_1} → {β : Type u_2} → [Add α] → [Neg β] → (α → β) → α → Prop
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.comm : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y),
  CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) =
    CategoryTheory.CategoryStruct.comp self.f Y.d
-- Init.Data.List.Find
List.exists_of_findSome?_eq_some : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → Option β},
  List.findSome? f l = some b → ∃ a ∈ l, f a = some b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_id_comp_H0Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥B.ρ.invariants ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) f 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso A).hom
      (CategoryTheory.CategoryStruct.comp ((Rep.invariantsFunctor k G).map f) h)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.mk.inj : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c}
  {f : (i : ι) → A.X i ⟶ B.X i}
  {comm' :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f j))
      HomologicalComplex.Hom.comm'._autoParam}
  {f_1 : (i : ι) → A.X i ⟶ B.X i}
  {comm'_1 :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f_1 i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f_1 j))
      HomologicalComplex.Hom.comm'._autoParam},
  { f := f, comm' := comm' } = { f := f_1, comm' := comm'_1 } → f = f_1
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.sdiff_coloops_indep_iff`. -/
Matroid.diff_coloops_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep (I \ M.coloops) ↔ M.Indep I
-- Lean.Data.Name
Lean.Name.hashEx : Lean.Name → UInt64
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.H1Cotangent.equiv_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  {ι' : Type u_1} (P : Algebra.Generators R S ι) (P' : Algebra.Generators R S ι')
  (c : ↥P.toExtension.cotangentComplex.ker),
  (Algebra.Generators.H1Cotangent.equiv P P') c =
    ⟨(Algebra.Extension.Cotangent.map (P.defaultHom P').toExtensionHom) ↑c, ⋯⟩
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppCommand : Lean.Command → Lean.CoreM Std.Format
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.id_f₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.CategoryStruct.id S).f₃ = CategoryTheory.CategoryStruct.id S.L₃
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Applying `AffineMap.homothety` on `Finset.affineCombination` towards one of the weighted points
is equivalent to moving the weights towards `Finset.affineCombinationSingleWeights`.  -/
Finset.homothety_affineCombination : ∀ {k : Type u_6} {V : Type u_7} {P : Type u_8} [inst : CommRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_9} [inst_4 : DecidableEq ι] (s : Finset ι) (p : ι → P) (w : ι → k) {i : ι},
  i ∈ s →
    ∀ (r : k),
      (AffineMap.homothety (p i) r) ((Finset.affineCombination k s p) w) =
        (Finset.affineCombination k s p) ((AffineMap.lineMap (Pi.single i 1) w) r)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.blsub_lt_ord : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} {c : Ordinal.{u}},
  o.card < c.cof → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.blsub f < c
-- Lean.Elab.InfoTree.Main
Lean.Elab.CommandContextInfo.saveNoFileMap : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadMCtx m] →
        [Lean.MonadOptions m] → [Lean.MonadResolveName m] → [Lean.MonadNameGenerator m] → m Lean.Elab.CommandContextInfo
-- Mathlib.Probability.UniformOn
/-- See `uniformOn_eq_zero'` for a version assuming `MeasurableSet s` instead of
`MeasurableSingletonClass Ω`.  -/
ProbabilityTheory.uniformOn_eq_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s : Set Ω} [MeasurableSingletonClass Ω],
  ProbabilityTheory.uniformOn s = 0 ↔ s.Infinite ∨ s = ∅
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.nonempty_basis : ∀ {G : Type u} {inst : Group G} [self : IsFreeGroup G], ∃ ι, Nonempty (FreeGroupBasis ι G)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- The identity lax functor.  -/
CategoryTheory.LaxFunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.LaxFunctor B B
-- Lean.DocString.Parser
Lean.Doc.Parser.OrderedListType.noConfusionType : Sort v✝ → Lean.Doc.Parser.OrderedListType → Lean.Doc.Parser.OrderedListType → Sort v✝
-- Mathlib.Analysis.Normed.Module.Basic
/-- This is a simpler version of `nnnorm_algebraMap` when `‖1‖ = 1` in `𝕜'`.  -/
nnnorm_algebraMap' : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  [NormOneClass 𝕜'] (x : 𝕜), ‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabWaitIfTypeMVar : Lean.Elab.Term.TermElab
-- Mathlib.Logic.Small.Defs
small_sigma : ∀ {α : Type u_2} (β : α → Type u_1) [Small.{w, u_2} α] [∀ (a : α), Small.{w, u_1} (β a)],
  Small.{w, max u_1 u_2} ((a : α) × β a)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The sum defined in Bessel's inequality is summable.  -/
Orthonormal.inner_products_summable : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (x : E) {v : ι → E}, Orthonormal 𝕜 v → Summable fun i => ‖inner 𝕜 (v i) x‖ ^ 2
-- Mathlib.ModelTheory.PartialEquiv
/-- The cofinal set of finite equivalences with a given element in their codomain.  -/
FirstOrder.Language.IsExtensionPair.definedAtRight : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → L.IsExtensionPair N M → N → Order.Cofinal (L.FGEquiv M N)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.  -/
BitVec.reduceHShiftRight' : Lean.Meta.Simp.DSimproc
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertListIfNew_perm_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ →
      (Std.Internal.List.insertListIfNew l₁ l₂).Perm (Std.Internal.List.insertList l₂ l₁)
-- Mathlib.Data.Int.ModEq
Int.modEq_abs : ∀ {n a b : ℤ}, a ≡ b [ZMOD |n|] ↔ a ≡ b [ZMOD n]
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
/-- The (topological) closure of a non-unital star subalgebra of a non-unital topological star
algebra is itself a non-unital star subalgebra.  -/
NonUnitalStarSubalgebra.topologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Star A] →
          [inst_3 : NonUnitalSemiring A] →
            [inst_4 : Module R A] →
              [ContinuousStar A] →
                [ContinuousConstSMul R A] →
                  [IsSemitopologicalSemiring A] → NonUnitalStarSubalgebra R A → NonUnitalStarSubalgebra R A
-- Lean.ProjFns
Lean.instReprAuxParentProjectionInfo.repr : Lean.AuxParentProjectionInfo → ℕ → Std.Format
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.ker_eq_bot_iff_range_eq_top : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {f : V →ₗ[K] V}, f.ker = ⊥ ↔ f.range = ⊤
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {f : M →ₙ* N},
  Subsemigroup.map f (Subsemigroup.comap f (Subsemigroup.map f S)) = Subsemigroup.map f S
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
for all basis vectors `x` and `y`.  -/
LinearMap.eq_adjoint_iff_basis : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {ι₁ : Type u_5} {ι₂ : Type u_6}
  (b₁ : Module.Basis ι₁ 𝕜 E) (b₂ : Module.Basis ι₂ 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E),
  A = LinearMap.adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), inner 𝕜 (A (b₁ i₁)) (b₂ i₂) = inner 𝕜 (b₁ i₁) (B (b₂ i₂))
-- Init.Data.UInt.Bitwise
USize.ofFin_and : ∀ (a b : Fin USize.size), USize.ofFin (a &&& b) = USize.ofFin a &&& USize.ofFin b
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_inv_iff_mul_le : ∀ {a b : ENNReal}, a ≤ b⁻¹ ↔ a * b ≤ 1
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₀ = CategoryTheory.CategoryStruct.id S.L₀
-- Mathlib.Order.Cover
WCovBy.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), (a ⩿ b) = (a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.State.mk.injEq : ∀ (steps : ℕ) (infos : Lean.SubExpr.PosMap Lean.Elab.Info)
  (holeIter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator) (steps_1 : ℕ)
  (infos_1 : Lean.SubExpr.PosMap Lean.Elab.Info) (holeIter_1 : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator),
  ({ steps := steps, infos := infos, holeIter := holeIter } =
      { steps := steps_1, infos := infos_1, holeIter := holeIter_1 }) =
    (steps = steps_1 ∧ infos = infos_1 ∧ holeIter = holeIter_1)
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The downward **local LYM inequality**. `𝒜` takes up less of `α^(r)` (the finsets of card `r`)
than `∂𝒜` takes up of `α^(r - 1)`.  -/
Finset.local_lubell_yamamoto_meshalkin_inequality_div : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] [inst_4 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  r ≠ 0 → Set.Sized r ↑𝒜 → ↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑𝒜.shadow.card / ↑((Fintype.card α).choose (r - 1))
-- Mathlib.Analysis.Complex.Circle
Circle.exp_nsmul : ∀ (x : ℝ) (n : ℕ), Circle.exp (n • x) = Circle.exp x ^ n
-- Init.Data.List.Perm
List.Perm.take : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ {i : ℕ}, (List.drop i l₁).Perm (List.drop i l₂) → (List.take i l₁).Perm (List.take i l₂)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLIntegral_setLAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  (f : α → ENNReal) (s : Set α), ∫⁻ (_x : α) in s, ⨍⁻ (a : α) in s, f a ∂μ ∂μ = ∫⁻ (x : α) in s, f x ∂μ
-- Mathlib.Topology.Spectral.Prespectral
Order.Ideal.mk.congr_simp : ∀ {P : Type u_2} [inst : LE P] (toLowerSet toLowerSet_1 : LowerSet P) (e_toLowerSet : toLowerSet = toLowerSet_1)
  (nonempty' : toLowerSet.carrier.Nonempty) (directed' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier),
  { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' } =
    { toLowerSet := toLowerSet_1, nonempty' := ⋯, directed' := ⋯ }
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.

WARNING: This has the potential to send `ext` into a loop if someone locally adds the inverse ext
lemma proving equality in `α →* Multiplicative β` from equality in `Additive α →+ β`.  -/
Additive.addMonoidHom_ext : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (f g : Additive α →+ β),
  AddMonoidHom.toMultiplicativeRight f = AddMonoidHom.toMultiplicativeRight g → f = g
-- Init.System.IO
IO.AccessRight.mk : Bool → Bool → Bool → IO.AccessRight
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k : α} {f : Option β → Option β} {hc : k ∈ t.alter k f}, (t.alter k f).getKey k hc = k
-- Lean.Syntax
Lean.SyntaxNode.getNumArgs : Lean.SyntaxNode → ℕ