mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `J` is `u`-small, `CommRingCat.{u}` has limits of shape `J`.  -/
CommRingCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J CommRingCat
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.add_const' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Add ι] [inst_1 : LinearOrder ι]
  [CanonicallyOrderedAdd ι] [Countable ι] [inst_4 : TopologicalSpace ι] [OrderTopology ι]
  {f : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasureTheory.IsStoppingTime f fun ω => τ ω + ↑i
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Iic : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.rev (Finset.Iic i) = Finset.Ici i.rev
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} {K' : Type u_4} [inst_1 : Field K] [inst_2 : Field K']
  [inst_3 : Algebra R K] [IsFractionRing R K] [inst_5 : Algebra R K'] [IsFractionRing R K']
  {I : FractionalIdeal (nonZeroDivisors R) K} (h : K →ₐ[R] K') [Nontrivial R], FractionalIdeal.map h I = 0 ↔ I = 0
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.neg_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y), -a - b = -b - a
-- Mathlib.Data.Set.Card
Set.ncard_congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), f a ha ∈ t) →
    (∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b) →
      (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b) → s.ncard = t.ncard
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.fun.injEq : ∀ (depth depth_1 : ℕ), (Mathlib.Tactic.Conv.Path.fun depth = Mathlib.Tactic.Conv.Path.fun depth_1) = (depth = depth_1)
-- Std.Data.DTreeMap.Internal.Operations
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.DTreeMap.Internal.Impl.diff : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      (t₁ : Std.DTreeMap.Internal.Impl α β) →
        Std.DTreeMap.Internal.Impl α β → t₁.Balanced → Std.DTreeMap.Internal.Impl α β
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.congr_fun : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  {f g : A →ₑ+[φ] B}, f = g → ∀ (x : A), f x = g x
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- Given `F : C ⥤ H`, `W : MorphismProperty C` and `X : C`, we say that `F` has a
pointwise left derived functor at `X` if `F` has a right Kan extension
at `L.obj X` for any localization functor `L : C ⥤ D` for `W`. In the
definition, this is stated for `L := W.Q`, see `hasPointwiseLeftDerivedFunctorAt_iff`
for the more general equivalence.  -/
CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt : {C : Type u₁} →
  {H : Type u₃} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → C → Prop
-- Mathlib.Data.UInt
/-- Is this an alphanumeric ASCII character?  -/
UInt8.isASCIIAlphanum : UInt8 → Bool
-- Mathlib.Order.Interval.Basic
NonemptyInterval.snd_sup : ∀ {α : Type u_1} [inst : Lattice α] (s t : NonemptyInterval α), (s ⊔ t).toProd.2 = s.toProd.2 ⊔ t.toProd.2
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_surjective_of_surjective : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β},
  Function.Surjective f → Function.Surjective ⇑(FreeAddGroup.lift f)
-- Init.Grind.Module.Basic
/-- A type where addition is right-cancellative, i.e. `a + c = b + c` implies `a = b`.
 -/
Lean.Grind.AddRightCancel : (M : Type u) → [Add M] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.ext_iff : ∀ {V : Type u} {G : SimpleGraph V} {x y : G.Subgraph}, x = y ↔ x.verts = y.verts ∧ x.Adj = y.Adj
-- Init.Notation
/-- `doElem` is a builtin syntax category for elements that can appear in the `do` notation.
For example, `let x ← e` is a `doElem`, and a `do` block consists of a list of `doElem`s.  -/
Lean.Parser.Category.doElem : Lean.Parser.Category
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : Unit → motive 4) (h_6 : (n : ℕ) → motive n.succ.succ.succ.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | 4 => h_5 ()
    | n.succ.succ.succ.succ.succ => h_6 n) =
    h_2 ()
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindEIO : ∀ {ε : Type} [inst : Nonempty ε], Lean.Order.MonoBind (EIO ε)
-- Lean.Expr
Lean.instInhabitedExpr : Inhabited Lean.Expr
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- For a bounded set `s : Set ℝ`, its `ediam` is equal to `sSup s - sInf s` reinterpreted as
`ℝ≥0∞`.  -/
Real.ediam_eq : ∀ {s : Set ℝ}, Bornology.IsBounded s → Metric.ediam s = ENNReal.ofReal (sSup s - sInf s)
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist_triangle : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty Z] (Φ : Z → X)
  (Ψ : Z → Y) (ε : ℝ),
  (∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε) →
    ∀ (x y z : X ⊕ Y), Metric.glueDist Φ Ψ ε x z ≤ Metric.glueDist Φ Ψ ε x y + Metric.glueDist Φ Ψ ε y z
-- Init.Data.UInt.Bitwise
USize.toNat_shiftLeft : ∀ (a b : USize), (a <<< b).toNat = a.toNat <<< (b.toNat % System.Platform.numBits) % 2 ^ System.Platform.numBits
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Section` is a right inverse to `S.rightHom`  -/
GroupExtension.Splitting.rightInverse_rightHom : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (self : S.Splitting), Function.RightInverse (↑self.toMonoidHom).toFun ⇑S.rightHom
-- Mathlib.Probability.Moments.Variance
/-- **Alias** of `ProbabilityTheory.evariance_lt_top`. -/
MeasureTheory.MemLp.evariance_lt_top : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ProbabilityTheory.evariance X μ < ⊤
-- Mathlib.Algebra.Ring.Equiv
MulEquiv.isCancelMulZero_iff : ∀ {A : Type u_7} {B : Type u_8} [inst : MulZeroClass A] [inst_1 : MulZeroClass B] (e : A ≃* B),
  IsCancelMulZero A ↔ IsCancelMulZero B
-- Init.Data.Array.MapIdx
List.mapIdxM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  {f : ℕ → α → m β}, Array.mapIdxM f l.toArray = List.toArray <$> List.mapIdxM f l
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
/-- **Alias** of the reverse direction of `MeasureTheory.memLp_prod_iff`. -/
MeasureTheory.MemLp.of_fst_snd : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : X → E × F},
  MeasureTheory.MemLp (fun x => (f x).1) p μ ∧ MeasureTheory.MemLp (fun x => (f x).2) p μ → MeasureTheory.MemLp f p μ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₁ → (t₁ \ t₂)[k]! = default
-- Mathlib.Util.Notation3
Mathlib.Notation3.BoundValueType.foldl.sizeOf_spec : sizeOf Mathlib.Notation3.BoundValueType.foldl = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.left : CategoryTheory.Limits.WalkingReflexivePair.one.Hom CategoryTheory.Limits.WalkingReflexivePair.zero
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEval.toMkEvalHorizontalComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEval m] → Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.HashMap.unitOfList l).getKey? k = none
-- Init.Data.BitVec.Lemmas
BitVec.toInt_shiftRight_lt : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, x.toInt >>> n < 2 ^ (w - 1)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivCodomain_symm_apply_ne : ∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X)
  (h : x' ≠ x), ↑((Equiv.subtypeEquivCodomain f).symm y) x' = f ⟨x', h⟩
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addEquiv_symm_apply : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β] (b : β), (AddEquiv.symm e.addEquiv) b = e.symm b
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iic_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n),
  ∑ i ≤ Fin.castLE h a, f i = ∑ i ≤ a, f (Fin.castLE h i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.Hom.hom_hom_zsmul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X] (f : G ⟶ H) (n : ℤ), (n • f).hom.hom = n • f.hom.hom
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasFiniteLimits_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasFiniteLimits Cᵒᵖ ↔ CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The canonical `MultilinearMap R s (⨂[R] i, s i)`.

`tprod R fun i => f i` has notation `⨂ₜ[R] i, f i`.  -/
PiTensorProduct.tprod : {ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → MultilinearMap R s (PiTensorProduct R fun i => s i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (distance distance_1 : ℕ),
      distance = distance_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ w) (s s_1 : aig.RefVec curr),
          s = s_1 →
            Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s =
              Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input_1 distance_1 curr hcurr s_1
-- Mathlib.Data.List.Sort
/-- For an antisymmetric relation, erasing then inserting is the identity.  -/
List.orderedInsert_erase : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [inst_1 : DecidableEq α] [Std.Antisymm r] (x : α)
  (xs : List α), x ∈ xs → List.Pairwise r xs → List.orderedInsert r x (xs.erase x) = xs
-- Batteries.Data.List.Lemmas
List.findIdxNth.go.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (s : ℕ) (a : α) (xs_1 : List α),
  List.findIdxNth.go p (a :: xs_1) 0 s = bif p a then s else List.findIdxNth.go p xs_1 0 (s + 1)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_center : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ↑(NonUnitalSubalgebra.center R A) = Set.center A
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.σ : {n : ℕ} → Fin (n + 1) → (FreeSimplexQuiver.mk (n + 1)).Hom (FreeSimplexQuiver.mk n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- The sine of a `Real.Angle`.  -/
Real.Angle.sin : Real.Angle → ℝ
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- First part of the First Main Theorem, qualitative version: If `f` is meromorphic on the complex
plane, then the characteristic functions of `f` and `f⁻¹` agree asymptotically up to a bounded
function.
 -/
ValueDistribution.isBigO_characteristic_sub_characteristic_inv : ∀ {f : ℂ → ℂ},
  Meromorphic f → (ValueDistribution.characteristic f ⊤ - ValueDistribution.characteristic f⁻¹ ⊤) =O[Filter.atTop] 1
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_of_Ioo : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α}, (∀ x ∈ s, ∀ y ∈ s, x < y → Set.Ioo x y ⊆ s) → s.OrdConnected
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.le_dualAnnihilator_iff_le_dualCoannihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {U : Submodule R (Module.Dual R M)} {V : Submodule R M}, U ≤ V.dualAnnihilator ↔ V ≤ U.dualCoannihilator
-- Mathlib.Order.Nucleus
/-- The largest nucleus sends everything to `⊤`.  -/
Nucleus.instTop : {X : Type u_1} → [inst : SemilatticeInf X] → [OrderTop X] → Top (Nucleus X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.strictAntiOn_arccos : StrictAntiOn Real.arccos (Set.Icc (-1) 1)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.exists_eventually_r_le_const_mul : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
-- Mathlib.RingTheory.Ideal.Prod
Ideal.isPrime_of_isPrime_prod_top' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal S}, (⊤.prod I).IsPrime → I.IsPrime
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight_inl : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj X₁)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj Y₁)]
  (h : CategoryTheory.Limits.IsInitial X₂),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight F f₁ f₂ h).inl =
    (CategoryTheory.Limits.IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂)
-- Mathlib.Tactic.Ring.RingNF
/-- Function elaborating `RingNF.Config`.  -/
Mathlib.Tactic.RingNF.elabConfig : Lean.Syntax →
  optParam Mathlib.Tactic.RingNF.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.RingNF.Config
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1SeminormedRing : {R : Type u_3} →
  {M : Type u_4} →
    [inst : SeminormedRing R] →
      [inst_1 : SeminormedAddCommGroup M] →
        [inst_2 : Module R M] →
          [IsBoundedSMul R M] →
            [inst_4 : Module Rᵐᵒᵖ M] →
              [IsBoundedSMul Rᵐᵒᵖ M] → [SMulCommClass R Rᵐᵒᵖ M] → SeminormedRing (TrivSqZeroExt R M)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_zero : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero (CategoryTheory.CategoryStruct.id F.X)
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of the range of a surjective homomorphism from a
nilpotent additive group is less or equal the nilpotency class of the domain.  -/
AddGroup.nilpotencyClass_le_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {G' : Type u_2} [inst_1 : AddGroup G'] (f : G →+ G'),
  Function.Surjective ⇑f → ∀ [h : AddGroup.IsNilpotent G], AddGroup.nilpotencyClass G' ≤ AddGroup.nilpotencyClass G
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} [inst_2 : SizeOf C] (hom : M.X ⟶ N.X)
  (left_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam)
  (right_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam),
  sizeOf { hom := hom, left_act_hom := left_act_hom, right_act_hom := right_act_hom } =
    1 + sizeOf hom + sizeOf left_act_hom + sizeOf right_act_hom
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.unitsWithZeroEquiv.eq_1 : ∀ {α : Type u_1} [inst : Group α],
  WithZero.unitsWithZeroEquiv =
    { toFun := fun a => WithZero.unzero ⋯, invFun := fun a => Units.mk0 ↑a ⋯, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Basic
nndist_nnnorm_nnnorm_le_nnnorm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), nndist ‖a‖₊ ‖b‖₊ ≤ ‖-a + b‖₊
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.shiftFunctorIso_ofHasShiftOfFullyFaithful : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful)
  (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a : A),
  CategoryTheory.Functor.commShiftIso F a = i a
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- **Kummer's Theorem**
Taking (`p - 1`) times the `p`-adic valuation of the binomial `n` over `k` equals the sum of the
digits of `k` plus the sum of the digits of `n - k` minus the sum of digits of `n`, all base `p`.
 -/
sub_one_mul_padicValNat_choose_eq_sub_sum_digits : ∀ {p k n : ℕ} [hp : Fact (Nat.Prime p)],
  k ≤ n → (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinForm.toQuadraticMap_isOrtho : ∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsCancelAdd R]
  [NoZeroDivisors R] [CharZero R] {B : LinearMap.BilinMap R M R} {x y : M},
  LinearMap.IsSymm B → (B.toQuadraticMap.IsOrtho x y ↔ (B x) y = 0)
-- Lean.Data.SMap
/-- Local constants defined in the current module.  -/
Lean.SMap.map₂ : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → Lean.PHashMap α β
-- Lean.Util.CollectAxioms
/-- Look up pre-computed axioms for an imported declaration.  -/
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState.find? : Lean.ExportedAxiomsState✝ → Lean.Environment → Lean.Name → Option (Array Lean.Name)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
IsOpen.exists_contMDiff_support_eq_aux : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] {n : ℕ∞} {s : Set H},
  IsOpen s → ∃ f, Function.support f = s ∧ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Icc_eq_integral_Ico' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X},
  μ {y} = 0 → ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instFullHomologicalComplexQuotient : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι), (HomotopyCategory.quotient V c).Full
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.isPullback_opens_inf_le : ∀ {X : AlgebraicGeometry.Scheme} {U V W : X.Opens} (hU : U ≤ W) (hV : V ≤ W),
  CategoryTheory.IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.tensor_edge : ∀ {X Y : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y'), (e₁.tensor e₂).edge = (e₁.edge, e₂.edge)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_foldr_sup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} (l : List (L.BoundedFormula α n))
  (v : α → M) (xs : Fin n → M), (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.toList_eq_toListModel : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β}, m.toList = Std.DHashMap.Internal.toListModel m.buckets
-- Mathlib.Probability.Moments.CovarianceBilinDual
/-- Continuous linear map from the dual to `Lp` equal to `MemLp.toLp` if `MemLp id p μ`
and to 0 otherwise.  -/
StrongDual.toLp : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {mE : MeasurableSpace E} →
      {𝕜 : Type u_2} →
        [inst_1 : RCLike 𝕜] →
          [inst_2 : NormedSpace 𝕜 E] →
            [OpensMeasurableSpace E] →
              (μ : MeasureTheory.Measure E) →
                (p : ENNReal) → [inst_4 : Fact (1 ≤ p)] → StrongDual 𝕜 E →L[𝕜] ↥(MeasureTheory.Lp 𝕜 p μ)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.beq_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : BEq β] [LawfulBEq β],
  m₁.WF → m₂.WF → (Std.DTreeMap.Raw.Const.beq m₁ m₂ = true ↔ m₁.Equiv m₂)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_mul_succ_eq : ∀ (n k : ℕ), n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse_bijective : ∀ {T : Type u_1} {N : Type u_2}, Function.Bijective ContextFreeRule.reverse
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.inv : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [inst : Inv β],
  Filter.EventuallyConst f l → Filter.EventuallyConst f⁻¹ l
-- Mathlib.Algebra.Group.Submonoid.Units
/-- A Galois coinsertion exists between the coercion from an additive subgroup of
additive units to an additive submonoid and the reduction from an additive submonoid to its unit
group.  -/
ofAddUnits_addUnits_gci : {M : Type u_1} → [inst : AddMonoid M] → GaloisCoinsertion AddSubgroup.ofAddUnits AddSubmonoid.addUnits
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_alter_of_not_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ k' ∈ t)
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_tsum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ : ProbabilityTheory.Kernel α β) [inst_1 : ProbabilityTheory.IsSFiniteKernel κ] {f : ι → α → β → ENNReal},
  (∀ (i : ι), Measurable (Function.uncurry (f i))) →
    κ.withDensity (∑' (n : ι), f n) = ProbabilityTheory.Kernel.sum fun n => κ.withDensity (f n)
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] [hG : IsAddCommutative G], AddSubgroup.center G = ⊤