mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
/-- The basis on `ι →₀ M` with basis vectors `fun ⟨i, x⟩ ↦ single i (b i x)`.  -/
Finsupp.basis : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {φ : ι → Type u_4} → ((i : ι) → Module.Basis (φ i) R M) → Module.Basis ((i : ι) × φ i) R (ι →₀ M)
-- Lean.Meta.Tactic.Apply
/-- Apply `And.intro` as much as possible to goal `mvarId`.
 -/
Lean.MVarId.splitAnd : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instZero : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddMonoid Y] → Zero (Function.locallyFinsuppWithin U Y)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_orderMonoidWithZeroHom_id : ∀ {α : Type u_2} [inst : NonAssocSemiring α] [inst_1 : Preorder α], ↑(OrderRingHom.id α) = OrderMonoidWithZeroHom.id α
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.match_4.congr_eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l) (l_1 : RBTree.RBNode α),
  l = l_1 →
    (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), l_1 = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
      (match l with
        | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
        | l => h_2 l) ≍
        h_2 l_1
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isEmbedding_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsEmbedding ⇑DomAddAct.mk.symm
-- Mathlib.LinearAlgebra.Isomorphisms
/-- The **first isomorphism law for modules**. The quotient of `M` by the kernel of `f` is linearly
equivalent to the range of `f`.  -/
LinearMap.quotKerEquivRange : {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → (f : M →ₗ[R] M₂) → (M ⧸ f.ker) ≃ₗ[R] ↥f.range
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.instSMulZeroClassUnitsRingOfIntegersMixedSpace : (K : Type u_1) →
  [inst : Field K] → SMulZeroClass (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.counit_obj_eq_map_counit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (j : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Coreflective j] (X : D),
  (CategoryTheory.coreflectorAdjunction j).counit.app (j.obj ((CategoryTheory.coreflector j).obj X)) =
    j.map ((CategoryTheory.coreflector j).map ((CategoryTheory.coreflectorAdjunction j).counit.app X))
-- Mathlib.Order.Concept
Concept.extent_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r),
  (⨆ i, f i).extent = lowerPolar r (⋂ i, (f i).intent)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n * log n). Adaptively chooses between the linear and log-linear algorithm depending
  on whether the input list is already sorted.

```
ofList' [1, 2, 3] = {1, 2, 3}
ofList' [2, 1, 1, 3] = {1, 2, 3}
```  -/
Ordnode.ofList' : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → List α → Ordnode α
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instCompleteLattice.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instCompleteLattice =
    { toPartialOrder := inferInstance.toPartialOrder, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯,
      sup_le := ⋯, inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (completeLatticeOfCompleteSemilatticeInf (GroupTopology α)).toSupSet, isLUB_sSup := ⋯,
      toInfSet := (completeLatticeOfCompleteSemilatticeInf (GroupTopology α)).toInfSet, isGLB_sInf := ⋯,
      toBoundedOrder := inferInstance }
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.refl_apply : ∀ {M : Type u_4} [inst : Add M] (m : M), (AddEquiv.refl M) m = m
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A `FiniteAddGrp` when given the discrete topology can be considered as a
profinite additive group.  -/
ProfiniteAddGrp.ofFiniteAddGrp : FiniteAddGrp.{u_1} → ProfiniteAddGrp.{u_1}
-- Mathlib.Algebra.Group.Pi.Basic
/-- If the one function is surjective, the codomain is trivial.  -/
uniqueOfSurjectiveOne : (α : Type u_4) → {β : Type u_5} → [inst : One β] → Function.Surjective 1 → Unique β
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_iteratedFDeriv_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (f : E → F), ‖iteratedFDeriv 𝕜 1 f x‖ = ‖fderiv 𝕜 f x‖
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence.eq_def : ∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size) (guess : ℕ) (hg : guess < stackPos),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst guess hg =
    if pat[guess] = pat[stackPos] then guess + 1
    else
      if h : guess = 0 then 0
      else
        have this := ⋯;
        String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst
          (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (guess - 1) ⋯) ⋯
-- Mathlib.Algebra.Lie.Prod
/-- Split equality of Lie algebra homomorphisms from a product into Lie algebra homomorphism over
each component, to allow `ext` to apply lemmas specific to `L₁ →ₗ L` and `L₂ →ₗ L`.

See note [partially-applied ext lemmas].  -/
LieHom.prod_ext : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] {f g : L₁ × L₂ →ₗ⁅R⁆ L},
  f.comp (LieHom.inl R L₁ L₂) = g.comp (LieHom.inl R L₁ L₂) →
    f.comp (LieHom.inr R L₁ L₂) = g.comp (LieHom.inr R L₁ L₂) → f = g
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.zero_val : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (d : F.WellOrderInductionData) [inst_2 : OrderBot J] (val₀ : F.obj (Opposite.op ⊥)),
  (CategoryTheory.Functor.WellOrderInductionData.Extension.zero d val₀).val = val₀
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).isColimit.desc s =
    CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F)
      { pt := s.pt, ι := { app := fun x => CategoryTheory.Limits.Sigma.desc fun x_1 => s.ι.app ↑x_1, naturality := ⋯ } }
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌈(b - v % r) / r⌉` numbers in `[0, b)` congruent to `v` mod `r`.  -/
Nat.count_modEq_card_eq_ceil : ∀ (b : ℕ) {r : ℕ}, 0 < r → ∀ (v : ℕ), ↑(Nat.count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉
-- Mathlib.CategoryTheory.Yoneda
/-- Version of `corepresentableByEquiv` with more general universe assumptions.  -/
CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type (max w v₁))) →
      (X : C) → F.CorepresentableBy X ≃ (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ≅ F)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.renameFun.congr_simp : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f f_1 : σ → τ) (e_f : f = f_1) [inst : Filter.TendstoCofinite f]
  [inst_1 : Semiring R] (a a_1 : MvPowerSeries σ R),
  a = a_1 → ∀ (a_2 a_3 : τ →₀ ℕ), a_2 = a_3 → MvPowerSeries.renameFun f a a_2 = MvPowerSeries.renameFun f_1 a_1 a_3
-- Std.Data.TreeMap.Raw.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.Raw.getKey : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap.Raw α β cmp) → (a : α) → a ∈ t → α
-- Mathlib.Topology.UniformSpace.CompareReals
/-- Real numbers constructed as in Bourbaki.  -/
CompareReals.Bourbakiℝ : Type
-- Mathlib.Data.Rat.Defs
Rat.mk'_num_den : ∀ (q : ℚ), { num := q.num, den := q.den, den_nz := ⋯, reduced := ⋯ } = q
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} (hf : Function.Injective f),
  s.disjiUnion (fun a => {f a}) ⋯ = Finset.map { toFun := f, inj' := hf } s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t.getKey a h = (t.getKey? a).get ⋯
-- Mathlib.Computability.Reduce
/-- **Alias** of `isTrans_oneOneReducible`. -/
transitive_oneOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], IsTrans (α → Prop) OneOneReducible
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.instCategory : CategoryTheory.Category.{u, u + 1} TopCommRingCat
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_single`. -/
SkewMonoidAlgebra.ofFinsupp_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G) (b : k),
  { coeff := fun₀ | a => b } = SkewMonoidAlgebra.single a b
-- Mathlib.Tactic.Linter.Style
/-- The `cdot` linter flags uses of the "cdot" `·` that are achieved by typing a character
different from `·`.
For instance, a "plain" dot `.` is allowed syntax, but is flagged by the linter.
It also flags "isolated cdots", i.e. when the `·` is on its own line.  -/
Mathlib.Linter.linter.style.cdot : Lean.Option Bool
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_C_mul : ∀ (R : Type u_1) [inst : Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S), (Polynomial.C r * p).smeval x = r • p.smeval x
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
/-- Nontrivial commutative semirings `R` satisfy the rank condition.

If `R` is moreover a ring, then it satisfies the strong rank condition, see
`commRing_strongRankCondition`. It is unclear whether this generalizes to semirings.  -/
rankCondition_of_nontrivial_of_commSemiring : ∀ {R : Type u_4} [inst : CommSemiring R] [Nontrivial R], RankCondition R
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.eq_3 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop)
  (x : Option (α × Stream'.WSeq α)) (x_1 : Option (β × Stream'.WSeq β)),
  (x = none → x_1 = none → False) →
    (∀ (a : α) (s : Stream'.WSeq α) (b : β) (t : Stream'.WSeq β), x = some (a, s) → x_1 = some (b, t) → False) →
      Stream'.WSeq.LiftRelO R C x x_1 = False
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Unfold the definition of `comp`.
This exists to streamline the proof of `MonoidalClosed.assoc`  -/
CategoryTheory.MonoidalClosed.comp_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y],
  CategoryTheory.MonoidalClosed.comp x y z =
    CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalClosed.compTranspose x y z)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.nsmul_inj_mod : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {x : G} {n m : ℕ}, n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x
-- Lean.Meta.Tactic.Grind.Types
/-- Key for the congruence theorem cache.  -/
Lean.Meta.Grind.CongrTheoremCacheKey : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (n : ℕ), 0 ≤ x.sqrtTwoAddSeries n
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsEquivalenceOfRingEquiv_inverse : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  (AlgCat.restrictScalarsEquivalenceOfRingEquiv e).inverse = AlgCat.restrictScalars e.symm.toRingHom
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type u_1} {I : J → Type u_2}
  {inst_1 : CategoryTheory.Category.{v_1, u_1} J} {inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)}
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} {base : k.fst ⟶ l.fst}
  {hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
        CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd))
      CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam}
  {base_1 : k.fst ⟶ l.fst} {hom_1 : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base_1) =
        CategoryTheory.CategoryStruct.comp hom_1 ((P l.fst).ι.app l.snd))
      CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam},
  { base := base, hom := hom, w := w } = { base := base_1, hom := hom_1, w := w_1 } → base = base_1 ∧ hom = hom_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Sigma.fst l).contains k = true
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- The **Marica-Schönheim Inequality**.  -/
Finset.card_le_card_diffs : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s : Finset α), s.card ≤ (s.diffs s).card
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.Scheme.quasiSeparatedSpace_of_isOpenCover : ∀ {X : AlgebraicGeometry.Scheme} {I : Type u_1} (U : I → X.Opens),
  TopologicalSpace.IsOpenCover U →
    (∀ (i : I), AlgebraicGeometry.IsAffineOpen (U i)) →
      (∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))) → QuasiSeparatedSpace ↥X
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.hasStrictDerivAt_exp : ∀ (x : ℂ), HasStrictDerivAt Complex.exp (Complex.exp x) x
-- Aesop.Frontend.Basic
Aesop.Frontend.Parser.bool_litTrue : Lean.ParserDescr
-- Mathlib.Tactic.FunProp.Elab
_private.Mathlib.Tactic.FunProp.Elab.0.Mathlib.Meta.FunProp.elabFunPropConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Meta.FunProp.Config
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_comp : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₃]
  [inst_8 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_9 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₃]
  [inst_10 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃),
  (CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J V))).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V) f)
          ((CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V) g))
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₃))
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_addConst : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  ∀ k ≥ 0,
    p.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (p.addConst k) = Lean.Grind.CommRing.Poly.denoteS ctx p + ↑k.toNat
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The map from `realSpace K → realSpace K` whose components is given by `expMap_single`. It is, in
some respect, a right inverse of `logMap`, see `logMap_expMap`.
 -/
NumberField.mixedEmbedding.fundamentalCone.expMap : {K : Type u_1} →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.realSpace K) (NumberField.mixedEmbedding.realSpace K)
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Var)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.var x with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | x => h_3 x) =
    h_2 x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0IsoOfIsTrivial.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupHomology.H0IsoOfIsTrivial A =
    (HomologicalComplex.isoHomologyπ (groupHomology.inhomogeneousChains A) 1 0 groupHomology.opcyclesIso₀._proof_1
          ⋯).symm ≪≫
      groupHomology.cyclesIso₀ A
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- `χ₈` takes values in `{0, 1, -1}`  -/
ZMod.isQuadratic_χ₈ : ZMod.χ₈.IsQuadratic
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp},
  t.Equiv Std.TreeMap.Raw.empty ↔ t.isEmpty = true
-- Mathlib.Data.Finset.Functor
Finset.instLawfulAlternative : ∀ [inst : (P : Prop) → Decidable P], LawfulAlternative Finset
-- Mathlib.Algebra.Ring.Parity
even_two : ∀ {α : Type u_2} [inst : AddMonoidWithOne α], Even 2
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkPullbackInv_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (V : TopologicalSpace.Opens ↑X) (hV : x ∈ V) {Z : C}
  (h : F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ V x hV)
      (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPullbackInv C f F x) h) =
    CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F V x hV) h
-- Mathlib.Order.Hom.PowersetCard
/-- The natural enumeration of the elements of linearly-ordered type.  -/
Set.powersetCard.orderIsoOfFin : {n : ℕ} → {I : Type u_2} → [inst : LinearOrder I] → (s : ↑(Set.powersetCard I n)) → Fin n ≃o ↥↑s
-- Lean.Parser.Command
Lean.Parser.Command.registerErrorExplanationStx.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_finsuppSum : ∀ {ι : 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 : AddCommMonoid N] (f : ι →₀ N) (g : ι → N → PolynomialModule R M),
  (f.sum g).coeff = f.sum fun i n => (g i n).coeff
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodalWeight_eq_eval_derivative_nodal : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  i ∈ s → Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)))⁻¹
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso_hom_iCycles_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom
      (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) =
    CategoryTheory.CategoryStruct.comp ((K.extend e).iCycles j')
      (CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNegNNRat.injEq : ∀ (inst : Lean.Expr) (q : ℚ) (n d proof inst_1 : Lean.Expr) (q_1 : ℚ) (n_1 d_1 proof_1 : Lean.Expr),
  (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof =
      Mathlib.Meta.NormNum.Result'.isNegNNRat inst_1 q_1 n_1 d_1 proof_1) =
    (inst = inst_1 ∧ q = q_1 ∧ n = n_1 ∧ d = d_1 ∧ proof = proof_1)
-- Mathlib.Tactic.Translate.Reorder
/-- Two permutations are considered equal if they permute in the same way.  -/
Mathlib.Tactic.Translate.Permutation.beq : Mathlib.Tactic.Translate.Permutation → Mathlib.Tactic.Translate.Permutation → Bool
-- Lean.Declaration
Lean.instInhabitedConstantInfo : Inhabited Lean.ConstantInfo
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The Riemann zeta function is real-valued for real arguments greater than 1.  -/
riemannZeta_im_eq_zero_of_one_lt : ∀ {x : ℝ}, 1 < x → (riemannZeta ↑x).im = 0
-- Mathlib.Tactic.FieldSimp
/-- Given `e₁` and `e₂`, cancel positive factors to construct a new inequality which is logically
equivalent to `e₁ < e₂`.  -/
Mathlib.Tactic.FieldSimp.reduceLtQ : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      (iM : Q(CommGroupWithZero «$M»)) →
        (iM' : Q(PartialOrder «$M»)) →
          Q(PosMulStrictMono «$M») →
            Q(PosMulReflectLT «$M») →
              Q(ZeroLEOneClass «$M») →
                (e₁ e₂ : Q(«$M»)) →
                  Mathlib.Tactic.AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» < «$e₂») = («$f₁» < «$f₂»)))
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.update_self : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α), f.update a (f.coeff a) = f