mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} {x y : D₁.Hom D₂}, x = y ↔ x.hom = y.hom
-- Mathlib.Combinatorics.Enumerative.Bell
/-- Number of partitions of a set of cardinality `m.sum`
whose parts have cardinalities given by `m`  -/
Multiset.bell : Multiset ℕ → ℕ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.Scheme.Hom.ker I.subschemeι = I
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveElabStep1 : Inhabited Lean.Elab.Command.InductiveElabStep1
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
/-- Conditionally complete partial orders (with suprema and infima) are partial orders
where every nonempty, directed set which is bounded above (respectively, below) has a
least upper (respectively, greatest lower) bound.  -/
ConditionallyCompletePartialOrder : Type u_3 → Type u_3
-- Mathlib.RepresentationTheory.Character
/-- Orthogonality of characters for irreducible representations of finite group over an
algebraically closed field whose characteristic doesn't divide the order of the group.  -/
FDRep.char_orthonormal : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] [IsAlgClosed k] [inst_3 : Fintype G]
  [Invertible ↑(Nat.card G)] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W],
  (↑(Nat.card G))⁻¹ * ∑ g, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then 1 else 0
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.instInhabited : Inhabited TopCommRingCat
-- Mathlib.Algebra.Algebra.Hom
RingHom.toIntAlgHom_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S], Function.Injective RingHom.toIntAlgHom
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- Cast between "equal" tensor powers.  -/
TensorPower.cast : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {i j : ℕ} → i = j → TensorPower R i M ≃ₗ[R] TensorPower R j M
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g),
  s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι g
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.isWF_support : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R), x.support.IsWF
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- `AddAction.period m a` is definitionally equal to
`Function.minimalPeriod (m +ᵥ ·) a`  -/
AddAction.period_eq_minimalPeriod : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α},
  AddAction.period m a = Function.minimalPeriod (fun x => m +ᵥ x) a
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
MonoidAlgebra.comul_def : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A],
  CoalgebraStruct.comul =
    TensorProduct.map ↑(MonoidAlgebra.coeffLinearEquiv R).symm ↑(MonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ
      CoalgebraStruct.comul ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv R)
-- Mathlib.Algebra.Group.Basic
sub_eq_sub_iff_add_eq_add : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c d : G}, a - b = c - d ↔ a + d = c + b
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.zero_vadd_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] (X : C) [inst_3 : CategoryTheory.AddModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero X)
      CategoryTheory.AddModObj.vadd =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Init.Grind.ToInt
/-- The embedding into the integers takes negation to negation, wrapped into the range interval.
 -/
Lean.Grind.ToInt.Neg : (α : Type u) → [Neg α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the index, counting from the left,
of an element equivalent to `x` if it exists.

```
findIndex 2 {1, 2, 4} = some 1
findIndex 4 {1, 2, 4} = some 2
findIndex 5 {1, 2, 4} = none
```  -/
Ordnode.findIndex : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Option ℕ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termK : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- To prove a property of a product, it suffices to prove that
the property is multiplicative and holds on factors.  -/
Finset.prod_induction : ∀ {ι : Type u_1} {s : Finset ι} {M : Type u_7} [inst : CommMonoid M] (f : ι → M) (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a * b)) → p 1 → (∀ x ∈ s, p (f x)) → p (∏ x ∈ s, f x)
-- Mathlib.Algebra.GradedMonoid
/-- The `Monoid` structure derived from `GMonoid A`.  -/
GradedMonoid.GradeZero.monoid : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddMonoid ι] → [GradedMonoid.GMonoid A] → Monoid (A 0)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.min_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {p q : (a : α) × β a},
  p ⊓ q = if (compare p.fst q.fst).isLE = true then p else q
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.get_ofFn.go : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n) (lb ub : ℕ) (h1 : lb < ub) (h2 : ub ≤ n),
  lb ≤ ↑i → ↑i < ub → (Lean.RArray.ofFn.go✝ f lb ub h1 h2).get ↑i = f i
-- Mathlib.CategoryTheory.Grothendieck
/-- Let `G` be an equivalence of categories. The functor induced via `pre` by `G.functor ⋙ G.inverse`
is naturally isomorphic to the functor induced via `map` by a whiskered version of `G`'s inverse
unit.
 -/
CategoryTheory.Grothendieck.preUnitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C CategoryTheory.Cat) →
          (G : D ≌ C) →
            CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight G.unitInv (G.functor.comp F)) ≅
              CategoryTheory.Grothendieck.pre (G.functor.comp F) (G.functor.comp G.inverse)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (t.insert k).min! = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Order.Concept
upperPolar_lowerPolar_monotone : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop), Monotone (upperPolar r ∘ lowerPolar r)
-- Mathlib.ModelTheory.PartialEquiv
/-- **Alias** of the forward direction of `FirstOrder.Language.isExtensionPair_iff_cod`. -/
FirstOrder.Language.IsExtensionPair.cod : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.IsExtensionPair M N → ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_eq_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) {x y : M × ↥S},
  (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
-- Mathlib.Topology.Order.LiminfLimsup
/-- Assume that, for any `a < b`, a sequence cannot be infinitely many times below `a` and
above `b`. If it is also ultimately bounded above and below, then it has to converge. This even
works if `a` and `b` are restricted to a dense subset.
 -/
tendsto_of_no_upcrossings : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [DenselyOrdered α] {f : Filter β} {u : β → α} {s : Set α},
  Dense s →
    (∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)) →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) tendsto_of_no_upcrossings._auto_1 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) tendsto_of_no_upcrossings._auto_3 →
          ∃ c, Filter.Tendsto u f (nhds c)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_34 : HSub Std.Time.Day.Offset Std.Time.Hour.Offset Std.Time.Hour.Offset
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are
negations of each other, then the oriented angles are negations of each other (even in degenerate
cases).  -/
Orientation.oangle_eq_neg_of_angle_eq_of_sign_eq_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {w x y z : V},
  InnerProductGeometry.angle w x = InnerProductGeometry.angle y z →
    (o.oangle w x).sign = -(o.oangle y z).sign → o.oangle w x = -o.oangle y z
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.source_inter_preimage_target_inter : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β),
  e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_4 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_4 id c pivot rupHints ratHints
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsIntegral Y] [Subsingleton ↥Y],
  AlgebraicGeometry.UniversallyOpen f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.MapsTo.div : ∀ {α : Type u_2} {β : Type u_3} [inst : Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  Set.MapsTo f₁ A B₁ → Set.MapsTo f₂ A B₂ → Set.MapsTo (f₁ / f₂) A (B₁ / B₂)
-- Init.Data.Float.Float
/-- Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not
reflexive since `NaN != NaN`, and it is not a congruence because `0.0 == -0.0`, but
`1.0 / 0.0 != 1.0 / -0.0`.

This function does not reduce in the kernel. It is compiled to the C equality operator.
 -/
Float.beq : Float → Float → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.swap_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y),
  s.swap.fst = s.snd
-- Mathlib.Data.Finset.Insert
Finset.mem_cons : ∀ {α : Type u_1} {s : Finset α} {a b : α} {h : a ∉ s}, b ∈ Finset.cons a s h ↔ b = a ∨ b ∈ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → m.size = m_1.size
-- Mathlib.Topology.MetricSpace.Bounded
Metric.ediam_univ_of_noncompact : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α] [NoncompactSpace α], Metric.ediam Set.univ = ⊤
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.map_ε_comp_counit_app_unit : ∀ {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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.LaxMonoidal.ε G))
      (adj.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) =
    CategoryTheory.Functor.OplaxMonoidal.η F
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] (toEmbedding : M ↪ N)
  (map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEmbedding.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEmbedding.toFun ∘ x))
      FirstOrder.Language.Embedding.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEmbedding.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Embedding.map_rel'._autoParam),
  sizeOf { toEmbedding := toEmbedding, map_fun' := map_fun', map_rel' := map_rel' } = 1 + sizeOf toEmbedding
-- Mathlib.GroupTheory.Congruence.Basic
Con.prod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (c : Con M) (d : Con N),
  c.prod d = { toSetoid := c.prod d.toSetoid, mul' := ⋯ }
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      Ordnode.BalancedSz l.size r.size → s = l.size + r.size + 1 → Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.mul` -/
MeasureTheory.StronglyMeasurable.fun_mul : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Mul β]
  [ContinuousMul β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i * g i
-- Mathlib.Data.Num.Basic
/-- The successor of a `Num` as a `PosNum`.  -/
Num.succ' : Num → PosNum
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
differentiableAt_const_cpow_of_neZero : ∀ (z : ℂ) [NeZero z] (t : ℂ), DifferentiableAt ℂ (fun s => z ^ s) t
-- Init.Data.Queue
/-- The dequeue list, which buffers elements ready to be dequeued
(with the head being the next item to be yielded by `dequeue?`).  -/
Std.Queue.dList : {α : Type u} → Std.Queue α → List α
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- For each `i : Fin (n + 1)`, this is a variant of the homotopy relation on
`n`-simplices that are constant on the boundary. Simplices `f` and `g` are related
if they appear respectively as the `i.castSucc` and `i.succ` faces of a
`n + 1`-simplex such that all the other faces are constant.  -/
SSet.PtSimplex.RelStruct : {X : SSet} → {n : ℕ} → {x : X.obj (Opposite.op { len := 0 })} → X.PtSimplex n x → X.PtSimplex n x → Fin (n + 1) → Type u
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.isOpen_ball : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, IsOpen (Euclidean.ball x r)
-- Mathlib.CategoryTheory.Category.ULift
/-- The categorical equivalence between `C` and `ULift C`.  -/
CategoryTheory.ULift.equivalence : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → C ≌ ULift.{u₂, u₁} C
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.fullNames : Lean.Option Bool
-- Mathlib.Algebra.Group.Ext
SubNegMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : SubNegMonoid M⦄, HAdd.hAdd = HAdd.hAdd → Neg.neg = Neg.neg → m₁ = m₂
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (μ : CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPost F)
  (X X_1 X_2 : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap μ).app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj X_1) (F.obj X_2)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) ((μ.app X_1).app X_2))
        ((μ.app X).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 X_2)))
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.summable_norm_sub_zpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L], ∀ n < -↑(Module.finrank ℤ ↥L), ∀ (x : E), Summable fun z => ‖↑z - x‖ ^ n
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.injective_le_monomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  CategoryTheory.MorphismProperty.injective C ≤ CategoryTheory.MorphismProperty.monomorphisms C
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.or_to_or : ∀ (a b : Bool), (a = true ∨ b = true) = ((a || b) = true)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η : F ⟶ G} → Inhabited (CategoryTheory.Oplax.StrongTrans.Modification η η)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α} (k_beq : (k == k') = true) (v : β k),
      List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
        ⟨k, v⟩ ∈ toInsert →
          ∀ {h : Std.Internal.List.containsKey k' (Std.Internal.List.insertList l toInsert) = true},
            Std.Internal.List.getValueCast k' (Std.Internal.List.insertList l toInsert) h = cast ⋯ v
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- `Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.sum_comp` for a version without `h`.  -/
Fintype.sum_bijective : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  (e : ι → κ), Function.Bijective e → ∀ (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∑ x, f x = ∑ x, g x
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.visitedFVars : Lean.Elab.Term.ToDepElimPattern.TopSort.State → Lean.FVarIdSet
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- Let `Eᵢ` and `E'ᵢ` be two families of normed `𝕜`-vector spaces.
Let `f` be a family of continuous `𝕜`-linear maps between `Eᵢ` and `E'ᵢ`, i.e.
`f : Πᵢ Eᵢ →L[𝕜] E'ᵢ`, then there is an induced continuous linear map
`⨂ᵢ Eᵢ → ⨂ᵢ E'ᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`.  -/
PiTensorProduct.mapL : {ι : Type u_1} →
  [inst : Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              {E' : ι → Type u_5} →
                [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] →
                  [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)] →
                    ((i : ι) → E i →L[𝕜] E' i) → (PiTensorProduct 𝕜 fun i => E i) →L[𝕜] PiTensorProduct 𝕜 fun i => E' i
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.trim : ∀ {α : Type u_1} {m : MeasurableSpace α} {H : Type u_8} [inst : NormedAddCommGroup H] {m0 : MeasurableSpace α}
  {μ' : MeasureTheory.Measure α} {f : α → H} (hm : m ≤ m0),
  MeasureTheory.Integrable f μ' → MeasureTheory.StronglyMeasurable f → MeasureTheory.Integrable f (μ'.trim hm)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateIsShared! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.Nat.Set
Nat.range_casesOn : ∀ {α : Type u_2} (x : α) (f : ℕ → α), (Set.range fun n => Nat.casesOn n x f) = {x} ∪ Set.range f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_gcd : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (a b : ℤ)
  (p₁ p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.eq_gcd_cert a b p₁ p₂ p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Init.Data.Stream
_private.Init.Data.Stream.0.Std.Stream.forIn.visit : {ρ : Type u_1} →
  {α : Type u_2} →
    {m : Type u_3 → Type u_4} → {β : Type u_3} → [Std.Stream ρ α] → [Monad m] → (α → β → m (ForInStep β)) → ρ → β → m β
-- Mathlib.LinearAlgebra.Finsupp.Span
Submodule.mem_sSup_iff_exists_finset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Set (Submodule R M)} {m : M}, m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
-- Mathlib.Order.Monotone.Defs
strictMono_of_le_iff_le : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ (x y : α), x ≤ y ↔ f x ≤ f y) → StrictMono f
-- Mathlib.Probability.Distributions.Gamma
/-- The pdf of the gamma distribution, as a function valued in `ℝ≥0∞`  -/
ProbabilityTheory.gammaPDF : ℝ → ℝ → ℝ → ENNReal
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.NatIso.pi_inv : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] {F G : (i : I) → CategoryTheory.Functor (C i) (D i)}
  (e : (i : I) → F i ≅ G i), (CategoryTheory.NatIso.pi e).inv = CategoryTheory.NatTrans.pi fun i => (e i).inv