mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_eq_iff : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate)
  (b : Module.Basis ι K V) (v : ι → V), ⇑(B.dualBasis hB b) = v ↔ ∀ (i j : ι), (B (v i)) (b j) = if j = i then 1 else 0
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The ring homomorphism that takes a section of the structure sheaf of `R` on the open set `U`,
implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates
the section on the point corresponding to a given prime ideal.  -/
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.openToLocalizationₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            x ∈ U →
              ((AlgebraicGeometry.structurePresheafInModuleCat R M).obj (Opposite.op U) ⟶
                ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_comp_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ L₃ : CategoryTheory.Functor C D} {R₁ R₂ R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (adj₃ : L₃ ⊣ R₃) (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂) {Z : CategoryTheory.Functor D C} (h : R₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₃) β) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.conjugateEquiv adj₁ adj₃) (CategoryTheory.CategoryStruct.comp β α)) h
-- Init.Data.String.TakeDrop
String.stripPrefix : String → String → String
-- Lean.Syntax
Lean.SyntaxNode.getIdAt : Lean.SyntaxNode → ℕ → Lean.Name
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux_image_relation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ),
  ⇑(Algebra.Presentation.aux✝ Q P) '' Set.range (Q.compRelationAux P) = Set.range Q.relation
-- Mathlib.Algebra.Group.Action.Defs
Semigroup.isScalarTower : ∀ {α : Type u_5} [inst : Semigroup α], IsScalarTower α α α
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.mem_pointwise_smul_iff_inv_smul_mem₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ (S : Subring R) (x : R), x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.zero_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {β : Type u_1} [inst_1 : EMetricSpace β] (f : α → β),
  LipschitzOnWith 0 f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight η h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h)
        (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp g h)).hom)
-- Mathlib.Order.SupIndep
/-- If the elements of a set are independent, then any pair within that set is disjoint.  -/
sSupIndep.pairwiseDisjoint : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSupIndep s → s.PairwiseDisjoint id
-- Std.Sync.Notify
Std.Notify.Consumer.normal.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (promise : IO.Promise α),
  sizeOf (Std.Notify.Consumer.normal promise) = 1 + sizeOf promise
-- Batteries.Tactic.Lint.Basic
/-- Returns true if `decl` should be checked
using `linter`, i.e., if there is no `nolint` attribute.  -/
Batteries.Tactic.Lint.shouldBeLinted : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → Lean.Name → m Bool
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le_of_finite : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R]
  [NoZeroDivisors A] {ι : Type w} [Finite ι] {x : ι → A},
  AlgebraicIndependent R x → Algebra.trdeg R A ≤ Cardinal.mk ι → IsTranscendenceBasis R x
-- Init.Data.SInt.Bitwise
Int16.zero_and : ∀ {a : Int16}, 0 &&& a = 0
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₆_diag : ∀ (i : Fin 6), CartanMatrix.E₆ i i = 2
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_compact : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ),
  IsCompact (NumberField.mixedEmbedding.convexBodySum K B)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α} {f : β → β}, (m.modify k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- If `a` is divisible by `4` and `b` is odd, then we can remove the factor `4` from `a`.  -/
Mathlib.Meta.NormNum.jacobiSymNat.double_even : ∀ (a b c : ℕ) (r : ℤ),
  a % 4 = 0 →
    b % 2 = 1 → a / 4 = c → Mathlib.Meta.NormNum.jacobiSymNat c b = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_terminatedAt_succ_iff : ∀ {α : Type u} {x : α} {s : Stream'.Seq α} {n : ℕ}, (Stream'.Seq.cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The evaluation map `MvPolynomial (ι' ⊕ ι) →ₐ[R] T` factors via this map. For more
details, see the module docstring at the beginning of the section.  -/
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {ι' : Type u_1} →
                {σ' : Type u_2} →
                  {T : Type u_3} →
                    [inst_3 : CommRing T] →
                      [inst_4 : Algebra S T] →
                        Algebra.Presentation S T ι' σ' →
                          Algebra.Presentation R S ι σ → MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' S
-- Mathlib.RingTheory.RingHom.Locally
RingHom.locally_of_locally : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f) →
    ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
      RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f →
        RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => Q) f
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.sub : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : AddGroup β]
  [ContinuousSub β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω - v i ω
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_finite : ∀ {α : Type u_1} {M : Matroid α} [M.Finite], M✶.Finite
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A discrete space is a CW complex.  -/
Topology.CWComplex.ofDiscreteTopology : {X : Type u_2} → [inst : TopologicalSpace X] → [DiscreteTopology X] → Topology.CWComplex Set.univ
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a division  -/
Subgroup.div : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Div ↥H
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (a : CochainComplex.HomComplex.CohomologyClass K L n),
  CochainComplex.HomComplex.CohomologyClass.homAddEquiv a = CochainComplex.HomComplex.CohomologyClass.toHom a
-- Mathlib.Order.Filter.Ker
Filter.mem_ker : ∀ {α : Type u_2} {f : Filter α} {a : α}, a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.hasColimit_const_of_isConnected : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) [CategoryTheory.IsConnected J], CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.const J).obj X)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.trunc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J}
  (iter iter_1 : Φ.Iteration j), iter = iter_1 → ∀ {j' : J} (hj' : j' ≤ j), iter.trunc hj' = iter_1.trunc hj'
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- The Roth number of a natural `N` is the largest integer `m` for which there is a subset of
`range N` of size `m` with no arithmetic progression of length 3.
Trivially, `rothNumberNat N ≤ N`, but Roth's theorem (proved in 1953) shows that
`rothNumberNat N = o(N)` and the construction by Behrend gives a lower bound of the form
`N * exp(-C sqrt(log(N))) ≤ rothNumberNat N`.
A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives
`rothNumberNat N = O(N / (log N)^(1+c))` for an absolute constant `c`.  -/
rothNumberNat : ℕ →o ℕ
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp f h)
-- Std.Data.TreeSet.Basic
Std.TreeSet.Equiv.mk : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet α cmp}, m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Order.PiLex
Pi.lex_iff_of_unique : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Unique ι] [inst_1 : (i : ι) → LT (β i)] {r : ι → ι → Prop} [Std.Irrefl r]
  {x y : (i : ι) → β i}, Pi.Lex r (fun {i} x1 x2 => x1 < x2) x y ↔ x default < y default
-- Mathlib.Order.LiminfLimsup
Filter.limsup_top_eq_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (u : β → α), Filter.limsup u ⊤ = ⨆ i, u i
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.Iterators.Types.Append.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {β α₁ : Type u_1} [inst : Std.Iterator α₁ m β] (it₁ : Std.IterM m β)
  (motive : it₁.Step → Sort u_3) (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Init.Data.List.Lemmas
List.cons_removeAll : ∀ {α : Type u_1} [inst : BEq α] {x : α} {xs ys : List α},
  (x :: xs).removeAll ys = if ys.contains x = false then x :: xs.removeAll ys else xs.removeAll ys
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cochainsMap_id : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G),
  ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id X.homogeneousCochains
-- Lean.Environment
Lean.EnvExtension.instInhabitedAsyncMode.default : Lean.EnvExtension.AsyncMode
-- Mathlib.Logic.Equiv.Fin.Basic
/-- Equivalence between `Fin m ⊕ Fin n` and `Fin (m + n)`  -/
finSumFinEquiv : {m n : ℕ} → Fin m ⊕ Fin n ≃ Fin (m + n)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.coeff_one : ∀ (k : ℕ) {e : ℕ}, Nat.rawCast 1 = e → k.rawCast = e * k
-- Mathlib.SetTheory.Ordinal.Family
/-- The least strict upper bound of a family of ordinals indexed by the set of ordinals less than
some `o : Ordinal.{u}`.  -/
Ordinal.blsub : (o : Ordinal.{u}) → ((a : Ordinal.{u}) → a < o → Ordinal.{max u v}) → Ordinal.{max u v}
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- If a right Kan extension is pointwise, then evaluating it at an object is isomorphic to
taking a limit.  -/
CategoryTheory.Functor.ranObjObjIsoLimit : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] →
                (F : CategoryTheory.Functor C H) →
                  [inst_4 : L.HasPointwiseRightKanExtension F] →
                    (X : D) →
                      (L.ran.obj F).obj X ≅
                        CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj X L).comp F)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_vecMulVec_star : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : StarMul α] (w : m → α) (v : n → α),
  (Matrix.vecMulVec w v).map star = (Matrix.vecMulVec (star v) (star w)).transpose
-- Mathlib.CategoryTheory.Sites.LocallySurjective
/-- Given `f : F ⟶ G`, a morphism between presieves, and `s : G.obj (op U)`, this is the sieve
of `U` consisting of the `i : V ⟶ U` such that `s` restricted along `i` is in the image of `f`.  -/
CategoryTheory.Presheaf.imageSieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        {FA : A → A → Type u_1} →
          {CA : A → Type w'} →
            [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory A FA] →
                {F G : CategoryTheory.Functor Cᵒᵖ A} →
                  (F ⟶ G) → {U : C} → CategoryTheory.ToType (G.obj (Opposite.op U)) → CategoryTheory.Sieve U
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.of_injective : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  IsFiniteLength R N → Function.Injective ⇑f → IsFiniteLength R M
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.f₁₂ = sq.f₁₃
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnRingHom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {R : Type u_10} [inst_9 : CommRing R] [inst_10 : TopologicalSpace R] [inst_11 : ChartedSpace H' R]
  [inst_12 : ContMDiffRing I' n R] (a : ContMDiffMap I I' N R n) (a_1 : N), ContMDiffMap.coeFnRingHom a a_1 = a a_1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsTrail → p.reverse.IsTrail
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProba_diracProbaInverse : ∀ {X : Type u_2} [inst : MeasurableSpace X] (μ : ↑(Set.range MeasureTheory.diracProba)),
  MeasureTheory.diracProba (MeasureTheory.diracProbaInverse μ) = ↑μ
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.instCoeTC : {α : Type u} → [inst : TopologicalSpace α] → CoeTC α (ConnectedComponents α)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientAddEquivOfEq.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {M N : AddSubgroup G} [inst_1 : M.Normal] [inst_2 : N.Normal] (h : M = N),
  QuotientAddGroup.quotientAddEquivOfEq h = { toEquiv := AddSubgroup.quotientEquivOfEq h, map_add' := ⋯ }
-- Mathlib.Logic.Function.Conjugate
/-- Reinterpret `Function.Commute f g` as `Function.Semiconj f g g`. These two predicates are
definitionally equal but have different dot-notation lemmas.  -/
Function.Commute.semiconj : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Semiconj f g g
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskering_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.whiskering E).obj c = CategoryTheory.Limits.Cone.whisker E c
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The topology of uniform convergence is T₂.  -/
UniformFun.instT2Space : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] [T2Space β], T2Space (UniformFun α β)
-- Mathlib.Order.WithBot
WithTop.toDual_lt_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithBot αᵒᵈ} {y : WithTop α}, WithTop.toDual y < x ↔ WithBot.ofDual x < y
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The transformation that turns a function `g` into
`n ^ p * ∑ u ∈ Finset.Ico n₀ n, g u / u ^ (p + 1)`.  -/
AkraBazziRecurrence.sumTransform : ℝ → (ℝ → ℝ) → ℕ → ℕ → ℝ
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processPendingLevel : Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.SetTheory.Ordinal.Rank
IsWellFounded.rank_lt_of_rel : ∀ {α : Type u} {a b : α} {r : α → α → Prop} [hwf : IsWellFounded α r],
  r a b → IsWellFounded.rank r a < IsWellFounded.rank r b
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals  -/
AnalyticOn.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {s : Set E},
  AnalyticOn ℂ f s → AnalyticOn ℂ g s → (∀ z ∈ s, f z ∈ Complex.slitPlane) → AnalyticOn ℂ (fun z => f z ^ g z) s
-- Mathlib.Tactic.SetNotationForOrder
/-- Subset relation: `a ⊆ b`.
For types tagged with `@[use_set_notation_for_order]`,
the relation `LE.le` is used instead of `Subset`.
The hover info shows which one is used. 

Conventions for notations in identifiers:

 * The recommended spelling of `⊆` in identifiers is `subset`. -/
Mathlib.Meta.SetNotationForOrder.subsetStx' : Lean.TrailingParserDescr
-- Lean.Elab.PreDefinition.Structural.BRecOn
_private.Lean.Elab.PreDefinition.Structural.BRecOn.0.Lean.Elab.Structural.throwToBelowFailed : {α : Type} → Lean.MetaM α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isColimit_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.colimit.isColimit F).desc c = CategoryTheory.Limits.colimit.desc F c
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.vadd_apply : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : MeasurableConstVAdd G α] (c : G), ⇑(MeasurableEquiv.vadd c) = fun x => c +ᵥ x
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `C^n` within a set at a point as continuity within this set at this
point, and being `C^n` in the corresponding extended chart.  -/
contMDiffWithinAt_iff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.instInhabitedInlineAttributeKind.default : Lean.Compiler.InlineAttributeKind
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.parts.injEq : ∀ (p p_1 : Array Lean.Elab.InlayHintLabelPart),
  (Lean.Elab.InlayHintLabel.parts p = Lean.Elab.InlayHintLabel.parts p_1) = (p = p_1)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_map : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (x : L₂),
  x ∈ LieSubalgebra.map f K ↔ ∃ y ∈ K, f y = x
-- Std.Time.Zoned.Database.Basic
/-- Retrieves the zone rules information (`ZoneRules`) for a given area at a specific point in time.
 -/
Std.Time.Database.getZoneRules : {α : Type} → [self : Std.Time.Database α] → α → String → IO Std.Time.TimeZone.ZoneRules
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s],
  p ≠ ⊤ →
    ∀ {μ : MeasureTheory.Measure β},
      (∀ᵐ (x : β) ∂μ, f x ∈ closure s) →
        MeasureTheory.eLpNorm (fun x => f x - y₀) p μ < ⊤ →
          Filter.Tendsto (fun n => MeasureTheory.eLpNorm (⇑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) - f) p μ)
            Filter.atTop (nhds 0)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instMulDistribMulActionSubtypeMem : {K : Type u} →
  [inst : DivisionRing K] →
    {X : Type u_1} → [inst_1 : Monoid X] → [MulDistribMulAction K X] → (F : Subfield K) → MulDistribMulAction (↥F) X