mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α) (w : ℕ)
  (input : aig.RefVec w) (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)}
  {k a : α} {v : β k},
  Std.Internal.List.getKey! a (Std.Internal.List.insertEntryIfNew k v l) =
    if (k == a) = true ∧ Std.Internal.List.containsKey k l = false then k else Std.Internal.List.getKey! a l
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- Given presentations of `T` over `S` and of `S` over `R`,
we may construct a presentation of `T` over `R`.  -/
Algebra.Presentation.comp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {ι' : Type u_1} →
                {σ' : Type u_2} →
                  {T : Type u_3} →
                    [inst_3 : CommRing T] →
                      [inst_4 : Algebra S T] →
                        Algebra.Presentation S T ι' σ' →
                          Algebra.Presentation R S ι σ →
                            [inst_5 : Algebra R T] → [IsScalarTower R S T] → Algebra.Presentation R T (ι' ⊕ ι) (σ' ⊕ σ)
-- Mathlib.Algebra.Order.Ring.Defs
IsOrderedRing.toIsOrderedAddMonoid : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsOrderedRing R], IsOrderedAddMonoid R
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.forgetEval_inv_app : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (X : HomologicalComplex V c),
  (HomologicalComplex.forgetEval V c i).inv.app X = CategoryTheory.CategoryStruct.id (X.X i)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_naturality_app : ∀ {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]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {G' H' : CategoryTheory.Functor C V}
  (ℌ' : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G' H')
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F H'] (η : G ⟶ G'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) (ℌ.map η ℌ')) ℌ'.ev_app =
    CategoryTheory.CategoryStruct.comp ℌ.ev_app η
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.liftBoundedOrder.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : Preorder α]
  [inst_2 : BoundedOrder α] (gi : GaloisInsertion l u),
  gi.liftBoundedOrder = { toOrderTop := gi.liftOrderTop, toOrderBot := ⋯.liftOrderBot }
-- Mathlib.Data.Analysis.Filter
CFilter.mk : {α : Type u_1} →
  {σ : Type u_2} →
    [inst : PartialOrder α] →
      (f : σ → α) →
        σ → (inf : σ → σ → σ) → (∀ (a b : σ), f (inf a b) ≤ f a) → (∀ (a b : σ), f (inf a b) ≤ f b) → CFilter α σ
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.ext : ∀ {n d : ℕ} (x y : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })),
  (∀ (i : Fin (d + 1)), x i = y i) → x = y
-- Lean.Parser.Syntax
Lean.Parser.Command.identPrec.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Nat.Basic
Nat.lt_of_sub_pos : ∀ {n m : ℕ}, 0 < n - m → m < n
-- Mathlib.RingTheory.WittVector.Frobenius
/-- `frobenius` is tautologically a polynomial function.  -/
WittVector.frobenius_isPoly : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.IsPoly p fun R _Rcr => ⇑WittVector.frobenius
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- The indicator of a set $A$ and a family of random variables $(X_1, ..., X_p)$ are independent
if for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$  -/
indicator_indepFun_pi_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P] [Finite S]
  {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
          ∫ (ω : Ω) in A, f fun x => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X x ω ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) (fun ω s => X s ω) P
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
/-- The chosen terminal object in `Cat` is terminal.  -/
CategoryTheory.Cat.chosenTerminalIsTerminal : CategoryTheory.Limits.IsTerminal CategoryTheory.Cat.chosenTerminal
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
/-- A finset of `finrank R M` vectors forms a basis if they span the whole space,
provided `R` satisfies the Orzech property.  -/
finsetBasisOfTopLeSpanOfCardEqFinrank : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [OrzechProperty R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            {s : Finset M} → ⊤ ≤ Submodule.span R ↑s → s.card = Module.finrank R M → Module.Basis (↥s) R M
-- Mathlib.Analysis.Normed.Group.Real
Real.norm : Norm ℝ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).functor.obj X).right = X.right
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.adj_homEquiv : ∀ (R : Type u) [inst : Ring R] (X : Type u) (M : ModuleCat R), (ModuleCat.adj R).homEquiv X M = ModuleCat.freeHomEquiv
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A category with weak equivalences is a category equipped with
a class of morphisms named "weak equivalences".  -/
HomotopicalAlgebra.CategoryWithWeakEquivalences : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sdiff_ne_prod_sdiff_iff : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq ι] [inst_1 : CancelCommMonoid M] {s t : Finset ι} {f : ι → M},
  ∏ i ∈ s \ t, f i ≠ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≠ ∏ i ∈ t, f i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = true → t.max! = default
-- Init.Prelude
/-- Propositional equality is `Decidable` for all elements of a type.

In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.
 -/
DecidableEq : Sort u → Sort (max 1 u)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.length_cycleBypass_le_length : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (w : G.Walk v v), w.cycleBypass.length ≤ w.length
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.isDynCoverOf_empty_right : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ}, Dynamics.IsDynCoverOf T F U n ∅ ↔ F = ∅
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.intersperseTR.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x y : α) → (xs : List α) → motive (x :: y :: xs)),
  (match [x] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: xs => h_3 x y xs) =
    h_2 x
-- Std.Time.Format.Modifier
Std.Time.Modifier.D.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.D presentation) = 1 + sizeOf presentation
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : β → β},
  (t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.Data.PNat.Prime
PNat.Coprime.gcd_mul_right_cancel : ∀ (m : ℕ+) {n k : ℕ+}, k.Coprime n → (m * k).gcd n = m.gcd n
-- Mathlib.Data.Set.Pairwise.Basic
Set.Nonempty.pairwise_iff_exists_forall : ∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} [IsEquiv α r] {s : Set ι},
  s.Nonempty → (s.Pairwise (Function.onFun r f) ↔ ∃ z, ∀ x ∈ s, r (f x) z)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_comp_tensorAssoc : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
  (Q₃ : QuadraticForm R M₃),
  QuadraticMap.comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanIndexEnd_left : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (j : (CategoryTheory.Limits.multicospanShapeEnd J).L),
  (CategoryTheory.Limits.multicospanIndexEnd F).left j = (F.obj (Opposite.op j)).obj j
-- Mathlib.Analysis.Convex.Function
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is strictly convex, it suffices
to verify the inequality `f (a • x + b • y) < a • f x + b • f y` for `x < y` and positive `a`, `b`.
The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.  -/
LinearOrder.strictConvexOn_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β]
  [inst_7 : LinearOrder E] {s : Set E} {f : E → β},
  Convex 𝕜 s →
    (∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y) →
      StrictConvexOn 𝕜 s f
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.induction_on : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {motive : Monoid.Coprod M N → Prop}
  (m : Monoid.Coprod M N),
  (∀ (m : M), motive (Monoid.Coprod.inl m)) →
    (∀ (n : N), motive (Monoid.Coprod.inr n)) →
      (∀ (x y : Monoid.Coprod M N), motive x → motive y → motive (x * y)) → motive m
-- Mathlib.Order.Zorn
/-- **Zorn's lemma**

If every chain has an upper bound, then there exists a maximal element.  -/
exists_maximal_of_chains_bounded : ∀ {α : Type u_1} {r : α → α → Prop},
  (∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub) →
    (∀ {a b c : α}, r a b → r b c → r a c) → ∃ m, ∀ (a : α), r m a → r a m
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v],
  v RatFunc.X ≤ 1 → {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
-- Mathlib.Data.Fin.Tuple.Basic
/-- Updating the first element of a tuple does not change the tail.  -/
Fin.tail_update_zero : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (q : (i : Fin (n + 1)) → α i) (z : α 0),
  Fin.tail (Function.update q 0 z) = Fin.tail q
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite : ∀ {w : ℕ} (cond : Bool) {a b c : BitVec w}, (bif cond then ~~~bif cond then a else b else c) = bif cond then ~~~a else c
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instTop.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := ⋯ } }
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Two triangles with the same points have the same orthocenter.  -/
Affine.Triangle.orthocenter_eq_of_range_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t₁ t₂ : Affine.Triangle ℝ P},
  Set.range t₁.points = Set.range t₂.points → t₁.orthocenter = t₂.orthocenter
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- The isomorphism from `GL n R` to the general linear group of a module
associated with a basis.  -/
Matrix.GeneralLinearGroup.toLin' : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          {V : Type u_1} →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → Module.Basis n R V → GL n R ≃* LinearMap.GeneralLinearGroup R V
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology],
  (S.map F).Exact ↔ CategoryTheory.Limits.IsZero (F.obj h.H)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- A family of `MvPowerSeries` in the form `1 + f i` is multipliable if the order of `f i`
tends to infinity.  -/
MvPowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top : ∀ {σ : Type u_3} {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {ι : Type u_5}
  {f : ι → MvPowerSeries σ R} [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι],
  Filter.Tendsto (fun i => (f i).order) Filter.atTop (nhds ⊤) → Multipliable fun x => 1 + f x
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_eq_sum_interpolate_insert_sdiff : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s t : Finset ι} {v : ι → F} (r : ι → F),
  Set.InjOn v ↑t →
    s.Nonempty →
      s ⊆ t →
        (Lagrange.interpolate t v) r = ∑ i ∈ s, (Lagrange.interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d),
  I.fstPiMapOfIsLimit c hd =
    CategoryTheory.Limits.Fan.IsLimit.lift hd fun i => CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (I.fst i)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (a : C) → (F.obj a ⟶ a) → CategoryTheory.Endofunctor.Algebra F
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_coeff : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ) (f : Polynomial R) (n : ℕ),
  ((Polynomial.hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
isMIntegralCurveOn_iff_isMIntegralCurveAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ},
  IsOpen s → (IsMIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsMIntegralCurveAt γ v t)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The free functor `Type u ⥤ AddCommMonCat`
sending a type `X` to the free commutative monoid on `X`.  -/
AddCommMonCat.free : CategoryTheory.Functor (Type u) AddCommMonCat
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A measure `μ` is called finite if `μ univ < ∞`.  -/
MeasureTheory.IsFiniteMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {f g : α → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) → f =ᵐ[μ] g
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [inst_5 : F.Additive]
  [inst_6 : G.Additive] [inst_7 : H.Additive],
  CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α)
      (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β)
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.generateMeasurableRec_subset : ∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}),
  MeasurableSpace.generateMeasurableRec s i ⊆ {t | MeasurableSpace.GenerateMeasurable s t}
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- A function in `Lp` can be approximated in `Lp` by continuous functions.  -/
MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [inst_3 : BorelSpace α]
  (E : Type u_2) [inst_4 : NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [NormedSpace ℝ E]
  [inst_6 : SecondCountableTopologyEither α E] [inst_7 : Fact (1 ≤ p)],
  p ≠ ⊤ → ∀ [μ.WeaklyRegular], (MeasureTheory.Lp.boundedContinuousFunction E p μ).topologicalClosure = ⊤
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go.eq_def : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (x : α) (i j : ℕ) (xs : List α),
  List.minIdxOn.go✝ f x i j xs =
    match xs with
    | [] => i
    | y :: ys => if f x ≤ f y then List.minIdxOn.go✝ f x i (j + 1) ys else List.minIdxOn.go✝ f y j (j + 1) ys
-- Init.Data.String.Lemmas.Basic
String.sliceTo_sliceFrom : ∀ {s : String} {pos : s.Pos} {pos' : (s.sliceFrom pos).Pos},
  (s.sliceFrom pos).sliceTo pos' = s.slice pos (String.Pos.ofSliceFrom pos') ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  ∅.Equiv m ↔ m.isEmpty = true
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.Equivalence.trans.eq_1 : ∀ {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] (e : C ≌ D) (f : D ≌ E),
  e.trans f =
    { functor := e.functor.comp f.functor, inverse := f.inverse.comp e.inverse,
      unitIso :=
        e.unitIso ≪≫
          CategoryTheory.Functor.isoWhiskerRight
              (e.functor.rightUnitor.symm ≪≫
                e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm)
              e.inverse ≪≫
            (e.functor.comp f.functor).associator f.inverse e.inverse,
      counitIso :=
        ((f.inverse.comp e.inverse).associator e.functor f.functor).symm ≪≫
          CategoryTheory.Functor.isoWhiskerRight
              (f.inverse.associator e.inverse e.functor ≪≫
                f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor)
              f.functor ≪≫
            f.counitIso,
      functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_left_π : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.π =
    X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_neg : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃), (-a).imK = -a.imK
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] [inst_4 : Inhabited α] {f : α → β → Bool} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filter f m).getKey! k = ((m.getKey? k).pfilter fun x h' => f x m[x]).get!
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Value of Riemann zeta at `-ℕ` in terms of `bernoulli`.  -/
riemannZeta_neg_nat_eq_bernoulli : ∀ (k : ℕ), riemannZeta (-↑k) = (-1) ^ k * ↑(bernoulli (k + 1)) / (↑k + 1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.denote_getD_eq_getLsbD : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool)
  (x : BitVec w) (xv : aig.RefVec w) (falseRef : aig.Ref),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx) →
    ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
      ∀ (idx : ℕ), ⟦assign, { aig := aig, ref := xv.getD idx falseRef }⟧ = x.getLsbD idx
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_bijective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B], Function.Bijective ContinuousAlgEquiv.symm
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x x' y : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F x x' → CommRingCat.Colimits.Relation F (x.mul y) (x'.mul y)