mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_multiset_prod : ∀ {s : Multiset ℝ}, (∀ x ∈ s, x ≠ 0) → Real.log s.prod = (Multiset.map (fun x => Real.log x) s).sum
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject C}
  (s : X.Splitting) (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ)
  {Z : C} (h : Y.obj Δ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (f.app Δ) h) =
    CategoryTheory.CategoryStruct.comp (s.φ f (Opposite.unop A.fst).len)
      (CategoryTheory.CategoryStruct.comp (Y.map A.e.op) h)
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.add_zsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddGroup α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → ∀ (n : ℤ), f (x + n • c) = ↑n.negOnePow • f x
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
/-- **Alias** of `Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_mem`.

---

Suppose we are given `∑ i, lᵢ * sᵢ = 1` ∈ `S`, and `S'` a subalgebra of `S` that contains
`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`.  -/
Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (S' : Subalgebra R S) {ι : Type u_3} (ι' : Finset ι) (s l : ι → S),
  ∑ i ∈ ι', l i * s i = 1 →
    (∀ (i : ι), s i ∈ S') → (∀ (i : ι), l i ∈ S') → ∀ (x : S), (∀ (i : ι), ∃ n, s i ^ n • x ∈ S') → x ∈ S'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.PrepareRenameParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.WF.mk : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.inner.WF → t.WF
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The chain complex `barComplex k G` as a projective resolution of `k` as a trivial
`k`-linear `G`-representation.  -/
Rep.barResolution : (k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.ProjectiveResolution (Rep.trivial k G k)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_le_trailingDegree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  q.coeff p.natTrailingDegree ≠ 0 → q.trailingDegree ≤ p.trailingDegree
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The condition that a property of morphisms is stable by finite coproducts.  -/
CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Given a short complex `S` of modules, this is the isomorphism between
the abstract `S.cycles` of the homology API and the more concrete description as
`LinearMap.ker S.g`.  -/
CategoryTheory.ShortComplex.moduleCatCyclesIso : {R : Type u} →
  [inst : Ring R] → (S : CategoryTheory.ShortComplex (ModuleCat R)) → S.cycles ≅ S.moduleCatLeftHomologyData.K
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.isEquivalence_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.Functor.id C).IsEquivalence
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_inv_apply_1_2 : ∀ {X Y Z : Type u}
  {x :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).1.2 = x.2.1
-- Mathlib.Algebra.Category.Grp.Shrink
GrpCat.shrinkFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] {X Y : C} (f : X ⟶ Y),
  (GrpCat.shrinkFunctor.{w, w', v, u} F).map f =
    GrpCat.ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (GrpCat.Hom.hom (F.map f))).comp Shrink.mulEquiv.toMonoidHom)
-- Mathlib.Algebra.Ring.Defs
distrib_three_right : ∀ {R : Type v} [inst : Mul R] [inst_1 : Add R] [RightDistribClass R] (a b c d : R),
  (a + b + c) * d = a * d + b * d + c * d
-- Init.Data.BitVec.Basic
BitVec.instHAppendHAddNat : {w v : ℕ} → HAppend (BitVec w) (BitVec v) (BitVec (w + v))
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ F).app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A subgraph is maximal acyclic iff its reachability relation agrees with the larger graph.  -/
SimpleGraph.maximal_isAcyclic_iff_reachable_eq : ∀ {V : Type u_1} {G F : SimpleGraph V},
  F ≤ G → F.IsAcyclic → (Maximal (fun F => F ≤ G ∧ F.IsAcyclic) F ↔ F.Reachable = G.Reachable)
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelHomClass.asymm`. -/
RelHomClass.isAsymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) [Std.Asymm s], Std.Asymm r
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- In the tangent bundle to the model space, the charts are just the canonical identification
between a product type and a sigma type, a.k.a. `TotalSpace.toProd`.  -/
tangentBundle_model_space_chartAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  (p : TangentBundle I H), (chartAt (ModelProd H E) p).toPartialEquiv = (Bundle.TotalSpace.toProd H E).toPartialEquiv
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.hom_eq : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄,
  (∀ (x : α), f (FreeMonoid.of x) = g (FreeMonoid.of x)) → f = g
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (b : β),
  Encodable.encode (Sum.inr b) = 2 * Encodable.encode b + 1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R),
  ((CategoryTheory.StructuredArrow.map₂ α β).obj X).left = X.left
-- Mathlib.Data.Countable.Basic
Sigma.uncountable : ∀ {α : Type u} {π : α → Type w} (a : α) [Uncountable (π a)], Uncountable (Sigma π)
-- Mathlib.Data.Nat.Choose.Lucas
/-- For a natural number `n` greater than `1`, assume that `n` is not a prime power, then
the greatest common divisor of  `choose n 1, ⋯, choose n (n - 1)` is `1`.  -/
Choose.gcd_choose_eq_one_of_not_isPrimePow : ∀ {n : ℕ}, 1 < n → ¬IsPrimePow n → (Finset.Icc 1 (n - 1)).gcd n.choose = 1
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- `Vars k` provides `n` variables $X_{f,1}, \dots, X_{f,n}$ for each monic polynomial
`f : k[X]` of degree `n`.  -/
AlgebraicClosure.Vars : (k : Type u) → [Field k] → Type u
-- Batteries.Data.List.Basic
/-- `O(|l₁| * (|l₁| + |l₂|))`. Computes whether `l₁` is a sublist of a permutation of `l₂`.
See `isSubperm_iff` for a characterization in terms of `List.Subperm`.
 -/
List.isSubperm : {α : Type u_1} → [BEq α] → List α → List α → Bool
-- Mathlib.Topology.UnitInterval
exists_monotone_Icc_subset_open_cover_unitInterval_prod_self : ∀ {ι : Sort u_1} {c : ι → Set (↑unitInterval × ↑unitInterval)},
  (∀ (i : ι), IsOpen (c i)) →
    Set.univ ⊆ ⋃ i, c i →
      ∃ t,
        t 0 = 0 ∧
          Monotone t ∧
            (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ×ˢ Set.Icc (t m) (t (m + 1)) ⊆ c i
-- Mathlib.Analysis.Analytic.Composition
/-- Natural equivalence between `(Σ (a : Composition n), Composition a.length)` and
`(Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun i))`, that shows up as a
change of variables in the proof that composition of formal multilinear series is associative.

Consider a composition `a` of `n` and a composition `b` of `a.length`. Then `b` indicates how to
group together some blocks of `a`, giving altogether `b.length` blocks of blocks. These blocks of
blocks can be called `d₀, ..., d_{a.length - 1}`, and one obtains a composition `c` of `n` by
saying that each `dᵢ` is one single block. The map `⟨a, b⟩ → ⟨c, (d₀, ..., d_{a.length - 1})⟩` is
the direct map in the equiv.

Conversely, if one starts from `c` and the `dᵢ`s, one can join the `dᵢ`s to obtain a composition
`a` of `n`, and register the lengths of the `dᵢ`s in a composition `b` of `a.length`. This is the
inverse map of the equiv.
 -/
Composition.sigmaEquivSigmaPi : (n : ℕ) →
  (a : Composition n) × Composition a.length ≃ (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).counitIso =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso
-- Mathlib.Order.Defs.PartialOrder
lt_asymm : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b < a
-- Mathlib.RingTheory.Int.Basic
Int.natAbs_euclideanDomain_gcd : ∀ (a b : ℤ), (EuclideanDomain.gcd a b).natAbs = a.gcd b
-- Mathlib.Order.BooleanAlgebra.Basic
sup_eq_sdiff_sup_sdiff_sup_inf : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.mk.injEq : ∀ (builderId ref : Lean.Name) (args : List Lean.DataValue) (builderId_1 ref_1 : Lean.Name)
  (args_1 : List Lean.DataValue),
  ({ builderId := builderId, ref := ref, args := args } = { builderId := builderId_1, ref := ref_1, args := args_1 }) =
    (builderId = builderId_1 ∧ ref = ref_1 ∧ args = args_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_notMem_div_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, 1 ∉ s / t ↔ Disjoint s t
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `orthogonal.orthogonal` preserves the `≤` ordering of two
subspaces.  -/
ClosedSubmodule.orthogonal_orthogonal_monotone : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : ClosedSubmodule 𝕜 E}, K₁ ≤ K₂ → K₁ᗮᗮ ≤ K₂ᗮᗮ
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.le_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (S T : CategoryTheory.Subfunctor F), S ≤ T ↔ ∀ (U : C), S.obj U ⊆ T.obj U
-- Init.Data.Sum.Lemmas
Sum.isRight_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  (Sum.map f g x).isRight = x.isRight
-- Init.Data.Nat.Div.Lemmas
Nat.succ_div_of_mod_ne_zero : ∀ {a b : ℕ}, (a + 1) % b ≠ 0 → (a + 1) / b = a / b
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newLocal.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (goal : Lean.Meta.Grind.Goal),
  sizeOf (Lean.Meta.Grind.IntroResult.newLocal✝ fvarId goal) = 1 + sizeOf fvarId + sizeOf goal
-- Init.Data.BitVec.Lemmas
BitVec.instAssociativeHXor : ∀ {w : ℕ}, Std.Associative fun x y => x ^^^ y
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} {x y : R.Hom R'}, x = y ↔ x.f = y.f
-- Mathlib.Analysis.Normed.Group.Basic
norm_eq_zero : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, ‖a‖ = 0 ↔ a = 0
-- Mathlib.Data.Multiset.Filter
Multiset.mapEmbedding_apply : ∀ {α : Type u_1} {β : Type v} (f : α ↪ β) (s : Multiset α), (Multiset.mapEmbedding f) s = Multiset.map (⇑f) s
-- Mathlib.Algebra.Lie.Nilpotent
/-- See also `LieModule.isNilpotent_iff_exists_ucs_eq_top`.  -/
LieModule.isNilpotent_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [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] [LieModule R L M],
  LieModule.IsNilpotent L M ↔ ∃ k, LieModule.lowerCentralSeries R L M k = ⊥
-- Mathlib.Probability.Moments.SubGaussian
/-- Let `Y` be a random process strongly adapted to a filtration `ℱ`, such that for all `i : ℕ`,
`Y i` is conditionally sub-Gaussian with parameter `cY i` with respect to `ℱ (i - 1)`.
In particular, `n ↦ ∑ i ∈ range n, Y i` is a martingale.
Then the sum `∑ i ∈ range n, Y i` is sub-Gaussian with parameter `∑ i ∈ range n, cY i`.  -/
ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ}
  {cY : ℕ → NNReal} {ℱ : MeasureTheory.Filtration ℕ mΩ} [inst_1 : MeasureTheory.IsZeroOrProbabilityMeasure μ],
  MeasureTheory.StronglyAdapted ℱ Y →
    ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) μ →
      ∀ (n : ℕ),
        (∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
          ProbabilityTheory.HasSubgaussianMGF (fun ω => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The right-associated triple tensor product as a functor.  -/
CategoryTheory.MonoidalCategory.rightAssocTensor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (C × C × C) C
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) (x : B'),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).obj x).as = F.obj x
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_of_find_le : ∀ {m n : ℕ} {p : Fin (m + n) → Prop} [inst : DecidablePred p] {hᵢ : ∃ i, p i} (hm : m ≤ ↑(Fin.find p hᵢ)),
  Fin.find p hᵢ = Fin.natAdd m (Fin.find (fun j => p (Fin.natAdd m j)) ⋯)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.cases : Bool → Lean.Meta.Grind.AttrKind
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.ofNat_ctorIdx : ∀ (x : CategoryTheory.Limits.WalkingParallelPair), CategoryTheory.Limits.WalkingParallelPair.ofNat x.ctorIdx = x
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- `unfiltered` will be shown in the unfiltered view.  -/
Mathlib.Tactic.ClickSuggestions.Result.unfiltered : {α : Type} → Mathlib.Tactic.ClickSuggestions.Result α → ProofWidgets.Html
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_inf : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} {x : X}, x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Mathlib.Order.Filter.Map
Filter.comap_id : ∀ {α : Type u_1} {f : Filter α}, Filter.comap id f = f
-- Lean.Meta.Tactic.Cases
/-- We say the major premise has independent indices IF
1- its type is *not* an indexed inductive family, OR
2- its type is an indexed inductive family, but all indices are distinct free variables, and
   all local declarations different from the major and its indices do not depend on the indices.
 -/
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.Cases.hasIndepIndices : Lean.Meta.Cases.Context → Lean.MetaM Bool
-- Init.Data.BitVec.Lemmas
BitVec.toInt_sshiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, (x.sshiftRight n).toInt = x.toInt >>> n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.Full.mapAddMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful], F.mapAddMon.Full
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInverseAssociator.eq_1 : ∀ (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.sum.inlCompInverseAssociator C D E =
    ((CategoryTheory.Sum.inl_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).inlCompSum'
      (((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).sum'
        (CategoryTheory.Sum.inr_ (C ⊕ D) E))
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
preserves finite biproducts.  -/
CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesProductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F],
  CategoryTheory.Limits.PreservesBiproductsOfShape J F
-- Mathlib.Data.Num.Bitwise
/-- Add two `SNum`s.  -/
SNum.add : SNum → SNum → SNum
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- Every algebra morphism from the even subalgebra is in one-to-one correspondence with a
bilinear map that sends duplicate arguments to the quadratic form, and contracts across
multiplication.  -/
CliffordAlgebra.even.lift : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) →
            {A : Type u_3} →
              [inst_3 : Ring A] →
                [inst_4 : Algebra R A] → CliffordAlgebra.EvenHom Q A ≃ (↥(CliffordAlgebra.even Q) →ₐ[R] A)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.expandIncomingCallHierarchy : ℕ → Lean.Lsp.DocumentUri → Lean.Lsp.Position → Lean.Lsp.Ipc.IpcM (Array Lean.Lsp.Ipc.CallHierarchy × ℕ)
-- Mathlib.Data.Finset.NatAntidiagonal
/-- The antidiagonal of `0` is the list `[(0, 0)]`  -/
Finset.Nat.antidiagonal_zero : Finset.HasAntidiagonal.antidiagonal 0 = {(0, 0)}
-- Init.Data.Int.DivMod.Lemmas
Int.divExact.congr_simp : ∀ (x x_1 : ℤ) (e_x : x = x_1) (y y_1 : ℤ) (e_y : y = y_1) (h : y ∣ x), x.divExact y h = x_1.divExact y_1 ⋯
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_zero : ∀ {R : Type u_1} [inst : Semiring R] (x : R), ∑ i ∈ Finset.range 0, x ^ i = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The forgetful functor from additive monoid objects to the ambient category
reflects isomorphisms.  -/
CategoryTheory.AddMon.instReflectsIsomorphismsForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.AddMon.forget C).ReflectsIsomorphisms
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.mk : {α : Type u} → [toPseudoMetricSpace : PseudoMetricSpace α] → (∀ {x y : α}, dist x y = 0 → x = y) → MetricSpace α
-- Mathlib.Algebra.GroupWithZero.Hom
/-- We define `x ↦ x^n` (for positive `n : ℕ`) as a `MonoidWithZeroHom`  -/
powMonoidWithZeroHom : {M₀ : Type u_6} → [inst : CommMonoidWithZero M₀] → {n : ℕ} → n ≠ 0 → M₀ →*₀ M₀
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreComp_inv_app_iso_inv : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : CategoryTheory.Core C),
  ((F.coreComp G).inv.app X).iso.inv = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.of))
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics as an iff (`Field` version).  -/
Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero' : ∀ {R : Type u_1} [inst : Field R] {a b c x1 x2 : R},
  a ≠ 0 →
    ((Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2} ↔
      x1 + x2 = -b / a ∧ x1 * x2 = c / a)
-- Init.Data.Array.Lemmas
Array.filterMap_eq_filter : ∀ {α : Type u_1} {stop : ℕ} {as : Array α} {p : α → Bool},
  stop = as.size → Array.filterMap (Option.guard fun x => p x) as 0 stop = Array.filter p as
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.alter.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α] {β : Type v}
  (m : Std.DHashMap.Raw α fun x => β) (a : α) (f : Option β → Option β),
  Std.DHashMap.Raw.Const.alter m a f =
    if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.Const.alter ⟨m, h⟩ a f) else ∅
-- Mathlib.Algebra.Group.Pi.Lemmas
Commute.pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {x y : (i : I) → f i},
  (∀ (i : I), Commute (x i) (y i)) → Commute x y
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Split a `Prop` in characteristic zero into equal and mixed characteristic.  -/
split_equalCharZero_mixedCharZero : ∀ (R : Type u_1) [inst : CommRing R] {P : Prop} [CharZero R],
  (∀ (a : Algebra ℚ R), P) → (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → P
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSlice_ne_startPos : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos},
  p ≠ (s.slice p₀ p₁ h).startPos → String.Slice.Pos.ofSlice p ≠ s.startPos
-- Mathlib.Algebra.Order.Monovary
monovaryOn_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Suppose `G` acts on `M` and `I` is a subgroup of `M`.
The inertia subgroup of `I` is the subgroup of `G` whose action is trivial mod `I`.  -/
AddSubgroup.inertia : {M : Type u_6} → [inst : AddGroup M] → AddSubgroup M → (G : Type u_7) → [inst : Group G] → [MulAction G M] → Subgroup G
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.unitEmbedding_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (k : Kˣ),
  ↑((IsDedekindDomain.FiniteAdeleRing.unitEmbedding R K) k) = (algebraMap K (IsDedekindDomain.FiniteAdeleRing R K)) ↑k
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.AdicCauchySequence.map_apply_coe : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N)
  (a : AdicCompletion.AdicCauchySequence I M) (n : ℕ), ↑((AdicCompletion.AdicCauchySequence.map I f) a) n = f (↑a n)