mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_zero : ↑0 = 0
-- Mathlib.Data.List.Sym
List.sym2.eq_2 : ∀ {α : Type u_1} (x_1 : α) (xs : List α), (x_1 :: xs).sym2 = List.map (fun y => s(x_1, y)) (x_1 :: xs) ++ xs.sym2
-- Lean.LocalContext
Lean.LocalContext.mk : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl →
  Lean.PersistentArray (Option Lean.LocalDecl) → Lean.FVarIdMap Lean.Name → Lean.LocalContext
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedFunctor_map_coe : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [inst_2 : HasFibers p] (S : 𝒮) {X Y : HasFibers.Fib p S} (φ : X ⟶ Y),
  ↑((HasFibers.inducedFunctor p S).map φ) = (HasFibers.ι S).map φ
-- Mathlib.Data.Stream.Defs
/-- An auxiliary definition for `Stream'.inits`.  -/
Stream'.initsCore : {α : Type u} → List α → Stream' α → Stream' (List α)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The intersection of two blocks is a block.  -/
MulAction.IsBlock.inter : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B₁ B₂ : Set X},
  MulAction.IsBlock G B₁ → MulAction.IsBlock G B₂ → MulAction.IsBlock G (B₁ ∩ B₂)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instPowPNat : Pow Complex.UnitDisc ℕ+
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_differentiable_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E},
  Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.ker_monodromyPerm : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x})),
  (⋯.monodromyPerm x).ker = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_zero : ∀ {α : Type u} [inst : Zero α] {β : Type u_1} (f : α → β), WithTop.map f 0 = ↑(f 0)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_inv : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {f : α → 𝕜} {g : α → 𝕜'}, ((fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹) ↔ f =Θ[l] g
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_norm_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β), MeasureTheory.HasFiniteIntegral (fun a => ‖f a‖) μ ↔ MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.mem_antidiagonalTuple : ∀ {n k : ℕ} {x : Fin k → ℕ}, x ∈ List.Nat.antidiagonalTuple k n ↔ ∑ i, x i = n
-- Lean.Meta.Closure
Lean.Meta.Closure.State.levelParams : Lean.Meta.Closure.State → Array Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `arsinh` is defined using a logarithm, `arsinh x = log (x + √(1 + x^2))`.  -/
Real.arsinh : ℝ → ℝ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool) (sz : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.filter f (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_1 =
    match f k' v' with
    | false =>
      match Std.DTreeMap.Internal.Impl.filter f l' ⋯ with
      | { impl := l'_1, balanced_impl := hl' } =>
        match Std.DTreeMap.Internal.Impl.filter f r' ⋯ with
        | { impl := r'_1, balanced_impl := hr' } => { impl := (l'_1.link2 r'_1 ⋯ ⋯).impl, balanced_impl := ⋯ }
    | true =>
      match Std.DTreeMap.Internal.Impl.filter f l' ⋯ with
      | { impl := l'_1, balanced_impl := hl' } =>
        match Std.DTreeMap.Internal.Impl.filter f r' ⋯ with
        | { impl := r'_1, balanced_impl := hr' } =>
          { impl := (Std.DTreeMap.Internal.Impl.link k' v' l'_1 r'_1 ⋯ ⋯).impl, balanced_impl := ⋯ }
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.pullbackSpecIso_hom_base_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (TensorProduct R S T)))) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) h)
-- Mathlib.NumberTheory.Padics.Complex
/-- The valuation on `PadicAlgCl p` has rank one.  -/
PadicAlgCl.instRankOneNNRealV : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Valued.v.RankOne
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.lowerBounds_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → s.Nonempty → lowerBounds s ⊆ s
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.transpose : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → A.transpose.IsHermitian
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_rfl : ∀ {V : Type u_1} [inst : Quiver V] {X Y : V} (f : X ⟶ Y), Quiver.homOfEq f ⋯ ⋯ = f
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom_infinite : ∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} (C : G.ComponentCompl L) (h : K ⊆ L),
  (↑C).Infinite → (↑(SimpleGraph.ComponentCompl.hom h C)).Infinite
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap (φ + φ') =
    CategoryTheory.ShortComplex.homologyMap φ + CategoryTheory.ShortComplex.homologyMap φ'
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.State.mk.inj : ∀ {f fType : Lean.Expr} {fArgs : Array Lean.Expr} {args : List Lean.Elab.Term.Arg}
  {namedArgs : List Lean.Elab.Term.NamedArg} {expectedType? : Option Lean.Expr}
  {etaArgs : Array (Lean.Name × Lean.Expr)} {toSetErrorCtx instMVars : Array Lean.MVarId} {propagateExpected : Bool}
  {resultTypeOutParam? : Option Lean.MVarId} {foundNamedArgs : Array Lean.Name} {f_1 fType_1 : Lean.Expr}
  {fArgs_1 : Array Lean.Expr} {args_1 : List Lean.Elab.Term.Arg} {namedArgs_1 : List Lean.Elab.Term.NamedArg}
  {expectedType?_1 : Option Lean.Expr} {etaArgs_1 : Array (Lean.Name × Lean.Expr)}
  {toSetErrorCtx_1 instMVars_1 : Array Lean.MVarId} {propagateExpected_1 : Bool}
  {resultTypeOutParam?_1 : Option Lean.MVarId} {foundNamedArgs_1 : Array Lean.Name},
  { f := f, fType := fType, fArgs := fArgs, args := args, namedArgs := namedArgs, expectedType? := expectedType?,
        etaArgs := etaArgs, toSetErrorCtx := toSetErrorCtx, instMVars := instMVars,
        propagateExpected := propagateExpected, resultTypeOutParam? := resultTypeOutParam?,
        foundNamedArgs := foundNamedArgs } =
      { f := f_1, fType := fType_1, fArgs := fArgs_1, args := args_1, namedArgs := namedArgs_1,
        expectedType? := expectedType?_1, etaArgs := etaArgs_1, toSetErrorCtx := toSetErrorCtx_1,
        instMVars := instMVars_1, propagateExpected := propagateExpected_1,
        resultTypeOutParam? := resultTypeOutParam?_1, foundNamedArgs := foundNamedArgs_1 } →
    f = f_1 ∧
      fType = fType_1 ∧
        fArgs = fArgs_1 ∧
          args = args_1 ∧
            namedArgs = namedArgs_1 ∧
              expectedType? = expectedType?_1 ∧
                etaArgs = etaArgs_1 ∧
                  toSetErrorCtx = toSetErrorCtx_1 ∧
                    instMVars = instMVars_1 ∧
                      propagateExpected = propagateExpected_1 ∧
                        resultTypeOutParam? = resultTypeOutParam?_1 ∧ foundNamedArgs = foundNamedArgs_1
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.add_comm_of_mem_isAddCommutative : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [IsAddCommutative ↥H] {a b : G}, a ∈ H → b ∈ H → a + b = b + a
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) h_1))
-- Mathlib.Geometry.Manifold.SmoothEmbedding
/-- Every `ModelWithCorners 𝕜 E H` is a smooth embedding when viewed as a map `H → E`.  -/
ModelWithCorners.isSmoothEmbedding : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] {H : Type u_6} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {n : ℕ},
  Manifold.IsSmoothEmbedding I (modelWithCornersSelf 𝕜 E₁) ↑n ↑I
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLT.toSMulPosMono : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero β]
  [SMulPosReflectLT α β], SMulPosMono α β
-- Mathlib.Order.SymmDiff
bihimp_of_le : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ≤ a → bihimp a b = a ⇨ b
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.c_eq_algebraMap : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R], MvPowerSeries.C = algebraMap R (MvPowerSeries σ R)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ : ∀ (X : TopCat),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) SSet.stdSimplex.toSSetObjI)
        (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I)) =
    TopCat.toSSet.map TopCat.ι₁
-- Mathlib.Order.RelClasses
/-- Set notation form of `Eq.ge` -/
Eq.superset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a = b → b ⊆ a
-- Lean.Parser.Do
Lean.Parser.Term.doRepeatUntil.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Nat.Cast.Basic
/-- We don't use `RingHomClass` here, since that might cause type-class slowdown for
`Subsingleton`.  -/
Nat.uniqueRingHom : {R : Type u_3} → [inst : NonAssocSemiring R] → Unique (ℕ →+* R)
-- Mathlib.Order.Filter.Pointwise
Filter.sub_bot : ∀ {α : Type u_2} [inst : Sub α] {f : Filter α}, f - ⊥ = ⊥
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toEquiv_eq_coe : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  f.toEquiv = ↑f
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Isomorphic functors become equal when lowered to `Subobject`.
(It's not as evil as usual to talk about equality between functors
because the categories are thin and skeletal.)  -/
CategoryTheory.Subobject.lower_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)) (h : F₁ ≅ F₂),
  CategoryTheory.Subobject.lower F₁ = CategoryTheory.Subobject.lower F₂
-- Mathlib.CategoryTheory.Grothendieck
/-- The Grothendieck construction is functorial: a natural transformation `α : F ⟶ G` induces
a functor `Grothendieck.map : Grothendieck F ⥤ Grothendieck G`.
 -/
CategoryTheory.Grothendieck.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C CategoryTheory.Cat} →
      (F ⟶ G) → CategoryTheory.Functor (CategoryTheory.Grothendieck F) (CategoryTheory.Grothendieck G)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.coe_mk : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (d : X → X → R)
  (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z),
  ⇑{ toFun := d, refl' := refl, symm' := symm, triangle' := triangle } = d
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.innerₛₗ.congr_simp : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [inst_10 : StarModule ℂ A], CStarModule.innerₛₗ = CStarModule.innerₛₗ
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_eq_zero_iff : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] (a : A), autoParam (IsSelfAdjoint a) CFC.negPart_eq_zero_iff._auto_1 → (a⁻ = 0 ↔ 0 ≤ a)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.mem_cons_iff : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  {x : ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl},
  x ∈ Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl ↔ x = (exp, coef) ∨ x ∈ tl
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.integrate_mono : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure]
  {f g : CompactlySupportedContinuousMap B ℝ}, f ≤ g → (H.integrate μA μC) f ≤ (H.integrate μA μC) g
-- Mathlib.RingTheory.Valuation.FiniteField
/-- **Alias** of `FiniteField.instIsTrivialOn`. -/
Valuation.FiniteField.instIsTrivialOn : ∀ {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [inst : Field Fq] [Finite Fq] [inst_2 : Ring A] [inst_3 : Algebra Fq A]
  [inst_4 : LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ), Valuation.IsTrivialOn Fq v
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the forward direction of `OpenPartialHomeomorph.IsImage.iff_preimage_eq`. -/
OpenPartialHomeomorph.IsImage.preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A positive definite quadratic form is positive on nonzero vectors.  -/
QuadraticMap.PosDef : {M : Type u_4} →
  {N : Type u_5} →
    {R₂ : Type u} →
      [inst : CommSemiring R₂] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R₂ M] →
            [PartialOrder N] → [inst_4 : AddCommMonoid N] → [inst_5 : Module R₂ N] → QuadraticMap R₂ M N → Prop
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` expressed with a norm instead of a distance.  -/
MeasureTheory.tendstoInMeasure_iff_norm : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddCommGroup E] {l : Filter ι} {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖}) l (nhds 0)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToExprIProp.toExpr : Mathlib.Tactic.ITauto.IProp → Lean.Expr
-- Mathlib.Algebra.Algebra.Rat
NNRat.instSMulCommClass' : ∀ {R : Type u_2} {S : Type u_3} [inst : DivisionSemiring S] [inst_1 : CharZero S] [inst_2 : SMul R S]
  [SMulCommClass S R S], SMulCommClass R ℚ≥0 S
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.inclusion_injective : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂),
  Function.Injective ⇑(StarSubalgebra.inclusion h)
-- Mathlib.GroupTheory.Sylow
/-- A sylow subgroup of G is also a sylow subgroup of a subgroup of G.  -/
Sylow.subtype : {p : ℕ} → {G : Type u_1} → [inst : Group G] → (P : Sylow p G) → {N : Subgroup G} → ↑P ≤ N → Sylow p ↥N
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup Mᵃᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_mul_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊
-- Init.Core
NonScalar.mk.injEq : ∀ (val val_1 : ℕ), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.ihomCurryIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  (CategoryTheory.MonoidalClosed.ihomCurryIso x y z).hom = CategoryTheory.MonoidalClosed.ihomCurry x y z
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_of_adjoin_splits : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E},
  (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    ∀ {L : IntermediateField F E} (f : ↥L →ₐ[F] K), IntermediateField.adjoin F S = ⊤ → ∃ φ, φ.comp L.val = f
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.GeometricallyIrreducible.iff_geometricallyIrreducible_fiber : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S),
  AlgebraicGeometry.GeometricallyIrreducible f ↔
    ∀ (s : ↥S), AlgebraicGeometry.GeometricallyIrreducible (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Init.Grind.Ring.Basic
/-- Scalar multiplication by natural numbers.  -/
Lean.Grind.Semiring.nsmul : {α : Type u} → [self : Lean.Grind.Semiring α] → SMul ℕ α
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.denote : Nat.Internal.Linear.Context → Nat.Internal.SOM.Poly → ℕ
-- Mathlib.Order.Preorder.Chain
/-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`.  -/
IsChain : {α : Type u_1} → (α → α → Prop) → Set α → Prop
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.rightUnitor_hom_apply : ∀ {X : Type u} {x : X} {p : PUnit.{u + 1}},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) (x, p) = x
-- Mathlib.Algebra.Field.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
Field.zpow_succ' : ∀ {K : Type u} [self : Field K] (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- A "proxy type" equivalent to `Affine.Simplex.PointsWithCircumcenterIndex` that is constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. See `Affine.Simplex.PointsWithCircumcenterIndex.proxyTypeEquiv` for the equivalence. (Generated by the `proxy_equiv%` elaborator.) -/
Affine.Simplex.PointsWithCircumcenterIndex.proxyType : ℕ → Type
-- Mathlib.Tactic.NormDet
/-- The `norm_det` simproc normalizes determinants of matrices written using `!![...]`
notation over a commutative ring.  -/
norm_det : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- When `α` is `Finite`, every `f : PreLp E p` satisfies `Memℓp f p`.  -/
Memℓp.all : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [Finite α]
  (f : (i : α) → E i), Memℓp f p
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_add' : ∀ {m n : ℤ}, Odd (m + n) ↔ (Odd n ↔ Even m)
-- Mathlib.Data.Finset.Insert
Finset.cons_eq_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s), Finset.cons a s h = insert a s
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.comapAddSubgroup_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (f : G ≃+ H) (H_1 : AddSubgroup G),
  (RelIso.symm f.comapAddSubgroup) H_1 = AddSubgroup.comap (↑f.symm) H_1
-- Init.Data.Nat.Lemmas
Nat.add_succ_sub_one : ∀ (m n : ℕ), m + n.succ - 1 = m + n
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.isInducing_toProd : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  Topology.IsInducing ⇑(Bundle.TotalSpace.toProd B F)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- Special case of the **Plünnecke-Ruzsa inequality**. Division version.  -/
Finset.pluennecke_ruzsa_inequality_pow_div : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (n : ℕ), ↑(B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ n * ↑A.card
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure.step : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} (s t : σ), t ∈ M.step s none → M.εClosure S s → M.εClosure S t
-- Mathlib.CategoryTheory.Category.Pointed
/-- **Alias** of `Pointed.of`.

---

Turns a point into a pointed type.  -/
Prod.Pointed : {X : Type u_1} → X → Pointed
-- Lean.Declaration
/-- Returns all top-level names to be defined by adding this declaration to the environment, i.e.
excluding nested helper declarations generated automatically.
 -/
Lean.Declaration.getTopLevelNames : Lean.Declaration → List Lean.Name
-- Mathlib.LinearAlgebra.Dimension.Free
rank_le_iff_exists_linearMap : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] [Module.Free R M₁] [StrongRankCondition R],
  Module.rank R M ≤ Module.rank R M₁ ↔ ∃ f, Function.Injective ⇑f