mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Semiquot
/-- `pure a` is `a` reinterpreted as an unspecified element of `{a}`.  -/
Semiquot.pure : {α : Type u_1} → α → Semiquot α
-- Mathlib.Tactic.CongrExclamation
Lean.MVarId.congrCore! : Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.iSup_add_one_lt_of_lt_cof : ∀ {α : Type u} {f : α → Ordinal.{u}} {a : Ordinal.{u}}, Cardinal.mk α < a.cof → (∀ (i : α), f i < a) → ⨆ i, f i + 1 < a
-- Mathlib.RingTheory.GradedAlgebra.Radical
Ideal.IsPrime.homogeneousCore : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommRing A] [inst_1 : AddCommMonoid ι] [inst_2 : LinearOrder ι]
  [IsOrderedCancelAddMonoid ι] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] {𝒜 : ι → σ}
  [inst_6 : GradedRing 𝒜] {I : Ideal A}, I.IsPrime → (Ideal.homogeneousCore 𝒜 I).toIdeal.IsPrime
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.tsum_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (e : γ ≃ β)
  (f : β → α), ∑' (c : γ), f (e c) = ∑' (b : β), f b
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_left_right : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime x (y + x * z)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} (input : aig.RefVec w)
  (distance curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input distance curr hcurr s =
    if hcurr1 : curr < w then
      if hcurr2 : curr < w - distance % w then
        have ref := input.get (distance % w + curr) ⋯;
        have s := s.push ref;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input distance (curr + 1) ⋯ s
      else
        have ref := input.get (curr - (w - distance % w)) ⋯;
        have s := s.push ref;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input distance (curr + 1) ⋯ s
    else
      have hcurr := ⋯;
      hcurr ▸ s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
MeasureTheory.AEStronglyMeasurable.inner_const : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E} {c : E},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => inner 𝕜 (f x) c) μ
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Makes the identity isomorphism from a proof two subsemirings of a multiplicative
monoid are equal.  -/
RingEquiv.subsemiringCongr : {R : Type u} → [inst : NonAssocSemiring R] → {s t : Subsemiring R} → s = t → ↥s ≃+* ↥t
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {γ : Type u_6} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (κ : ProbabilityTheory.Kernel α Ω)
  (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.IndepFun f g κ μ =
    ProbabilityTheory.Kernel.Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) κ μ
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.instReprFixedParamPerms : Repr Lean.Elab.FixedParamPerms
-- Mathlib.CategoryTheory.Category.Pointed
/-- Morphisms in `Pointed`.  -/
Pointed.Hom : Pointed → Pointed → Type u
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeOption.match_1.splitter : {n : ℕ} →
  (motive : Option (Fin n) → Sort u_1) →
    (x : Option (Fin n)) → (Unit → motive none) → ((i : ℕ) → (h : i < n) → motive (some ⟨i, h⟩)) → motive x
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaCongrRight_symm : ∀ {α : Sort u_3} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a),
  (Equiv.psigmaCongrRight F).symm = Equiv.psigmaCongrRight fun a => (F a).symm
-- Mathlib.RingTheory.NoetherNormalization
/-- `hom1` is a homomorphism from `k[X_0,...X_{n-1}]` to `k[X_1,...X_n][X]/φ(T(I))`,
where `φ` is the isomorphism from `k[X_0,...X_{n-1}]` to `k[X_1,...X_n][X]`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.hom1 : {k : Type u_1} →
  [inst : Field k] →
    {n : ℕ} →
      (f : MvPolynomial (Fin (n + 1)) k) →
        (I : Ideal (MvPolynomial (Fin (n + 1)) k)) →
          MvPolynomial (Fin n) k →ₐ[MvPolynomial (Fin n) k]
            Polynomial (MvPolynomial (Fin n) k) ⧸
              Ideal.map (MvPolynomial.finSuccEquiv k n) (Ideal.map (NoetherNormalization.T✝ f) I)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.dist_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (y : α), LipschitzWith 1 fun x => dist x y
-- Mathlib.Analysis.Calculus.LHopital
deriv.lhopital_zero_atTop_on_Ioi : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  DifferentiableOn ℝ f (Set.Ioi a) →
    (∀ x ∈ Set.Ioi a, deriv g x ≠ 0) →
      Filter.Tendsto f Filter.atTop (nhds 0) →
        Filter.Tendsto g Filter.atTop (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atTop l →
            Filter.Tendsto (fun x => f x / g x) Filter.atTop l
-- Mathlib.Algebra.Free
FreeAddMagma.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- For a reduced, crystallographic, irreducible root pairing other than `𝔤₂`, if the sum of two
roots is a root, the bottom chain coefficient is either one or zero according to whether they are
perpendicular.

To see that this lemma fails for `𝔤₂`, let `α` (short) and `β` (long) be a base. Then the roots
`α` and `α + β` provide a counterexample.  -/
RootPairing.chainBotCoeff_if_one_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [inst_5 : Finite ι]
  [inst_6 : CharZero R] [inst_7 : IsDomain R] {i j : ι} [inst_8 : P.IsNotG2],
  P.root i + P.root j ∈ Set.range ⇑P.root → RootPairing.chainBotCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.toPreOneHypercover_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks], E.toPreOneHypercover.toPreZeroHypercover = E
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.Matcher.modifyStep.match_1.splitter : {α σ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    [inst : BEq α] →
      (m : Array.Matcher α) →
        [inst_1 : Std.Iterator σ n α] →
          (it : Std.IterM n σ) →
            (motive : it.internalState.inner.Step → Sort u_3) →
              (x : it.internalState.inner.Step) →
                ((property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) →
                    motive ⟨Std.IterStep.done, property⟩) →
                  ((it' : Std.IterM n α) →
                      (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                        motive ⟨Std.IterStep.skip it', property⟩) →
                    ((it' : Std.IterM n α) →
                        (x : α) →
                          (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' x)) →
                            motive ⟨Std.IterStep.yield it' x, property⟩) →
                      motive x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData)
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂)
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.instInhabitedCommandCodeActions : Inhabited Lean.CodeAction.CommandCodeActions
-- Mathlib.Order.Interval.Set.Monotone
strictMonoOn_Ici_of_pred_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {ψ : α → β} [inst_2 : PredOrder α]
  [IsPredArchimedean α] {n : α}, (∀ (m : α), n < m → ψ (Order.pred m) < ψ m) → StrictMonoOn ψ (Set.Ici n)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.add_comm : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.FindModelResult.mk : Lean.Expr → Option Manifold.Elab.NormedSpaceInfo → Manifold.Elab.FindModelResult
-- Mathlib.RingTheory.AdicCompletion.Completeness
/-- [Stacks Tag 05GG](https://stacks.math.columbia.edu/tag/05GG) ((2)) -/
AdicCompletion.pow_smul_top_eq_ker_eval : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ}, I.FG → I ^ n • ⊤ = (AdicCompletion.eval I M n).ker
-- Mathlib.Analysis.Convex.Uniform
exists_forall_sphere_dist_add_le_two_sub : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ},
  0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.hasFDerivWithinAt : ∀ {𝕜 : 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] {x : E}
  {s : Set E} (iso : E ≃L[𝕜] F), HasFDerivWithinAt (⇑iso) (↑iso) s x
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The normalized chain complex of a simplicial set `X` with coefficients in `R`.
In degree `n`, it consists of a coproduct of copies of `R` indexed by the
nondegenerate `n`-simplices of `X`.  -/
SSet.normalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] → [inst_2 : CategoryTheory.Preadditive C] → SSet → C → ChainComplex C ℕ
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
continuous functions when `0 < p < ∞`, version in terms of `∫`.  -/
MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α]
  [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ},
  0 < p →
    ∀ {f : α → E},
      MeasureTheory.MemLp f (ENNReal.ofReal p) μ →
        ∀ {ε : ℝ},
          0 < ε →
            ∃ g,
              HasCompactSupport g ∧
                ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g (ENNReal.ofReal p) μ
-- Mathlib.Order.Lattice
Antitone.map_inf : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeSup β] {f : α → β},
  Antitone f → ∀ (x y : α), f (min x y) = f x ⊔ f y
-- Init.Data.BitVec.Lemmas
/-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
the bits from `xlo` when `start + len` is within `xlo`.
 -/
BitVec.extractLsb'_append_eq_of_add_le : ∀ {v w : ℕ} {xhi : BitVec v} {xlo : BitVec w} {start len : ℕ},
  start + len ≤ w → BitVec.extractLsb' start len (xhi ++ xlo) = BitVec.extractLsb' start len xlo
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric
second derivative. Version in a complete space. One could also give a version avoiding
completeness but requiring that `f` is a local diffeomorphism.  -/
VectorField.pullbackWithin_lieBracketWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} {t : Set F},
  minSmoothness 𝕜 2 ≤ n →
    ContDiffWithinAt 𝕜 n f s x →
      DifferentiableWithinAt 𝕜 V t (f x) →
        DifferentiableWithinAt 𝕜 W t (f x) →
          UniqueDiffOn 𝕜 s →
            x ∈ s →
              x ∈ closure (interior s) →
                Set.MapsTo f s t →
                  VectorField.pullbackWithin 𝕜 f (VectorField.lieBracketWithin 𝕜 V W t) s x =
                    VectorField.lieBracketWithin 𝕜 (VectorField.pullbackWithin 𝕜 f V s)
                      (VectorField.pullbackWithin 𝕜 f W s) s x
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.contains_empty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering}, Std.DTreeMap.Internal.Cell.empty.contains = false
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_eq_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
-- Mathlib.Algebra.Notation.Defs
ite_mul_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a b c d : α),
  ((if P then a else b) * if P then c else d) = if P then a * c else b * d
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_sum_left : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {ι : Type u_3} {s : Finset ι} {x : ι → E} {y : E},
  inner A (∑ i ∈ s, x i) y = ∑ i ∈ s, inner A (x i) y
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- For `p = 1` (hence, for any `p ≤ 1`), the condition `LiouvilleWith p x` is trivial.  -/
liouvilleWith_one : ∀ (x : ℝ), LiouvilleWith 1 x
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_le_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet Q P)
-- Mathlib.Data.Set.Sigma
Set.insert_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι},
  (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t
-- Mathlib.Data.EReal.Inv
EReal.le_div_iff_mul_le : ∀ {a b c : EReal}, b > 0 → b ≠ ⊤ → (a ≤ c / b ↔ a * b ≤ c)
-- Batteries.Data.UnionFind.Basic
/-- Auxiliary function for find operation  -/
Batteries.UnionFind.findAux : (self : Batteries.UnionFind) → Fin self.size → Batteries.UnionFind.FindAux self.size
-- Init.Data.List.ToArray
List.insertIdx_toArray : ∀ {α : Type u_1} (l : List α) (i : ℕ) (a : α) (h : i ≤ l.toArray.size),
  l.toArray.insertIdx i a h = (l.insertIdx i a).toArray
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_le_toColex : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α},
  toColex s ≤ toColex t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
-- Mathlib.Data.List.Shortlex
List.Shortlex.trichotomous : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r], Std.Trichotomous (List.Shortlex r)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_eq_exp_neg_multiplicity : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r ≠ 0 → v.intValuation r = WithZero.exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))
-- Mathlib.GroupTheory.Submonoid.Center
/-- For an additive monoid, the units of the center inject into the center of the units.  -/
addUnitsCenterToCenterAddUnits : (M : Type u_1) → [inst : AddMonoid M] → AddUnits ↥(AddSubmonoid.center M) →+ ↥(AddSubmonoid.center (AddUnits M))
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.congr_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y) {Z : D} (h_1 : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1))
-- Init.Data.Int.DivMod.Lemmas
Int.emod_lt : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a % b < ↑b.natAbs
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Inhabited ↥(spinGroup Q)
-- Lean.Level
Lean.instReprLMVarId : Repr Lean.LMVarId
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.sInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {S : Set (Set E)}, (∀ s ∈ S, AbsConvex 𝕜 s) → AbsConvex 𝕜 (⋂₀ S)
-- Mathlib.Combinatorics.Colex
Finset.Colex.instDecidableLE : {α : Type u_1} → [inst : PartialOrder α] → [DecidableEq α] → [DecidableLE α] → DecidableLE (Colex (Finset α))
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.rightIso.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma R₁ L₁} (α : X ≅ Y),
  CategoryTheory.Comma.rightIso α = (CategoryTheory.Comma.snd R₁ L₁).mapIso α
-- Mathlib.MeasureTheory.Function.EssSup
/-- Essential supremum of `f` with respect to measure `μ`: the smallest `c : β` such that
`f x ≤ c` a.e.  -/
essSup : {α : Type u_1} →
  {β : Type u_2} → [ConditionallyCompleteLattice β] → {x : MeasurableSpace α} → (α → β) → MeasureTheory.Measure α → β
-- Batteries.Data.List.Basic
/-- `List.mapWithPrefixSuffix f l` maps `f` across a list `l`.
For each `a ∈ l` with `l = pref ++ [a] ++ suff`, `a` is mapped to `f pref a suff`.
Example: if `f : list Nat → Nat → list Nat → β`,
`List.mapWithPrefixSuffix f [1, 2, 3]` will produce the list
`[f [] 1 [2, 3], f [1] 2 [3], f [1, 2] 3 []]`.
 -/
List.mapWithPrefixSuffix : {α : Type u_1} → {β : Type u_2} → (List α → α → List α → β) → List α → List β
-- Init.Data.UInt.Basic
instModUInt8 : Mod UInt8
-- Mathlib.Topology.MetricSpace.Holder
holderOnWith_one : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C 1 f s ↔ LipschitzOnWith C f s
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.go_eq : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β} {bs : List β},
  Std.IterM.toListRev.go it bs = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => Std.IterM.toListRev.go it' (out :: bs)
      | Std.IterStep.skip it' => Std.IterM.toListRev.go it' bs
      | Std.IterStep.done => pure bs
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.skeletal : CategoryTheory.Skeletal SimplexCategory
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → M),
  (∑ i ∈ s, if i ∈ t then f i else 0) = ∑ i ∈ s ∩ t, f i
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.compContinuousLinearMap_id : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), p.compContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) = p
-- Mathlib.Algebra.Category.MonCat.Basic
addEquivIsoAddCommMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y],
  addEquivIsoAddCommMonCatIso =
    { hom := TypeCat.ofHom fun e => e.toAddCommMonCatIso, inv := TypeCat.ofHom fun i => i.commMonCatIsoToAddEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Analysis.Convex.Between
Sbtw.left_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Sbtw R x y z → x ≠ y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α},
  t.WF →
    (Array.find? (fun x => compare x.1 k == Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toArray t) = none ↔ k ∉ t)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] [inst_5 : SizeOf C] [inst_6 : SizeOf J]
  (F : CategoryTheory.Functor J C) (isoBot : F.obj ⊥ ≅ X)
  (isWellOrderContinuous :
    autoParam F.IsWellOrderContinuous CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam)
  (incl : F ⟶ (CategoryTheory.Functor.const J).obj Y)
  (isColimit : CategoryTheory.Limits.IsColimit { pt := Y, ι := incl })
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp isoBot.inv (incl.app ⊥) = f)
      CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam),
  sizeOf
      { F := F, isoBot := isoBot, isWellOrderContinuous := isWellOrderContinuous, incl := incl, isColimit := isColimit,
        fac := fac } =
    1 + sizeOf F + sizeOf isoBot + sizeOf isWellOrderContinuous + sizeOf incl + sizeOf isColimit + sizeOf fac
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.single_add : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) (m₁ m₂ : M),
  PolynomialModule.single R n (m₁ + m₂) = PolynomialModule.single R n m₁ + PolynomialModule.single R n m₂
-- Mathlib.Logic.Hydra
Relation.instIsWellFoundedMultisetCutExpand : ∀ {α : Type u_1} {r : α → α → Prop} [h : IsWellFounded α r], IsWellFounded (Multiset α) (Relation.CutExpand r)
-- Init.Data.SInt.Basic
instPowInt16Nat : Pow Int16 ℕ