mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_cosh : Measurable Real.cosh
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_le_of_infEDist`.

---

Bounding the Hausdorff edistance by bounding the edistance of any point
in each set to the other set  -/
EMetric.hausdorffEdist_le_of_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
  (∀ x ∈ s, Metric.infEDist x t ≤ r) → (∀ x ∈ t, Metric.infEDist x s ≤ r) → Metric.hausdorffEDist s t ≤ r
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.isIso_functor : ∀ {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] (e : CategoryTheory.IsoCat C D), e.functor.IsIso
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.isAlgebraic_of_not_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  ¬Function.Injective ⇑(algebraMap R A) → Algebra.IsAlgebraic R A
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.mk : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (F : X → Type u_3)
  [inst_2 : (x : X) → TopologicalSpace (F x)] [∀ (x : X), DiscreteTopology (F x)]
  (e : (x : X) → Bundle.Trivialization (F x) f), (∀ (x : X), x ∈ (e x).baseSet) → IsCoveringMap f
-- Lean.Parser.Term
Lean.Parser.Term.letExpr : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.trans'_target : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source),
  (f.trans' g e).target = g.target
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The `MonoidHom` associated to an inclusion of `Submonoid`s.  -/
Submonoid.inclusion : {M : Type u_1} → [inst : MulOneClass M] → {S T : Submonoid M} → S ≤ T → ↥S →* ↥T
-- Mathlib.Data.Set.Piecewise
Set.piecewise_empty : ∀ {α : Type u_1} {δ : α → Sort u_7} (f g : (i : α) → δ i) [inst : (i : α) → Decidable (i ∈ ∅)], ∅.piecewise f g = g
-- Mathlib.Order.UpperLower.Basic
not_bddAbove_Ici : ∀ {α : Type u_1} [inst : Preorder α] (a : α) [NoMaxOrder α], ¬BddAbove (Set.Ici a)
-- Plausible.Testable
Plausible.Testable.forallTypesTestable : {var : String} →
  {f : Type → Prop} → [Plausible.Testable (f ℤ)] → Plausible.Testable (Plausible.NamedBinder var (∀ (x : Type), f x))
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processNonReserved : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_iff_exists_natCard_le_addOrderOf : ∀ {α : Type u_1} [inst : AddGroup α] [Finite α], IsAddCyclic α ↔ ∃ g, Nat.card α ≤ addOrderOf g
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Given a tower `L / ↥E / L' / K` of field extensions, where `E` is an `L'`-intermediate field of
`L`, reinterpret `E` as a `K`-intermediate field of `L`.  -/
IntermediateField.restrictScalars : (K : Type u_1) →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field L'] →
            [inst_3 : Algebra K L] →
              [inst_4 : Algebra K L'] →
                [inst_5 : Algebra L' L] → [IsScalarTower K L' L] → IntermediateField L' L → IntermediateField K L
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyoneda.eq_1 : AddCommGrpCat.coyoneda =
  {
    obj := fun M =>
      { obj := fun N => AddCommGrpCat.of (↑(Opposite.unop M) →+ ↑N),
        map := fun {X Y} f => AddCommGrpCat.ofHom (AddMonoidHom.compHom (AddCommGrpCat.Hom.hom f)), map_id := ⋯,
        map_comp := ⋯ },
    map := fun {X Y} f =>
      { app := fun N => AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f.unop).compHom', naturality := ⋯ },
    map_id := AddCommGrpCat.coyoneda._proof_4, map_comp := @AddCommGrpCat.coyoneda._proof_5 }
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.ind : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {β : OreLocalization S X → Prop},
  (∀ (r : X) (s : ↥S), β (r /ₒ s)) → ∀ (q : OreLocalization S X), β q
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_of_subsingleton : ∀ {α : Type u} [Subsingleton α] {s : Set α}, s.Subsingleton
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- The quotient by a two-sided ideal that is maximal as a left ideal is a division ring.
This is a `def` rather than `instance`, since users
will have computable inverses (and `qsmul`, `ratCast`) in some applications.

See note [reducible non-instances].  -/
Ideal.Quotient.divisionRing : {R : Type u_3} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → [I.IsMaximal] → DivisionRing (R ⧸ I)
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.copy_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) {g : C ⟶ D} (h : Homotopy f.hom g),
  (f.copy h).inv = f.inv
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X},
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x ↔
    AlgebraicGeometry.LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f)
-- Init.Data.Format.Basic
/-- Increases the indentation level by the default amount.
 -/
Std.Format.nestD : Std.Format → Std.Format
-- Lean.Meta.Tactic.Split
/-- - `eqs` are free variables `h_eq : discr = discrVar`. `eqs.size == discrs.size`
- `altEqs` are free variables of the form `h_altEq : discr = pattern`. `altEqs.size = numDiscrEqs ≤ discrs.size`
This method executes `k altEqsNew subst` where
- `altEqsNew` are fresh free variables of the form `h_altEqNew : discrVar = pattern`
- `subst` are terms of the form `h_eq.trans h_altEqNew : discr = pattern`. We use `subst` later to replace occurrences of `h_altEq` with `h_eq.trans h_altEqNew`.
 -/
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.generalizeMatchDiscrs.withNewAltEqs : Lean.Meta.MatcherInfo →
  Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with negation.  -/
InnerProductSpace.laplacianWithin_neg : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E} {s : Set E},
  UniqueDiffOn ℝ s → x ∈ s → InnerProductSpace.laplacianWithin (-f) s x = -InnerProductSpace.laplacianWithin f s x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.congrIsometry_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H),
  (TensorProduct.congrIsometry f g).symm = TensorProduct.congrIsometry f.symm g.symm
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.OLeanEntry.mk : Lean.KeyedDeclsAttribute.Key → Lean.Name → Lean.KeyedDeclsAttribute.OLeanEntry
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousInv.mk : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : Inv G], (Continuous fun a => a⁻¹) → ContinuousInv G
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverMincard_union_le : ∀ {X : Type u_1} (T : X → X) (F G : Set X) (U : SetRel X X) (n : ℕ),
  Dynamics.coverMincard T (F ∪ G) U n ≤ Dynamics.coverMincard T F U n + Dynamics.coverMincard T G U n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_le_maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instAddOffset : Add Std.Time.Hour.Offset
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.mk.sizeOf_spec : ∀ (hoverInfo : Lean.Server.Completion.HoverInfo) (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.CompletionInfo),
  sizeOf { hoverInfo := hoverInfo, ctx := ctx, info := info } = 1 + sizeOf hoverInfo + sizeOf ctx + sizeOf info
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldl_eq_foldl_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.TreeSet.foldl f init t = List.foldl f init t.toList
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.neg_pos_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, 0 < -a ↔ a < 0
-- Mathlib.NumberTheory.FLT.Polynomial
/-- Nonsolvability of the Fermat-Catalan equation.  -/
Polynomial.flt_catalan : ∀ {k : Type u_1} [inst : Field k] {p q r : ℕ},
  p ≠ 0 →
    q ≠ 0 →
      r ≠ 0 →
        q * r + r * p + p * q ≤ p * q * r →
          ↑p ≠ 0 →
            ↑q ≠ 0 →
              ↑r ≠ 0 →
                ∀ {a b c : Polynomial k},
                  a ≠ 0 →
                    b ≠ 0 →
                      c ≠ 0 →
                        IsCoprime a b →
                          ∀ {u v w : k},
                            u ≠ 0 →
                              v ≠ 0 →
                                w ≠ 0 →
                                  Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0 →
                                    a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f] [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.UniversallyOpen f] [AlgebraicGeometry.IsIntegral S] [AlgebraicGeometry.IsLocallyNoetherian S],
  AlgebraicGeometry.IsIntegral X
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.modThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionOfShapeOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] [W.IsMultiplicative]
  [W.RespectsIso] [CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{w, w, v, u} W],
  W.IsStableUnderTransfiniteCompositionOfShape J
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftEquiv_symm_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (f : L →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p], (PerfectRing.liftEquiv M i p).symm f = f.comp i
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.liftEquiv_symm_apply_coe : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  (g : S →+* WittVector p R) (k : ℕ), ↑(WittVector.liftEquiv.symm g) k = (WittVector.truncate k).comp g
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lift_card_sInf_compl_le : ∀ (s : Set Ordinal.{u}), Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ Cardinal.mk ↑s
-- Mathlib.Order.Completion
DedekindCut.ofObject_eq_principal : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Concept.ofObject (fun x1 x2 => x1 ≤ x2) a = DedekindCut.principal a
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.apply_eq_of_lt_firstDiff : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, n < PiNat.firstDiff x y → x n = y n
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {X Y : CategoryTheory.Mon (CategoryTheory.Functor C D)} (f : X ⟶ Y)
  (X_1 : C), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_of_frequently_le' : ∀ {α : Type u_6} {β : Type u_7} [inst : CompleteLattice β] {f : Filter α} {u : α → β} {x : β},
  (∃ᶠ (a : α) in f, u a ≤ x) → Filter.liminf u f ≤ x
-- Mathlib.Order.Filter.Pointwise
Filter.pureAddHom_apply : ∀ {α : Type u_2} [inst : Add α] (a : α), Filter.pureAddHom a = pure a
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_cons : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream'.WSeq α),
  Stream'.WSeq.map f (Stream'.WSeq.cons a s) = Stream'.WSeq.cons (f a) (Stream'.WSeq.map f s)
-- Mathlib.Analysis.Complex.Basic
/-- The algebra structure from `Algebra.complexToReal` is a normed algebra.  -/
NormedAlgebra.complexToReal : {A : Type u_2} → [inst : SeminormedRing A] → [NormedAlgebra ℂ A] → NormedAlgebra ℝ A
-- Mathlib.Topology.Order
coinduced_nhdsAdjoint : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (l : Filter α),
  TopologicalSpace.coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (Filter.map f l)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Init.Grind.AC
Lean.Grind.AC.norm_aci : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.Commutative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (e : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq),
  e.toSeq.erase0.sort.beq' s = true → Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_symm_comm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {α : r₁ ⟶ r₂}
  {β : r₂ ⟶ r₁},
  CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.id r₁ →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₁).symm β)
        ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α) =
      CategoryTheory.CategoryStruct.id l₁
-- Mathlib.Analysis.Analytic.Binomial
Real.one_div_sub_hasFPowerSeriesOnBall_zero : ∀ {r : ℝ},
  r ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (r - x)) (FormalMultilinearSeries.ofScalars ℝ fun n => (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ
-- Mathlib.Data.Part
Part.left_dom_of_inter_dom : ∀ {α : Type u_1} [inst : Inter α] {a b : Part α}, (a ∩ b).Dom → a.Dom
-- Lean.Elab.PreDefinition.Structural.FindRecArg
_private.Lean.Elab.PreDefinition.Structural.FindRecArg.0.Lean.Elab.Structural.dedup : {m : Type → Type u_1} → {α : Type} → [Monad m] → (α → α → m Bool) → Array α → m (Array α)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.pow_right_injective_iff_pow_injective : ∀ {M : Type u_1} [inst : Monoid M] {n : M}, (Function.Injective fun m => n ^ m) ↔ Function.Injective (Submonoid.pow n)
-- Lean.Parser.Do
Lean.Parser.Term.doIfLetPure.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f] {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x (CategoryTheory.inv f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f)
        h) =
    h
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The `d`th coefficient of a power of a multivariate power series
is the sum, indexed by `finsuppAntidiag (Finset.range n) d`, of products of coefficients  -/
MvPowerSeries.coeff_pow : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ}
  (d : σ →₀ ℕ),
  (MvPowerSeries.coeff d) (f ^ n) =
    ∑ l ∈ (Finset.range n).finsuppAntidiag d, ∏ i ∈ Finset.range n, (MvPowerSeries.coeff (l i)) f
-- Mathlib.Data.Multiset.Functor
Multiset.fmap_def : ∀ {α' β' : Type u_1} {s : Multiset α'} (f : α' → β'), f <$> s = Multiset.map f s
-- Std.Http.Internal.Char
Std.Http.Internal.Char.qdtext.eq_2 : Std.Http.Internal.Char.qdtext ' ' = (true || decide ('#' ≤ ' ' ∧ ' ' ≤ '[') || decide (']' ≤ ' ' ∧ ' ' ≤ '~'))
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A functor has a colimit iff there exists a lub.  -/
Preorder.hasColimit_iff_hasLUB : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasColimit F ↔ ∃ x, IsLUB (Set.range F.obj) x
-- Std.Http.Protocol.H1.Reader
/-- The incoming message head.
 -/
Std.Http.Protocol.H1.Reader.messageHead : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Message.Head dir
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}}, forM t f = forM t.toList f
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {n : WithTop ℕ∞} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B]
  [inst_18 : FiberBundle F₁ E₁] [inst_19 : VectorBundle 𝕜 F₁ E₁] [inst_20 : FiberBundle F₂ E₂]
  [inst_21 : VectorBundle 𝕜 F₂ E₂] [inst_22 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_23 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB],
  VectorPrebundle.IsContMDiff IB (Bundle.ContinuousLinearMap.vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂) n
-- Mathlib.Order.Filter.Bases.Basic
/-- `IsAntitoneBasis s` means the image of `s` is a filter basis such that `s` is decreasing.  -/
Filter.IsAntitoneBasis : {α : Type u_1} → {ι'' : Type u_6} → [Preorder ι''] → (ι'' → Set α) → Prop
-- Init.Data.UInt.Bitwise
UInt64.toBitVec_xor : ∀ (a b : UInt64), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.IsLocalization.primeHeight_comap : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsLocalization S A] (J : Ideal A) [inst_4 : J.IsPrime],
  Ideal.primeHeight✝ (Ideal.comap (algebraMap R A) J) = Ideal.primeHeight✝ J
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.decodePosNum.match_1.eq_3 : ∀ (motive : List Bool → Sort u_1) (x : List Bool) (h_1 : (l : List Bool) → motive (false :: l))
  (h_2 : (l : List Bool) → motive (true :: l)) (h_3 : (x : List Bool) → motive x),
  (∀ (l : List Bool), x = false :: l → False) →
    (∀ (l : List Bool), x = true :: l → False) →
      (match x with
        | false :: l => h_1 l
        | true :: l => h_2 l
        | x => h_3 x) =
        h_3 x
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.out_truncateFun : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R),
  (WittVector.truncateFun n x).out = WittVector.init n x
-- Mathlib.Analysis.CStarAlgebra.Spectrum
_private.Mathlib.Analysis.CStarAlgebra.Spectrum.0.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_injective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective FreeAddGroup.toWord
-- Init.Data.Float.Float32
/-- Divides 32-bit floating-point numbers according to IEEE 754. Typically used via the `/` operator.

In Lean, division by zero typically yields zero. For `Float32`, it instead yields either `Inf`,
`-Inf`, or `NaN`.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C division operator.
 -/
Float32.div : Float32 → Float32 → Float32
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.continuousOn_rpow : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : NonnegSpectrumClass ℝ A]
  [inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [CompleteSpace A] (r : ℝ),
  ContinuousOn (fun x => x ^ r) {a | IsStrictlyPositive a}
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.mkHom_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {s t : CategoryTheory.Limits.Trident f} (k : s.pt ⟶ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp k t.ι = s.ι) CategoryTheory.Limits.Trident.mkHom._auto_1),
  (CategoryTheory.Limits.Trident.mkHom k w).hom = k
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiff.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f g : M → G}, ContMDiff I' I n f → ContMDiff I' I n g → ContMDiff I' I n fun x => f x / g x
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- the cochain complex must have homology  -/
CategoryTheory.InjectiveResolution.hasHomology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.InjectiveResolution Z) (i : ℕ),
  HomologicalComplex.HasHomology self.cocomplex i
-- Mathlib.Topology.Algebra.ConstMulAction
continuous_const_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] [inst_4 : TopologicalSpace β] {f : β → α} (c : G),
  (Continuous fun x => c • f x) ↔ Continuous f