mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_segment_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [CompleteSpace F] (ω : E →L[𝕜] F) (a b : E), ∫ᶜ (x : E) in Path.segment a b, ω = ω (b - a)
-- Mathlib.Analysis.Analytic.Inverse
/-- The left inverse to a formal multilinear series is indeed a left inverse, provided its linear
term is invertible.  -/
FormalMultilinearSeries.leftInv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → (p.leftInv i x).comp p = FormalMultilinearSeries.id 𝕜 E x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {M : Type u_7} {N : Type u_8}
  [inst_6 : Monoid M] [inst_7 : DistribMulAction M F] [inst_8 : SMulCommClass S M F] [inst_9 : Monoid N]
  [inst_10 : DistribMulAction N F] [inst_11 : SMulCommClass S N F] [inst_12 : SMul M N] [IsScalarTower M N F],
  IsScalarTower M N (E →ₛₗ.[σ] F)
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getLetIdDeclVars : Lean.TSyntax `Lean.Parser.Term.letIdDecl → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- The alternating group is a characteristic subgroup of the permutation group.  -/
instCharacteristicPermAlternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], (alternatingGroup α).Characteristic
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.getDₘ : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → β → β
-- Init.Data.Order.ClassesExtra
/-- This typeclass states that the synthesized `Ord α` instance is compatible with the `LE α`
instance. This means that according to `compare`, the following are equivalent:

* `a` is less than or equal to `b` according to `compare`.
* `b` is greater than or equal to `b` according to `compare`.
* `a ≤ b` holds.

`LawfulOrderOrd α` automatically entails that `Ord α` is oriented (see `OrientedOrd α`)
and that `LE α` is total.

`Ord α` and `LE α` mutually determine each other in the presence of `LawfulOrderOrd α`.
 -/
Std.LawfulOrderOrd : (α : Type u) → [Ord α] → [LE α] → Prop
-- Mathlib.Analysis.RCLike.Basic
RCLike.sqrt_normSq_eq_norm : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, √(RCLike.normSq z) = ‖z‖
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesMap'_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.opcyclesMap' (φ - φ') h₁ h₂ =
    CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ - CategoryTheory.ShortComplex.opcyclesMap' φ' h₁ h₂
-- Lean.Server.Requests
Lean.Server.handleLspRequest : String → Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)
-- Init.Data.String.Basic
String.Slice.Pos.slice_inj : ∀ {s : String.Slice} {p₀ p₁ pos pos' : s.Pos} {h₁ : p₀ ≤ pos} {h₁' : p₀ ≤ pos'} {h₂ : pos ≤ p₁} {h₂' : pos' ≤ p₁},
  pos.slice p₀ p₁ h₁ h₂ = pos'.slice p₀ p₁ h₁' h₂' ↔ pos = pos'
-- Mathlib.Data.Set.Prod
Set.prod_nonempty_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.herglotzLogIntegrand_circleAverage_tendsto : ∀ {ρ w : ℂ} {R : ℝ},
  0 < R →
    ‖ρ‖ = R →
      ‖w‖ < R →
        ∀ {r : ℕ → ℝ},
          (∀ (n : ℕ), r n < R) →
            Filter.Tendsto r Filter.atTop (nhds R) →
              Filter.Tendsto (fun n => Real.circleAverage (herglotzLogIntegrand✝ w ρ) 0 (r n)) Filter.atTop
                (nhds (Real.circleAverage (herglotzLogIntegrand✝ w ρ) 0 R))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.p_opcyclesMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {Z : C} (h : L.opcycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) h) =
    CategoryTheory.CategoryStruct.comp (φ.f i) (CategoryTheory.CategoryStruct.comp (L.pOpcycles i) h)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- A tensor product of symmetric bilinear maps is symmetric.  -/
LinearMap.BilinMap.tmul_isSymm : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₁]
  [inst_5 : AddCommMonoid N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁]
  [inst_9 : Module R N₁] [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : SMulCommClass R A N₁] [inst_14 : IsScalarTower R A N₁] [inst_15 : Module R M₂] [inst_16 : Module R N₂]
  {B₁ : LinearMap.BilinMap A M₁ N₁} {B₂ : LinearMap.BilinMap R M₂ N₂},
  (∀ (x y : M₁), (B₁ x) y = (B₁ y) x) →
    (∀ (x y : M₂), (B₂ x) y = (B₂ y) x) → ∀ (x y : TensorProduct R M₁ M₂), ((B₁.tmul B₂) x) y = ((B₁.tmul B₂) y) x
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instLineDerivSMulReal : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F], LineDerivSMul ℝ E (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U)))
  {t : Set ι}, t.Finite → t.Nonempty → X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.Eigenvalues.val : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (f : Module.End R M) → f.Eigenvalues → R
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_iff_initial_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Initial], G.Initial ↔ (F.comp G).Initial
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.finite_of_finite_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.IsFiniteMeasure (μ.conv ν)
-- Mathlib.Tactic.NormNum.NatFib
/-- Evaluates the `Nat.fib` function.  -/
Mathlib.Meta.NormNum.evalNatFib : Mathlib.Meta.NormNum.NormNumExt
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.filter_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).Equiv ↑m ↔ ∀ (a : α) (h : m.contains a = true), f a (m.get a h) = true)
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.toHomUnits.eq_1 : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : Monoid M] (f : G →* M),
  f.toHomUnits = Units.liftRight f (fun g => { val := f g, inv := f g⁻¹, val_inv := ⋯, inv_val := ⋯ }) ⋯
-- Mathlib.Topology.Algebra.Group.Pointwise
singleton_add_mem_nhds_of_nhds_zero : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α),
  s ∈ nhds 0 → {a} + s ∈ nhds a
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_ite_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => x = b] (a : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop],
  (∏'[L] (b' : β), if b' = b then a b' else 1) = a b
-- Init.Data.Order.Opposite
/-- Creates a {name}`Min` instance from a {name}`Max` instance.

The result is a {lean}`Min α` instance that uses {lean}`max.max` as its {name}`min` operation.

If {name}`max` obeys laws, then {lean}`max.oppositeMin` obeys the corresponding laws for {name}`Min`.
To automatically derive these laws, use {lit}`open scoped Std.OppositeOrderInstances`.

For example, one can use the derived instances to prove properties about the opposite {name}`Min`
instance:

```lean
open scoped Std.OppositeOrderInstances in
example [LE α] [DecidableLE α] [Max α] [Std.LawfulOrderLeftLeaningMax α] {a b : α} :
    letI : LE α := LE.opposite inferInstance
    letI : Min α := (inferInstance : Max α).oppositeMin
    min a b = if a ≤ b then a else b :=
  letI : LE α := LE.opposite inferInstance
  letI : Min α := (inferInstance : Max α).oppositeMin
  Std.min_eq_if
```

Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMin α`
instance for the opposite order that is required by {name}`min_eq_if`.
 -/
Max.oppositeMin : {α : Type u_1} → Max α → Min α
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- If `F : J ⥤ Type w₀` and `c : F.CoconeTypes` is colimit, then
`c` satisfies a heterogeneous universe version of the universal
property of colimits.  -/
CategoryTheory.Functor.CoconeTypes.IsColimit.desc : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → {c : F.CoconeTypes} → c.IsColimit → (c' : F.CoconeTypes) → c.pt → c'.pt
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const.instIsSFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μβ], ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.const α μβ)
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_and : ∀ (a b : UInt32), (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
-- Mathlib.Data.Finset.Insert
Finset.not_nontrivial_singleton : ∀ {α : Type u_1} {a : α}, ¬{a}.Nontrivial
-- Mathlib.Tactic.ScopedNS
/-- `scoped[NS]` is similar to the `scoped` modifier on attributes and notations,
but it scopes the syntax in the specified namespace instead of the current namespace.
```
scoped[Matrix] postfix:1024 "ᵀ" => Matrix.transpose
-- declares `ᵀ` as a notation for matrix transposition
-- which is only accessible if you `open Matrix` or `open scoped Matrix`.

namespace Nat

scoped[Nat.Count] attribute [instance] CountSet.fintype
-- make the definition Nat.CountSet.fintype an instance,
-- but only if `Nat.Count` is open
```
 -/
Mathlib.Tactic.scopedNS : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_whiskerRight : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  {X₁ X₂ : C₁ × C₂} (f : X₁ ⟶ X₂) (X : C₁ × C₂),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X =
    CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.1 X.1)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.2 X.2)
-- Mathlib.Data.Nat.Prime.Defs
Nat.dvd_prime : ∀ {p m : ℕ}, Nat.Prime p → (m ∣ p ↔ m = 1 ∨ m = p)
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- If `b` is weakly between `a` and `c`, and `p -ᵥ a` is orthogonal to `c -ᵥ a`,
then `p` is at least as close to `b` as to `c`.  -/
EuclideanGeometry.dist_le_of_wbtw_of_inner_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c p : P}, Wbtw ℝ a b c → inner ℝ (p -ᵥ a) (c -ᵥ a) = 0 → dist p b ≤ dist p c
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalMonoidHom_apply : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → MulOneClass (f i)] (i : I) (g : (i : I) → f i),
  (Pi.evalMonoidHom f i) g = g i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasAdditiveReduction.not_hasGoodReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.HasAdditiveReduction R W → ¬WeierstrassCurve.HasGoodReduction R W
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedCnstr : Inhabited Lean.Meta.Grind.EMatch.Cnstr
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceNatCastCore : Lean.Expr → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasCoproducts_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasProducts C],
  CategoryTheory.Limits.HasCoproducts Cᵒᵖ
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restriction of a `MonoidHom` to its range interpreted as a `Submonoid`.  -/
MonoidHom.mrangeRestrict : {M : Type u_1} →
  [inst : MulOneClass M] → {N : Type u_5} → [inst_1 : MulOneClass N] → (f : M →* N) → M →* ↥(MonoidHom.mrange f)
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piEquivLim.eq_1 : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {equiv : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j}
  (nat : InverseSystem.IsNatEquiv f equiv) (equivLim : F i ≃ ↑(InverseSystem.limit f i)) (hi : Order.IsSuccPrelimit i),
  InverseSystem.piEquivLim nat equivLim hi =
    InverseSystem.piSplitLE
      (equiv, equivLim.trans ((InverseSystem.invLimEquiv nat).trans (InverseSystem.piLTLim hi).symm))
-- Init.Data.Vector.Lemmas
Vector.anyM_toList : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Vector α n},
  List.anyM p xs.toList = Vector.anyM p xs
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_comp' : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] {G : Type u_4} [inst_14 : AddCommMonoid G] [inst_15 : Module R G]
  [inst_16 : StarAddMonoid G] [inst_17 : StarModule R G] [inst_18 : TopologicalSpace G] [inst_19 : ContinuousStar G]
  (f : E →L[R] F) (g : G →L[R] E),
  star (WithConv.toConv (f ∘SL g)) =
    WithConv.toConv ((star (WithConv.toConv f)).ofConv ∘SL (star (WithConv.toConv g)).ofConv)
-- Init.Data.Range.Polymorphic.Char
Char.pRangeSucc?_eq : Std.PRange.succ? = Char.succ?
-- Mathlib.LinearAlgebra.Complex.Module
nonneg_iff_realPart_imaginaryPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a : A}, 0 ≤ a ↔ 0 ≤ realPart a ∧ imaginaryPart a = 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The second projection `(homotopyCofiber φ).X i ⟶ G.X i`.  -/
HomologicalComplex.homotopyCofiber.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 : ι) → HomologicalComplex.homotopyCofiber.X φ i ⟶ G.X i
-- Init.Data.String.Iterate
/-- Creates an iterator over all characters \(Unicode code points\) in `s`, starting from the end
of the slice and iterating towards the start.

Example:

* `"abc".toSlice.revChars.toList = ['c', 'b', 'a']`

* `"ab∀c".toSlice.revChars.toList = ['c', '∀', 'b', 'a']`
 -/
String.Slice.revChars : (s : String.Slice) → Std.Iter Char
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (self : P.RightHomotopy f g), CategoryTheory.CategoryStruct.comp self.h P.p₀ = f
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.underObj.eq_1 : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) {X : T}
  (f : CategoryTheory.Under X), W.underObj f = W f.hom
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → (Equiv.pointReflection s.center) p₂ = p₁
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.continuousWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → ContinuousWithinAt f s x
-- Mathlib.NumberTheory.ZetaValues
/-- The Bernoulli polynomial, extended from `[0, 1)` to the unit circle.  -/
periodizedBernoulli : ℕ → UnitAddCircle → ℝ
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent_torsionBySet_of_isCoprime : ∀ {A : Type u_1} (M : Type u_2) [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M] [inst_2 : Module A M]
  (J : Ideal A), IsCoprime I J → Ideal.primaryComponent (↥(Submodule.torsionBySet A M ↑J)) I = ⊥
-- Mathlib.Geometry.Manifold.Riemannian.Basic
TangentSpace.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_2} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_3}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (_x : M), TangentSpace I _x = E
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} (Z : C) (g₁ : Z ⟶ I₁.Y) (g₂ : Z ⟶ I₂.Y)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f)
      CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam)
  (Z_1 : C) (g₁_1 : Z_1 ⟶ I₁.Y) (g₂_1 : Z_1 ⟶ I₂.Y)
  (w_1 :
    autoParam (CategoryTheory.CategoryStruct.comp g₁_1 I₁.f = CategoryTheory.CategoryStruct.comp g₂_1 I₂.f)
      CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam),
  ({ Z := Z, g₁ := g₁, g₂ := g₂, w := w } = { Z := Z_1, g₁ := g₁_1, g₂ := g₂_1, w := w_1 }) =
    (Z = Z_1 ∧ g₁ ≍ g₁_1 ∧ g₂ ≍ g₂_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapId'.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryTheory.CategoryStruct.id b),
  F.mapId' f hf = F.map₂Iso (CategoryTheory.eqToIso ⋯) ≪≫ F.mapId b
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.prod_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  (s : NonUnitalSubring R), s.prod ⊤ = NonUnitalSubring.comap (NonUnitalRingHom.fst R S) s
-- Mathlib.Data.Stream.Init
Stream'.take_zero : ∀ {α : Type u} (s : Stream' α), Stream'.take 0 s = []
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.namespace.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.namespace = 1
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Algebra.IsQuadraticExtension.finrank_eq_two' : ∀ {R : Type u_2} {S : Type u_3} {inst : CommSemiring R} {inst_1 : StrongRankCondition R} {inst_2 : Semiring S}
  {inst_3 : Algebra R S} [self : Algebra.IsQuadraticExtension R S], Module.finrank R S = 2
-- Mathlib.Order.WithBot
WithBot.lt_ofDual_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithTop α} {y : WithBot αᵒᵈ}, x < WithBot.ofDual y ↔ y < WithTop.toDual x
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] {X Y : CategoryTheory.Idempotents.Karoubi A} (f : X ⟶ Y),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.F Λ).map f).f = Λ.F.map f.f - Λ.F.map 0
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The 2-morphism filling the triangle diagram.  -/
CategoryTheory.Bicategory.RightLift.counit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} → (t : CategoryTheory.Bicategory.RightLift f g) → CategoryTheory.CategoryStruct.comp t.lift f ⟶ g
-- Mathlib.Order.Category.BddLat
BddLat.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory BddLat fun x1 x2 => BoundedLatticeHom ↑x1.toLat ↑x2.toLat
-- Init.Data.BitVec.Decidable
BitVec.forall_cons_iff : ∀ {n : ℕ} {P : BitVec (n + 1) → Prop}, (∀ (v : BitVec (n + 1)), P v) ↔ ∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v)
-- Init.Data.List.Sort.Impl
/-- An intermediate speed-up for `mergeSort`.
This version uses the tail-recursive `mergeTR` function as a subroutine.

This is not the final version we use at runtime, as `mergeSortTR₂` is faster.
This definition is useful as an intermediate step in proving the `@[csimp]` lemma for `mergeSortTR₂`.
 -/
List.MergeSort.Internal.mergeSortTR : {α : Type u_1} → List α → autoParam (α → α → Bool) List.MergeSort.Internal.mergeSortTR._auto_1 → List α
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchClone.tmpStar : Lean.Expr
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.lmapDomain_disjoint_ker : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_7} (f : α → α') {s : Set α},
  (∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) → Disjoint (Finsupp.supported M R s) (Finsupp.lmapDomain M R f).ker
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.mk.injEq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (set : ℕ → Set α)
  (set_mem : ∀ (i : ℕ), set i ∈ C) (finite : ∀ (i : ℕ), μ (set i) < ⊤) (spanning : ⋃ i, set i = Set.univ)
  (set_1 : ℕ → Set α) (set_mem_1 : ∀ (i : ℕ), set_1 i ∈ C) (finite_1 : ∀ (i : ℕ), μ (set_1 i) < ⊤)
  (spanning_1 : ⋃ i, set_1 i = Set.univ),
  ({ set := set, set_mem := set_mem, finite := finite, spanning := spanning } =
      { set := set_1, set_mem := set_mem_1, finite := finite_1, spanning := spanning_1 }) =
    (set = set_1)