mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastShiftRightConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.ShiftTarget w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst aig target).vec.get idx hidx }⟧ =
    if hidx : target.distance + idx < w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance + idx) hidx }⟧
    else false
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.mk.inj : ∀ {tokens : Lean.Parser.TokenTable} {kinds : Lean.Parser.SyntaxNodeKindSet} {categories : Lean.Parser.ParserCategories}
  {tokens_1 : Lean.Parser.TokenTable} {kinds_1 : Lean.Parser.SyntaxNodeKindSet}
  {categories_1 : Lean.Parser.ParserCategories},
  { tokens := tokens, kinds := kinds, categories := categories } =
      { tokens := tokens_1, kinds := kinds_1, categories := categories_1 } →
    tokens = tokens_1 ∧ kinds = kinds_1 ∧ categories = categories_1
-- Mathlib.Algebra.Polynomial.Splits
/-- A polynomial of degree `2` with a root splits.  -/
Polynomial.Splits.of_natDegree_eq_two : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R} {x : R}, f.natDegree = 2 → Polynomial.eval x f = 0 → f.Splits
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The condition that `h : A.PairingCore` involves only inner horns.  -/
SSet.Subcomplex.PairingCore.IsInner : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → Prop
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : M ≃+ P}
  (H : AddSubmonoid.map k.symm.toAddMonoidHom T = S) (x : M), (f.ofAddEquivOfDom H) (k x) = f x
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_norm : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : SeminormedAddCommGroup β],
  MeasureTheory.stoppedProcess (fun t ω => ‖u t ω‖) τ = fun i ω => ‖MeasureTheory.stoppedProcess u τ i ω‖
-- Mathlib.Analysis.Distribution.TestFunction
/-- The inclusion of the space `𝓓^{n}(Ω, F)` into the space `E →ᵇ F` of bounded continuous
functions as a continuous `𝕜`-linear map.  -/
TestFunction.toBoundedContinuousFunctionCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {n : ℕ∞} →
                      [inst_6 : Algebra ℝ 𝕜] →
                        [inst_7 : IsScalarTower ℝ 𝕜 F] → TestFunction Ω F n →L[𝕜] BoundedContinuousFunction E F
-- Mathlib.Order.Closure
LowerAdjoint.le_closure_iff : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u)
  (x y : α), x ≤ u (l.toFun y) ↔ u (l.toFun x) ≤ u (l.toFun y)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- The tensor product of modules is commutative, up to linear equivalence.  -/
TensorProduct.comm : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      (N : Type u_8) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → TensorProduct R M N ≃ₗ[R] TensorProduct R N M
-- Mathlib.Probability.Process.Predictable
/-- **Alias** of `MeasureTheory.IsStronglyPredictable.stronglyAdapted`.

---

A predictable process is adapted.  -/
MeasureTheory.IsPredictable.adapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E]
  [inst_1 : LinearOrder ι] [inst_2 : OrderBot ι] [inst_3 : MeasurableSpace ι] [inst_4 : TopologicalSpace ι]
  [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : MeasureTheory.Filtration ι m} {u : ι → Ω → E},
  MeasureTheory.IsStronglyPredictable 𝓕 u → MeasureTheory.StronglyAdapted 𝓕 u
-- Mathlib.Data.Seq.Computation
Computation.terminates_def : ∀ {α : Type u} (s : Computation α), s.Terminates ↔ ∃ n, (↑s n).isSome = true
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Auxiliary definition for `equivalenceModuleMonoidAlgebra`.  -/
Rep.unitIsoAddEquiv : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        {V : Rep.{w, u, v} k G} → ↑V ≃+ ↑((Rep.toModuleMonoidAlgebra.comp Rep.ofModuleMonoidAlgebra).obj V)
-- Aesop.Forward.State
/-- Erase a pattern substitution from the cluster state.  -/
Aesop.ClusterState.erasePatSubst : Aesop.Substitution → Aesop.PremiseIndex → Aesop.ClusterState → Aesop.ClusterState
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.smul_left_def : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : SMul R S] (x : WithVal v) (s : S), x • s = x.ofVal • s
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The right homology map data expressing that null homotopic maps induce the zero
morphism in right homology.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.ofNullHomotopic : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (H₁ : S₁.RightHomologyData) →
          (H₂ : S₂.RightHomologyData) →
            (h₀ : S₁.X₁ ⟶ S₂.X₁) →
              (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) →
                (h₁ : S₁.X₂ ⟶ S₂.X₁) →
                  (h₂ : S₁.X₃ ⟶ S₂.X₂) →
                    (h₃ : S₁.X₃ ⟶ S₂.X₃) →
                      (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) →
                        CategoryTheory.ShortComplex.RightHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁
                          H₂
-- Mathlib.Algebra.Order.Ring.Defs
one_sub_le_one_add_mul_one_sub : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b c : R},
  c + b * c ≤ a + b → 1 - a ≤ (1 + b) * (1 - c)
-- Mathlib.Order.OrderDual
OrderDual.instIsTransLe : ∀ {α : Type u_1} [inst : LE α] [T : IsTrans α LE.le], IsTrans αᵒᵈ LE.le
-- Mathlib.Algebra.Group.Submonoid.Support
/-- A submonoid is pointed if it has zero support.  -/
Submonoid.IsMulPointed : {G : Type u_1} → [inst : Group G] → Submonoid G → Prop
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPProofs : Lean.Options → Bool
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the oriented angle between three points is `π / 2`, so is the unoriented angle
(reversed).  -/
EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_univ_iff : ∀ {α : Type u}, Set.univ.Infinite ↔ Infinite α
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `edist_one_right`. -/
edist_one_eq_enorm : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), edist a 1 = ‖a‖ₑ
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instCoeSortType.eq_1 : AddSemigrp.instCoeSortType = { coe := AddSemigrp.carrier }
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.InitiallySmall.mk : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J], (∃ S x F, F.Initial) → CategoryTheory.InitiallySmall J
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.small : ∀ {L : FirstOrder.Language} {α : Type u'} [Small.{u, u'} α], Small.{u, max u u'} (L.Term α)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.Hom.hom.eq_1 : ∀ {M N : ProfiniteAddGrp.{u}} (f : M.Hom N), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_EStateM : ∀ {ε σ δ α : Type u_1} {x : EStateM ε σ α} {h : ε → EStateM ε σ α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))}
  [inst : EStateM.Backtrackable δ σ],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q = fun s =>
    (Std.Do.wp x).apply
      (Q.1, fun e s' => (Std.Do.wp (h e)).apply Q (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s)),
        Q.2.2)
      s
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Icc_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Icc a b = Set.Icc (b / c) (a / c)
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.IsProper.lintegral_mul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {f g : X → ENNReal},
  π.IsProper →
    𝓑 ≤ 𝓧 → Measurable f → Measurable g → ∀ (x₀ : X), ∫⁻ (x : X), g x * f x ∂π x₀ = g x₀ * ∫⁻ (x : X), f x ∂π x₀
-- Mathlib.CategoryTheory.Category.Quiv
/-- The forgetful functor from categories to quivers.  -/
CategoryTheory.Quiv.forget : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Quiv
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.lintegral_le_meas : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  (∀ (a : α), f a ≤ 1) → (∀ a ∈ sᶜ, f a = 0) → ∫⁻ (a : α), f a ∂μ ≤ μ s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k).getKey a h' = t.getKey a ⋯
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.sup`. -/
DeltaGeneratedSpace.sup : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {t₁ t₂ : TopologicalSpace Y},
  Topology.IsGeneratedBy X Y → Topology.IsGeneratedBy X Y → Topology.IsGeneratedBy X Y
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivFunctorCompFstIso_hom_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (X_1 : A),
  (CategoryTheory.Sum.functorEquivFunctorCompFstIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inl X_1))
-- Mathlib.Analysis.Normed.Module.Convex
Filter.Eventually.segment_of_prod_nhds : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {α : Type u_2} {f : Filter α} {x : E}
  {y z : α → E} {r : α → E → Prop},
  Filter.Tendsto y f (nhds x) →
    Filter.Tendsto z f (nhds x) →
      (∀ᶠ (p : α × E) in f ×ˢ nhds x, r p.1 p.2) → ∀ᶠ (χ : α) in f, ∀ v ∈ segment ℝ (y χ) (z χ), r χ v
-- Mathlib.Data.Finset.Lattice.Fold
map_finset_inf' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  [inst_2 : FunLike F α β] [InfHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ι → α),
  f (s.inf' hs g) = s.inf' hs (⇑f ∘ g)
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.isOrderedAddCancelMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α}, IsOrderedCancelAddMonoid (AddLocalization s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.filterMap_equiv_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filterMap (fun k => Option.guard fun v => f k v) t).Equiv (Std.DTreeMap.filter f t)
-- Mathlib.Data.Fintype.Inv
Function.Embedding.left_inv_of_invOfMemRange : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β) (b : ↑(Set.range ⇑f)),
  f (f.invOfMemRange b) = ↑b
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.natCast_div_mul_eq_nsmul : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q r : 𝕜) (m : ℕ), ↑(↑m / q * r) = m • ↑(r / q)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedPartialFixpointType.default : Lean.Elab.PartialFixpointType
-- Lean.PrettyPrinter
_private.Lean.PrettyPrinter.0.Lean.PrettyPrinter.maybePrependExprSizes : Lean.Expr → Std.Format → Lean.MetaM Std.Format
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_cexp_neg_mul_sum_add : ∀ {b : ℂ} {ι : Type u_2} [inst : Fintype ι],
  0 < b.re →
    ∀ (c : ι → ℂ),
      ∫ (v : ι → ℝ), Complex.exp (-b * ∑ i, ↑(v i) ^ 2 + ∑ i, c i * ↑(v i)) =
        (↑Real.pi / b) ^ (↑(Fintype.card ι) / 2) * Complex.exp ((∑ i, c i ^ 2) / (4 * b))
-- Mathlib.RingTheory.Artinian.Module
Function.Surjective.isArtinianRing : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] {f : F}, Function.Surjective ⇑f → ∀ [H : IsArtinianRing R], IsArtinianRing S
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.prodMkLeft_comp_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ],
  (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.prodMkLeft α η) = (μ.bind ⇑κ).bind ⇑η
-- Lean.Elab.Binders
/-- Expand `matchAlts` syntax into a full `match`-expression.
Example:
```
| 0, true => alt_1
| i, _    => alt_2
```
expands into (for tactic == false)
```
fun x_1 x_2 =>
match @x_1, @x_2 with
| 0, true => alt_1
| i, _    => alt_2
```
and (for tactic == true)
```
intro x_1; intro x_2;
match @x_1, @x_2 with
| 0, true => alt_1
| i, _    => alt_2
```

If `useExplicit = true`, we add a `@` before `fun` to disable implicit lambdas. We disable them when processing `let` and `let rec` declarations
to make sure the behavior is consistent with top-level declarations where we can write
```
def f : {α : Type} → α → α
  | _, a => a
```
We use `useExplicit = false` when we are elaborating the `fun | ... => ... | ...` notation. See issue #1132.
If `@fun` is used with this notation, the we set `useExplicit = true`.
We also use `useExplicit = false` when processing `instance ... where` notation declarations. The motivation is to have compact declarations such as
```
instance [Alternative m] : MonadLiftT Option m where
monadLift -- We don't want to provide the implicit arguments of `monadLift` here. One should use `monadLift := @fun ...` if they want to provide them.
  | some a => pure a
  | none => failure
```

Remark: we add `@` at discriminants to make sure we don't consume implicit arguments, and to make the behavior consistent with `fun`.
Example:
```
inductive T : Type 1 :=
| mkT : (forall {a : Type}, a -> a) -> T

def makeT (f : forall {a : Type}, a -> a) : T :=
  mkT f

def makeT' : (forall {a : Type}, a -> a) -> T
| f => mkT f
```
The two definitions should be elaborated without errors and be equivalent.
 -/
Lean.Elab.Term.expandMatchAltsIntoMatch : Lean.Syntax → Lean.Syntax → optParam Bool true → Lean.MacroM Lean.Syntax
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.ret.inj : ∀ {x x_1 : Lean.IR.Arg}, Lean.IR.FnBody.ret x = Lean.IR.FnBody.ret x_1 → x = x_1
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeftEquiv_trans : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂]
  [inst_2 : MulOneClass M₃] [inst_3 : Monoid N] (e₁₂ : M₁ ≃* M₂) (e₂₃ : M₂ ≃* M₃),
  (e₁₂.trans e₂₃).monoidHomCongrLeftEquiv = e₁₂.monoidHomCongrLeftEquiv.trans e₂₃.monoidHomCongrLeftEquiv
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.derivative_iterate : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k : ℕ)
  (f : LaurentSeries V), (⇑(LaurentSeries.derivative R))^[k] f = k.factorial • (LaurentSeries.hasseDeriv R k) f
-- Mathlib.Algebra.Quaternion
Quaternion.instGroupWithZero : {R : Type u_1} → [inst : Field R] → [inst_1 : LinearOrder R] → [IsStrictOrderedRing R] → GroupWithZero (Quaternion R)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.beq_zero_eq_ite' : ∀ {b : Bool} {a : BitVec 1}, (b == (a == 0#1)) = (a == bif b then 0#1 else 1#1)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_leftUnitor_hom_eq_leftUnitor_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D] [inst_5 : CategoryTheory.MonoidalCategoryStruct D]
  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D)
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)],
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor d).hom =
    (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)).hom
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_whiskerRight : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {L M : QuadraticModuleCat R} (f : L ⟶ M)
  (N : QuadraticModuleCat R),
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) =
    (QuadraticModuleCat.Hom.toIsometry f).tmul (QuadraticMap.Isometry.id N.form)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Any pair of finite measures `μ` and `ν`, `HaveLebesgueDecomposition`. That is to say,
there exist a measure `ξ` and a measurable function `f`, such that `ξ` is mutually singular
with respect to `ν` and `μ = ξ + ν.withDensity f`.

This is not an instance since this is also shown for the more general σ-finite measures with
`MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite`.  -/
MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], μ.HaveLebesgueDecomposition ν
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.le_def' : ∀ {x y : ℝ}, x ≤ y ↔ x < y ∨ x = y
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.comp.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (hnp : N →ₙ* P)
  (hmn : M →ₙ* N), hnp.comp hmn = { toFun := fun x => hnp (hmn x), map_mul' := ⋯ }
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.prev : ∀ {l m₁ : List Char} {c : Char} {m₂ r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l (m₁ ++ c :: m₂) r s →
    s.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { byteIdx := String.utf8Len m₁ }
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_ground : ∀ {α : Type u_1} {E : Set α}, (Matroid.freeOn E).E = E
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBot_neg : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  LieModule.chainBot (-α) β = LieModule.chainTop α β
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.mk.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MultispanShape} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (left : J.L → C) (right : J.R → C) (fst : (a : J.L) → left a ⟶ right (J.fst a))
  (snd : (a : J.L) → left a ⟶ right (J.snd a)), sizeOf { left := left, right := right, fst := fst, snd := snd } = 1
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), AddSubgroup.comap K.subtype H = H.addSubgroupOf K
-- Lean.Parser.Extension
Lean.Parser.internal.parseQuotWithCurrentStage : Lean.Option Bool
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (t.insert k v).minKey? = some (t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k')
-- Init.Data.BitVec.Lemmas
BitVec.sle.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.sle y = decide (x.toInt ≤ y.toInt)
-- Mathlib.Data.Nat.Totient
Nat.totient_mul_of_prime_of_dvd : ∀ {p n : ℕ}, Nat.Prime p → p ∣ n → (p * n).totient = p * n.totient
-- Std.Http.Data.Body.Basic
/-- Gets the declared size of the body.
 -/
Std.Http.Body.getKnownSize : {α : Type} → [self : Std.Http.Body α] → α → Std.Async.Async (Option Std.Http.Body.Length)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termι' : Lean.ParserDescr
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.natCast_def' : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : AddCommMonoidWithOne A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoidWithOne B] [inst_4 : Module R B] (n : ℕ), ↑n = 1 ⊗ₜ[R] ↑n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.edges_takeUntil_subset_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).edges ⊆ p.edges
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.Ideal.mk_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {m n : ℕ},
  m ≤ n →
    ∀ (r : AdicCompletion.AdicCauchySequence I R),
      (Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_pow_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (n : ℕ),
  autoParam (p a) cfc_pow_id._auto_1 → cfc (fun x => x ^ n) a = a ^ n
-- Lean.MetavarContext
/-- This field tracks how old a metavariable is. It is set using a counter at `MetavarContext`.
We primarily use the index of a level metavariable for pretty printing.  -/
Lean.LevelMetavarDecl.index : Lean.LevelMetavarDecl → ℕ
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.reflectsColimit_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.ReflectsColimit (F.comp G) H],
  CategoryTheory.Limits.ReflectsColimit G H