mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- A universal colimit is a colimit.  -/
CategoryTheory.IsUniversalColimit.isColimit : {J : Type v'} →
  [inst : CategoryTheory.Category.{u', v'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {c : CategoryTheory.Limits.Cocone F} → CategoryTheory.IsUniversalColimit c → CategoryTheory.Limits.IsColimit c
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a : α),
  ⇑e '' Set.Iic a = Set.Iic (e a)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.epic_of_localizationMap : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {P : Type u_4} [inst_2 : Monoid P] {j k : N →* P},
  j.comp f.toMonoidHom = k.comp f.toMonoidHom → j = k
-- Mathlib.NumberTheory.NumberField.CMField
/-- The index of the image of `unitsMulComplexConjInv` divides `2`.
 -/
NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  (NumberField.IsCMField.unitsMulComplexConjInv K).range.index ∣ 2
-- Aesop.Search.Expansion.Simp
Aesop.addLetDeclsToSimpTheoremsUnlessZetaDelta : Lean.Meta.Simp.Context → Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_iff_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P'),
  CategoryTheory.Presieve.IsSheafFor P R ↔ CategoryTheory.Presieve.IsSheafFor P' R
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mk_eq_one : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {g : G} {h : g ∈ H}, ⟨g, h⟩ = 1 ↔ g = 1
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.checkKinds : Lean.Elab.DefKind → Lean.Elab.DefKind → Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isOpenEmbedding_exp : Topology.IsOpenEmbedding Real.exp
-- Mathlib.Order.Filter.Basic
Filter.sup_sets_eq : ∀ {α : Type u} {f g : Filter α}, (f ⊔ g).sets = f.sets ∩ g.sets
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.symmCompOfNondegenerate_left_apply : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate)
  (v w : V), (B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, the type of `AddCommMonoid` homomorphisms `f : M →+ N` such that `N` is
isomorphic to the localization of `M` at the AddSubmonoid generated by `x`.  -/
AddSubmonoid.LocalizationMap.AwayMap : {M : Type u_1} → [AddCommMonoid M] → M → (N' : Type u_4) → [AddCommMonoid N'] → Type (max u_1 u_4)
-- Mathlib.Algebra.Order.Floor.Div
gc_mul_ceilDiv : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : CeilDiv α α] {a : α},
  0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a * x
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An invariant block of a group action is a block.  -/
AddAction.IsInvariantBlock.isBlock : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsInvariantBlock G B → AddAction.IsBlock G B
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Monotone convergence theorem** expressed with limits.  -/
MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) →
        Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.val_step_filter : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → Bool},
  ↑(Std.Iter.filter f it).step =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      if f out = true then Std.IterStep.yield (Std.Iter.filter f it') out else Std.IterStep.skip (Std.Iter.filter f it')
    | Std.IterStep.skip it' => Std.IterStep.skip (Std.Iter.filter f it')
    | Std.IterStep.done => Std.IterStep.done
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.HashSet.Raw.ofList l).contains k = l.contains k
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.instContainsZeroIntUpPlusOfHasZeroObject : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C], (HomotopyCategory.plus C).ContainsZero
-- Mathlib.Data.Nat.PSub
Nat.ppred_eq_some : ∀ {m n : ℕ}, n.ppred = some m ↔ m.succ = n
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
isLUB_csSup' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α}, BddAbove s → IsLUB s (sSup s)
-- Init.Data.Prod
Prod.forall : ∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instRing : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] → [IsOrderedCancelAddMonoid Γ] → [inst : Ring R] → Ring (HahnSeries Γ R)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.smul_continuousOn : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9}
  [inst_6 : NormedRing 𝕜] [SecondCountableTopologyEither X E] [inst_8 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] {f : X → 𝕜}
  {g : X → E} {s : Set X},
  IsLocallyClosed s →
    MeasureTheory.LocallyIntegrableOn f s μ →
      ContinuousOn g s → MeasureTheory.LocallyIntegrableOn (fun x => f x • g x) s μ
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.hasMul : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → Mul (MulChar R R')
-- Mathlib.Algebra.Group.Units.Hom
Units.map_injective : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] {f : M →* N},
  Function.Injective ⇑f → Function.Injective ⇑(Units.map f)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero : ∀ {α : Type u_1} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  [inst_2 : MeasurableSpace α] {f : α → ε}, MeasureTheory.eLpNorm' f 0 0 = 1
-- Mathlib.GroupTheory.Finiteness
Group.FG.mk : ∀ {G : Type u_3} [inst : Group G], ⊤.FG → Group.FG G
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k k' fallback : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKeyD k' fallback =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_eq_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImage.uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f)
  (l : CategoryTheory.Limits.image f ⟶ F'.I),
  CategoryTheory.CategoryStruct.comp l F'.m = CategoryTheory.Limits.image.ι f → l = CategoryTheory.Limits.image.lift F'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.Δ.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R),
  W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The constructed cofan is indeed a colimit  -/
TopCat.sigmaCofanIsColimit : {ι : Type v} → (β : ι → TopCat) → CategoryTheory.Limits.IsColimit (TopCat.sigmaCofan β)
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint over `F` and `A ⊔ B = E`, then the `Module.finrank` of
`E` over `B` is equal to the `Module.finrank` of `A` over `F`.
 -/
IntermediateField.LinearDisjoint.finrank_right_eq_finrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [Module.Finite F ↥B], A.LinearDisjoint ↥B → A ⊔ B = ⊤ → Module.finrank (↥B) E = Module.finrank F ↥A
-- Mathlib.Data.List.Basic
List.idxOf_inj : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} {x y : α}, x ∈ l → (List.idxOf x l = List.idxOf y l ↔ x = y)
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on a typed expression `e : α`,
returning a typed expression `lit : ℕ`, and a proof of `isNat e lit`.  -/
Mathlib.Meta.NormNum.deriveNat : {u : Lean.Level} →
  {α : Q(Type u)} →
    (e : Q(«$α»)) →
      (_inst : autoParam Q(AddMonoidWithOne «$α») Mathlib.Meta.NormNum.deriveNat._auto_1) →
        Lean.MetaM ((lit : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat «$e» «$lit»))
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.prop_retractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : C},
  P Y → ∀ (r : CategoryTheory.Retract X Y), P.retractClosure X
-- Mathlib.Computability.Primrec.Basic
Primrec.encode_iff : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
  (Primrec fun a => Encodable.encode (f a)) ↔ Primrec f
-- Mathlib.Order.Irreducible
/-- An inf-irreducible element is a non-top element which isn't the infimum of anything bigger.  -/
InfIrred : {α : Type u_2} → [SemilatticeInf α] → α → Prop
-- Mathlib.Algebra.Opposites
AddOpposite.instDiv : {α : Type u_1} → [Div α] → Div αᵃᵒᵖ
-- Mathlib.Algebra.Order.Group.Basic
zsmul_left_mono : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α},
  0 ≤ a → Monotone fun n => n • a
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_6 : ∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr) (k : ℤ),
  Int.Internal.Linear.Expr.toPoly'.go coeff (a.mulR k) =
    bif k == 0 then id else Int.Internal.Linear.Expr.toPoly'.go (coeff.mul k) a
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.mk.sizeOf_spec : ∀ (induction : Bool) (typeNames : Array Lean.Name) (elimName : Lean.Name),
  sizeOf { induction := induction, typeNames := typeNames, elimName := elimName } =
    1 + sizeOf induction + sizeOf typeNames + sizeOf elimName
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.measure_condCDF_Iic : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ),
  (ProbabilityTheory.condCDF ρ a).measure (Set.Iic x) = ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x)
-- Mathlib.NumberTheory.Ostrowski
/-- The standard absolute value on `ℚ` is not equivalent to any `p`-adic absolute value.  -/
Rat.AbsoluteValue.not_real_isEquiv_padic : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Rat.AbsoluteValue.real.IsEquiv (Rat.AbsoluteValue.padic p)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a negative constant, `fun x ↦ r * f x` tends to infinity along a filter `l`
if and only if `f` tends to negative infinity along `l`.  -/
Filter.tendsto_const_mul_atTop_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot)
-- Mathlib.RingTheory.Filtration
/-- An `I`-filtration on the module `M` is a sequence of decreasing submodules `N i` such that
`I • (N i) ≤ N (i + 1)`. Note that we do not require the filtration to start from `⊤`.  -/
Ideal.Filtration : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_3) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_3
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If two morphisms are known to be equal, then their cokernels are isomorphic.  -/
CategoryTheory.Limits.cokernelIsoOfEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasCokernel g] →
              f = g → (CategoryTheory.Limits.cokernel f ≅ CategoryTheory.Limits.cokernel g)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Another characterization lemma for the scalar multiplication on the Ore localization delivering
Ore witnesses and conditions bundled in a sigma type.  -/
OreLocalization.oreDivSMulChar' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : MulAction R X] →
            (r₁ : R) →
              (r₂ : X) →
                (s₁ s₂ : ↥S) →
                  (r' : R) ×' (s' : ↥S) ×' ↑s' * r₁ = r' * ↑s₂ ∧ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.toOfSimplex_ι : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.toOfSimplex x) (SSet.Subcomplex.ofSimplex x).ι =
    SSet.yonedaEquiv.symm x
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
measurableEmbedding_sigmoid : MeasurableEmbedding unitInterval.sigmoid
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
/-- An extension of the `NonUnitalContinuousFunctionalCalculus` requiring that `cfcₙHom` is an
isometry.  -/
NonUnitalIsometricContinuousFunctionalCalculus : (R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [IsTopologicalSemiring R] →
                [ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [StarRing A] →
                      [MetricSpace A] → [inst_9 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.one_seq : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.one.seq =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} →
          {A : CategoryTheory.Functor C (Type w)} →
            (app : (c : C) → A.obj c → (F.obj c ⟶ G.obj c)) →
              autoParam
                  (∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
                    CategoryTheory.CategoryStruct.comp (F.map f)
                        (app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
                      CategoryTheory.CategoryStruct.comp (app c a) (G.map f))
                  CategoryTheory.Functor.HomObj.naturality._autoParam →
                F.HomObj G A
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero : ∀ {w : ℕ} {c : Bool} {a e : BitVec w}, (a * bif c then 0#w else e) = bif c then 0#w else a * e
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The family of seminorms that induce the weak operator topology, namely `‖y (A x)‖` for
all `x` and `y`.  -/
ContinuousLinearMapWOT.seminorm : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] → E → StrongDual 𝕜₂ F → Seminorm 𝕜₂ (E →SWOT[σ] F)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Characterizing the forward direction of `rightUnitor` via the universal maps.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app : ∀ {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.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] (x : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
        CategoryTheory.MonoidalCategory.DayConvolutionUnit.can)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit F U).app
          (x, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).hom
      (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).inv)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef.mk.injEq : ∀ {α : Type} (ref ref_1 : IO.Ref (Lean.Meta.LazyDiscrTree α)), ({ ref := ref } = { ref := ref_1 }) = (ref = ref_1)
-- Mathlib.LinearAlgebra.Matrix.Basis
mul_basis_toMatrix : ∀ {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : Fintype ι'] [inst_6 : Finite κ] [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] [inst_9 : DecidableEq ι']
  (b₁ : Module.Basis ι R M) (b₂ : Module.Basis ι' R M) (b₃ : Module.Basis κ R N) (A : Matrix κ ι R),
  A * b₁.toMatrix ⇑b₂ = (LinearMap.toMatrix b₂ b₃) ((Matrix.toLin b₁ b₃) A)
-- Mathlib.Probability.Distributions.Exponential
/-- The pdf of the exponential distribution depending on its rate  -/
ProbabilityTheory.exponentialPDFReal : ℝ → ℝ → ℝ
-- Mathlib.GroupTheory.CoprodI
/-- Induct on a word by adding letters one at a time without reduction,
effectively inducting on the underlying `List`.  -/
Monoid.CoprodI.Word.consRecOn : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {motive : Monoid.CoprodI.Word M → Sort u_4} →
        (w : Monoid.CoprodI.Word M) →
          motive Monoid.CoprodI.Word.empty →
            ((i : ι) →
                (m : M i) →
                  (w : Monoid.CoprodI.Word M) →
                    (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Monoid.CoprodI.Word.cons m w h1 h2)) →
              motive w
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_eq_false_iff_forall_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulHashable α] [EquivBEq α]
  {p : α → β → Bool}, m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) m[a] = false
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff_notMem_span : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s : Set ι}, LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ Submodule.span K (v '' (s \ {i}))
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : α → β} {a : α}, IsLocalMin f a → IsLocalMax (fun x => -f x) a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_eq_withBotDegree_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R),
  m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBy.mk_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (a b : R)
  (x : ↥(Submodule.torsionBy R M a)), (Ideal.Quotient.mk (R ∙ a)) b • x = b • x
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.mk : {α : Type u} →
  {β : Type v} →
    [inst : PseudoEMetricSpace α] →
      [inst_1 : PseudoEMetricSpace β] → (toEquiv : α ≃ β) → Isometry toEquiv.toFun → α ≃ᵢ β
-- Mathlib.Topology.Algebra.Monoid
Submonoid.commMonoidTopologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M]
  [inst_3 : T2Space M] (s : Submonoid M) (hs : ∀ (x y : ↥s), x * y = y * x),
  s.commMonoidTopologicalClosure hs = { toMonoid := s.topologicalClosure.toMonoid, mul_comm := ⋯ }
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_lt_toNNRat_iff_of_nonneg : ∀ {p q : ℚ}, 0 ≤ q → (q.toNNRat < p.toNNRat ↔ q < p)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The canonical map `P ⟶ L₂.X₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.φ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.P ⟶ S.L₂.X₂
-- Std.Tactic.BVDecide.Syntax
/-- Split up local declarations of structures that are collections of other supported types into their
individual parts automatically.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.structures : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- **Alias** of `Matroid.eRk_le_eRk_add_eRk_sdiff`. -/
Matroid.eRk_le_eRk_add_eRk_diff : ∀ {α : Type u_1} {X Y : Set α} (M : Matroid α), Y ⊆ X → M.eRk X ≤ M.eRk Y + M.eRk (X \ Y)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasSum_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → β}, Function.Injective g → (∀ x ∉ Set.range g, f x = 0) → (HasSum (f ∘ g) a ↔ HasSum f a)
-- Mathlib.Order.Hom.Basic
OrderHomClass.monotone : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : FunLike F α β]
  [OrderHomClass F α β] (f : F), Monotone ⇑f
-- Mathlib.Data.Set.Card
Set.exists_subset_encard_eq : ∀ {α : Type u_1} {s : Set α} {k : ℕ∞}, k ≤ s.encard → ∃ t ⊆ s, t.encard = k
-- Mathlib.Order.CompleteBooleanAlgebra
PUnit.sInf_eq : ∀ (s : Set PUnit.{u + 1}), sInf s = PUnit.unit
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.instIsIdOfIsIdCoe : ∀ {M : Type u_1} [inst : Monoid M] {σ : M →* M} [h : CompTriple.IsId ⇑σ], MonoidHom.CompTriple.IsId σ
-- Mathlib.Topology.Algebra.InfiniteSum.Module
HasSum.smul : ∀ {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace M] [T3Space M] [ContinuousAdd M]
  [ContinuousSMul R M] {f : ι → R} {g : κ → M} {s : R} {t : M},
  HasSum f s → HasSum g t → (Summable fun x => f x.1 • g x.2) → HasSum (fun x => f x.1 • g x.2) (s • t)