mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.mulHeightBound_eq : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K]
  (p : ι' → MvPolynomial ι K),
  Height.mulHeightBound p =
    (Multiset.map (fun v => ⨆ j, (p j).coeff.sum fun x c => v c) Height.AdmissibleAbsValues.archAbsVal).prod *
      ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (MvPolynomial.coeff (↑s) (p j))) 1
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_natDegree_le : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.natDegree ≤ f.natDegree
-- Mathlib.MeasureTheory.Measure.Content
/-- The underlying additive function  -/
MeasureTheory.Content.toFun : {G : Type w} → [inst : TopologicalSpace G] → MeasureTheory.Content G → TopologicalSpace.Compacts G → NNReal
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.sum_to_range : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Set.range (Profinite.NobelingProof.GoodProducts.sum_to C ho) =
    Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ∪
      Profinite.NobelingProof.GoodProducts.MaxProducts C ho
-- Std.Time.Format.DateFormat
/-- Abbreviated weekday names (7 elements, index 0 = Mon).
 -/
Std.Time.DateFormatSymbols.weekdayShort : Std.Time.DateFormatSymbols → Vector String 7
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_one_lt_d9 : Real.exp 1 < 2.7182818286
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Attempts to find the value with key `k : α` in `t` and panics if there is no such key.
 -/
RBTree.RBSet.find! : {α : Type u_1} → {cmp : α → α → Ordering} → [Inhabited α] → RBTree.RBSet α cmp → α → α
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The $L^1$ norm is less than the $L^\infty$ norm
scaled by the cardinality.  -/
Pi.sum_nnnorm_apply_le_nnnorm : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)]
  (f : (i : ι) → G i), ∑ i, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- An element in `d.Extension val₀ j` induces an element in `d.Extension val₀ i` when `i ≤ j`.  -/
CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] →
            {val₀ : F.obj (Opposite.op ⊥)} → {j : J} → d.Extension val₀ j → {i : J} → i ≤ j → d.Extension val₀ i
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_eq_one_iff_unique : ∀ {α : Type u}, Cardinal.toNat (Cardinal.mk α) = 1 ↔ Subsingleton α ∧ Nonempty α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall.mk.injEq : ∀ («to» : Lean.Lsp.CallHierarchyItem) (fromRanges : Array Lean.Lsp.Range) (to_1 : Lean.Lsp.CallHierarchyItem)
  (fromRanges_1 : Array Lean.Lsp.Range),
  ({ «to» := «to», fromRanges := fromRanges } = { «to» := to_1, fromRanges := fromRanges_1 }) =
    («to» = to_1 ∧ fromRanges = fromRanges_1)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.left_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s = s ∪ t ↔ t ⊆ s
-- Mathlib.Data.Finsupp.SMul
/-- `Finsupp.comapSMul` is distributive  -/
Finsupp.comapDistribMulAction : {α : Type u_1} →
  {M : Type u_3} →
    {G : Type u_5} → [inst : Monoid G] → [MulAction G α] → [inst_2 : AddCommMonoid M] → DistribMulAction G (α →₀ M)
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A] [inst_5 : Bialgebra R B] [inst_6 : Algebra R A]
  [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A],
  CoalgebraStruct.comul =
    ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
        (Algebra.TensorProduct.map (Bialgebra.comulAlgHom S A) (Bialgebra.comulAlgHom R B))).toLinearMap
-- Mathlib.SetTheory.Ordinal.Basic
/-- To define a function on ordinals, it suffices to define them on order types of well-orders.

Since `LinearOrder` is data-carrying, `liftOnWellOrder_type` is not a definitional equality, unlike
`Quotient.liftOn_mk` which is always def-eq.  -/
Ordinal.liftOnWellOrder : {δ : Sort v} →
  Ordinal.{u_1} →
    (f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ) →
      (∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
          [inst_3 : WellFoundedLT β],
          ((Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2) → f α = f β) →
        δ
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.isoApp_trans : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) (g : Y ≅ Z),
  CategoryTheory.DifferentialObject.isoApp (f ≪≫ g) =
    CategoryTheory.DifferentialObject.isoApp f ≪≫ CategoryTheory.DifferentialObject.isoApp g
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_mod_lt : ∀ {R : Type u} [inst : Field R] (p : Polynomial R) {q : Polynomial R}, q ≠ 0 → (p % q).degree < q.degree
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone : ∀ {I : Type u} (X : I → TopCat), CategoryTheory.IsIso (FundamentalGroupoidFunctor.piTopToPiCone X)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The interior of a simplex is the set of points that can be expressed as an affine combination
of the vertices with weights in a set `I`.  -/
Affine.Simplex.setInterior : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → Set k → {n : ℕ} → Affine.Simplex k P n → Set P
-- Init.Data.List.Lex
List.map_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [Std.Asymm fun x1 x2 => x1 < x2]
  [Std.Trichotomous fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {l₁ l₂ : List α} {f : α → β}, (∀ (x y : α), x < y → f x < f y) → l₁ ≤ l₂ → List.map f l₁ ≤ List.map f l₂
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_left_inj : ∀ {a b c : ENNReal}, a ≠ ⊤ → (b + a = c + a ↔ b = c)
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `f a ≤ B a`;
* `B` has right derivative `B'` at every point of `[a, b)`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
  is bounded above by `B'`.

Then `f x ≤ B x` everywhere on `[a, b]`.  -/
image_le_of_liminf_slope_right_le_deriv_boundary : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    ∀ {B B' : ℝ → ℝ},
      f a ≤ B a →
        ContinuousOn B (Set.Icc a b) →
          (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
            (∀ x ∈ Set.Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) →
              ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchResult.mk.injEq : ∀ {α : Type} (elts elts_1 : Array (Array (Array α))), ({ elts := elts } = { elts := elts_1 }) = (elts = elts_1)
-- Mathlib.Analysis.Analytic.Binomial
Real.one_div_one_sub_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun x => 1 / (1 - x)) (FormalMultilinearSeries.ofScalars ℝ 1) 0 1
-- Init.Data.UInt.Lemmas
UInt32.lt_asymm : ∀ {a b : UInt32}, a < b → ¬b < a
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgEquiv.toBialgIso_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Bialgebra R X]
  [inst_4 : Bialgebra R Y] (e : X ≃ₐc[R] Y), e.symm.toBialgIso = e.toBialgIso.symm
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.run.match_1.eq_2 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → Sort u_2) (ca : Computation α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (ca : Computation α) → motive (Sum.inr ca)),
  (match Sum.inr ca with
    | Sum.inl a => h_1 a
    | Sum.inr ca => h_2 ca) =
    h_2 ca
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.toHeap.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (x : ℕ) (res : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : (x : ℕ) → (res : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.HeapNode.nil x res)
  (h_2 :
    (a : α) →
      (c s : Batteries.BinomialHeap.Imp.HeapNode α) →
        (n : ℕ) →
          (res : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a c s) n res),
  (match Batteries.BinomialHeap.Imp.HeapNode.nil, x, res with
    | Batteries.BinomialHeap.Imp.HeapNode.nil, x, res => h_1 x res
    | Batteries.BinomialHeap.Imp.HeapNode.node a c s, n, res => h_2 a c s n res) =
    h_1 x res
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.symm : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  s₁.Equivalent s₂ → s₂.Equivalent s₁
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.u_iInf : ∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {u : α → β}
  {l : β → α}, GaloisConnection l u → ∀ {f : ι → α}, u (iInf f) = ⨅ i, u (f i)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space `E` gives
an internal direct sum decomposition of `E`.  -/
LinearMap.IsSymmetric.direct_sum_isInternal : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E],
  T.IsSymmetric → DirectSum.IsInternal fun μ => Module.End.eigenspace T (↑T 1 μ)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The range of the inclusion map is equal to the kernel of the projection map.  -/
AddGroupExtension.range_inl_eq_ker_rightHom : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (self : AddGroupExtension N E G), self.inl.range = self.rightHom.ker
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_four : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 4 → M), ∏ i, f i = f 0 * f 1 * f 2 * f 3
-- Mathlib.Topology.Instances.CantorSet
preCantorSet_succ : ∀ (n : ℕ), preCantorSet (n + 1) = (fun x => x / 3) '' preCantorSet n ∪ (fun x => (2 + x) / 3) '' preCantorSet n
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Reified `lhs`  -/
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.rlhs : Lean.Meta.Grind.Arith.CommRing.DiseqCnstr → Lean.Meta.Grind.Arith.CommRing.RingExpr
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.smallSchroder.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ),
  (n = 0 → False) →
    (match n.succ with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | n.succ => h_3 n) =
      h_3 n
-- Lean.Data.NameMap.Basic
Lean.NameHashSet.instInhabited : Inhabited Lean.NameHashSet
-- Init.Data.Array.Basic
Array.instForIn'InferInstanceMembershipOfMonad : {α : Type u} → {m : Type u_1 → Type u_2} → [Monad m] → ForIn' m (Array α) α inferInstance
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkAtomCached.match_1.eq_1 : ∀ {α : Type} (decls : Array (Std.Sat.AIG.Decl α)) (decl : Std.Sat.AIG.Decl α)
  (motive : Option (Std.Sat.AIG.CacheHit decls decl) → Sort u_1) (hit : Std.Sat.AIG.CacheHit decls decl)
  (h_1 : (hit : Std.Sat.AIG.CacheHit decls decl) → motive (some hit)) (h_2 : Unit → motive none),
  (match some hit with
    | some hit => h_1 hit
    | none => h_2 ()) =
    h_1 hit
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.offset_of_isLongestRevMatchAt : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat.isEmpty = false →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ → pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Multipliable.hasProd_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {a : α} [T2Space α] [L.NeBot], Multipliable f L → (HasProd f a L ↔ ∏'[L] (b : β), f b = a)
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to an `Int64`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toInt64 : Float.Model → Int64
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.hasCoeOpens.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.hasCoeOpens = { coe := OpenAddSubgroup.toOpens }
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.le_addRothNumber : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s t : Finset α},
  ThreeAPFree ↑s → s ⊆ t → s.card ≤ addRothNumber t
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map_comp_inlAlgHom : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N),
  (TrivSqZeroExt.map f).comp (TrivSqZeroExt.inlAlgHom R' R' M) = TrivSqZeroExt.inlAlgHom R' R' N
-- Init.Data.Sum.Basic
Sum.getRight?_inl : ∀ {α : Type u_1} {β : Type u_2} {x : α}, (Sum.inl x).getRight? = none
-- Mathlib.Order.Category.BddLat
BddLat.hom_ext_iff : ∀ {X Y : BddLat} {f g : X ⟶ Y}, f = g ↔ BddLat.Hom.hom f = BddLat.Hom.hom g
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.ofMon : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setRoot.eq_1 : ∀ {α : Type u_1} (v : α),
  RBTree.RBNode.setRoot v RBTree.RBNode.nil =
    RBTree.RBNode.node RBTree.RBColor.red RBTree.RBNode.nil v RBTree.RBNode.nil
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_le_of_le_left : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => c ≤ x], c ≤ a → {x ∈ Finset.Ico a b | c ≤ x} = Finset.Ico a b
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.ControlStack.stateT.stM : Lean.Elab.Do.MonadInfo → Array Lean.Elab.Do.MutVar → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β},
  ⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y)
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- Shifting `f` by `(1 / (2 * ‖w‖ ^ 2)) • w` negates the integral in the Riemann-Lebesgue lemma.  -/
fourierIntegral_half_period_translate : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : V → E}
  [inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] [inst_5 : InnerProductSpace ℝ V]
  [inst_6 : FiniteDimensional ℝ V] {w : V},
  w ≠ 0 →
    ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f (v + (fun w => (1 / (2 * ‖w‖ ^ 2)) • w) w) =
      -∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformCauchySeqOn.add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (f + f') l s
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.one_le_mult : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, 1 ≤ ↑w.mult
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.isLeast_opNorm : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F),
  IsLeast {c | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.equivMonComonCounitIsoAppX M).inv.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.Data.Int.Bitwise
Int.lnot.eq_2 : ∀ (n : ℕ), (Int.negSucc n).lnot = ↑n
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.integral_traj_partialTraj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] {a b : ℕ},
  a ≤ b →
    ∀ {x₀ : (i : ↥(Finset.Iic a)) → X ↑i} {f : ((n : ℕ) → X n) → E},
      MeasureTheory.Integrable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
        ∫ (x : (i : ↥(Finset.Iic b)) → X ↑i),
            ∫ (y : (n : ℕ) → X n),
              f y ∂(ProbabilityTheory.Kernel.traj κ b) x ∂(ProbabilityTheory.Kernel.partialTraj κ a b) x₀ =
          ∫ (x : (n : ℕ) → X n), f x ∂(ProbabilityTheory.Kernel.traj κ a) x₀
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.union!_equiv_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ m₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁.union! m₂).Equiv (m₃.union! m₄)
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.cons_mem_paths_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {p : Quiver.Path X Y} {f : Y ⟶ Z}, W.paths (p.cons f) ↔ W.paths p ∧ W f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLT_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, cmp a k = Ordering.lt} (h : t₁.Equiv t₂), t₁.getEntryLT k h' = t₂.getEntryLT k ⋯
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.of_surjective_algHom : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Algebra.QuasiFinite R S] (f : S →ₐ[R] T),
  Function.Surjective ⇑f → Algebra.QuasiFinite R T
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- See `le_linearGrowthSup_add` for a version with swapped argument `u` and `v`.  -/
LinearGrowth.le_linearGrowthSup_add' : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthInf u + LinearGrowth.linearGrowthSup v ≤ LinearGrowth.linearGrowthSup (u + v)
-- Mathlib.Algebra.Ring.Equiv
/-- `RingEquivClass F R S` states that `F` is a type of ring structure preserving equivalences.
You should extend this class when you extend `RingEquiv`.  -/
RingEquivClass : (F : Type u_7) → (R : Type u_8) → (S : Type u_9) → [Mul R] → [Add R] → [Mul S] → [Add S] → [EquivLike F R S] → Prop
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.instInhabited : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} → [inst_2 : CategoryTheory.EnrichedCategory V C] → Inhabited (CategoryTheory.EnrichedFunctor V C C)
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α}, l.contains k = false → k ∈ m.insertManyIfNewUnit l → k ∈ m
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {T : CategoryTheory.Over A} {X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A}
  (f : CategoryTheory.yoneda.obj X ⟶ (CategoryTheory.overEquivPresheafCostructuredArrow A).functor.obj T),
  (CategoryTheory.overEquivPresheafCostructuredArrow A).functor.map
      ((CategoryTheory.ConcreteCategory.hom
          (((CategoryTheory.CostructuredArrow.toOverCompCoyoneda A).inv.app (Opposite.op X)).app T))
        f) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).hom.app X) f
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_eq_div' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p q : Polynomial K),
  RatFunc.mk p q =
    {
      toFractionRing :=
        (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p /
          (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }
-- Init.SimpLemmas
Bool.not_eq_false' : ∀ (b : Bool), ((!b) = false) = (b = true)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_one : ∀ {w : ℕ}, 1 < w → (1#w).toInt = 1
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize_tail? : ∀ {α : Type u_1} {le : α → α → Bool} {s' s : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.tail? le s = some s' → s.realSize = s'.realSize + 1
-- Mathlib.Probability.Kernel.Composition.MeasureComp
/-- This lemma allows to rewrite the composition of a measure and a kernel as the composition
of two kernels, which allows to transfer properties of `∘ₖ` to `∘ₘ`.  -/
MeasureTheory.Measure.comp_eq_comp_const_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β}, μ.bind ⇑κ = (κ.comp (ProbabilityTheory.Kernel.const Unit μ)) ()
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonnegg.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (a b : ℕ) (h_1 : (a b : ℕ) → motive (Int.ofNat a) (Int.ofNat b))
  (h_2 : (a b : ℕ) → motive (Int.ofNat a) (Int.negSucc b)) (h_3 : (a b : ℕ) → motive (Int.negSucc a) (Int.ofNat b))
  (h_4 : (a a_1 : ℕ) → motive (Int.negSucc a) (Int.negSucc a_1)),
  (match Int.ofNat a, Int.ofNat b with
    | Int.ofNat a, Int.ofNat b => h_1 a b
    | Int.ofNat a, Int.negSucc b => h_2 a b
    | Int.negSucc a, Int.ofNat b => h_3 a b
    | Int.negSucc a, Int.negSucc a_1 => h_4 a a_1) =
    h_1 a b
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.revSkip?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos res : s.Pos},
  pos.revSkip? P = some res ↔ ∃ (h : pos ≠ s.startPos), res = pos.prev h ∧ P ((pos.prev h).get ⋯)
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toCommRingCatIso_hom : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toCommRingCatIso.hom = CommRingCat.ofHom ↑e