mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ ι : F ⟶ G} (Γ : CategoryTheory.Lax.LaxTrans.Modification η θ)
  (Δ : CategoryTheory.Lax.LaxTrans.Modification θ ι) (a : B),
  (Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.indep' : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {p1 p2 : Set (Set Ω)},
  (∀ s ∈ p1, MeasurableSet s) →
    (∀ s ∈ p2, MeasurableSet s) →
      IsPiSystem p1 →
        IsPiSystem p2 →
          ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ →
            ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) κ μ
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.map_topologicalClosure_le : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : TopologicalSpace B] [inst_9 : Star B] [inst_10 : NonUnitalSemiring B]
  [inst_11 : Module R B] [inst_12 : IsSemitopologicalSemiring B] [inst_13 : ContinuousConstSMul R B]
  [inst_14 : ContinuousStar B] (s : NonUnitalStarSubalgebra R A) {φ : A →⋆ₙₐ[R] B},
  Continuous ⇑φ →
    NonUnitalStarSubalgebra.map φ s.topologicalClosure ≤ (NonUnitalStarSubalgebra.map φ s).topologicalClosure
-- Mathlib.GroupTheory.Complement
/-- The collection of right transversals of a subgroup.  -/
AddSubgroup.RightTransversal : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → Type (max 0 u_1)
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- Continuous functions are dense in `MeasureTheory.Lp`, `1 ≤ p < ∞`. This theorem assumes that
the domain is a compact space because otherwise `ContinuousMap.toLp` is undefined. Use
`BoundedContinuousFunction.toLp_denseRange` if the domain is not a compact space.  -/
ContinuousMap.toLp_denseRange : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [inst_3 : BorelSpace α]
  (E : Type u_2) [inst_4 : NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal}
  [inst_5 : SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (𝕜 : Type u_3) [inst_6 : NormedRing 𝕜]
  [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] [inst_10 : CompactSpace α] [μ.WeaklyRegular]
  [inst_12 : MeasureTheory.IsFiniteMeasure μ], p ≠ ⊤ → DenseRange ⇑(ContinuousMap.toLp p μ 𝕜)
-- Mathlib.Topology.Defs.Induced
Topology.IsQuotientMap.surjective : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsQuotientMap f → Function.Surjective f
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_inv_rpow_eq_iff : ∀ {x : ENNReal} {y : ℝ}, (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1
-- Mathlib.Tactic.Linarith.Datatypes
/-- `l.contains n` is true iff `n` is the first element of a pair in `l`.
 -/
Mathlib.Tactic.Linarith.Linexp.contains : ℕ → Mathlib.Tactic.Linarith.Linexp → Bool
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} {k : β → α}
  {lb : Filter β}, f =o[𝕜; l] g → Filter.Tendsto k lb l → (f ∘ k) =o[𝕜; lb] (g ∘ k)
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalPresentable X κ] (J : Type w) [inst_3 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsCardinalFiltered J κ],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X)
  (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) (i : ι) {Z : C}
  (h : Y i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w)
      (CategoryTheory.CategoryStruct.comp (s.π i) h) =
    CategoryTheory.CategoryStruct.comp (a i) h
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_left_of_gcd_eq_one : ∀ {n m k : ℕ}, n.gcd m = 1 → (k * n).gcd m = k.gcd m
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
comap_neg_leftUniformSpace : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  UniformSpace.comap (⇑(Equiv.neg G)) (IsTopologicalAddGroup.leftUniformSpace G) =
    IsTopologicalAddGroup.rightUniformSpace G
-- Aesop.Index.Basic
Aesop.IndexingMode.brecOn_2.go : {motive_1 : Aesop.IndexingMode → Sort u} →
  {motive_2 : Array Aesop.IndexingMode → Sort u} →
    {motive_3 : List Aesop.IndexingMode → Sort u} →
      (t : List Aesop.IndexingMode) →
        ((t : Aesop.IndexingMode) → t.below → motive_1 t) →
          ((t : Array Aesop.IndexingMode) → Aesop.IndexingMode.below_1 t → motive_2 t) →
            ((t : List Aesop.IndexingMode) → Aesop.IndexingMode.below_2 t → motive_3 t) →
              motive_3 t ×' Aesop.IndexingMode.below_2 t
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.p_descOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) {Z : C}
  (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C} (X : C)
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A) {Z : C}
  (h : B ⟹ CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategoryStruct.tensorObj A X)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) h)
-- Mathlib.Algebra.Lie.Killing
/-- The converse of this is true in characteristic zero; it is
`LieAlgebra.HasTrivialRadical.instIsKilling`. There are counterexamples
over fields with positive characteristic.

Note that when the coefficients are a field this instance is redundant since we have
`LieAlgebra.IsKilling.instSemisimple` and `LieAlgebra.IsSemisimple.instHasTrivialRadical`.  -/
LieAlgebra.IsKilling.instHasTrivialRadical : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R],
  LieAlgebra.HasTrivialRadical R L
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.foldrAux.eq_def : ∀ {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : String.Pos.Raw),
  String.Legacy.foldrAux f a s i begPos =
    if h : begPos < i then
      have this := ⋯;
      have i := String.Pos.Raw.prev s i;
      have a := f (String.Pos.Raw.get s i) a;
      String.Legacy.foldrAux f a s i begPos
    else a
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.epi_iff_surjective : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of monoids commutes.  -/
Con.lift_coe : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
  (H : c ≤ Con.ker f) (x : M), (c.lift f H) ↑x = f x
-- Mathlib.Data.List.Perm.Basic
_private.Mathlib.Data.List.Perm.Basic.0.List.«term_*_» : Lean.TrailingParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ((∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rcc_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toArray[i]? = none ↔ (n + 1 - m).toNat ≤ i
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Returns true if the parameter is an explicit parameter that has neither a default value nor a tactic.
 -/
Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit : Lean.PrettyPrinter.Delaborator.ParamKind → Bool
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse : Type
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.stronglyMeasurable_uncurry_gaussianPDF : MeasureTheory.StronglyMeasurable fun x =>
  match x with
  | (μ, v, x) => ProbabilityTheory.gaussianPDF μ v x
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.barComplex.d.eq_1 : ∀ (k G : Type u) [inst : CommRing k] (n : ℕ) [inst_1 : Group G],
  Rep.barComplex.d k G n =
    Rep.freeLift k G (Rep.free k G (Fin n → G)) fun g =>
      (fun₀ | fun i => g i.succ => MonoidAlgebra.single (g 0) 1) +
        ∑ j, fun₀ | j.contractNth (fun x1 x2 => x1 * x2) g => MonoidAlgebra.single 1 ((-1) ^ (↑j + 1))
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.hasSum_integral_sum_dirac : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {f : X → E} [inst_1 : NormedSpace ℝ E] [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal} [CompleteSpace E],
  (∀ (i : ι), c i ≠ ⊤) →
    (Summable fun i => (c i).toReal * ‖f (x i)‖) →
      HasSum (fun i => (c i).toReal • f (x i))
        (∫ (x : X), f x ∂MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i))
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul' : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x + y * x) + 1#w = ~~~y * x
-- Aesop.Tree.Data
Aesop.Rapp.setScriptSteps? : Option (Array Aesop.Script.LazyStep) → Aesop.Rapp → Aesop.Rapp
-- Aesop.BuiltinRules
Aesop.BuiltinRules.pEmpty_false : ∀ (h : PEmpty.{u_1}), False
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_succ : ∀ (o : Ordinal.{u_1}), ZFSet.vonNeumann (Order.succ o) = (ZFSet.vonNeumann o).powerset
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_empty : ∀ {α : Type u}, FreeGroup.invRev [] = []
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.toEmbedding_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.toEmbedding.toHom = f.toHom
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instEmptyCollection : {α : Type u} → {cmp : α → α → Ordering} → EmptyCollection (Std.TreeSet.Raw α cmp)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_le_preBeth : ∀ (o : Ordinal.{u_1}), Cardinal.preAleph o ≤ Cardinal.preBeth o
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint_toContinuousLinearMap : ∀ {𝕜 : 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] (A : E →ₗ[𝕜] F),
  LinearMap.toContinuousLinearMap (LinearMap.adjoint A) =
    ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- `ContMDiffOn I I' n f s` indicates that the function `f : M → M'` between manifolds
is `n` times continuously differentiable in a set `s : Set M`.

`f` is `n` times continuously differentiable on `s` if it is continuous on `s` and,
for any pair of points, it is `n` times continuously differentiable `s` in the charts
around these points.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions.  -/
ContMDiffOn : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → WithTop ℕ∞ → (M → M') → Set M → Prop
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {km : α}, t.max! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.instReprTZSpec.repr : Std.Time.Database.TZdb.TZSpec → ℕ → Std.Format
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitEpi f] {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).fst =
    let c' := CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι c) ⋯;
    have i' := CategoryTheory.Limits.isKernelCompMono i (CategoryTheory.section_ f) ⋯;
    have i'' := CategoryTheory.Preadditive.isLimitForkOfKernelFork i';
    (CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.fromPreimage_app_hom_apply_coe : ∀ {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) (U : SimplexCategoryᵒᵖ) (x : (A.preimage p).toSSet.obj U),
  ↑((CategoryTheory.ConcreteCategory.hom ((A.fromPreimage p).app U)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom fun x => ↑x) (p.app U))) x
-- Lean.Message
_private.Lean.Message.0.Lean.MessageData.hasSyntheticSorry.visit : Option Lean.MetavarContext → Lean.MessageData → Bool
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape'_toTransfiniteCompositionOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  (c : HomotopicalAlgebra.RelativeCellComplex basicCell f) {I : CategoryTheory.MorphismProperty C}
  (hc : ∀ (s : c.Cells), I (basicCell s.j s.i)),
  (c.transfiniteCompositionOfShape' hc).toTransfiniteCompositionOfShape = c.toTransfiniteCompositionOfShape
-- Mathlib.LinearAlgebra.Dimension.Localization
IsBaseChange.lift_rank_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {T : Type uT}
  [inst_3 : CommRing T] [NoZeroDivisors T] [inst_5 : Algebra R T] [FaithfulSMul R T] {P : Type uP}
  [inst_7 : AddCommGroup P] [inst_8 : Module R P] [inst_9 : Module T P] [inst_10 : IsScalarTower R T P] {g : M →ₗ[R] P},
  IsBaseChange T g → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
-- Mathlib.Order.Height
Set.one_le_chainHeight_iff : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), 1 ≤ s.chainHeight r ↔ s.Nonempty
-- Mathlib.Analysis.Calculus.ImplicitContDiff
IsContDiffImplicitAt.bijective : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  {E₂ : Type u_3} [inst_3 : NormedAddCommGroup E₂] [inst_4 : NormedSpace 𝕜 E₂] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E₁ × E₂ → F} {f' : E₁ × E₂ →L[𝕜] F}
  {u : E₁ × E₂}, IsContDiffImplicitAt n f f' u → Function.Bijective ⇑(f' ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂)
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierInv_sum : ∀ {ι : Type u_1} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F]
  [inst_2 : FourierTransformInv E F] [FourierInvAdd E F] (f : ι → E) (s : Finset ι),
  FourierTransformInv.fourierInv (∑ i ∈ s, f i) = ∑ i ∈ s, FourierTransformInv.fourierInv (f i)
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMap_zero : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃),
  g.compMultilinearMap 0 = 0
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is
equicontinuous at `x₀`.  -/
IsUniformInducing.equicontinuousAt_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_8} [tX : TopologicalSpace X] [uα : UniformSpace α]
  [uβ : UniformSpace β] {F : ι → X → α} {x₀ : X} {u : α → β},
  IsUniformInducing u → (EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀)
-- Mathlib.AlgebraicGeometry.Normalization
/-- Normalization commutes with smooth base change.  -/
AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] [AlgebraicGeometry.Smooth g],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.normalizationPullback f g)
-- Mathlib.AlgebraicTopology.SingularSet
instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex : SSet.toTop.IsLeftKanExtension SSet.toTopSimplex.inv
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.ι₁_h : ∀ {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : TopCat.Homotopy f₀ f₁), CategoryTheory.CategoryStruct.comp TopCat.ι₁ F.h = f₁
-- Aesop.Rule.Forward
Aesop.ForwardRule.instHashable : Hashable Aesop.ForwardRule
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.LiftPropAt.eq_1 : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') (x : M),
  ChartedSpace.LiftPropAt P f x = ChartedSpace.LiftPropWithinAt P f Set.univ x
-- Init.Data.Rat.Lemmas
Rat.mkRat_mul_right : ∀ {n : ℤ} {d a : ℕ}, a ≠ 0 → mkRat (n * ↑a) (d * a) = mkRat n d
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe : ∀ {α : Type u} (p q : α → Prop) (a : { x // q ↑x }), ↑((Equiv.subtypeSubtypeEquivSubtypeInter p q) a) = ↑↑a
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.id : Lean.Elab.FVarAliasInfo → Lean.FVarId
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone)
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_inv_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`.  -/
ENNReal.mul_inv_cancel_left' : ∀ {a b : ENNReal}, (a = 0 → b = 0) → (a = ⊤ → b = 0) → a * (a⁻¹ * b) = b
-- Mathlib.Logic.Function.Basic
Function.Involutive.leftInverse : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.LeftInverse f f
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeLspNotification : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.Notification α → IO Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m.erase k).getKey! k = default
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  {c : CategoryTheory.Limits.KernelFork (f - g)} (i : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Fork f g),
  (CategoryTheory.Preadditive.isLimitForkOfKernelFork i).lift s = i.lift (CategoryTheory.Preadditive.kernelForkOfFork s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey! k = m₁.getKey! k
-- Lean.Server.Rpc.Basic
Lean.Lsp.instToStringRpcRef : ToString Lean.Lsp.RpcRef
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.isCoveringMapOn : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → IsCoveringMapOn f Set.univ
-- Aesop.Tree.Data
Aesop.Rapp.isIrrelevant : Aesop.Rapp → Bool
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd : ONote → ℕ+ → ONote → ONote
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The support of an ideal sheaf. Use `IdealSheafData.support` instead for most occasions.  -/
AlgebraicGeometry.Scheme.IdealSheafData.supportSet : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → Set ↥X
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.const.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremArgs.const = 1
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure in an inner product space.  -/
MeasureTheory.charFun : {E : Type u_2} → {mE : MeasurableSpace E} → [Inner ℝ E] → MeasureTheory.Measure E → E → ℂ
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Specialization of `Option.getD` to values in `WithZero α` that respects API boundaries.  -/
WithZero.unzeroD : {α : Type u} → α → WithZero α → α
-- Lean.Parser.Do
Lean.Parser.Term.termBeforeDo.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_pi : ∀ {α : Type u_1} {β : α → Type u_3} [inst : Fintype α], Nat.card ((a : α) → β a) = ∏ a, Nat.card (β a)
-- Lean.Meta.Basic
Lean.Meta.isDefEqNoConstantApprox : Lean.Expr → Lean.Expr → Lean.MetaM Bool