mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Find
List.findIdx_subtype : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.findIdx f l = List.findIdx g l.unattach
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.Preadditive.mono_iff_injective' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toNonUnitalRingHom_injective : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  Function.Injective RingEquiv.toNonUnitalRingHom
-- Init.Data.UInt.Lemmas
USize.eq_of_toBitVec_eq : ∀ {a b : USize}, a.toBitVec = b.toBitVec → a = b
-- Std.Time.Format.Basic
Std.Time.instInhabitedGenericFormat.default : {awareness : Std.Time.Awareness} → Std.Time.GenericFormat awareness
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ],
  (∀ {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'],
      ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id S) χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ') →
    p.IsCocartesian f φ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonCompletionClientCapabilities : Lean.ToJson Lean.Lsp.CompletionClientCapabilities
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAt.const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt f f' x → HasDerivAt (fun x => c - f x) (-f') x
-- Mathlib.RingTheory.Noetherian.Defs
/-- A (semi)ring is Noetherian if it is Noetherian as a module over itself,
i.e. all its ideals are finitely generated.  -/
IsNoetherianRing : (R : Type u_1) → [Semiring R] → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'}, MDiffAt f z → ∀ (s : 𝕜), MDiffAt (s • f) z
-- Mathlib.Order.ScottContinuity.Complete
scottContinuous_inf_right : ∀ {β : Type u_2} [inst : CompleteLinearOrder β] (a : β), ScottContinuous fun b => min a b
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {x y : sq₁.Hom sq₂},
  x.τ₁ = y.τ₁ → x.τ₂ = y.τ₂ → x.τ₃ = y.τ₃ → x.τ₄ = y.τ₄ → x = y
-- Std.Http.Data.Method
/-- Create a new activity resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-13.5
 -/
Std.Http.Method.mkactivity : Std.Http.Method
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mem_top : ∀ {M : Type u_1} [inst : Add M] (x : M), x ∈ ⊤
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.zpow_smul_mod_minimalPeriod : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (a : G) (b : α) (n : ℤ),
  a ^ (n % ↑(Function.minimalPeriod (fun x => a • x) b)) • b = a ^ n • b
-- Mathlib.Order.Hom.Bounded
TopHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Top α] [inst_1 : Top β] [inst_2 : Top γ] (f : TopHom β γ)
  (g : TopHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.Const.get : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [inst : Std.TransCmp cmp] → (t : Std.ExtDTreeMap α (fun x => β) cmp) → (a : α) → a ∈ t → β
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_toIsometryEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toIsometryEquiv = ⇑e
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The Sylvester matrix of two polynomials `f` and `g` of degrees `m` and `n` respectively is a
`(m+n) × (m+n)` matrix with the coefficients of `f` and `g` arranged in a specific way. Here, `m`
and `n` are free variables, not necessarily equal to the actual degrees of the polynomials `f` and
`g`.

Note that the natural definition would be a `Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R` but we prefer
having this as a square matrix to take determinants later on.
 -/
Polynomial.sylvester : {R : Type u_1} → [inst : Semiring R] → Polynomial R → Polynomial R → (m n : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffWithinAt_finsetProd'`. -/
contMDiffWithinAt_finset_prod' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x
-- Mathlib.Data.Num.Prime
PosNum.decidablePrime : DecidablePred PosNum.Prime
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.coe_ofTop_symm_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {h : p = ⊤} (x : M), ↑((LinearEquiv.ofTop p h).symm x) = x
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the left adjoint is fully faithful, then the unit is an isomorphism.  -/
CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful],
  CategoryTheory.IsIso h.unit
-- Mathlib.Data.Set.Image
Set.image_sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set (α ⊕ β)) (f : α → γ) (g : β → γ),
  Sum.elim f g '' s = f '' Sum.inl ⁻¹' s ∪ g '' Sum.inr ⁻¹' s
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.logError : Lean.Elab.Term.MVarErrorInfo → Option Lean.MessageData → Lean.Elab.TermElabM Unit
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
_private.Mathlib.LinearAlgebra.ExteriorPower.Basic.0.exteriorPower.presentation.relations.match_1.eq_1 : ∀ (R : Type u_1) (ι : Type u_2) (M : Type u_3) (motive : exteriorPower.presentation.Rels R ι M → Sort u_4) (m : ι → M)
  (i : ι) (x y : M) (h_1 : (m : ι → M) → (i : ι) → (x y : M) → motive (exteriorPower.presentation.Rels.add m i x y))
  (h_2 : (m : ι → M) → (i : ι) → (r : R) → (x : M) → motive (exteriorPower.presentation.Rels.smul m i r x))
  (h_3 :
    (m : ι → M) →
      (i j : ι) → (hm : m i = m j) → (hij : i ≠ j) → motive (exteriorPower.presentation.Rels.alt m i j hm hij)),
  (match exteriorPower.presentation.Rels.add m i x y with
    | exteriorPower.presentation.Rels.add m i x y => h_1 m i x y
    | exteriorPower.presentation.Rels.smul m i r x => h_2 m i r x
    | exteriorPower.presentation.Rels.alt m i j hm hij => h_3 m i j hm hij) =
    h_1 m i x y
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.isChain_toList_nonempty : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), List.IsChain (fun x y => Nonempty (y ⟶ x)) p.toList
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.mk.sizeOf_spec : ∀ (elimApp : Lean.Expr) (elimArgs : Array Lean.Expr) (motive : Lean.MVarId) (alts : Array Lean.Elab.Tactic.ElimApp.Alt)
  (others : Array Lean.MVarId) (complexArgs : Array Lean.Expr),
  sizeOf
      { elimApp := elimApp, elimArgs := elimArgs, motive := motive, alts := alts, others := others,
        complexArgs := complexArgs } =
    1 + sizeOf elimApp + sizeOf elimArgs + sizeOf motive + sizeOf alts + sizeOf others + sizeOf complexArgs
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciInf_sub : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddRightMono G], BddBelow (Set.range f) → ∀ (a : G), (⨅ i, f i) - a = ⨅ i, f i - a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instSymmVeq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], Std.Symm fun x1 x2 => x1 =ᵥ x2
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.rangeRestrict_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (x : L), f.rangeRestrict x = ⟨f x, ⋯⟩
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_mapMulHom : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Mul α] [inst_1 : Mul β] [inst_2 : Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ)
  (x : WithOne α), (WithOne.mapMulHom g) ((WithOne.mapMulHom f) x) = (WithOne.mapMulHom (g.comp f)) x
-- Init.Data.SInt.Lemmas
Int64.toBitVec_add : ∀ {a b : Int64}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.mk.injEq : ∀ {n : ℕ} (boundaries : Finset (Fin n.succ)) (zero_mem : 0 ∈ boundaries) (getLast_mem : Fin.last n ∈ boundaries)
  (boundaries_1 : Finset (Fin n.succ)) (zero_mem_1 : 0 ∈ boundaries_1) (getLast_mem_1 : Fin.last n ∈ boundaries_1),
  ({ boundaries := boundaries, zero_mem := zero_mem, getLast_mem := getLast_mem } =
      { boundaries := boundaries_1, zero_mem := zero_mem_1, getLast_mem := getLast_mem_1 }) =
    (boundaries = boundaries_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (cmp (t.insert k v).minKey! k).isLE = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filterMap_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        true ↔
      ∃ (h : Std.Internal.List.containsKey k l = true), (f k (Std.Internal.List.getValueCast k l h)).isSome = true)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_add_eq_map_conv_map' : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : AddMonoid M]
  [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] {f g : Ω → M},
  Measurable f →
    Measurable g →
      MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) →
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g μ) →
          ProbabilityTheory.IndepFun f g μ →
            MeasureTheory.Measure.map (f + g) μ = (MeasureTheory.Measure.map f μ).conv (MeasureTheory.Measure.map g μ)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The equivalence class of a constant function: `[fun _ : α => b]`, based on the equivalence
relation of being almost everywhere equal  -/
MeasureTheory.AEEqFun.const : (α : Type u_1) →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → β → α →ₘ[μ] β
-- Init.Data.Nat.Basic
Nat.add_one_sub_one : ∀ (n : ℕ), n + 1 - 1 = n
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.acc_single : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) →
    (∀ (i : ι), WellFounded (s i)) →
      ∀ [inst_1 : DecidableEq ι] {i : ι},
        Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) i → ∀ (a : α i), Acc (DFinsupp.Lex r s) fun₀ | i => a
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.instDecidableIsCliqueCoeFinsetOfDecidableEqOfDecidableRelAdj : {α : Type u_1} →
  (G : SimpleGraph α) → [DecidableEq α] → [DecidableRel G.Adj] → {s : Finset α} → Decidable (G.IsClique ↑s)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeOpEquiv_inverse : ∀ (J : Type w), (CategoryTheory.Limits.widePushoutShapeOpEquiv J).inverse = CategoryTheory.Limits.widePullbackShapeOp J
-- Mathlib.Tactic.Algebraize
/-- A list of terms passed to `algebraize` as argument.  -/
Mathlib.Tactic.algebraizeTermSeq : Lean.ParserDescr
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Prop structure holding the assumptions of the Picard-Lindelöf theorem.
`IsPicardLindelof f t₀ x₀ a r L K`, where `t₀ ∈ Icc tmin tmax`, means that the time-dependent vector
field `f` satisfies the conditions to admit an integral curve `α : ℝ → E` to `f` defined on
`Icc tmin tmax` with the initial condition `α t₀ = x`, where `‖x - x₀‖ ≤ r`. Note that the initial
point `x` is allowed to differ from the point `x₀` about which the conditions on `f` are stated.  -/
IsPicardLindelof : {E : Type u_1} →
  [NormedAddCommGroup E] →
    (ℝ → E → E) → {tmin tmax : ℝ} → ↑(Set.Icc tmin tmax) → E → NNReal → NNReal → NNReal → NNReal → Prop
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A), NonUnitalStarSubalgebra.map (NonUnitalStarAlgHom.id R A) S = S
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.startsWith_prop_eq_head? : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice},
  s.startsWith P = Option.any (fun x => decide (P x)) s.copy.toList.head?
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.remainingBytes.match_1.splitter : (motive : String.Legacy.Iterator → Sort u_1) →
  (x : String.Legacy.Iterator) → ((s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }) → motive x
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.exists_pos : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith c l f g' → ∃ c' > 0, Asymptotics.IsBigOWith c' l f g'
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isUnit_iff_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {s : Finset α}, IsUnit s ↔ ∃ a, s = {a}
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsZeroApplyForall : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂],
  IsZeroApply (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, (Std.DHashMap.filter f m).contains k = Option.any (f k) (m.get? k)
-- Lean.Declaration
/-- Information associated with constant declarations.  -/
Lean.ConstantInfo : Type
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingCompOf_le_lowerCentralSeries : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [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] (x : L) (k : ℕ),
  LieModule.posFittingCompOf R M x ≤ LieModule.lowerCentralSeries R L M k
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_inv_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.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F] (x y : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit G F).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).inv.app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.CategoryStruct.comp (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (y, x))
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map (β_ (y, x).2 (y, x).1).inv))
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instInhabited : (α : Type u_2) → [inst : SupSet α] → Inhabited (sSupHom α α)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.toSubsemigroup_inj : ∀ {M : Type u_1} [inst : MulOneClass M] {s t : Submonoid M}, s.toSubsemigroup = t.toSubsemigroup ↔ s = t
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of `ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem₀`. -/
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∏ j ∈ s, f j) (f i) κ μ
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_right_le_length_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert → toInsert.length ≤ (Std.Internal.List.insertList l toInsert).length
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_mul_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), a⁺ᵐ * a⁻ᵐ = |a|ₘ
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replaceTR.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (b c : α), l.replaceTR b c = List.replaceTR.go✝ l b c l #[]
-- Mathlib.MeasureTheory.Function.EssSup
essInf_congr_ae : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f g : α → β}, f =ᵐ[μ] g → essInf f μ = essInf g μ
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearEquiv.ofIsHomeomorph.congr_simp : ∀ {S : Type u_1} [inst : Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [inst_1 : Semiring S₁]
  {σ : S →+* S₁} {σ' : S₁ →+* S} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] [inst_6 : Module S M] [inst_7 : TopologicalSpace M₁]
  [inst_8 : AddCommMonoid M₁] [inst_9 : Module S₁ M₁] (f f_1 : M ≃ₛₗ[σ] M₁) (e_f : f = f_1) (hf : IsHomeomorph ⇑f),
  ContinuousLinearEquiv.ofIsHomeomorph f hf = ContinuousLinearEquiv.ofIsHomeomorph f_1 ⋯
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_div_left_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : Group G] [MeasurableMul G] [MeasurableInv G] (f : G → E) (μ : MeasureTheory.Measure G) [μ.IsInvInvariant]
  [μ.IsMulLeftInvariant] (x' : G), ∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ
-- Mathlib.Order.Antichain
IsAntichain.preimage_compl : ∀ {α : Type u_1} {s : Set α} [inst : BooleanAlgebra α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → IsAntichain (fun x1 x2 => x1 ≤ x2) (compl ⁻¹' s)
-- Batteries.Data.List.Basic
/-- `l.swap i j` exchanges the elements at positions `i` and `j` of `l`.
If either index is out of bounds, `l` is returned unchanged.  -/
List.swap : {α : Type u_1} → List α → ℕ → ℕ → List α
-- Mathlib.Order.Filter.Map
Filter.neBot_inf_comap_iff_map' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β},
  (Filter.comap f G ⊓ F).NeBot ↔ (G ⊓ Filter.map f F).NeBot
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.add_int_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α] [inst_1 : NonAssocRing β],
  Function.Antiperiodic f c → ∀ (n : ℤ), f (x + ↑n * c) = ↑↑n.negOnePow * f x
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.mk'_mem_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} {y : ↥M} {I : Ideal S},
  IsLocalization.mk' S x y ∈ I ↔ (algebraMap R S) x ∈ I
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).getKey k ⋯ = t₂.getKey k mem
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulDistribMulActionMonoidHom : {A : Type u_5} →
  {M : Type u_6} →
    {B : Type u_7} →
      [inst : Monoid M] →
        [inst_1 : Monoid A] → [MulDistribMulAction M A] → [inst_3 : CommMonoid B] → MulDistribMulAction Mᵈᵐᵃ (A →* B)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_iterate : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  (g : α →ₘ[μ] γ) {f : α → α} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ) (n : ℕ),
  (fun x => x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯
-- Mathlib.Analysis.RCLike.Basic
RCLike.map_to_real : ∀ {K : Type u_1} [inst : RCLike K], RCLike.map K ℝ = RCLike.reCLM
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.zero : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop}, Nat.RecursiveIn.below ⋯
-- Mathlib.Topology.Order.Monotone
/-- If a monotone function sending `top` to `top` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed infimum of the composition.  -/
Monotone.map_iInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β}
  {g : ι → α}, ContinuousAt f (iInf g) → Monotone f → f ⊤ = ⊤ → f (iInf g) = iInf (f ∘ g)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_obj_ρ : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A : Rep.{w, u, v} k G) (B : Rep.{u_1, u, v} k G),
  (A.ihom.obj B).ρ = A.ρ.linHom B.ρ