mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Date.PlainDate
/-- Subtracts a given number of weeks from a `PlainDate`.
 -/
Std.Time.PlainDate.subWeeks : Std.Time.PlainDate → Std.Time.Week.Offset → Std.Time.PlainDate
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The functor `SmallObject.functor f S : Arrow S ⥤ Arrow S` that is part of
the small object argument for a family of morphisms `f`, on morphisms.  -/
CategoryTheory.SmallObject.functorMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S T X Y : C} →
            {πX : X ⟶ S} →
              {πY : Y ⟶ T} →
                (CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) →
                  [inst_1 :
                      CategoryTheory.Limits.HasColimitsOfShape
                        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                    [inst_2 :
                        CategoryTheory.Limits.HasColimitsOfShape
                          (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] →
                      [inst_3 :
                          CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                            (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                        [inst_4 :
                            CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY)
                              (CategoryTheory.SmallObject.functorObjLeft f πY)] →
                          CategoryTheory.SmallObject.functorObj f πX ⟶ CategoryTheory.SmallObject.functorObj f πY
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.semivariation_apply_le_bound : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X}, μ.semivariation s ≤ ↑μ.bound
-- Mathlib.Data.Finsupp.Basic
Finsupp.support_subtypeDomain : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} [D : DecidablePred p] {f : α →₀ M},
  (Finsupp.subtypeDomain p f).support = Finset.subtype p f.support
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- Since the map `b ↦ cramer A b` is linear in `b`, it must be multiplication by some matrix. This
matrix is `A.adjugate`.  -/
Matrix.cramer_eq_adjugate_mulVec : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α), A.cramer b = A.adjugate.mulVec b
-- Aesop.Script.UScript
Aesop.Script.UScript.validate : Aesop.Script.UScript → Lean.MetaM Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k fallback : α},
  (Std.ExtDHashMap.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (Std.ExtDHashMap.Const.get m x_2 ⋯)).isSome).getD fallback
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformSpace : {α : Type u_1} → [inst : UniformSpace α] → UniformSpace (TopologicalSpace.Compacts α)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.idxOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (v : α), xs.idxOf? v = Option.map (fun x => ↑x) (xs.finIdxOf? v)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.fst_comp_prod : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (f : A →A[R] B)
  (g : A →A[R] C), (ContinuousAlgHom.fst R B C).comp (f.prod g) = f
-- Mathlib.Order.Grade
Flag.coe_covBy_coe : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Flag α} {a b : ↥s}, ↑a ⋖ ↑b ↔ a ⋖ b
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_top : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S], Ideal.spanNorm R ⊤ = ⊤
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_left_le_mk_sub : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → ArchimedeanClass.mk a ≤ ArchimedeanClass.mk (a - b)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.mk.injEq : ∀ (simp : Lean.Meta.Simp.Context) (simpMethods : Lean.Meta.Simp.Methods) (config : Lean.Grind.Config)
  (anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)) (cheapCases reportMVarIssue : Bool)
  (splitSource : Lean.Meta.Grind.SplitSource) (ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource)
  (symPrios : Lean.Meta.Grind.SymbolPriorities) (extensions : Lean.Meta.Grind.ExtensionStateArray)
  (debug ematchDiag : Bool) (simp_1 : Lean.Meta.Simp.Context) (simpMethods_1 : Lean.Meta.Simp.Methods)
  (config_1 : Lean.Grind.Config) (anchorRefs?_1 : Option (Array Lean.Meta.Grind.AnchorRef))
  (cheapCases_1 reportMVarIssue_1 : Bool) (splitSource_1 : Lean.Meta.Grind.SplitSource)
  (ematchDiagSource_1 : Lean.Meta.Grind.EMatchDiagSource) (symPrios_1 : Lean.Meta.Grind.SymbolPriorities)
  (extensions_1 : Lean.Meta.Grind.ExtensionStateArray) (debug_1 ematchDiag_1 : Bool),
  ({ simp := simp, simpMethods := simpMethods, config := config, anchorRefs? := anchorRefs?, cheapCases := cheapCases,
        reportMVarIssue := reportMVarIssue, splitSource := splitSource, ematchDiagSource := ematchDiagSource,
        symPrios := symPrios, extensions := extensions, debug := debug, ematchDiag := ematchDiag } =
      { simp := simp_1, simpMethods := simpMethods_1, config := config_1, anchorRefs? := anchorRefs?_1,
        cheapCases := cheapCases_1, reportMVarIssue := reportMVarIssue_1, splitSource := splitSource_1,
        ematchDiagSource := ematchDiagSource_1, symPrios := symPrios_1, extensions := extensions_1, debug := debug_1,
        ematchDiag := ematchDiag_1 }) =
    (simp = simp_1 ∧
      simpMethods = simpMethods_1 ∧
        config = config_1 ∧
          anchorRefs? = anchorRefs?_1 ∧
            cheapCases = cheapCases_1 ∧
              reportMVarIssue = reportMVarIssue_1 ∧
                splitSource = splitSource_1 ∧
                  ematchDiagSource = ematchDiagSource_1 ∧
                    symPrios = symPrios_1 ∧ extensions = extensions_1 ∧ debug = debug_1 ∧ ematchDiag = ematchDiag_1)
-- Init.Data.BitVec.Bitblast
BitVec.sdiv_neg : ∀ {w : ℕ} {x y : BitVec w}, y ≠ BitVec.intMin w → x.sdiv (-y) = -x.sdiv y
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Let `X` be a metric space. Let `K : ι → Set X` be a locally finite family of closed sets, let
`U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there exists a
positive continuous function `δ : C(X, ℝ≥0)` such that for any `i` and `x ∈ K i`, we have
`Metric.closedBall x (δ x) ⊆ U i`.  -/
Metric.exists_continuous_nnreal_forall_closedBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : MetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x ↑(δ x) ⊆ U i
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Auxiliary definition for `equivMonComonCounitIsoApp`.  -/
CategoryTheory.Bimon.equivMonComonCounitIsoAppX : {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.ofMonComon C).comp (CategoryTheory.Bimon.toMonComon C)).obj M).X ≅ M.X
-- Lean.PrettyPrinter.Delaborator.DeclWithSig
Lean.PrettyPrinter.Delaborator.declSigWithId : Lean.Parser.Parser
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.instInhabitedWithInitial.default : {C : Type u} → CategoryTheory.WithInitial C
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.trans_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_some_getD_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β}, m.contains a = true → m[a]? = some (m.getD a fallback)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.toFun_eq_coe : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  (p : AlgebraNorm R S), p.toFun = ⇑p
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.of_nat : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] [inst_2 : Sub E],
  (∀ (t : ℕ → T),
      Monotone t →
        Filter.EventuallyConst t Filter.atTop →
          ProbabilityTheory.iIndepFun (fun i ω => X (t (i + 1)) ω - X (t i) ω) P) →
    ProbabilityTheory.HasIndepIncrements X P
-- Init.Grind.Interactive
/-- `intro~ x₁ ... xₙ` is shorthand for `intro (internalize := false)`.  -/
Lean.Parser.Tactic.Grind.symIntroLight : Lean.ParserDescr
-- Mathlib.Algebra.Notation.Defs
mul_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a : α) (b : P → α) (c : ¬P → α),
  (a * if h : P then b h else c h) = if h : P then a * b h else a * c h
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_congr : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {k k' : α}, (k == k') = true → m.get! k = m.get! k'
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.run_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type 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] {α : Type u}
  (x : OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp x post epost ⦄ x.run ⦃ Std.Internal.Do.EPost.Cons.pushOption post epost; epost.tail ⦄
-- Mathlib.FieldTheory.SeparableClosure
/-- The separable closure of `F` in `E` is separable over `F`.  -/
separableClosure.isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Algebra.IsSeparable F ↥(separableClosure F E)
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.single : ∀ {I : Type u_4} [inst : Fintype I] [inst_1 : DecidableEq I] (R : I → Type u_5) [inst_2 : (i : I) → Semiring (R i)],
  CompleteOrthogonalIdempotents fun x => Pi.single x 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_eq_get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m},
  Std.ExtDHashMap.Const.get m a h = (Std.ExtDHashMap.Const.get? m a).get ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey?.isNone = t.isEmpty
-- Mathlib.Algebra.Order.GroupWithZero.Basic
MonotoneOn.mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Preorder M₀] [inst_3 : Preorder α]
  {f g : α → M₀} [PosMulMono M₀] [MulPosMono M₀] {s : Set α},
  MonotoneOn f s → MonotoneOn g s → (∀ x ∈ s, 0 ≤ f x) → (∀ x ∈ s, 0 ≤ g x) → MonotoneOn (f * g) s
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressBegin.mk.inj : ∀ {toWorkDoneProgressReport : Lean.Lsp.WorkDoneProgressReport} {title : String}
  {toWorkDoneProgressReport_1 : Lean.Lsp.WorkDoneProgressReport} {title_1 : String},
  { toWorkDoneProgressReport := toWorkDoneProgressReport, title := title } =
      { toWorkDoneProgressReport := toWorkDoneProgressReport_1, title := title_1 } →
    toWorkDoneProgressReport = toWorkDoneProgressReport_1 ∧ title = title_1
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated additive monoids is finitely generated.  -/
Prod.instAddMonoidFG : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] [AddMonoid.FG M] [AddMonoid.FG N],
  AddMonoid.FG (M × N)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_eq_neg_one_iff : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R ≃+* S) {x : R},
  f x = -1 ↔ x = -1
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- To show that `[Quiver V]` is an arborescence with root `r : V`, it suffices to
- provide a height function `V → ℕ` such that every arrow goes from a
  lower vertex to a higher vertex,
- show that every vertex has at most one arrow to it, and
- show that every vertex other than `r` has an arrow to it.  -/
Quiver.arborescenceMk : {V : Type u} →
  [inst : Quiver V] →
    (r : V) →
      (height : V → ℕ) →
        (∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b) →
          (∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f) →
            (∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)) → Quiver.Arborescence V
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.toArray : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Array α
-- Mathlib.RingTheory.Etale.Locus
/-- We say that an `R`-algebra `A` is etale at a prime `q` of `A`
if `A_q` is formally etale over `R`.  -/
Algebra.IsEtaleAt : (R : Type u_1) →
  {A : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (q : Ideal A) → [q.IsPrime] → Prop
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.precompL_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Eₗ] [inst_2 : SeminormedAddCommGroup Fₗ] [inst_3 : SeminormedAddCommGroup Gₗ]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 Eₗ]
  [inst_7 : NormedSpace 𝕜 Fₗ] [inst_8 : NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (u : Eₗ →L[𝕜] E) (f : Fₗ) (g : Eₗ),
  (((ContinuousLinearMap.precompL Eₗ L) u) f) g = (L (u g)) f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.subtype_coe : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p},
  Measurable f → Measurable fun a => ↑(f a)
-- Mathlib.Data.Sym.Sym2
Equiv.sigmaQuotFromRel_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (sym : Std.Symm r) {r' : β → β → Prop} (f : r →r r')
  (z : ↑(Sym2.fromRel sym)),
  (Equiv.sigmaQuotFromRel sym f) z =
    Sym2.fromRelNdrec ↑z ⋯ (fun a₁ a₂ h => ⟨Quot.mk r' (f a₁), ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.directed_filtration : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  {i : WithTop (Module.rank F E).ord.ToType}, Directed (fun x1 x2 => x1 ≤ x2) fun j => Field.Emb.Cardinal.filtration ↑j
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- The natural transformation `F ⟶ F.rightDerived 0`.  -/
CategoryTheory.Functor.toRightDerivedZero : {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 : CategoryTheory.Functor C D) → [inst_5 : F.Additive] → F ⟶ F.rightDerived 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  CategoryTheory.AddMonObj.zero = CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor
-- Mathlib.Algebra.Order.Round
round_natCast : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (n : ℕ),
  round ↑n = ↑n
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Connected.sum_sup_edge : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {v : V} {w : W},
  G.Connected → H.Connected → ((G ⊕g H) ⊔ SimpleGraph.edge (Sum.inl v) (Sum.inr w)).Connected
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (x : R), (Polynomial.C x).roots = 0
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.toAffineMap_injective : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f g : P →ᴬ[R] Q}, ↑f = ↑g → f = g
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.isoMk_hom_hom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A}
  (iso : (a : A) → F.functor a ≅ G.functor a)
  (comm :
    ∀ (n a a' : A) (ha' : n + a = a'),
      CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n))
          (G.shiftIso n a a' ha').hom)
  (a : A), (CategoryTheory.SingleFunctors.isoMk iso comm).hom.hom a = (iso a).hom
-- Mathlib.RingTheory.Congruence.Hom
RingCon.coe_quotientKerEquivRangeₐ_mkₐ : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (f : M →ₐ[R] P) (x : M), ↑((RingCon.quotientKerEquivRangeₐ f) ↑x) = f x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.OplaxTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
      (self.naturality (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom
              (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))))))
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Cardinal.eventuallyConst_of_monotone : ∀ {β : Type v} [inst : PartialOrder β] {f : Cardinal.{v} → β} [Small.{v, v} β],
  Monotone f → Filter.EventuallyConst f Filter.atTop
-- Init.Data.BitVec.Lemmas
BitVec.ofBool_or_ofBool : ∀ {b b' : Bool}, BitVec.ofBool b ||| BitVec.ofBool b' = BitVec.ofBool (b || b')
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_filterMap : ∀ {α β γ δ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : β → Option γ} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filterMap f it) =
    Std.IterM.fold
      (fun d b =>
        match f b with
        | some c => g d c
        | x => d)
      init it
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compAlongComposition_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G] {n : ℕ}
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (v : Fin n → E),
  (q.compAlongComposition p c) v = (q c.length) (p.applyComposition c v)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.measurable_coe : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  {s : Set β}, MeasurableSet s → Measurable fun a => (κ a) s
-- Mathlib.Algebra.Order.IsBotOne
IsBotZeroClass.mk : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Zero α], IsBot 0 → IsBotZeroClass α
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The open cells are pairwise disjoint. Use `RelCWComplex.pairwiseDisjoint` or
`RelCWComplex.disjoint_openCell_of_ne` instead.  -/
Topology.RelCWComplex.pairwiseDisjoint' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D],
  Set.univ.PairwiseDisjoint fun ni => ↑(Topology.RelCWComplex.map ni.fst ni.snd) '' Metric.ball 0 1
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.ofLowerSet_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : Topology.WithLowerSet α},
  Topology.WithLowerSet.ofLowerSet a ≤ Topology.WithLowerSet.ofLowerSet b ↔ a ≤ b
-- Lean.Compiler.NoncomputableAttr
/-- Mark in the environment extension that the given declaration has been declared by the user as `noncomputable`.  -/
Lean.addNoncomputable : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineMap.lineMap_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {Q : AffineSubspace k P} {p₀ p₁ : P} (c : k),
  p₀ ∈ Q → p₁ ∈ Q → (AffineMap.lineMap p₀ p₁) c ∈ Q
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.rightComp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type w)
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] (X : C) {Y Z : C} (g : Y ⟶ Z) (f : X ⟶ Y),
  (CategoryTheory.Linear.rightComp R X g) f = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Topology.NhdsWithin
nhdsWithin_neBot_of_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α}, x ∈ s → (nhdsWithin x s).NeBot