mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.constCocone_ι : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C),
  (CategoryTheory.Limits.constCocone J X).ι = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const J).obj X)
-- Mathlib.Data.Vector.MapLemmas
/-- If an accumulation function `f`, given an initial state `s`, produces `s` as its output state
for all possible input bits, then the state is redundant and can be optimized out.
 -/
List.Vector.mapAccumr₂_eq_map₂_of_constant_state : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {xs : List.Vector α n} {ys : List.Vector β n}
  (f : α → β → σ → σ × γ) (s : σ),
  (∀ (a : α) (b : β), (f a b s).1 = s) →
    List.Vector.mapAccumr₂ f xs ys s = (s, List.Vector.map₂ (fun x y => (f x y s).2) xs ys)
-- Mathlib.Topology.Algebra.Group.Defs
Continuous.neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G}, Continuous f → Continuous (-f)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFunDual_map_add_const : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [BorelSpace E] (r : E) (L : StrongDual ℝ E),
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun x => x + r) μ) L =
    MeasureTheory.charFunDual μ L * Complex.exp (↑(L r) * Complex.I)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The canonical submersive `R`-presentation of `R` with no generators and no relations.  -/
Algebra.SubmersivePresentation.id : (R : Type u) → [inst : CommRing R] → Algebra.SubmersivePresentation R R PEmpty.{w + 1} PEmpty.{t + 1}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} (m m_1 : Std.DHashMap α fun x => β) (e_m : m = m_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), Std.DHashMap.Const.get m a h = Std.DHashMap.Const.get m_1 a_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Prelax functors preserve identity 2-morphisms.  -/
CategoryTheory.PrelaxFunctor.map₂_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.PrelaxFunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.toLinearMap_comulAlgHom : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  (Bialgebra.comulAlgHom R A).toLinearMap = CoalgebraStruct.comul
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.splitter : {σ : String.Slice → Type} →
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
    {s : String.Slice} →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (motive : searcher.Step → Sort u_1) →
          (x : searcher.Step) →
            ((searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                (startPos endPos : s.Pos) →
                  (hps :
                      searcher.IsPlausibleStep
                        (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos))) →
                    x = ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ →
                      motive
                        ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩) →
              ((searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                  (startPos endPos : s.Pos) →
                    (hps :
                        searcher.IsPlausibleStep
                          (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos))) →
                      x =
                          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos),
                            hps⟩ →
                        motive
                          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos),
                            hps⟩) →
                ((searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    (hps : searcher.IsPlausibleStep (Std.IterStep.skip searcher')) →
                      x = ⟨Std.IterStep.skip searcher', hps⟩ → motive ⟨Std.IterStep.skip searcher', hps⟩) →
                  ((property : searcher.IsPlausibleStep Std.IterStep.done) →
                      x = ⟨Std.IterStep.done, property⟩ → motive ⟨Std.IterStep.done, property⟩) →
                    motive x
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.eraseManyEntries_eq_eraseListₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (l : List ((a : α) × β a)), ↑(m.eraseManyEntries l) = m.eraseListₘ (List.map (fun x => x.fst) l)
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin : ∀ {𝕜 : 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] [CompleteSpace F]
  (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ),
  0 < p.radius → HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → List α → Array α → Sort u_2) (n : ℕ) (a : α) (l : List α) (acc : Array α)
  (h_1 : (l : List α) → (acc : Array α) → motive 0 l acc) (h_2 : (x : ℕ) → (acc : Array α) → motive x [] acc)
  (h_3 : (n : ℕ) → (a : α) → (l : List α) → (acc : Array α) → motive n.succ (a :: l) acc),
  (match n.succ, a :: l, acc with
    | 0, l, acc => h_1 l acc
    | x, [], acc => h_2 x acc
    | n.succ, a :: l, acc => h_3 n a l acc) =
    h_3 n a l acc
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.val_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : TrivialStar R] [inst_2 : AddCommGroup A]
  [inst_3 : StarAddMonoid A] [inst_4 : Monoid R] [inst_5 : DistribMulAction R A] [inst_6 : StarModule R A] (r : R)
  (x : ↥(skewAdjoint A)), ↑(r • x) = r • ↑x
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type with negation that satisfies `(- f) x = - (f x)` is an involutive
negation if `β` is an involutive negation.  -/
FunLike.involutiveNeg : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Neg F] → [inst_2 : InvolutiveNeg β] → [IsNegApply F α β] → InvolutiveNeg F
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.noConfusionType : Sort v✝ → Lean.Lsp.FoldingRangeKind → Lean.Lsp.FoldingRangeKind → Sort v✝
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.mul_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A B : Matrix n' n' R}, Commute A B → ∀ (i : ℤ), (A * B) ^ i = A ^ i * B ^ i
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieRing.mk : {L : Type u_1} →
  [toNonUnitalNonAssocRing : NonUnitalNonAssocRing L] →
    (∀ (x y z : L), associator x y z = associator x z y) → RightPreLieRing L
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateIncImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → ℕ → Bool → Bool → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.toValuation_ofValuation : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : Valuation R (Multiplicative Γ₀ᵒᵈ)), AddValuation.toValuation (AddValuation.ofValuation v) = v
-- Mathlib.Analysis.PSeries
Finset.le_sum_schlomilch' : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ},
  (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      Monotone u → ∀ (n : ℕ), ∑ k ∈ Finset.Ico (u 0) (u n), f k ≤ ∑ k ∈ Finset.range n, (u (k + 1) - u k) • f (u k)
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.equivIntAlgEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] (self : R ≃ₐ[ℤ] S),
  (RingEquiv.equivIntAlgEquiv R S).symm self = self.toRingEquiv
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_sub : ∀ (x y : ℂ), Complex.cosh (x - y) = Complex.cosh x * Complex.cosh y - Complex.sinh x * Complex.sinh y
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- 1. All `C^n` algebraic structures on `G` are `Prop`-valued classes that extend
`IsManifold I n G`. This way we save users from adding both
`[IsManifold I n G]` and `[ContMDiffMul I n G]` to the assumptions. While many API
lemmas hold true without the `IsManifold I n G` assumption, we're not aware of a
mathematically interesting monoid on a topological manifold such that (a) the space is not a
`IsManifold`; (b) the multiplication is `C^n` at `(a, b)` in the charts
`extChartAt I a`, `extChartAt I b`, `extChartAt I (a * b)`.

2. Because of `ModelProd` we can't assume, e.g., that a `LieGroup` is modelled on `𝓘(𝕜, E)`. So,
we formulate the definitions and lemmas for any model.

3. While smoothness of an operation implies its continuity, lemmas like
`continuousMul_of_contMDiffMul` can't be instances because otherwise Lean would have to search
for `ContMDiffMul I n G` with unknown `𝕜`, `E`, `H`, and `I : ModelWithCorners 𝕜 E H`. If users
need `[ContinuousMul G]` in a proof about a `C^n` monoid, then they need to either add
`[ContinuousMul G]` as an assumption (worse) or use `haveI` in the proof (better).
 -/
LibraryNote.Design_choices_about_smooth_algebraic_structures : Batteries.Util.LibraryNote
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.prod_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) (i : A),
  (f.prod g) i = (f i, g i)
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.of_finrank_eq_succ : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ},
  Module.finrank K V = n.succ → FiniteDimensional K V
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isGLB_preimage' : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : β},
  IsGLB (⇑f ⁻¹' s) (f.symm x) ↔ IsGLB s x
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `A` is free as `R`-module.
Then the centralizer of `1 ⊗ B ⊆ A ⊗ B` is `A ⊗ C(B)` where `C(B)` is the center of `B`.
 -/
Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Module.Free R A],
  Subalgebra.centralizer R ↑Algebra.TensorProduct.includeRight.range =
    (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.center R B).val).range
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isRightInversion_of_mem_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B},
  cs.IsReduced ω → ∀ {t : W}, t ∈ cs.rightInvSeq ω → cs.IsRightInversion (cs.wordProd ω) t
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_whiskerRight_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ X₂ : CategoryTheory.Comon C} (f : X₁ ⟶ X₂)
  (X : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.X
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_le_veblenWith_iff_right : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}},
  Order.IsNormal f → (Ordinal.veblenWith f o a ≤ Ordinal.veblenWith f o b ↔ a ≤ b)
-- Mathlib.GroupTheory.Rank
AddGroup.rank_range_le : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddGroup.FG G] {f : G →+ H},
  AddGroup.rank ↥f.range ≤ AddGroup.rank G
-- Mathlib.Order.Hom.Basic
OrderIso.conj_symm_apply : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : β →o β),
  f.conj.symm a = EquivLike.inv (f.arrowCongr f) a
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.map_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  Polynomial.map T.subtype (p.toSubring T hp) = p
-- Mathlib.Data.Matrix.Mul
Matrix.mul_left_injective_iff_vecMul_injective : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [Nonempty l]
  [inst_2 : Fintype m] {A : Matrix m n α},
  (Function.Injective fun B => B * A) ↔ Function.Injective fun v => Matrix.vecMul v A
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : ↥p), (p.projection q hpq) ↑x = ↑x
-- Mathlib.Algebra.Module.LinearMap.DivisionRing
LinearMap.surjective_iff_ne_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : DivisionSemiring R] [inst_2 : Module R M]
  {f : M →ₗ[R] R}, Function.Surjective ⇑f ↔ f ≠ 0
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.empty_set_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (N : Submodule R M), ∅ • N = ⊥
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty : ∀ {α : Type u} (S : Set (Set α)), (∀ (T : Finset (Set α)), ↑T ⊆ S → (⋂₀ ↑T).Nonempty) → ∃ F, S ⊆ (↑F).sets
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubsetResult.strict.injEq : ∀ (s s_1 : Lean.Grind.AC.Seq), (Lean.Grind.AC.SubsetResult.strict s = Lean.Grind.AC.SubsetResult.strict s_1) = (s = s_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instIsMonHomFst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N]
  [inst_4 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsMonHom (CategoryTheory.SemiCartesianMonoidalCategory.fst M N)
-- Mathlib.NumberTheory.Primorial
primorial_ne_zero : ∀ (n : ℕ), primorial n ≠ 0
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.currFile : Mathlib.Tactic.ClickSuggestions.SectionKind
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {a : α}
  [inst_3 : Fintype β], a +ᵥ Finset.univ = Finset.univ
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `Submonoid.FG` in terms of `Set.Finite` instead of `Finset`.  -/
Submonoid.fg_iff : ∀ {M : Type u_1} [inst : Monoid M] (P : Submonoid M), P.FG ↔ ∃ S, Submonoid.closure S = P ∧ S.Finite
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (self : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (self.ge n).IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.ext_iff : ∀ {X Y : Pointed} {x y : X.Hom Y}, x = y ↔ x.toFun = y.toFun
-- Mathlib.LinearAlgebra.Dimension.Constructions
span_lt_of_subset_of_card_lt_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {s : Set M} [inst_4 : Fintype ↑s] {t : Submodule R M},
  s ⊆ ↑t → s.toFinset.card < Module.finrank R ↥t → Submodule.span R s < t
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.ForwardSliceSearcher.skipPrefix?_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → String.Slice.Pattern.ForwardPattern.skipPrefix? pat s = some s.startPos
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.ofCocone_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cocone F)
  (j : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.Cotrident.ofCocone t).ι.app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
-- Init.ShareCommon
ShareCommon.Object.eq : ShareCommon.Object → ShareCommon.Object → Bool
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_zipWith : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → Zero (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : (i : ι) → Zero (β₁ i)]
  [inst_4 : (i : ι) → Zero (β₂ i)] [inst_5 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_6 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] {f : (i : ι) → β₁ i → β₂ i → β i} {hf : ∀ (i : ι), f i 0 0 = 0}
  {g₁ : Π₀ (i : ι), β₁ i} {g₂ : Π₀ (i : ι), β₂ i}, (DFinsupp.zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
-- Mathlib.RepresentationTheory.Invariants
/-- The intertwining map between the `G ⧸ S`-representation on the invariants of `ρ|_S` and `ρ`.  -/
Representation.quotientToInvariants_lift : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {V : Type u_5} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [inst_4 : S.Normal] →
                    Representation.IntertwiningMap (MonoidHom.comp (ρ.quotientToInvariants S) (QuotientGroup.mk' S)) ρ
-- Init.Data.List.Pairwise
List.Pairwise.imp : ∀ {α : Type u_1} {R S : α → α → Prop},
  (∀ {a b : α}, R a b → S a b) → ∀ {l : List α}, List.Pairwise R l → List.Pairwise S l
-- Std.Http.Data.Request
Std.Http.Request.mk : {t : Type} → Std.Http.Request.Head → t → Std.Http.Extensions → Std.Http.Request t
-- Init.Data.Bool
Bool.beq_self_right : ∀ (a b : Bool), ((a == b) == b) = a
-- Mathlib.Data.EReal.Operations
EReal.add_le_of_le_sub : ∀ {a b c : EReal}, a ≤ b - c → a + c ≤ b
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratAdd_result : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRatAdd →
    p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
      f.performRatAdd c p rupHints ratHints = (f', true) → f' = f.insert c
-- Mathlib.Data.Set.Disjoint
Disjoint.subset_right_of_subset_union : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t ∪ u → Disjoint s t → s ⊆ u
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fromProd_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  ((CategoryTheory.Comma.fromProd L R).obj X).left = X.1
-- Std.Internal.Parsec.String
_private.Std.Internal.Parsec.String.0.Std.Internal.Parsec.String.digitsCore : ℕ → Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.Dynamics.Ergodic.Conservative
/-- If `f` is a conservative self-map and `s` is a measurable set of positive measure, then
`ae μ`-frequently we have `x ∈ s` and `s` returns to `s` under infinitely many iterations of `f`.  -/
MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ᵐ (x : α) ∂μ, x ∈ s ∧ ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₄_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
      _auto_369✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
      _auto_371✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
      _auto_373✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝))
      _auto_375✝),
  (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 0 = app₀
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- A single step in encoding an `Expr` into `Key`s.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.encodingStep : Lean.Expr → Bool → Lean.Meta.RefinedDiscrTree.LazyM✝ Lean.Meta.RefinedDiscrTree.Key
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.splitMatch : Lean.MVarId → Lean.Expr → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_le_toMeasure_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) (s : Set α), p.toOuterMeasure s ≤ p.toMeasure s
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalDone : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Normed.Ring.Basic
Nat.norm_cast_le : ∀ {α : Type u_2} [inst : SeminormedRing α] (n : ℕ), ‖↑n‖ ≤ ↑n * ‖1‖
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_top : ∀ {G : Type u_1} [inst : Group G], Nat.card ↥⊤ = Nat.card G
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version relative to a set, with general index set.  -/
tendstoUniformlyOn_tsum : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
  {f : α → β → F},
  Summable u →
    ∀ {s : Set β},
      (∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) →
        TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) Filter.atTop s
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The quotient of `X₁ ⊕ X₂` by the relation `PushoutRel' f g`.  -/
CategoryTheory.Limits.Types.Pushout' : {S X₁ X₂ : Type u} → (S ⟶ X₁) → (S ⟶ X₂) → Type u