mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.Floor
Measurable.nat_floor : ∀ {α : Type u_1} {R : Type u_2} [inst : MeasurableSpace α] [inst_1 : Semiring R] [inst_2 : LinearOrder R]
  [inst_3 : FloorSemiring R] [inst_4 : TopologicalSpace R] [OrderTopology R] [inst_6 : MeasurableSpace R]
  [OpensMeasurableSpace R] {f : α → R} [IsStrictOrderedRing R], Measurable f → Measurable fun x => ⌊f x⌋₊
-- Init.Prelude
/-- Concatenates a list of lists into a single list, preserving the order of the elements.

`O(|flatten L|)`.

Examples:
* `[["a"], ["b", "c"]].flatten = ["a", "b", "c"]`
* `[["a"], [], ["b", "c"], ["d", "e", "f"]].flatten = ["a", "b", "c", "d", "e", "f"]`
 -/
List.flatten : {α : Type u_1} → List (List α) → List α
-- Mathlib.Logic.Basic
ite_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {p : Prop} [inst_1 : Decidable p] {a b : α} {s : β},
  (if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_vsub_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {b c : β}, {b} -ᵥ {c} = {b -ᵥ c}
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_mul_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), Metric.ball 1 δ * s = Metric.thickening δ s
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_image_eq_source_inter_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set β}, s ⊆ e.target → ↑e.symm '' s = e.source ∩ ↑e ⁻¹' s
-- Mathlib.Data.Sum.Basic
Sum.exists_sum : ∀ {α : Type u} {β : Type v} {γ : α ⊕ β → Sort u_3} (p : ((ab : α ⊕ β) → γ ab) → Prop),
  (∃ fab, p fab) ↔ ∃ fa fb, p fun t => Sum.rec fa fb t
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_e : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A], (AlgebraicIndependent.matroid R A).E = Set.univ
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.below.compl : ∀ {α : Type u_2} {𝒜 : Set (Set α)} {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop} (s : Set α)
  (hs : MeasureTheory.generateSetAlgebra 𝒜 s),
  MeasureTheory.generateSetAlgebra.below hs → motive s hs → MeasureTheory.generateSetAlgebra.below ⋯
-- Mathlib.Data.Nat.Multiplicity
_private.Mathlib.Data.Nat.Multiplicity.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_add_cos : ∀ (x y : ℂ), Complex.cos x + Complex.cos y = 2 * Complex.cos ((x + y) / 2) * Complex.cos ((x - y) / 2)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- Subsets of bounded sets are bounded.  -/
Bornology.IsVonNBounded.subset : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {s₁ s₂ : Set E}, s₁ ⊆ s₂ → Bornology.IsVonNBounded 𝕜 s₂ → Bornology.IsVonNBounded 𝕜 s₁
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.singleton_eq_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {p : (a : α) × β a},
  {p} = ∅.insert p.fst p.snd
-- Mathlib.Data.Finset.Sups
Finset.image_sups : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : SemilatticeSup α] [inst_3 : SemilatticeSup β] [inst_4 : FunLike F α β] [SupHomClass F α β] (f : F)
  (s t : Finset α), Finset.image (⇑f) (s ⊻ t) = Finset.image (⇑f) s ⊻ Finset.image (⇑f) t
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.mk_coe : ∀ {𝕜 : 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] (e : PartialEquiv H E)
  (a : e.source = Set.univ) (b : if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑e) else Set.range ↑e = Set.univ)
  (c : (interior (Set.range ↑e)).Nonempty) (d : Continuous ↑e) (d' : Continuous e.invFun),
  ↑{ toPartialEquiv := e, source_eq := a, convex_range' := b, nonempty_interior' := c, continuous_toFun := d,
        continuous_invFun := d' } =
    ↑e
-- Batteries.Recycling.RBTree.Basic
/-- True if the specified `cut` matches at least one element of of `t`.  -/
RBTree.RBSet.MemP : {α : Type u_1} → {cmp : α → α → Ordering} → (α → Ordering) → RBTree.RBSet α cmp → Prop
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst : CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S))
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f).left] {i j : J} (f : i ⟶ j),
  AlgebraicGeometry.IsOpenImmersion
    (((F.comp (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)).comp (CategoryTheory.Over.forget S)).map f)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If three points are not collinear, the angle between them is less than π.  -/
EuclideanGeometry.angle_lt_pi_of_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, ¬Collinear ℝ {p₁, p₂, p₃} → EuclideanGeometry.angle p₁ p₂ p₃ < Real.pi
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOp : {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.CreatesLimits F] → CategoryTheory.CreatesColimits F.op
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertMany_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {ρ : Type w} [inst : ForIn Id ρ (α × β)]
  {motive : (Std.DHashMap α fun x => β) → Prop} (m : Std.DHashMap α fun x => β) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap α fun x => β) (a : α) (b : β), motive m → motive (m.insert a b)) →
      motive (Std.DHashMap.Const.insertMany m l)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph : ∀ {V : Type u} {G : SimpleGraph V} (H : G.Subgraph),
  H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is an open ball
centered at `x` and intersecting `s` only at `x`.  -/
Metric.exists_ball_inter_eq_singleton_of_mem_discrete : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  IsDiscrete s → ∀ {x : α}, x ∈ s → ∃ ε > 0, Metric.ball x ε ∩ s = {x}
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) (W : (J.Cover X)ᵒᵖ),
  (J.diagramNatTrans η X).app W =
    CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W)
      (fun x =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) x)
          (η.app (Opposite.op x.Y)))
      ⋯
-- Mathlib.Order.Hom.Lex
Prod.Lex.prodLexAssoc_apply : ∀ (α : Type u_4) (β : Type u_5) (γ : Type u_6) [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (a : Lex (Lex (α × β) × γ)),
  (Prod.Lex.prodLexAssoc α β γ) a = toLex ((ofLex (ofLex a).1).1, toLex ((ofLex (ofLex a).1).2, (ofLex a).2))
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_self_right : ∀ (n : ℕ), (n + 1).choose n = n + 1
-- Mathlib.Algebra.Torsor.Basic
/-- `Equiv.constVAdd` as a homomorphism from `Multiplicative G` to `Equiv.perm P`  -/
Equiv.constVAddHom : (G : Type u_3) → (P : Type u_4) → [inst : AddGroup G] → [AddTorsor G P] → Multiplicative G →* Equiv.Perm P
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) [inst_2 : CategoryTheory.Limits.HasColimit F]
  (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)) {j k : Jᵒᵖ} (f : j ⟶ k),
  (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).map f =
    CategoryTheory.CategoryStruct.comp
      ((F.map f.unop).c.app
        (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).base).obj U)))
      ((F.obj (Opposite.unop k)).presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.Order.RelClasses
/-- **Alias** of `ssubset_irrefl`.

---

Set notation form of `lt_irrefl` -/
ssubset_irrfl : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] (a : α), ¬a ⊂ a
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_bot`.

---

The orthogonal projection onto the trivial submodule is the zero map.  -/
Submodule.orthogonalProjection_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊥.orthogonalProjectionOnto = 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Ici : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.image (Fin.cast h) (Finset.Ici i) = Finset.Ici (Fin.cast h i)
-- Mathlib.Algebra.Group.Commute.Basic
/-- **Alias** of the reverse direction of `AddCommute.neg_right_iff`. -/
AddCommute.neg_right : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → AddCommute a (-b)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNewUnit.eq_2 : ∀ {α : Type u} [inst : BEq α] (l : List ((_ : α) × Unit)) (hd : α) (tl : List α),
  Std.Internal.List.insertListIfNewUnit l (hd :: tl) =
    Std.Internal.List.insertListIfNewUnit (Std.Internal.List.insertEntryIfNew hd () l) tl
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval_C : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) {c : K},
  RatFunc.eval f a (RatFunc.C c) = f c
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Ici_eq_Ioi_iInf : ∀ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ι → R},
  ⨅ i, f i ∉ Set.range f → ⋃ i, Set.Ici (f i) = Set.Ioi (⨅ i, f i)
-- Mathlib.Order.Circular
Btw.mk : {α : Type u_1} → (α → α → α → Prop) → Btw α
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Normal.of_map_injective : ∀ {G : Type u_6} {H : Type u_7} [inst : Group G] [inst_1 : Group H] {φ : G →* H},
  Function.Injective ⇑φ → ∀ {L : Subgroup G}, (Subgroup.map φ L).Normal → L.Normal
-- Init.Data.SInt.Lemmas
Int16.lt_iff_toInt_lt : ∀ {x y : Int16}, x < y ↔ x.toInt < y.toInt
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.writeResponse : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.Response α → IO Unit
-- Mathlib.Control.Traversable.Instances
List.naturality : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G] [LawfulApplicative F]
  (η : ApplicativeTransformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : List α),
  (fun {α} => η.app α) (List.traverse f x) = List.traverse ((fun {α} => η.app α) ∘ f) x
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk.injEq : ∀ {M : Type u_3} [inst : Add M] (carrier : Set M) (add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier)
  (carrier_1 : Set M) (add_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a + b ∈ carrier_1),
  ({ carrier := carrier, add_mem' := add_mem' } = { carrier := carrier_1, add_mem' := add_mem'_1 }) =
    (carrier = carrier_1)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topCat_hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} TopCat
-- Mathlib.Data.List.Enum
List.forall_mem_zipIdx : ∀ {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop},
  (∀ x ∈ l.zipIdx n, p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], n + i)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.ToType.mk_apply : ∀ {o : Ordinal.{u_1}} (x : ↑(Set.Iio o)), Ordinal.ToType.mk x = (Ordinal.enum fun x1 x2 => x1 < x2) ⟨↑x, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_mul_complex_Ioi : ∀ {a : ℂ}, a.re < 0 → ∀ (c : ℝ), ∫ (x : ℝ) in Set.Ioi c, Complex.exp (a * ↑x) = -Complex.exp (a * ↑c) / a
-- Mathlib.Analysis.Calculus.FDeriv.Defs
HasFDerivAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (f' : E →L[𝕜] F) (x : E),
  HasFDerivAt f f' x = HasFDerivAtFilter f f' (nhds x ×ˢ pure x)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_apply_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat}
  [inst_1 : CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) (x : ↑(SemiRingCat.FilteredColimits.R F)),
  (SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom t) x =
    (SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom t) x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
/-- An inductive datatype used specifically for the output of the `reduce` function. The intended
meaning of each constructor is explained in the docstring of the `reduce` function.
 -/
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult : Type u → Type u
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnAddMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y] (a : LocallyConstant X Y)
  (a_1 : X), LocallyConstant.coeFnAddMonoidHom a a_1 = a a_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get? k' = some k
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) The limit cone. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.c : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} → AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f → CategoryTheory.Limits.Cone D
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.ext : ∀ {G : Type u} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : ClosedAddSubgroup G},
  (↑x).carrier = (↑y).carrier → x = y
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `OverArrows η s` in `s`.  -/
CategoryTheory.OverPresheafAux.OverArrows.map₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {η : F ⟶ A} →
        {X Y : C} →
          {s : CategoryTheory.yoneda.obj X ⟶ A} →
            {t : CategoryTheory.yoneda.obj Y ⟶ A} →
              CategoryTheory.OverPresheafAux.OverArrows η t →
                (f : X ⟶ Y) →
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s →
                    CategoryTheory.OverPresheafAux.OverArrows η s
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.imp_sup_right : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n), T.Imp ψ (φ ⊔ ψ)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMap_mk : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {J : Ideal R} {I : Ideal S} [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] {f : R →+* S} {H : J ≤ Ideal.comap f I} {x : R},
  (Ideal.quotientMap I f H) ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f x)
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The projection from the pullback to the first component.
 -/
CompHausLike.pullback.fst : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) → (g : Y ⟶ B) → [inst : CompHausLike.HasExplicitPullback f g] → CompHausLike.pullback f g ⟶ X
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_eq_zero_iff : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : Fintype n] {v : n → R},
  (∀ (w : n → R), v ⬝ᵥ w = 0) ↔ v = 0
-- Mathlib.Algebra.Order.Group.Cyclic
/-- Given a cyclic linearly ordered commutative group, this is a generator that is `< 1`.  -/
LinearOrderedCommGroup.genLTOne : (G : Type u_1) →
  [inst : CommGroup G] → [inst_1 : LinearOrder G] → [IsOrderedMonoid G] → [Nontrivial G] → [IsCyclic G] → G
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.instIsGCDMonoidOfIsCancelMulZero : ∀ (R : Type u) [inst : CommRing R] [IsBezout R] [IsCancelMulZero R], IsGCDMonoid R
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.ofArray : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : Array α}, (Std.TreeSet.Raw.ofArray a cmp).WF
-- Mathlib.Topology.Irreducible
Topology.IsOpenEmbedding.irreducibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : Y → X},
  Topology.IsOpenEmbedding f → ∀ [IrreducibleSpace X] [Nonempty Y], IrreducibleSpace Y
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
ZeroHom.withBotMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), ⇑f.withBotMap = WithBot.map ⇑f
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.dist_integral_le_lintegral_edist : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f →
    μ.Integrable g →
      dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ ‖B‖ * (∫⁻ (a : X), edist (f a) (g a) ∂μ.variation).toReal
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Given a functor `F : C ⥤ D`, if `F.map p₁` and `F.map p₂` form a jointly monic pair of
morphisms, and if `F` preserves pullbacks, then `F` preserves reflexive relations.  -/
CategoryTheory.TransitiveRelation.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {R X : C} →
          {p₁ p₂ : R ⟶ X} →
            CategoryTheory.TransitiveRelation p₁ p₂ →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.JointlyMono₂ (F.map p₁) (F.map p₂)] →
                  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] →
                    CategoryTheory.TransitiveRelation (F.map p₁) (F.map p₂)
-- Mathlib.Analysis.Normed.Order.UpperLower
IsLowerSet.exists_subset_ball : ∀ {ι : Type u_2} [inst : Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ} {δ : ℝ},
  IsLowerSet s →
    x ∈ closure s →
      0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s
-- Init.Data.List.FinRange
List.finRange_reverse : ∀ {n : ℕ}, (List.finRange n).reverse = List.map Fin.rev (List.finRange n)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.instEquivLike : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] → EquivLike (P ≃ᵃⁱ[𝕜] P₂) P P₂
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.w'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z)
  [inst_2 : F.Full] [F.Faithful] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hf.fst' (F.map g)) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (hf.snd (F.map g)) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ε_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 :
    ∀ {X S : C} (πX : X ⟶ S),
      CategoryTheory.Limits.HasColimitsOfShape
        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
  (π : CategoryTheory.Arrow C),
  (CategoryTheory.SmallObject.ε f).app π =
    CategoryTheory.Arrow.homMk (CategoryTheory.SmallObject.ιFunctorObj f π.hom)
      (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Arrow C)).obj π).right) ⋯
-- Mathlib.Analysis.Normed.Group.Basic
/-- A scaled closed ball is a closed ball.  -/
setOf_div_mem_closedBall_eq_closedBall'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a : E} {r : ℝ},
  {x | x / a ∈ Metric.closedBall 1 r} = Metric.closedBall a r
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.instNontrivialRingOfIntegers : ∀ (K : Type u_1) [inst : Field K], Nontrivial (NumberField.RingOfIntegers K)
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.gaussNorm_monomial : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) (c : ℝ) [ZeroHomClass F R ℝ]
  (n : ℕ) (r : R), Polynomial.gaussNorm v c ((Polynomial.monomial n) r) = v r * c ^ n
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) (x : ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)),
  (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y) x = IsLocalRing.closedPoint ↑(Y.residueField y)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
exists_dist_lt_lt : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x z : E} {δ ε : ℝ},
  0 < δ → 0 < ε → dist x z < ε + δ → ∃ y, dist x y < δ ∧ dist y z < ε
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- If `D` is already an enriched ordinary category, it is equivalent to `ForgetEnrichment V D`.  -/
CategoryTheory.ForgetEnrichment.equiv : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u''} →
        [inst_2 : CategoryTheory.Category.{v'', u''} D] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D] → CategoryTheory.ForgetEnrichment V D ≌ D
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_left : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x, y - x} = Ideal.span {x, y}
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.instEvalTermCastMode : Lean.Elab.ConfigEval.EvalTerm Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instContinuousEval : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  ContinuousEval (ContDiffMapSupportedIn E F n K) E F