mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNum.match_1.eq_1 : ∀ (motive : Num → Sort u_1) (h_1 : Unit → motive Num.zero) (h_2 : (n : PosNum) → motive (Num.pos n)),
  (match Num.zero with
    | Num.zero => h_1 ()
    | Num.pos n => h_2 n) =
    h_1 ()
-- Init.Data.Array.Lemmas
Array.foldr_map_hom' : ∀ {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α} {start : ℕ},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) →
    start = xs.size → Array.foldr f' (g a) (Array.map g xs) start = g (Array.foldr f a xs)
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderIso.image_setOfPred_minimal`. -/
OrderIso.image_setOf_minimal : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (P : α → Prop),
  ⇑f '' {x | Minimal P x} = {x | Minimal (fun x => P (f.symm x)) x}
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `exists_isOpen_xor_mem`. -/
exists_isOpen_xor'_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {x y : X}, x ≠ y → ∃ U, IsOpen U ∧ Xor (x ∈ U) (y ∈ U)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.mulDistribMulAction : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] →
      [inst_1 : Monoid α] → [MulDistribMulAction R' α] → (S : Subsemiring R') → MulDistribMulAction (↥S) α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntry!_eq_getEntry! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α]
  [inst_3 : Inhabited ((a : α) × β a)] {k : α} {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.getEntry! k = Std.Internal.List.getEntry! k t.toListModel
-- Mathlib.Computability.Encoding
Computability.decode_encodeBool : ∀ (b : Bool), Computability.decodeBool (Computability.encodeBool b) = b
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Countable unions of compact sets are σ-compact.  -/
isSigmaCompact_sUnion_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)},
  S.Countable → (∀ s ∈ S, IsCompact s) → IsSigmaCompact (⋃₀ S)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The "right" map `Y ⟶ Z`.  -/
CategoryTheory.IsRegularMono.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.IsRegularMono f] → Y ⟶ CategoryTheory.IsRegularMono.Z f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.add_iff_right : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : AddCommGroup β] [IsTopologicalAddGroup β],
  MeasureTheory.StronglyMeasurable f → (MeasureTheory.StronglyMeasurable (f + g) ↔ MeasureTheory.StronglyMeasurable g)
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperHemicontinuousAt_iff_frequently`. -/
UpperHemicontinuousAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) →
    UpperHemicontinuousAt f x
-- Init.Data.SInt.Lemmas
Int64.not_lt_minValue : ∀ {a : Int64}, ¬a < Int64.minValue
-- Mathlib.Combinatorics.Matroid.Minor.Delete
/-- The deletion `M ＼ D` is the restriction of a matroid `M` to `M.E \ D`.
Its independent sets are the `M`-independent subsets of `M.E \ D`.  -/
Matroid.delete : {α : Type u_1} → Matroid α → Set α → Matroid α
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (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.yield it' out, h⟩ 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_1 it' out h
-- Mathlib.Data.List.Map2
List.zipLeft_cons_cons : ∀ {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β),
  (a :: as).zipLeft (b :: bs) = (a, some b) :: as.zipLeft bs
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_iff_exists_natCard_le_orderOf : ∀ {α : Type u_1} [inst : Group α] [Finite α], IsCyclic α ↔ ∃ g, Nat.card α ≤ orderOf g
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Associated.normalizedFactors_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a b : α},
  Associated a b → UniqueFactorizationMonoid.normalizedFactors a = UniqueFactorizationMonoid.normalizedFactors b
-- Mathlib.RingTheory.OrzechProperty
/-- A ring `R` satisfies the Orzech property, if for any finitely generated `R`-module `M`,
any surjective homomorphism `f : N → M` from a submodule `N` of `M` to `M` is injective.

NOTE: In the definition we need to assume that `M` has the same universe level as `R`, but it
in fact implies the universe polymorphic versions
`OrzechProperty.injective_of_surjective_of_injective`
and `OrzechProperty.injective_of_surjective_of_submodule`.  -/
OrzechProperty : (R : Type u) → [Semiring R] → Prop
-- Mathlib.Algebra.Group.Pi.Units
Pi.instSubsingletonAddUnits : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] [∀ (i : ι), Subsingleton (AddUnits (M i))],
  Subsingleton (AddUnits ((i : ι) → M i))
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_toLinearMap : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑↑e = e.toLinearMap
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.refl_apply : ∀ {M : Type u_4} [inst : Mul M] (m : M), (MulEquiv.refl M) m = m
-- Mathlib.LinearAlgebra.Ray
/-- An arbitrary nonzero vector giving a ray.  -/
Module.Ray.someVector : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Module.Ray R M → M
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of strands associated with a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.strands : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    Mathlib.Tactic.BicategoryLike.NormalExpr →
      Mathlib.Tactic.BicategoryLike.CoherenceM ρ (List (List Mathlib.Tactic.Widget.StringDiagram.Strand))
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Monotone.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α]
  [inst_4 : Preorder β] {f : β → α}, Monotone f → Antitone fun x => (f x)⁻¹
-- Init.Data.List.Basic
List.eraseIdx_cons_succ : ∀ {α : Type u_1} {a : α} {as : List α} {i : ℕ}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F), deriv (fun x => c - f x) x = -deriv f x
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.prev.eq_1 : ∀ (x : String.Pos.Raw) (s : String) (b stopPos : String.Pos.Raw),
  { str := s, startPos := b, stopPos := stopPos }.prev x =
    if x.offsetBy b = b then x else { byteIdx := (String.Pos.Raw.prev s (x.offsetBy b)).byteIdx - b.byteIdx }
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject C}
  (s : X.Splitting) (f g : X ⟶ Y), (∀ (n : ℕ), s.φ f n = s.φ g n) → f = g
-- Mathlib.Topology.UnitInterval
unitInterval.eq_one_or_eq_zero_of_le_mul : ∀ {i j : ↑unitInterval}, i ≤ j * i → i = 0 ∨ j = 1
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.lctx : ProofWidgets.ExprWithCtx → Lean.LocalContext
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (S : L.Substructure M) (g : L.Hom N P) (f : L.Hom M N),
  FirstOrder.Language.Substructure.map g (FirstOrder.Language.Substructure.map f S) =
    FirstOrder.Language.Substructure.map (g.comp f) S
-- Mathlib.Tactic.CategoryTheory.Bicategory.Basic
/-- Use the coherence theorem for bicategories to solve equations in a bicategory,
where the two sides only differ by replacing strings of bicategory structural morphisms
(that is, associators, unitors, and identities)
with different strings of structural morphisms with the same source and target.

That is, `bicategory` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `bicategory_coherence`.
 -/
Mathlib.Tactic.Bicategory.tacticBicategory : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Combination
/-- A convex combination of two centers of mass is a center of mass as well. This version
deals with two different index types.  -/
Finset.centerMass_segment' : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} {ι' : Type u_6} [inst : Field R] [inst_1 : AddCommGroup E]
  [inst_2 : Module R E] (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E) (wt : ι' → R) (zt : ι' → E),
  ∑ i ∈ s, ws i = 1 →
    ∑ i ∈ t, wt i = 1 →
      ∀ (a b : R),
        a + b = 1 →
          a • s.centerMass ws zs + b • t.centerMass wt zt =
            (s.disjSum t).centerMass (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt)
-- Mathlib.Algebra.Group.Units.Defs
/-- The inverse value of `val` in the base `Monoid`.  -/
Units.inv : {α : Type u} → [inst : Monoid α] → αˣ → α
-- Mathlib.Data.Set.Semiring
SetSemiring.down_ssubset_down : ∀ {α : Type u_1} {s t : SetSemiring α}, SetSemiring.down s ⊂ SetSemiring.down t ↔ s < t
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- The base ring is a left identity for the tensor product of coalgebras, up to
coalgebra equivalence.  -/
Coalgebra.TensorProduct.lid : (R : Type u_5) →
  (P : Type u_9) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid P] → [inst_2 : Module R P] → [inst_3 : Coalgebra R P] → TensorProduct R R P ≃ₗc[R] P
-- Aesop.Script.SScript
Aesop.Script.instInhabitedSScript.default : Aesop.Script.SScript
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveWhiskeringRight : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Preadditive E], (CategoryTheory.Functor.whiskeringRight C D E).Additive
-- Init.Data.Rat.Lemmas
Rat.floor_lt_iff : ∀ {a : ℚ} {x : ℤ}, a.floor < x ↔ a < ↑x
-- Mathlib.Data.Multiset.MapFold
Multiset.rel_map_right : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset α} {t : Multiset γ} {f : γ → β},
  Multiset.Rel r s (Multiset.map f t) ↔ Multiset.Rel (fun a b => r a (f b)) s t
-- Mathlib.Data.Set.Function
Set.exists_injOn_iff_injective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [Nonempty β], (∃ f, Set.InjOn f s) ↔ ∃ f, Function.Injective f
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Smooth.mk : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  autoParam (Algebra.FormallySmooth R A) Algebra.Smooth.formallySmooth._autoParam →
    autoParam (Algebra.FinitePresentation R A) Algebra.Smooth.finitePresentation._autoParam → Algebra.Smooth R A
-- Mathlib.CategoryTheory.Sites.CoproductSheafCondition
/-- Let `E` be a pre-`0`-hypercover with pairwise pullbacks. If `∐ᵢ Eᵢ` is a universal coproduct
and the presheaf `F` preserves products, then the multifork associated to the single object
`0`-hypercover `{ ∐ᵢ Eᵢ ⟶ S }` is exact if and only if the multifork for `E` is exact.
 -/
CategoryTheory.PreZeroHypercover.isLimitSigmaOfIsColimitEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
        {S : C} →
          (E : CategoryTheory.PreZeroHypercover S) →
            [inst_2 : E.HasPullbacks] →
              {c : CategoryTheory.Limits.Cofan E.X} →
                (hc : CategoryTheory.Limits.IsColimit c) →
                  CategoryTheory.IsUniversalColimit c →
                    [inst_3 : (E.sigmaOfIsColimit hc).HasPullbacks] →
                      [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)] →
                        (F : CategoryTheory.Functor Cᵒᵖ A) →
                          [CategoryTheory.Limits.PreservesLimit
                                (CategoryTheory.Discrete.functor fun i => Opposite.op (E.toPreOneHypercover.X i)) F] →
                            [CategoryTheory.Limits.PreservesLimit
                                  (CategoryTheory.Discrete.functor fun i => Opposite.op (E.toPreOneHypercover.Y' i))
                                  F] →
                              CategoryTheory.Limits.IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
                                CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)
-- Mathlib.Logic.Equiv.Basic
/-- A sigma type over a subtype is equivalent to the sigma set over the original type,
if the fiber is empty outside of the subset  -/
Equiv.sigmaSubtypeEquivOfSubset : {α : Type u_9} → (p : α → Type v) → (q : α → Prop) → (∀ (x : α) (a : p x), q x) → (x : Subtype q) × p ↑x ≃ (x : α) × p x
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
IsUltrametricDist.invariantExtension_apply : ∀ (K : Type u_1) [inst : NormedField K] (L : Type u_2) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (x : L),
  (IsUltrametricDist.invariantExtension K L) x = ⨆ σ, (IsUltrametricDist.algNormOfAlgEquiv σ) x
-- Mathlib.Topology.Separation.Regular
/-- This technique to witness `HasSeparatingCover` in regular Lindelöf topological spaces
will be used to prove regular Lindelöf spaces are normal.  -/
IsClosed.HasSeparatingCover : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X],
  IsClosed s → IsClosed t → Disjoint s t → HasSeparatingCover s t
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Ioo : ∀ {a b : ℝ}, MeasureTheory.volume.real (Set.Ioo a b) = max (b - a) 0
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.foldlM_list : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : List α} {init : β} {f : β → α → m β}
  (inv : Std.Internal.Do.Invariant xs β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun b' =>
        inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'; epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs, property := ⋯ } init ⦄ List.foldlM f init xs ⦃ fun b =>
      inv { «prefix» := xs, suffix := [], property := ⋯ } b; epost ⦄
-- Init.Data.SInt.Lemmas
ISize.mul_assoc : ∀ (a b c : ISize), a * b * c = a * (b * c)
-- Std.Http.Server.Config
/-- Converts to HTTP/1.1 config.
 -/
Std.Http.Config.toH1Config : Std.Http.Config → Std.Http.Protocol.H1.Config
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsBigO.trans_isEquivalent : ∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f : α → β₂} {g₁ g₂ : α → β}, f =O[l] g₁ → Asymptotics.IsEquivalent l g₁ g₂ → f =O[l] g₂
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.of_isIso : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [inst_7 : CategoryTheory.IsIso τ]
  [CategoryTheory.NatTrans.CommShift τ A], CategoryTheory.NatTrans.CommShift (CategoryTheory.inv τ) A
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.instBEqAtomicFact.beq : Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.Order.AtomicFact → Bool
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.beq : Std.Tactic.BVDecide.Gate
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isMaximumIndepSet_iff : ∀ {α : Type u_3} [inst : Finite α] (G : SimpleGraph α) (s : Finset α),
  G.IsMaximumIndepSet s ↔ G.IsIndepSet ↑s ∧ ∀ (t : Finset α), G.IsIndepSet ↑t → t.card ≤ s.card
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.existsAddOfLe : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [ExistsMulOfLE α], ExistsAddOfLE (Additive α)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instMonoidWithZero : {A : Type u_1} → [inst : NonUnitalNonAssocSemiring A] → [inst_1 : StarAddMonoid A] → MonoidWithZero (A →⋆ₙ+* A)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_apply : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
  s.indicator f a = if a ∈ s then f a else 0
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'_apply' : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix n n R₁) (v w : n → R₁), ((Matrix.toBilin' M) v) w = v ⬝ᵥ M.mulVec w
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.sum' : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {I : ℕ → α},
  Monotone I →
    ∀ {n : ℕ}, ∑ i ∈ Finset.range n, eVariationOn f (Set.Icc (I i) (I (i + 1))) = eVariationOn f (Set.Icc (I 0) (I n))
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_eq_right_iff : ∀ {R : Type u} [inst : LinearOrder R] {x y : Tropical R}, x + y = y ↔ y ≤ x
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.IsCompleteBetween.induce : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : Set V},
  G.IsCompleteBetween s t →
    ∀ (u : Set V), (SimpleGraph.induce u G).IsCompleteBetween (Subtype.val ⁻¹' s) (Subtype.val ⁻¹' t)
-- Init.Data.UInt.Lemmas
USize.ofNat_mod : ∀ {a b : ℕ},
  a < 2 ^ System.Platform.numBits →
    b < 2 ^ System.Platform.numBits → USize.ofNat (a % b) = USize.ofNat a % USize.ofNat b
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_comp_ofLEMk_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X Y : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h₁ : X ≤ Y) (h₂ : Y ≤ CategoryTheory.Subobject.mk f) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (CategoryTheory.CategoryStruct.comp (Y.ofLEMk f h₂) h) =
    CategoryTheory.CategoryStruct.comp (X.ofLEMk f ⋯) h
-- Mathlib.Data.Nat.Nth
Nat.le_nth_of_lt_nth_succ : ∀ {p : ℕ → Prop} {k a : ℕ}, a < Nat.nth p (k + 1) → p a → a ≤ Nat.nth p k
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel projection is natural.  -/
CategoryTheory.Limits.coker.π : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Arrow.rightFunc ⟶ CategoryTheory.Limits.coker C
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a functor `F` is zero, then any cocone for `F` with a zero point is colimit.  -/
CategoryTheory.Limits.IsColimit.ofIsZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.Limits.HasZeroObject C] →
            {F : CategoryTheory.Functor D C} →
              (c : CategoryTheory.Limits.Cocone F) →
                CategoryTheory.Limits.IsZero F → CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Limits.IsColimit c
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.pow_add_period_smul : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (n : ℕ) (m : M) (a : α),
  m ^ (n + MulAction.period m a) • a = m ^ n • a
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] {E : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} E] [inst_4 : CategoryTheory.HasShift E A] [P.IsStableUnderShift A]
  [P.IsClosedUnderIsomorphisms] (F : CategoryTheory.Functor E C) [F.CommShift A],
  (P.inverseImage F).IsStableUnderShift A
-- Mathlib.Data.Sym.Basic
Sym.ext_iff : ∀ {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n}, s₁ = s₂ ↔ ↑s₁ = ↑s₂
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop_set_of_lt : ∀ {α : Type u} (x : α) (s : Stream'.Seq α) {m n : ℕ}, m < n → (s.set m x).drop n = s.drop n
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algHom_ext'_iff : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f g : Polynomial A →ₐ[R] B},
  f = g ↔ f.comp Polynomial.CAlgHom = g.comp Polynomial.CAlgHom ∧ f Polynomial.X = g Polynomial.X
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.noZeroDivisors : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedRing α] [NoZeroDivisors α],
  NoZeroDivisors { x // 0 ≤ x }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_nil_end : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (q : G.Walk u v), SimpleGraph.Walk.nil.IsSubwalk q
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.union_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_whiskerLeft : ∀ {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} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor E C} (α : F ⟶ G),
  CategoryTheory.NatTrans.op (H.whiskerLeft α) =
    CategoryTheory.CategoryStruct.comp (H.opComp G).hom
      (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.op α)) (H.opComp F).inv)
-- Init.Data.List.Nat.Erase
List.eraseIdx_set : ∀ {α : Type u_1} {xs : List α} {i : ℕ} {a : α} {j : ℕ},
  (xs.set i a).eraseIdx j =
    if j < i then (xs.eraseIdx j).set (i - 1) a else if j = i then xs.eraseIdx i else (xs.eraseIdx j).set i a
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.eventuallyConst_inv_set_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant],
  Filter.EventuallyConst s⁻¹ (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)