mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.instIsInnerOfIso : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
  [inst : P.IsProper] [P.IsInner], (P.ofIso e hA).IsInner
-- Std.Tactic.Do.Syntax
Lean.Parser.Category.mrevertPat : Lean.Parser.Category
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_sndX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (HomologicalComplex.homotopyCofiber.sndX φ i) =
    CategoryTheory.CategoryStruct.id (G.X i)
-- Mathlib.Topology.Separation.Regular
/-- A space is completely normal iff it is hereditarily normal.
 -/
completelyNormalSpace_iff_forall_normalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X], CompletelyNormalSpace X ↔ ∀ (s : Set X), NormalSpace ↑s
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_le_filterMap : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) {s t : Multiset α},
  s ≤ t → Multiset.filterMap f s ≤ Multiset.filterMap f t
-- Std.Time.DateTime
/-- Add `Month.Offset` to a `DateTime`, clipping to the last valid day.
 -/
Std.Time.DateTime.addMonthsClip : Std.Time.DateTime → Std.Time.Month.Offset → Std.Time.DateTime
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The terms corresponding to the `⁅E, F⁆`-relations.  -/
CartanMatrix.Relations.EF : (R : Type u) →
  {B : Type v} → [inst : CommRing R] → [DecidableEq B] → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.instFunLikeReal : {K : Type u_1} → [inst : Field K] → FunLike (NumberField.InfinitePlace K) K ℝ
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.symm_trans : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ),
  φ.symm.trans φ = ContRepresentation.Equiv.refl σ
-- Mathlib.Analysis.Oscillation
/-- The oscillation of `f` at `x` within a neighborhood `D` of `x` is equal to `oscillation f x`  -/
oscillationWithin_nhds_eq_oscillation : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] (f : E → F) (D : Set E) (x : E),
  D ∈ nhds x → oscillationWithin f D x = oscillation f x
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_map_fst : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M) (q : Submodule R M₂),
  Submodule.map (LinearMap.fst R M M₂) (p.prod q) = p
-- Mathlib.RingTheory.IsTensorProduct
TensorProduct.isPushout' : ∀ {R : Type u_8} {S : Type u_9} {T : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], Algebra.IsPushout R T S (TensorProduct R S T)
-- Init.Prelude
/-- The canonical type with one element. This element is written `()`.

`Unit` has a number of uses:
* It can be used to model control flow that returns from a function call without providing other
  information.
* Monadic actions that return `Unit` have side effects without computing values.
* In polymorphic types, it can be used to indicate that no data is to be stored in a particular
  field.
 -/
Unit : Type
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toList_filter : ∀ {β : Type v} {α : Type u} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : α → β → Bool},
  (Std.DHashMap.Raw.Const.toList ↑(Std.DHashMap.Internal.Raw₀.filter f m)).Perm
    (List.filter (fun p => f p.1 p.2) (Std.DHashMap.Raw.Const.toList ↑m))
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.degree_eq : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : G.LocallyFinite] {d : ℕ}, G.IsRegularOfDegree d → ∀ (v : V), G.degree v = d
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getKey? k (List.filter (fun p => !l₂.contains p.fst) l₁) = none
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_three : ∀ {α : Type u_1} {s : Multiset α}, s.card = 3 ↔ ∃ x y z, s = {x, y, z}
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofIntLE : ∀ {n : ℤ} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt),
  (ISize.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n
-- Init.Data.List.Impl
/-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs`  -/
_private.Init.Data.List.Impl.0.List.zipWithTR.go : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → List α → List β → Array γ → List γ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist to a set and to its closure coincide  -/
Metric.infEDist_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, Metric.infEDist x (closure s) = Metric.infEDist x s
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextn.eq_def : ∀ {s : String.Slice} (p : s.Pos) (n : ℕ),
  p.nextn n =
    match n with
    | 0 => p
    | n.succ => if h : p ≠ s.endPos then (p.next h).nextn n else p
-- Mathlib.Data.List.Chain
List.isChain_iff_forall_rel_of_append_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
  List.IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_map_star : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R →⋆* S) (x : ↥(unitary R)), ↑((Unitary.map f) (star x)) = f (star ↑x)
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.targetRange : Lean.Lsp.LocationLink → Lean.Lsp.Range
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT.congr_simp : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n n_1 : ℕ∞),
  n = n_1 → Topology.RelCWComplex.skeletonLT C n = Topology.RelCWComplex.skeletonLT C n_1
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.leftUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.LaxTrans.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Comma.hasColimit_of_closedUnderColimitsOfShape : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_3} {J : Type u_4} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} B] [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤))
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderColimitsOfShape J]
  [CategoryTheory.Limits.HasColimit (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))],
  CategoryTheory.Limits.HasColimit D
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.eq_mul_inv_iff_mul_eq : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] {φ₁ φ₂ φ₃ : MvPowerSeries σ k},
  MvPowerSeries.constantCoeff φ₃ ≠ 0 → (φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
DegLex.exists_iff : ∀ {α : Type u_1} {p : DegLex α → Prop}, (∃ a, p a) ↔ ∃ a, p (toDegLex a)
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {P : CategoryTheory.Subobject Y} (h : P.Factors 0), P.factorThru 0 h = 0
-- Lean.Meta.IndPredBelow
Lean.Meta.IndPredBelow.RecursionContext.mk.sizeOf_spec : ∀ (belows : Lean.FVarIdMap (Lean.Name × Lean.Expr)) (motives : Lean.FVarIdMap (ℕ × Lean.Expr)),
  sizeOf { belows := belows, motives := motives } = 1 + sizeOf belows + sizeOf motives
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If a predicate depends only on `f x - x` and holds for all `0 ≤ x ≤ 1`,
then it holds for all `x`.  -/
CircleDeg1Lift.forall_map_sub_of_Icc : ∀ (f : CircleDeg1Lift) (P : ℝ → Prop), (∀ x ∈ Set.Icc 0 1, P (f x - x)) → ∀ (x : ℝ), P (f x - x)
-- Lean.Meta.Constructions.CasesOnSameCtor
/-- This constructs a matcher for a match statement that matches on the constructors of
a data type in parallel. So if `h : x1.ctorIdx = x2.ctorIdx`, then it implements
```
match x1, x2, h with
| ctor1 .. , ctor1 .. , _ => ...
| ctor2 .. , ctor2 .. , _ => ...
```
The normal matcher supports such matches, but implements them using nested `casesOn`, which
leads to a quadratic blow-up. This function uses the per-constructor eliminators to implement this
more efficiently.

This is useful for implementing or deriving functionality like `BEq`, `DecidableEq`, `Ord` and
proving their lawfulness.

One could imagine a future where `match` compilation is smart enough to do that automatically; then
this module can be dropped.

Note that for some data types where the indices determine the constructor (e.g. `Vec`), this leads
to less efficient code than the normal matcher, as this needs to read the constructor tag on both
arguments, whereas the normal matcher produces code that reads just the first argument’s tag, and
then boldly reads the second argument’s fields.
 -/
Lean.mkCasesOnSameCtor : Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Homology.Augment
/-- A chain map from a single object cochain complex in degree zero to a cochain complex
can be reinterpreted as a cochain complex.

This is the inverse construction of `toTruncate`.
 -/
CochainComplex.fromSingle₀AsComplex : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        (C : CochainComplex V ℕ) → (X : V) → ((CochainComplex.single₀ V).obj X ⟶ C) → CochainComplex V ℕ
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.liftAddEquiv_apply_apply : ∀ {α : Type u} {G : Type u_1} [inst : AddCommGroup G] (a : α → Multiplicative G)
  (a_1 : Additive (Abelianization (FreeGroup α))),
  (FreeAbelianGroup.liftAddEquiv a) a_1 = Additive.ofMul ((Abelianization.lift (FreeGroup.lift a)) (Additive.toMul a_1))
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : β →CO γ) (g : α →CO β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.componentComplFunctor_map : ∀ {V : Type u} (G : SimpleGraph V) {X Y : (Finset V)ᵒᵖ} (f : X ⟶ Y),
  G.componentComplFunctor.map f = TypeCat.ofHom (SimpleGraph.ComponentCompl.hom ⋯)
-- Init.Data.String.Termination
String.Slice.Pos.Down.mk.inj : ∀ {s : String.Slice} {inner inner_1 : s.Pos}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.mk_eq_mk_iff : ∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v w : V)
  (hv : v ≠ 0) (hw : w ≠ 0), Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
-- Lean.Compiler.IR.CompilerM
/-- Returns additional names that compiler env exts may want to call `getModuleIdxFor?` on.  -/
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.getIRExtraConstNames : Lean.Environment → Lean.OLeanLevel → optParam Bool false → Array Lean.Name
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Ici : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α) [inst_2 : Fintype ↑(Set.Ici a)],
  Fintype.card ↑(Set.Ici a) = (Finset.Ici a).card
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBinaryBicone_inl : ∀ {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] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y), (F.mapBinaryBicone b).inl = F.map b.inl
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (x : PrimeSpectrum R),
  ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod ⊤
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.leftAlgebra : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CommSemiring S] →
                    [inst_6 : Algebra S A] → [SMulCommClass R S A] → Algebra S (TensorProduct R A B)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.neg_right_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_6} [inst_2 : AddCommGroup N] [inst_3 : TopologicalSpace N] [inst_4 : IsTopologicalAddGroup N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.MutuallySingular (-w) ↔ v.MutuallySingular w
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_mul_const : ∀ {a : ENNReal}, a ≠ ⊤ → Continuous fun x => x * a
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.add : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s t : Set E},
  Balanced 𝕜 s → Balanced 𝕜 t → Balanced 𝕜 (s + t)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsLocallyPresentable.exists_cardinal : ∀ (C : Type u) [hC : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsLocallyPresentable.{w, v, u} C],
  ∃ κ, ∃ (x : Fact κ.IsRegular), CategoryTheory.IsCardinalLocallyPresentable C κ
-- Mathlib.Order.WithBot
WithTop.ofDual_map : ∀ {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithTop αᵒᵈ),
  WithTop.ofDual (WithTop.map f a) = WithBot.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithTop.ofDual a)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a a' : α},
  Std.Internal.List.getKey? a l = some a' → Std.Internal.List.containsKey a' l = true
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The scalar multiplication of family of elements of a presheaf of modules `M` over `R`
by a family of elements of `R`.  -/
CategoryTheory.Presieve.FamilyOfElements.smul : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M : PresheafOfModules R} →
        {X : C} →
          {P : CategoryTheory.Presieve X} →
            CategoryTheory.Presieve.FamilyOfElements (R.comp (CategoryTheory.forget RingCat)) P →
              CategoryTheory.Presieve.FamilyOfElements (M.presheaf.comp (CategoryTheory.forget Ab)) P →
                CategoryTheory.Presieve.FamilyOfElements (M.presheaf.comp (CategoryTheory.forget Ab)) P
-- Mathlib.Order.Directed
DirectedOn.insert : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] (a : α) {s : Set α},
  DirectedOn r s → (∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c) → DirectedOn r (insert a s)
-- Mathlib.Data.Nat.Fib.Zeckendorf
/-- The greatest index of a Fibonacci number less than or equal to `n`.  -/
Nat.greatestFib : ℕ → ℕ
-- Mathlib.GroupTheory.Congruence.Basic
Con.congr_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} {d : Con N} (e : M ≃* N)
  (h : c = Con.comap ⇑e ⋯ d), (Con.congr e h).symm = Con.congr e.symm ⋯
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.seminormedAddCommGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : AddSubgroupClass S E]
  (s : S),
  AddSubgroupClass.seminormedAddCommGroup s =
    { toNorm := (AddSubgroupClass.seminormedAddGroup s).toNorm, toAddCommGroup := AddSubgroupClass.toAddCommGroup s,
      toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, and the second point is not outside the sphere, the second point is weakly
between the first point and the result of `secondInter`.  -/
EuclideanGeometry.Sphere.wbtw_secondInter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p p' : P},
  p ∈ s → dist p' s.center ≤ s.radius → Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
-- Std.Time.Format.Basic
Std.Time.FormatPart.string.injEq : ∀ (val val_1 : String), (Std.Time.FormatPart.string val = Std.Time.FormatPart.string val_1) = (val = val_1)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMul_cancels_iff : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.Cancels (-u) (HNNExtension.NormalWord.unitsSMul φ u w) ↔ ¬HNNExtension.NormalWord.Cancels u w
-- Init.Data.List.Basic
/-- Checks whether the first list is a suffix of the second.

The relation `List.IsSuffixOf` expresses this property with respect to logical equality.

Examples:
* `[2, 3].isSuffixOf [1, 2, 3] = true`
* `[2, 3].isSuffixOf [1, 2, 3, 4] = false`
* `[2, 3].isSuffixOf [1, 2] = false`
* `[2, 3].isSuffixOf [1, 1, 2, 3] = true`
 -/
List.isSuffixOf : {α : Type u} → [BEq α] → List α → List α → Bool
-- Mathlib.Data.List.Duplicate
List.Duplicate.below : {α : Type u_1} →
  {x : α} → {motive : (a : List α) → List.Duplicate x a → Prop} → {a : List α} → List.Duplicate x a → Prop
-- Mathlib.Data.Nat.Cast.Defs
/-- The numeral `((0+1)+⋯)+1`.  -/
Nat.unaryCast : {R : Type u_1} → [One R] → [Zero R] → [Add R] → ℕ → R
-- Mathlib.Data.Sym.Basic
_private.Mathlib.Data.Sym.Basic.0.SymOptionSuccEquiv.decode.match_1.eq_2 : ∀ {α : Type u_1} {n : ℕ} (motive : Sym (Option α) n ⊕ Sym α n.succ → Sort u_2) (s : Sym α n.succ)
  (h_1 : (s : Sym (Option α) n) → motive (Sum.inl s)) (h_2 : (s : Sym α n.succ) → motive (Sum.inr s)),
  (match Sum.inr s with
    | Sum.inl s => h_1 s
    | Sum.inr s => h_2 s) =
    h_2 s
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_last_apply_castSucc : ∀ {n : ℕ} (i : Fin n), (finSuccEquiv' (Fin.last n)) i.castSucc = some i
-- Mathlib.Data.Setoid.Partition
/-- Given a collections of sets `s : ι → Set α` that forms an indexed partition, we can group
some of the sets to obtain a coarser partition.  -/
IndexedPartition.coarserPartition : {ι : Type u_1} →
  {α : Type u_2} →
    {s : ι → Set α} →
      IndexedPartition s →
        {κ : Type u_4} → (g : ι → κ) → Function.Surjective g → IndexedPartition fun k => ⋃ i ∈ g ⁻¹' {k}, s i
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instAddCommGroup : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddCommGroup 𝕜] → [inst_1 : LE α] → AddCommGroup (IncidenceAlgebra 𝕜 α)
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {P : CategoryTheory.Subobject Z} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : P.Factors g),
  CategoryTheory.CategoryStruct.comp f (P.factorThru g h) = P.factorThru (CategoryTheory.CategoryStruct.comp f g) ⋯
-- Mathlib.Analysis.Fourier.ZMod
/-- For a primitive Dirichlet character `χ`, the Fourier transform of `χ` is a constant multiple
of `χ⁻¹` (and the constant is essentially the Gauss sum).  -/
DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N},
  χ.IsPrimitive → ∀ (k : ZMod N), ZMod.dft (⇑χ) k = χ⁻¹ (-k) * gaussSum χ ZMod.stdAddChar
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  [inst_1 : IsAdicComplete I A] {f : PowerSeries A}, H.mod' ((Ideal.Quotient.mk (Ideal.span {g})) f) = H.mod f
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.asFunctor_obj_d : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3}
  {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) (t : T) (i j : ι),
  (C.asFunctor.obj t).d i j = (C.d i j).app t
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_of_continuousOn : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R] {s : Set X}
  [inst_3 : Zero ↑s] {f : X → R} {g : ContinuousMapZero (↑s) R} (hf : ContinuousOn f s) (hf₀ : f ↑0 = 0),
  ContinuousMapZero.mkD (s.domRestrict f) g = { toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf₀ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_congr_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f =ᵐ[μ] g → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
-- Lean.Elab.InfoTree.Types
Lean.Elab.CustomInfo.mk.injEq : ∀ (stx : Lean.Syntax) (value : Dynamic) (stx_1 : Lean.Syntax) (value_1 : Dynamic),
  ({ stx := stx, value := value } = { stx := stx_1, value := value_1 }) = (stx = stx_1 ∧ value = value_1)
-- Lean.Data.Lsp.Internal
/-- Whether this location link was generated by a fallback handler.
If the file worker can't produce any non-fallback location links, the watchdog tries again
using its reference information from the ileans and ilean updates.
 -/
Lean.Lsp.LeanLocationLink.isDefault : Lean.Lsp.LeanLocationLink → Bool
-- Mathlib.Topology.Constructions
Sigma.nhds_mk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] (i : ι) (x : σ i),
  nhds ⟨i, x⟩ = Filter.map (Sigma.mk i) (nhds x)
-- Init.Prelude
Nat.lt_or_ge : ∀ (n m : ℕ), n < m ∨ n ≥ m
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a b : α} {fallback : β},
  cmp a b = Ordering.eq → Std.ExtDTreeMap.Const.getD t a fallback = Std.ExtDTreeMap.Const.getD t b fallback
-- Mathlib.Topology.Instances.Matrix
instContinuousSMulMatrix : ∀ {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace α]
  [inst_2 : SMul α R] [ContinuousSMul α R], ContinuousSMul α (Matrix m n R)