mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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] {h e f : L}
  {m : M} {μ : R} {t : IsSl2Triple h e f},
  t.HasPrimitiveVectorWith m μ →
    ∀ [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] {n : ℕ},
      μ = ↑n → ∀ {i : ℕ}, i ≤ n → ((LieModule.toEnd R L M) f ^ i) m ≠ 0
-- Mathlib.Combinatorics.Digraph.Basic
/-- The relation that one `Digraph` is a spanning subgraph of another.
Note that `Digraph.IsSubgraph G H` should be spelled `G ≤ H`.
 -/
Digraph.IsSubgraph : {V : Type u_2} → Digraph V → Digraph V → Prop
-- Mathlib.Topology.VectorBundle.Constructions
instSMulPullbackOfModule : (R : Type u_1) →
  {B : Type u_3} →
    (E : B → Type u_5) →
      {B' : Type u_6} →
        (f : B' → B) →
          [inst : Semiring R] →
            [inst_1 : (x : B) → AddCommMonoid (E x)] → [i : (x : B) → Module R (E x)] → (x : B') → SMul R ((f *ᵖ E) x)
-- Mathlib.Order.Hom.WithTopBot
WithTop.toDualBotEquiv_coe : ∀ {α : Type u_1} [inst : LE α] (a : α), WithTop.toDualBotEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.derivative_apply : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (f : LaurentSeries V), (LaurentSeries.derivative R) f = (LaurentSeries.hasseDeriv R 1) f
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
to zero as `μ s` tends to zero.  -/
MeasureTheory.tendsto_setLIntegral_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_4} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ →
    ∀ {l : Filter ι} {s : ι → Set α},
      Filter.Tendsto (⇑μ ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫⁻ (x : α) in s i, f x ∂μ) l (nhds 0)
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.omap : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.PHashMap Lean.Meta.Grind.Origin (List α)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_node3R : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  Ordnode.All P (l.node3R x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_filter_key : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {f : α → Bool} {k : α},
  m.WF → (Std.HashMap.Raw.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Init.Data.List.Find
List.findIdx?_go_eq_map_findFinIdx?_go_val : ∀ {α : Type u_1} {l xs : List α} {p : α → Bool} {i : ℕ} {h : xs.length + i = l.length},
  List.findIdx?.go p xs i = Option.map (fun x => ↑x) (List.findFinIdx?.go p l xs i h)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.ext : ∀ {F : PFunctor.{uA, uB}} [inst : Inhabited F.M] [inst_1 : DecidableEq F.A] (x y : F.M),
  (∀ (ps : PFunctor.Approx.Path F), PFunctor.M.iselect ps x = PFunctor.M.iselect ps y) → x = y
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
CliffordAlgebra.changeFormEquiv.congr_simp : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B B_1 : LinearMap.BilinForm R M} (e_B : B = B_1)
  (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q),
  CliffordAlgebra.changeFormEquiv h = CliffordAlgebra.changeFormEquiv ⋯
-- Mathlib.Order.Filter.SmallSets
/-- `g` converges to `f.smallSets` if for all `s ∈ f`, eventually we have `g x ⊆ s`.  -/
Filter.tendsto_smallSets_iff : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → Set β},
  Filter.Tendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ (x : α) in la, f x ⊆ t
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm.congr_simp : ∀ (R : Type u_1) (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],
  LieModule.traceForm R L M = LieModule.traceForm R L M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- the dimension of the 1-codimensional face  -/
SSet.prodStdSimplex.pairingCore.Type₁.d : {m : ℕ} → {k : Fin (m + 1)} → {n : ℕ} → SSet.prodStdSimplex.pairingCore.Type₁ k n → ℕ
-- Init.Prelude
/-- Locally modifies the reader monad's value while running an action.

During the inner action `x`, reading the value returns `f` applied to the original value. After
control returns from `x`, the reader monad's value is restored.
 -/
MonadWithReader.withReader : {ρ : outParam (Type u)} → {m : Type u → Type v} → [self : MonadWithReader ρ m] → {α : Type u} → (ρ → ρ) → m α → m α
-- Mathlib.Data.Int.Init
Int.pred_succ : ∀ (a : ℤ), a.succ.pred = a
-- Mathlib.Tactic.Linter.FindDeprecations
/-- These are the names of the directories containing all the files that should be inspected.
For reporting, the script assumes there is no sub-dir of the `repo` dir that contains
`repo` as a substring.
However, the script should still remove old deprecations correctly even if that happens.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.repos : Lean.NameSet
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → t ⊆ s → AnalyticWithinAt 𝕜 f t x
-- Std.Async.Timer
/-- If:
- `Interval.tick` was called on `i` before the timer restarts counting from now and the next tick
   happens in `duration`.
- `i` is not yet or not anymore running this is a no-op.
 -/
Std.Async.Interval.reset : Std.Async.Interval → IO Unit
-- Mathlib.Algebra.Field.Opposite
AddOpposite.op_ratCast : ∀ {α : Type u_1} [inst : RatCast α] (q : ℚ), AddOpposite.op ↑q = ↑q
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
/-- The isomorphism of categories of bifunctors given by currying.  -/
CategoryTheory.curryingIso : {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] →
            CategoryTheory.Cat.of (CategoryTheory.Functor C (CategoryTheory.Functor D E)) ≅
              CategoryTheory.Cat.of (CategoryTheory.Functor (C × D) E)
-- Mathlib.Algebra.Order.Field.Basic
exists_pos_lt_mul : ∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  0 < a → ∀ (b : α), ∃ c, 0 < c ∧ b < c * a
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.instIsIsoFunctorObjOfBasedFunctor : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : F ⟶ G) [CategoryTheory.IsIso α],
  CategoryTheory.IsIso α.toNatTrans
-- Mathlib.RingTheory.Algebraic.LinearIndependent
/-- If `E / F` is a field extension, `x` is an element of `E` transcendental over `F`,
then `{(x - a)⁻¹ | a : F}` is linearly independent over `F`.  -/
Transcendental.linearIndependent_sub_inv : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  Transcendental F x → LinearIndependent F fun a => (x - (algebraMap F E) a)⁻¹
-- Init.Data.ByteArray.Lemmas
_private.Init.Data.ByteArray.Lemmas.0.ByteArray.size.match_1.eq_1 : ∀ (motive : ByteArray → Sort u_1) (bs : Array UInt8) (h_1 : (bs : Array UInt8) → motive { data := bs }),
  (match { data := bs } with
    | { data := bs } => h_1 bs) =
    h_1 bs
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_eq_iff_of_lt_aleph0 : ∀ {a : Cardinal.{u}} (n : ℕ), a < Cardinal.aleph0 → (Cardinal.toNat a = n ↔ a = ↑n)
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.norm_inv_mul_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {s : Set E} {a b : E} {r : ℝ}
  {f : E → F} {C : NNReal}, LipschitzOnWith C f s → a ∈ s → b ∈ s → ‖a⁻¹ * b‖ ≤ r → ‖(f a)⁻¹ * f b‖ ≤ ↑C * r
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanStaleDependencyParams.mk : Lean.Lsp.DocumentUri → Lean.Lsp.LeanStaleDependencyParams
-- Mathlib.Algebra.Free
FreeAddMagma.hom_ext : ∀ {α : Type u} {β : Type v} [inst : Add β] {f g : FreeAddMagma α →ₙ+ β},
  ⇑f ∘ FreeAddMagma.of = ⇑g ∘ FreeAddMagma.of → f = g
-- Mathlib.Analysis.Normed.Module.Dual
/-- Given a neighborhood `s` of the origin in a normed space `E`, the dual norms of all elements of
the polar `polar 𝕜 s` are bounded by a constant.  -/
NormedSpace.isBounded_polar_of_mem_nhds_zero : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → Bornology.IsBounded (StrongDual.polar 𝕜 s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {X_1 Y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (f : X_1 ⟶ Y), (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor F G X).map f = f.snd
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.zero : Real.smoothTransition 0 = 0
-- Mathlib.Data.Set.Restrict
Set.domRestrict₂_comp_domRestrict : ∀ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t), Set.domRestrict₂ hst ∘ t.domRestrict = s.domRestrict
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- The functor assigning, to a finite set in `V`, the set of connected components in its complement.
 -/
SimpleGraph.componentComplFunctor : {V : Type u} → SimpleGraph V → CategoryTheory.Functor (Finset V)ᵒᵖ (Type u)
-- Mathlib.Algebra.Homology.Opposite
/-- The opposite of a homotopy between morphisms of homological complexes.  -/
Homotopy.op : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {ι : Type u_2} →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Preadditive V] →
          {F G : HomologicalComplex V c} →
            {φ₁ φ₂ : F ⟶ G} →
              Homotopy φ₁ φ₂ →
                Homotopy ((HomologicalComplex.opFunctor V c).map φ₁.op) ((HomologicalComplex.opFunctor V c).map φ₂.op)
-- Init.Data.Int.DivMod.Basic
Int.ofNat_tdiv : ∀ (m n : ℕ), ↑(m / n) = (↑m).tdiv ↑n
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.le.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (h_1 : (val : β) → motive none (some val))
  (h_2 : Unit → motive none none) (h_3 : (val : α) → motive (some val) none)
  (h_4 : (x : α) → (y : β) → motive (some x) (some y)),
  (match none, none with
    | none, some val => h_1 val
    | none, none => h_2 ()
    | some val, none => h_3 val
    | some x, some y => h_4 x y) =
    h_2 ()
-- Mathlib.Data.Nat.Factorization.Defs
Nat.prod_pow_dvd_of_le_factorization : ∀ {n : ℕ} {f : ℕ →₀ ℕ}, f ≤ n.factorization → (f.prod fun x1 x2 => x1 ^ x2) ∣ n
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
times how many they are.  -/
Finset.sum_card_le : ∀ {α : Type u_2} [inst : DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [inst_1 : Fintype α],
  (∀ (a : α), {b ∈ B | a ∈ b}.card ≤ n) → ∑ s ∈ B, s.card ≤ Fintype.card α * n
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.simpMatchCore : Lean.Name → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limCompFlipIsoWhiskerLim_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X_1 : K),
  (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X_1)).inv
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X_1).inv
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.toJointlyMono₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂), CategoryTheory.JointlyMono₂ p₁ p₂
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_updateBucket_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β},
      (Std.DHashMap.Internal.toListModel
            (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a
              (Std.DHashMap.Internal.AssocList.Const.alter a f))).Perm
        (Std.Internal.List.Const.alterKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Probability.IdentDistrib
/-- If `f` and `g` are identically distributed and `f` is a.e. strongly measurable, so is `g`.  -/
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable g ν
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termι'_3 : Lean.ParserDescr
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) (f : ℝ → ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f = (s, f)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_sum : ∀ {α : Type u_1} {β : Type u_2} [Finite α] [Finite β], Nat.card (α ⊕ β) = Nat.card α + Nat.card β
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_add_distrib : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f g : ι → M},
  ∑ x ∈ s, (f x + g x) = ∑ x ∈ s, f x + ∑ x ∈ s, g x
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.allRoots_subset_range_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [inst_6 : DecidableEq M], ↑(RootPairing.EmbeddedG2.allRoots P).toFinset ⊆ Set.range ⇑P.root
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.isPlausibleStep_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.Iter α}
  {step : Std.IterStep (Std.Iter α) α}, it.IsPlausibleStep step ↔ step = Std.Rxo.Iterator.step it
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given representations `A, B` and a type `α`, this is the natural representation isomorphism
`A ⊗ (α →₀ B) ≅ (A ⊗ B) →₀ α` sending `a ⊗ₜ single x b ↦ single x (a ⊗ₜ b)`.  -/
Rep.finsuppTensorRight : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (A B : Rep.{u, u, v} k G) →
          (α : Type u) →
            [DecidableEq α] →
              CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.finsupp α B) ≅
                Rep.finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)...Std.PRange.succ hi).toList = List.map Std.PRange.succ (lo...hi).toList
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.symmetry : ∀ {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.SymmetricCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.SymmetricCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.braiding G F).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
-- Lean.Widget.InteractiveCode
/-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`.  -/
Lean.Widget.SubexprInfo.subexprPos : Lean.Widget.SubexprInfo → Lean.SubExpr.Pos
-- Init.Data.Vector.Perm
Vector.Perm.push : ∀ {α : Type u_1} {n : ℕ} (x : α) {xs ys : Vector α n}, xs.Perm ys → (xs.push x).Perm (ys.push x)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedLitValue : Inhabited Lean.Compiler.LCNF.LitValue
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.continuousSMul : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] (self : TopModuleCat R), ContinuousSMul R ↑self.toModuleCat
-- Lean.Data.DeclarationRange
Lean.instInhabitedDeclarationRanges.default : Lean.DeclarationRanges
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
isLeast_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α],
  s.Nonempty → IsLeast s (sInf s)
-- Mathlib.Topology.VectorBundle.Hom
hom_trivializationAt_baseSet : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] (x₀ : B),
  (trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀).baseSet =
    (trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet
-- Init.Data.Range.Polymorphic.RangeIterator
/-- The pure function mapping a range iterator of type `Iter` to the next step of the iterator.
 -/
Std.Rxo.Iterator.step : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] → [inst : LT α] → [DecidableLT α] → Std.Iter α → Std.IterStep (Std.Iter α) α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.hom.app CategoryTheory.Limits.WalkingParallelPair.one =
  CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingParallelPair.one
-- Mathlib.MeasureTheory.Measure.Hausdorff
IsometryEquiv.hausdorffMeasure_preimage : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) (s : Set Y),
  (MeasureTheory.Measure.hausdorffMeasure d) (⇑e ⁻¹' s) = (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.Data.Erased
/-- `(>>=)` operation on `Erased`.

This is a separate definition because `α` and `β` can live in different
universes (the universe is fixed in `Monad`).
 -/
Erased.bind : {α : Sort u_1} → {β : Sort u_2} → Erased α → (α → Erased β) → Erased β
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
PrimeSpectrum.instNoetherianSpace : ∀ (R : Type u) [inst : CommSemiring R] [IsNoetherianRing R], TopologicalSpace.NoetherianSpace (PrimeSpectrum R)
-- Mathlib.Data.Seq.Defs
/-- Flatten a sequence of sequences. (It is required that the
sequences be nonempty to ensure productivity; in the case
of an infinite sequence of `nil`, the first element is never
generated.)  -/
Stream'.Seq.join : {α : Type u} → Stream'.Seq (Stream'.Seq1 α) → Stream'.Seq α
-- Mathlib.Topology.Maps.Basic
isClosedMap_iff_comap_nhdsSet_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f ↔ ∀ {s : Set Y}, Filter.comap f (nhdsSet s) ≤ nhdsSet (f ⁻¹' s)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The isomorphism between the terminal object in `SimplexCategory` and `⦋0⦌`.  -/
SimplexCategory.topIsoZero : ⊤_ SimplexCategory ≅ { len := 0 }
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.symm_comp_self : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.symm.comp f = FirstOrder.Language.Equiv.refl L M
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.exists_mem_range : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), ∃ n < p, x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p]
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
NormedAddCommGroup.dist_eq : ∀ {E : Type u_8} [self : NormedAddCommGroup E] (x y : E), dist x y = ‖-x + y‖
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.kernelSubobjectIso f = CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.kernel.ι f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.size = 0
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
/-- A bump function normed so that `∫ x, f.normed μ x ∂μ = 1`.  -/
ContDiffBump.normed : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [HasContDiffBump E] → [inst : MeasurableSpace E] → {c : E} → ContDiffBump c → MeasureTheory.Measure E → E → ℝ
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_ball_symmetry : ∀ {β : Type ub} {V : SetRel β β} [V.IsSymm] {x y : β}, x ∈ UniformSpace.ball y V ↔ y ∈ UniformSpace.ball x V
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.cocones_map_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {X Y : (CategoryTheory.Functor J C)ᵒᵖ} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.cocones J C).map f).app X_1 = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g