mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.AssocList
Batteries.AssocList.forIn.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [inst : Monad m] (init : δ)
  (f : α × β → δ → m (ForInStep δ)) (a : α) (b : β) (es : Batteries.AssocList α β),
  (Batteries.AssocList.cons a b es).forIn init f = do
    let __do_lift ← f (a, b) init
    match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => es.forIn d f
-- Lean.Environment
Lean.Kernel.Exception.deepRecursion : Lean.Kernel.Exception
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.insert : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  {w : ℕ} →
    Std.Tactic.BVDecide.BVExpr.Cache aig →
      Std.Tactic.BVDecide.BVExpr w → aig.RefVec w → Std.Tactic.BVDecide.BVExpr.Cache aig
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves finite biproducts if it preserves biproducts of shape `J`
whenever `J` is a finite type.  -/
CategoryTheory.Limits.PreservesFiniteBiproducts.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms}
  [self : CategoryTheory.Limits.PreservesFiniteBiproducts F] {J : Type} [Finite J],
  CategoryTheory.Limits.PreservesBiproductsOfShape J F
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadMap_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {f : {β : Type u} → m β → m β} {x : o α} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps]
  [inst_1 : MonadFunctor n o] [inst_2 : MonadFunctorT m n],
  (Std.Do.wp (monadMap f x)).apply Q = (Std.Do.wp (MonadFunctor.monadMap (fun {β} => monadMap fun {β} => f) x)).apply Q
-- Mathlib.FieldTheory.Galois.Notation
/-- Notation for `Gal(L/K) := L ≃ₐ[K] L`.

`L ≃ₐ[K] L` will pretty-print as `Gal(L/K)` when `L` and `K` are both fields.

Although this notation works for all automorphism groups of algebras, we should only use this
notation when `L/K` is an extension of fields.
 -/
«termGal(_/_)» : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The completion of a number field at an infinite place, as a one-field structure wrapping the
completion `v.1.Completion` of `K` at the underlying absolute value.  -/
NumberField.InfinitePlace.Completion : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → Type u_1
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsInitial.to_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) {Y Z : C}
  (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (t.to Y) f = t.to Z
-- Std.Do.SPred.SPred
Std.Do.SPred.entails_cons_intro : ∀ {σs : List (Type u)} {σ : Type u} {P Q : Std.Do.SPred (σ :: σs)}, (∀ (s : σ), P s ⊢ₛ Q s) → P ⊢ₛ Q
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_congr_meas : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → (μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, MeasurableSet t → μ t = ν t)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_le_card_width : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
  A.eRank ≤ ENat.card n
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.liftPostcompIso_hom_hom : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_7, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C E A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] (Φ : A → CategoryTheory.Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (a : A),
  (F.liftPostcompIso G Φ hΦ).hom.hom a = (hΦ a).hom
-- Mathlib.Analysis.Convex.Star
starConvex_sUnion : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {S : Set (Set E)}, (∀ s ∈ S, StarConvex 𝕜 x s) → StarConvex 𝕜 x (⋃₀ S)
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.mapₐ_coe : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Rₚ : Type u_8)
  [inst_5 : CommSemiring Rₚ] [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization M Rₚ] (Aₚ : Type u_9)
  [inst_8 : CommSemiring Aₚ] [inst_9 : Algebra R Aₚ] [inst_10 : Algebra A Aₚ] [inst_11 : IsScalarTower R A Aₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type u_10) [inst_13 : CommSemiring Bₚ]
  [inst_14 : Algebra R Bₚ] [inst_15 : Algebra B Bₚ] [inst_16 : IsScalarTower R B Bₚ]
  [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] [inst_18 : Algebra Rₚ Aₚ] [inst_19 : Algebra Rₚ Bₚ]
  [inst_20 : IsScalarTower R Rₚ Aₚ] [inst_21 : IsScalarTower R Rₚ Bₚ] (f : A →ₐ[R] B),
  ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f) = ⇑(IsLocalization.map Bₚ f.toRingHom ⋯)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIso_functor_map_hom_h_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂),
  ∀ i ≤ n₀ + ↑q₁,
    CategoryTheory.IsIso
      (((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).map (CategoryTheory.homOfLE hq).op).hom.h.f i)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- There is some limit cone for `F`  -/
CategoryTheory.Limits.HasLimit.exists_limit : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor J C} [self : CategoryTheory.Limits.HasLimit F],
  Nonempty (CategoryTheory.Limits.LimitCone F)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_congr_set : ∀ {𝕜 : 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 t : Set M} {x : M}
  {n : WithTop ℕ∞}, s =ᶠ[nhds x] t → (ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.toEquiv_trans : ∀ {G : Type u_1} {H : Type u_2} {K : Type u_3} [inst : Add G] [inst_1 : Add H] [inst_2 : Add K] {a : G} {b : H} {c : K}
  (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c), (e₁.trans e₂).toEquiv = e₁.trans e₂.toEquiv
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (x : Urysohns.CU P) (x_1 : X),
  Urysohns.CU.approx 0 x x_1 = x.Uᶜ.indicator 1 x_1
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.archimedeanClassOrderIsoWithTop_apply : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] [inst_4 : Archimedean R] [inst_5 : Nontrivial R] (x : Lex (HahnSeries Γ R)),
  (HahnSeries.archimedeanClassOrderIsoWithTop Γ R) (ArchimedeanClass.mk x) = (ofLex x).orderTop
-- Batteries.Data.Float.Rat
/-- Convert this rational number to a `Float` value.  -/
Rat.toFloat : ℚ → Float
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects finite colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteColimits F.unop],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions : Lean.ToJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.mk.sizeOf_spec : ∀ (globPattern : String) (kind? : Option ℕ),
  sizeOf { globPattern := globPattern, kind? := kind? } = 1 + sizeOf globPattern + sizeOf kind?
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureInformation.toJson : Lean.Lsp.SignatureInformation → Lean.Json
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A compact exhaustion eventually covers any compact set.  -/
CompactExhaustion.exists_superset_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) {s : Set X}, IsCompact s → ∃ n, s ⊆ K n
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.ofRepr.injEq : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (repr repr_1 : E ≃ₗᵢ[𝕜] ↥(lp (fun x => 𝕜) 2)),
  ({ repr := repr } = { repr := repr_1 }) = (repr = repr_1)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Two equal natural transformations `L₁ ⟶ L₂` yield naturally isomorphic functors
`P.Comma L₁ R Q W ⥤ P.Comma L₂ R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.mapLeftEq : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (R : CategoryTheory.Functor B T) →
              {P : CategoryTheory.MorphismProperty T} →
                {Q : CategoryTheory.MorphismProperty A} →
                  {W : CategoryTheory.MorphismProperty B} →
                    [inst_3 : Q.IsMultiplicative] →
                      [inst_4 : W.IsMultiplicative] →
                        {L₁ L₂ : CategoryTheory.Functor A T} →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              (l l' : L₁ ⟶ L₂) →
                                (h : l = l') →
                                  (hl :
                                      ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
                                        P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom)) →
                                    CategoryTheory.MorphismProperty.Comma.mapLeft R l hl ≅
                                      CategoryTheory.MorphismProperty.Comma.mapLeft R l' ⋯
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.neg_symm_apply : ∀ (α : Type u) [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a : αᵒᵈ),
  (RelIso.symm (OrderIso.neg α)) a = -OrderDual.ofDual a
-- Mathlib.Data.DList.Instances
Batteries.instLawfulTraversableDList : LawfulTraversable Batteries.DList
-- Init.Data.List.Lemmas
List.mem_cons_self : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ a :: l
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for strict monotonicity of scalar multiplication by positive elements on the left,
namely `a₁ < a₂ → a₁ • b < a₂ • b` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
SMulPosStrictMono : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero β] → Prop
-- Lean.Elab.BuiltinNotation
/-- Auxiliary function for expanding the `·` notation.
The extra state `Array Syntax` contains the new binder names.
If `stx` is a `·`, we create a fresh identifier, store it in the
extra state, and return it. Otherwise, we just return `stx`.
 -/
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.expandCDot?.go : Option Lean.Name → Lean.Syntax → StateT (Array Lean.Ident) Lean.MacroM Lean.Syntax
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderType : optParam Bool false → Lean.Parser.Parser
-- Mathlib.FieldTheory.SeparablyGenerated
MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {a : ι → K}
  {F : MvPolynomial ι k},
  (MvPolynomial.aeval a) F = 0 → ∀ (i : ι), (Polynomial.aeval (a i)) (F.toPolynomialAdjoinImageCompl a i) = 0
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_le_of_trailingDegree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ} {hp : p ≠ 0},
  ↑n ≤ p.trailingDegree → n ≤ p.natTrailingDegree
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local max on `s` at `a`, `f'` is a derivative of `f` at `a` within `s`, and
both `y` and `-y` belong to the positive tangent cone of `s` at `a`, then `f' y ≤ 0`.  -/
IsLocalMinOn.hasFDerivWithinAt_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {a y : E},
  IsLocalMinOn f s a → HasFDerivWithinAt f f' s a → y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → f' y = 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
LinearIsometryEquiv.ofLinearIsometry.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (f f_1 : E →ₛₗᵢ[σ₁₂] E₂) (e_f : f = f_1) (g g_1 : E₂ →ₛₗ[σ₂₁] E) (e_g : g = g_1)
  (h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id),
  LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂ = LinearIsometryEquiv.ofLinearIsometry f_1 g_1 ⋯ ⋯
-- Mathlib.Algebra.DirectSum.Module
/-- Inclusion of each component into the direct sum.  -/
DirectSum.lof : (R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      (M : ι → Type w) →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → [DecidableEq ι] → (i : ι) → M i →ₗ[R] DirectSum ι fun i => M i
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)}
  (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (i : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (f.proj i) = (c.inj i).op
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- Constructor for morphisms in the category `LaxMonoidalFunctor C D`.  -/
CategoryTheory.LaxMonoidalFunctor.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F G : CategoryTheory.LaxMonoidalFunctor C D} →
              (f : F.toFunctor ⟶ G.toFunctor) → [CategoryTheory.NatTrans.IsMonoidal f] → F ⟶ G
-- Mathlib.FieldTheory.AbelRuffini
_private.Mathlib.FieldTheory.AbelRuffini.0.induction_step : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y z : E},
  x ∈ solvableByRad F E →
    y ∈ solvableByRad F E →
      z ∈ solvableByRad F E →
        Group.IsSolvable (minpoly F x).Gal →
          Group.IsSolvable (minpoly F y).Gal → z ∈ F⟮x, y⟯ → Group.IsSolvable (minpoly F z).Gal
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.stronglyMeasurable : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0},
  MeasureTheory.Martingale f ℱ μ → ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_pi : Complex.sin ↑Real.pi = 0
-- Mathlib.Order.Filter.Bases.Basic
Filter.mem_iff_inf_principal_compl : ∀ {α : Type u_1} {f : Filter α} {s : Set α}, s ∈ f ↔ f ⊓ Filter.principal sᶜ = ⊥
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.le_of_opNNNorm_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) {C : NNReal}, ‖f‖₊ ≤ C → ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Gal(K/k)} {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsConj φ σ → ↑(MulAction.stabilizer Gal(K/k) (NumberField.InfinitePlace.mk φ)) = {1, σ}
-- Lean.AuxRecursor
Lean.isCasesOnRecursor : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addLeftStrictMono_of_addLeftReflectLE : ∀ (N : Type u_2) [inst : Add N] [inst_1 : LinearOrder N] [AddLeftReflectLE N], AddLeftStrictMono N
-- Mathlib.RingTheory.Polynomial.GaussNorm
_private.Mathlib.RingTheory.Polynomial.GaussNorm.0.Polynomial.aux_bdd : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R)
  [ZeroHomClass F R ℝ], BddAbove {x | ∃ i, v (p.coeff i) * c ^ i = x}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Init.Coe
instCoeTCOfCoe_1 : {α : Sort u_1} → {β : Sort u_2} → [Coe α β] → CoeTC α β
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.orbit.eq_or_disjoint : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a b : X),
  MulAction.orbit G a = MulAction.orbit G b ∨ Disjoint (MulAction.orbit G a) (MulAction.orbit G b)
-- Mathlib.Data.Seq.Defs
/-- Prepend an element to a sequence  -/
Stream'.Seq.cons : {α : Type u} → α → Stream'.Seq α → Stream'.Seq α
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.quasiMeasurePreserving_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}, MeasureTheory.Measure.QuasiMeasurePreserving Prod.fst (μ.prod ν) μ
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctor_η : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Discrete.addMonoidalFunctor F) =
    CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.Topology.UrysohnsLemma
/-- A variation of Urysohn's lemma. In a `R1Space X`, for a closed set `t` and a relatively
compact open set `s` such that `t ⊆ s`, there is a continuous function `f` supported in `s`,
`f x = 1` on `t` and `0 ≤ f x ≤ 1`.  -/
exists_tsupport_one_of_isOpen_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {s t : Set X},
  IsOpen s →
    IsCompact (closure s) → IsClosed t → t ⊆ s → ∃ f, tsupport ⇑f ⊆ s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.isUniformizer_of_maximalIdeal_eq_span : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [inst_2 : v.IsRankOneDiscrete] {r : ↥v.valuationSubring},
  IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {r} → v.IsUniformizer ↑r
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonApplyWorkspaceEditParams.toJson : Lean.Lsp.ApplyWorkspaceEditParams → Lean.Json
-- Init.Tactics
/-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
The syntax is the same as term-mode `let rec`.

The tactic supports all the same syntax variants and options as the `let` term.
 -/
Lean.Parser.Tactic.letrec : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.proof : Lean.Meta.Grind.InjectiveTheorem → Lean.Expr
-- Init.Data.Float.Model.Float
Float.instDecidableEqModel.decEq : (x x_1 : Float.Model) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.instHasFactorizationOppositeOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.HasFactorization W₂], W₂.op.HasFactorization W₁.op
-- Init.Data.Sum.Basic
/-- Swaps the factors of a sum type.

The constructor `Sum.inl` is replaced with `Sum.inr`, and vice versa.
 -/
Sum.swap : {α : Type u_1} → {β : Type u_2} → α ⊕ β → β ⊕ α
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (η : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
  (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ η).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight η (F.obj X)
-- Std.Tactic.BVDecide.LRAT.Checker
/-- Check whether `lratProof` is a valid LRAT certificate for the unsatisfiability of `cnf`.
 -/
Std.Tactic.BVDecide.LRAT.check : Array Std.Tactic.BVDecide.LRAT.IntAction → Std.Sat.CNF ℕ → Bool
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.Functor.id C).OplaxMonoidal
-- Mathlib.Tactic.Basic
Mathlib.Tactic.withResetServerInfo.Result.mk.inj : ∀ {α : Type} {result? : Option α} {msgs : Lean.MessageLog} {trees : Lean.PersistentArray Lean.Elab.InfoTree}
  {result?_1 : Option α} {msgs_1 : Lean.MessageLog} {trees_1 : Lean.PersistentArray Lean.Elab.InfoTree},
  { result? := result?, msgs := msgs, trees := trees } = { result? := result?_1, msgs := msgs_1, trees := trees_1 } →
    result? = result?_1 ∧ msgs = msgs_1 ∧ trees = trees_1
-- Init.Data.Iterators.Combinators.FilterMap
/-- If `it` is an iterator, then `it.map f` is another iterator that applies a
function `f` to all values emitted by `it` and emits the result.

In situations where `f` is monadic, use `mapM` instead.

**Marble diagram:**

```text
it         ---a --b --c --d -e ----⊥
it.map     ---a'--b'--c'--d'-e'----⊥
```

(given that `f a = a'`, `f b = b'` etc.)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.Iter.map : {α β γ : Type w} → [Std.Iterator α Id β] → (f : β → γ) → Std.Iter β → Std.Iter γ