mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.hasColimit_comp_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E}, CategoryTheory.Limits.HasColimit (F.comp G) ↔ CategoryTheory.Limits.HasColimit G
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex that was constructed using `CWComplex.mkFinite` is finite.  -/
Topology.CWComplex.finite_mkFinite : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X)
  (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C), Topology.RelCWComplex.Finite C
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite  -/
Matrix.posSemidef_conjTranspose_mul_self : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype m] [Finite n] [StarOrderedRing R] (A : Matrix m n R), (A.conjTranspose * A).PosSemidef
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get_eq_get? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (l : Std.DTreeMap.Internal.Impl α β) {h : k ∈ l}, some (l.get k h) = l.get? k
-- Mathlib.Data.Stream.Init
Stream'.get_succ_cons : ∀ {α : Type u} (n : ℕ) (s : Stream' α) (x : α), (Stream'.cons x s).get n.succ = s.get n
-- Init.Data.String.Basic
String.toList_injective : ∀ {s₁ s₂ : String}, s₁.toList = s₂.toList → s₁ = s₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Const.toList t) = none ↔ t.contains k = false
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- The filter of sets `s` such that `sᶜ` has finite measure.  -/
MeasureTheory.Measure.cofinite : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Filter α
-- Mathlib.Algebra.Ring.Subring.Defs
/-- The natural ring hom from a subring of ring `R` to `R`.  -/
Subring.subtype : {R : Type u} → [inst : NonAssocRing R] → (s : Subring R) → ↥s →+* R
-- Mathlib.NumberTheory.Padics.PadicNumbers
Int.padicValuation_lt_one_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x : ℤ}, (Int.padicValuation p) x < 1 ↔ ↑p ∣ x
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- A morphism of locally ringed spaces is a morphism of ringed spaces
such that the morphisms induced on stalks are local ring homomorphisms.  -/
AlgebraicGeometry.LocallyRingedSpace.Hom : AlgebraicGeometry.LocallyRingedSpace → AlgebraicGeometry.LocallyRingedSpace → Type u
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, (∀ (b : B), m.as.app b = n.as.app b) → m = n
-- Std.Time.Internal.Bounded
_private.Std.Time.Internal.Bounded.0.Int.tdiv.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_1 m n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inter_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))],
  (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mk.inj : ∀ {R : Type u} {inst : NonUnitalNonAssocSemiring R} {toAddSubmonoid : AddSubmonoid R}
  {mul_mem' : ∀ {a b : R}, a ∈ toAddSubmonoid.carrier → b ∈ toAddSubmonoid.carrier → a * b ∈ toAddSubmonoid.carrier}
  {toAddSubmonoid_1 : AddSubmonoid R}
  {mul_mem'_1 :
    ∀ {a b : R}, a ∈ toAddSubmonoid_1.carrier → b ∈ toAddSubmonoid_1.carrier → a * b ∈ toAddSubmonoid_1.carrier},
  { toAddSubmonoid := toAddSubmonoid, mul_mem' := mul_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, mul_mem' := mul_mem'_1 } →
    toAddSubmonoid = toAddSubmonoid_1
-- Mathlib.Tactic.DeriveTraversable
/-- derive the `traverse` definition and declare `Traversable` using this.  -/
Mathlib.Deriving.Traversable.deriveTraversable : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toArray_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.keys.toArray = m.keysArray
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- a map `I₁ × I₂ → I₁`  -/
CategoryTheory.GradedObject.TriangleIndexData.p₁₂ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {J : Type u_4} →
        [inst : Zero I₂] →
          {r : I₁ × I₂ × I₃ → J} → {π : I₁ × I₃ → J} → CategoryTheory.GradedObject.TriangleIndexData r π → I₁ × I₂ → I₁
-- Mathlib.GroupTheory.Index
Subgroup.instFiniteIndexMin : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.FiniteIndex] [K.FiniteIndex], (H ⊓ K).FiniteIndex
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_add : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableAdd M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => c + f x) μ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] (f : α →ₘ[μ] β), Measurable ↑f
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.named.sizeOf_spec : ∀ (s : Lean.TSyntax `Lean.Parser.Term.namedArgument),
  sizeOf (Lean.PrettyPrinter.Delaborator.AppImplicitArg.named s) = 1 + sizeOf s
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.map.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f) (F : CategoryTheory.Functor C D),
  se.map F = { section_ := F.map se.section_, id := ⋯ }
-- Lean.Server.Requests
Lean.Server.registerCompleteStatefulLspRequestHandler : String →
  (paramType : Type) →
    [Lean.FromJson paramType] →
      [Lean.Lsp.FileSource paramType] →
        (respType : Type) →
          [Lean.ToJson respType] →
            (stateType : Type) →
              [TypeName stateType] →
                stateType →
                  (paramType → stateType → Lean.Server.RequestM (respType × stateType)) →
                    (Lean.Lsp.DidChangeTextDocumentParams → StateT stateType Lean.Server.RequestM Unit) → IO Unit
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin_basisFun : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  Matrix.toBilin (Pi.basisFun R₁ n) = Matrix.toBilin'
-- Init.Data.List.Basic
List.filter_nil : ∀ {α : Type u} {p : α → Bool}, List.filter p [] = []
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.IsOver.restrictSource : ∀ {X Y S : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {f : X.PartialIso Y},
  AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY f →
    ∀ (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source),
      AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY (f.restrictSource U hU hU')
-- Mathlib.MeasureTheory.Order.Lattice
/-- We say that a type has `MeasurableInf₂` if `uncurry (· ⊓ ·)` is a measurable functions.
For a typeclass assuming measurability of `(c ⊓ ·)` and `(· ⊓ c)` see `MeasurableInf`.  -/
MeasurableInf₂ : (M : Type u_1) → [MeasurableSpace M] → [Min M] → Prop
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_self_eq_zero : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : Ring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  {v : n → R}, v ⬝ᵥ v = 0 ↔ v = 0
-- Mathlib.Algebra.Category.Grp.Zero
AddCommGrpCat.isZero_of_iff_subsingleton : ∀ {G : Type u_1} [inst : AddCommGroup G], CategoryTheory.Limits.IsZero (AddCommGrpCat.of G) ↔ Subsingleton G
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxiHasSize.eq_1 : ISize.instRxiHasSize = { size := fun lo => (2 ^ (System.Platform.numBits - 1) - lo.toInt).toNat }
-- Std.Data.Internal.List.Associative
/-- Returns the smallest key in an associative list.  -/
Std.Internal.List.minKey? : {α : Type u} → {β : α → Type v} → [Ord α] → List ((a : α) × β a) → Option α
-- Init.Data.List.ControlImpl
List.flatMapM.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (x : List α) (x_1 : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs) (a : α) (as : List α)
  (bs : List (List β)),
  x = a :: as →
    x_1 = bs →
      (match x, x_1 with
        | [], bs => h_1 bs
        | a :: as, bs => h_2 a as bs) ≍
        h_2 a as bs
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_eq_arrow_of_eq : ∀ {α β : Type u} [Infinite α], Cardinal.mk α = Cardinal.mk β → Cardinal.mk (α ≃ β) = Cardinal.mk (α → β)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- A fixed point of `f` is a periodic point of `f` of any prescribed period.  -/
Function.IsFixedPt.isPeriodicPt : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.IsFixedPt f x → ∀ (n : ℕ), Function.IsPeriodicPt f n x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_coeHom : ⇑Real.Angle.coeHom = Real.Angle.coe
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.ext : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f g : MeasureTheory.Filtration ι m},
  ↑f = ↑g → f = g
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
/-- Upgrade of `F.mapExtAddHom` assuming `F` is linear.  -/
CategoryTheory.Functor.mapExtLinearMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          [inst_3 : CategoryTheory.Abelian D] →
            (F : CategoryTheory.Functor C D) →
              [F.Additive] →
                [CategoryTheory.Limits.PreservesFiniteLimits F] →
                  [CategoryTheory.Limits.PreservesFiniteColimits F] →
                    [inst_7 : CategoryTheory.HasExt C] →
                      [inst_8 : CategoryTheory.HasExt D] →
                        (R : Type u_1) →
                          [inst_9 : Ring R] →
                            [inst_10 : CategoryTheory.Linear R C] →
                              [inst_11 : CategoryTheory.Linear R D] →
                                [CategoryTheory.Functor.Linear R F] →
                                  (X Y : C) →
                                    (n : ℕ) →
                                      CategoryTheory.Abelian.Ext X Y n →ₗ[R]
                                        CategoryTheory.Abelian.Ext (F.obj X) (F.obj Y) n
-- Mathlib.RingTheory.DividedPowers.Basic
/-- Given a nonempty `s : Finset ι` and a family `r : ι → R` such that `r i ∈ I` for all `i ∈ S`,
one has `hI.dpow n (∏ i ∈ s, r i) = n.factorial ^ (s.card - 1) • (∏ i ∈ s, hI.dpow n (r i))`
for all `n : ℕ`.  -/
DividedPowers.dpow_prod : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {ι : Type u_3} {r : ι → A} {s : Finset ι},
  s.Nonempty →
    (∀ i ∈ s, r i ∈ I) → ∀ {n : ℕ}, hI.dpow n (∏ i ∈ s, r i) = n.factorial ^ (s.card - 1) • ∏ i ∈ s, hI.dpow n (r i)
-- Mathlib.Data.Nat.ModEq
Nat.modulus_add_modEq_iff : ∀ {n a b : ℕ}, n + a ≡ b [MOD n] ↔ a ≡ b [MOD n]
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coe_lt_degree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, ↑n < p.degree ↔ n < p.natDegree
-- Mathlib.Data.Set.Opposite
Set.mem_op : ∀ {α : Type u_1} {s : Set α} {a : αᵒᵖ}, a ∈ s.op ↔ Opposite.unop a ∈ s
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_add : ∀ (a b : Ordinal.{v}), Ordinal.lift.{u, v} (a + b) = Ordinal.lift.{u, v} a + Ordinal.lift.{u, v} b
-- ProofWidgets.Component.FilterDetails
ProofWidgets.FilterDetailsProps.mk.sizeOf_spec : ∀ (summary filtered all : ProofWidgets.Html) (initiallyFiltered : Bool),
  sizeOf { summary := summary, filtered := filtered, all := all, initiallyFiltered := initiallyFiltered } =
    1 + sizeOf summary + sizeOf filtered + sizeOf all + sizeOf initiallyFiltered
-- Aesop.Forward.State
/-- This flag is `true` if all `slotQueues` are potentially nonempty. Before
that point, we do not add any hyps to the variable maps since the rule cannot
possibly produce a complete match.  -/
Aesop.ClusterState.haveHypForEachSlot : Aesop.ClusterState → Bool
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderAssociator.associator_inv_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderAssociator] (c c' c'' : C),
  P (CategoryTheory.MonoidalCategoryStruct.associator c c' c'').inv
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_nil : ∀ {b : ℕ}, Nat.ofDigits b [] = 0
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_c_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.toPoly.natDegree = 0
-- Mathlib.Data.Complex.Basic
Complex.normSq_zero : Complex.normSq 0 = 0
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.cyclotomic_eval_lt_add_one_pow_totient : ∀ {n : ℕ} {q : ℝ}, 3 ≤ n → 1 < q → Polynomial.eval q (Polynomial.cyclotomic n ℝ) < (q + 1) ^ n.totient
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The range of a monoid homomorphism from a group is a subgroup.  -/
MonoidHom.range : {G : Type u_1} → [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → (G →* N) → Subgroup N
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.matrix_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J K : Type}
  [inst_2 : Finite J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_4 : Finite K] {f : J → C}
  {g h : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (n : (k : K) → g k ⟶ h k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
      (CategoryTheory.Limits.biproduct.map n) =
    CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j k) (n k)
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.op_adj₃ : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.op.adj₃ = q.adj₁.op
-- Mathlib.CategoryTheory.Yoneda
/-- The natural transformation `yoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X)`
when `F : C ⥤ D` and `X : C`.  -/
CategoryTheory.yonedaMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v₁, u_1} D] →
        (F : CategoryTheory.Functor C D) →
          (X : C) → CategoryTheory.yoneda.obj X ⟶ F.op.comp (CategoryTheory.yoneda.obj (F.obj X))
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Subring.isIntegrallyClosed_iff : ∀ {A : Type u_2} [inst : CommRing A] {C : Type u_5} [inst_1 : SetLike C A] [inst_2 : SubringClass C A] {S : C}
  [IsFractionRing (↥S) A], IsIntegrallyClosed ↥S ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
-- Std.Http.Protocol.H1.Writer
/-- Checks if the writer is closed (cannot process more data).
 -/
Std.Http.Protocol.H1.Writer.isClosed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Init.Data.Array.QSort.Basic
_private.Init.Data.Array.QSort.Basic.0.Array.qpartition.loop.eq_def : ∀ {α : Type u_1} {n : ℕ} (lt : α → α → Bool) (lo hi : ℕ) (hhi : hi < n) (pivot : α) (as : Vector α n) (i k : ℕ)
  (ilo : lo ≤ i) (ik : i ≤ k) (w : k ≤ hi),
  Array.qpartition.loop✝ lt lo hi hhi pivot as i k ilo ik w =
    if h : k < hi then
      if lt as[k] pivot = true then Array.qpartition.loop✝ lt lo hi hhi pivot (as.swap i k ⋯ ⋯) (i + 1) (k + 1) ⋯ ⋯ ⋯
      else Array.qpartition.loop✝ lt lo hi hhi pivot as i (k + 1) ilo ⋯ ⋯
    else (⟨i, ⋯⟩, as.swap i hi ⋯ hhi)
-- Mathlib.NumberTheory.WellApproximable
approxOrderOf.smul_subset_of_coprime : ∀ {A : Type u_1} [inst : SeminormedCommGroup A] {a : A} {n : ℕ} (δ : ℝ),
  (orderOf a).Coprime n → a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ
-- Mathlib.Data.Sign.Basic
SignType.range_eq : ∀ {α : Type u_1} (f : SignType → α), Set.range f = {f SignType.zero, f SignType.neg, f SignType.pos}
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq →
    Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited (β a)], Std.Internal.List.getValueCast! a l = (Std.Internal.List.getValueCast? a l).get!
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.ne_one_iff_exists : ∀ {α : Type u} {x : WithOne α}, x ≠ 1 ↔ ∃ a, ↑a = x
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.mk : {X : Type u_3} →
  [toMetricSpace : MetricSpace X] →
    [toCompleteSpace : CompleteSpace X] → TopologicalSpace.UpgradedIsCompletelyMetrizableSpace X
-- Lean.Expr
/-- Return `true` if the given expression is a constant.  -/
Lean.Expr.isConst : Lean.Expr → Bool
-- Mathlib.Order.Filter.ENNReal
Real.limsup_of_not_isBoundedUnder : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → ℝ}, ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u → Filter.limsup u f = 0
-- Mathlib.Computability.Partrec
Nat.Partrec.below.prec : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop} {f g : ℕ →. ℕ} (a : Nat.Partrec f) (a_1 : Nat.Partrec g),
  Nat.Partrec.below a → motive f a → Nat.Partrec.below a_1 → motive g a_1 → Nat.Partrec.below ⋯
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A linear map maps a generalized eigenrange into itself.  -/
Module.End.map_genEigenrange_le : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Module.End K V}
  {μ : K} {n : ℕ}, Submodule.map f (f.genEigenrange μ ↑n) ≤ f.genEigenrange μ ↑n
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.VAdd.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)],
  Sigma.VAdd = { vadd := fun a => Sigma.map id fun x x_1 => a +ᵥ x_1 }
-- Init.Data.Range.Lemmas
Std.Legacy.Range.forM_eq_forM_range' : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (r : Std.Legacy.Range) (f : ℕ → m PUnit.{u_1 + 1}),
  forM r f = forM (List.range' r.start r.size r.step) f
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_bool_toNat : ∀ (b : Bool) (i : ℕ), b.toNat.testBit i = (decide (i = 0) && b)
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_le : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {a : α}, LowerSet.Iic a ≤ s ↔ a ∈ s
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.params : Lean.CollectLevelParams.State → Array Lean.Name
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The vertices of a simplex plus its circumcenter.  -/
Affine.Simplex.pointsWithCircumcenter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            {n : ℕ} → Affine.Simplex ℝ P n → Affine.Simplex.PointsWithCircumcenterIndex n → P
-- Init.Data.Vector.Monadic
Vector.idRun_forIn'_yield_eq_foldl : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β),
  (forIn' xs init fun a m b => ForInStep.yield <$> f a m b).run =
    Vector.foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => (f a h b).run)
      init xs.attach
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.det_det_aux : ∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  {M : Matrix m m S} [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] (k : m) [inst_4 : Fintype m] [inst_5 : Fintype n]
  {f : S →+* Matrix n n R},
  (∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
      (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det) →
    ((f M.det).det - ((Matrix.comp m m n n R) (M.map ⇑f)).det) * (f (M k k)).det ^ (Fintype.card m - 1) = 0
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.mk : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  (∀ {s : Set H} {x : H} {u : Set H} {f : H → H'}, IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)) →
    (∀ {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H},
        e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)) →
      (∀ {s : Set H} {x : H} {f g : H → H'}, (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x) →
        (∀ {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'},
            e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x) →
          G.LocalInvariantProp G' P
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup'_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α},
  a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_le_add_one_right_iff : ∀ {a b : WithBot ℕ∞}, a + 1 ≤ b + 1 ↔ a ≤ b
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_univ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, derivWithin f Set.univ = deriv f
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.Contradiction.Config.useDecide : Lean.Meta.Contradiction.Config → Bool
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsCompl.isTopCompl_iff_projectionOnto : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : IsCompl p q),
  Submodule.IsTopCompl p q ↔ Continuous ⇑(p.projectionOnto q h)