mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Semiconj.Units
AddSemiconjBy.addUnits_zsmul_right : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M},
  AddSemiconjBy a ↑x ↑y → ∀ (m : ℤ), AddSemiconjBy a ↑(m • x) ↑(m • y)
-- Mathlib.Analysis.Calculus.Deriv.Inv
hasDerivAt_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, x ≠ 0 → HasDerivAt (fun y => y⁻¹) (-(x ^ 2)⁻¹) x
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.IsDiscrete.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  autoParam (∀ (X Y : C), Subsingleton (X ⟶ Y)) CategoryTheory.IsDiscrete.subsingleton._autoParam →
    (∀ {X Y : C} (f : X ⟶ Y), X = Y) → CategoryTheory.IsDiscrete C
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensor_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_one_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : One γ], Sum.elim 1 1 = 1
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.

`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.find?` always terminates after finitely many steps.

Examples:
* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 5) = pure (some 1)`
* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 1) = pure none`
 -/
Std.IterM.find? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → (β → Bool) → m (Option β)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.unop_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g) (X_1 : CategoryTheory.Limits.WalkingCospan),
  c.unop.π.app X_1 =
    CategoryTheory.CategoryStruct.comp (c.ι.app X_1).unop
      (match X_1 with
          | none => CategoryTheory.Iso.refl X
          | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl Y
          | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl Z).inv.unop
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_add_zero : ∀ (a : Ordinal.{u_1}), Ordinal.nfp (fun x => a + x) 0 = a * Ordinal.omega0
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.bot_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (i : C), ⊥.obj i = ⊥
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.instRespectsLeftOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms],
  (CategoryTheory.MorphismProperty.ofObjectProperty P Q).RespectsLeft (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.CategoryTheory.Presentable.Basic
/-- A category has `κ`-filtered colimits if it has colimits of shape `J`
for any `κ`-filtered category `J`.  -/
CategoryTheory.HasCardinalFilteredColimits : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_eq_top_or_isMaximal_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S],
  Function.Surjective ⇑f → ∀ {I : Ideal R}, I.IsMaximal → Ideal.map f I = ⊤ ∨ (Ideal.map f I).IsMaximal
-- Init.Data.BitVec.Lemmas
BitVec.udiv_one : ∀ {w : ℕ} {x : BitVec w}, x / 1#w = x
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict.comm_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {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'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) (i j : ι) {Z : C} (h : L.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.homRestrict.f ψ i)
      (CategoryTheory.CategoryStruct.comp (L.d i j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (K.d (e.f i) (e.f j)) (ComplexShape.Embedding.homRestrict.f ψ j)) h
-- Mathlib.GroupTheory.Index
AddSubgroup.add_mem_iff_of_index_two : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 → ∀ {a b : G}, a + b ∈ H ↔ (a ∈ H ↔ b ∈ H)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableAdd₂.measurable_add : ∀ {M : Type u_2} {inst : MeasurableSpace M} {inst_1 : Add M} [self : MeasurableAdd₂ M], Measurable fun p => p.1 + p.2
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.isQuotientMap_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M), Topology.IsQuotientMap ⇑S.mkQ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {f : α → β → Bool} {k : α},
  (Std.ExtHashMap.filter f m)[k]! = (m[k]?.pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.Order.Hom.WithTopBot
SupHom.withTop.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : SupHom α β),
  f.withTop = { toFun := WithTop.map ⇑f, map_sup' := ⋯ }
-- Init.Omega.IntList
Lean.Omega.IntList.neg_get : ∀ (xs : Lean.Omega.IntList) (i : ℕ), (-xs).get i = -xs.get i
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f) =
    CategoryTheory.ChosenPullbacksAlong.pullbackMap R.hom T.hom R.hom S.hom (CategoryTheory.CategoryStruct.id R.left)
      (CategoryTheory.Over.Hom.left f) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodalWeight_ne_zero : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Set.InjOn v ↑s → i ∈ s → Lagrange.nodalWeight s v i ≠ 0
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_fin_surjective : ∀ (R : Type u_3) {n m : ℕ} [inst : CommRing R], m ≤ n → Function.Surjective ⇑(MvPolynomial.esymmAlgHom (Fin m) R n)
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the fourth quadrant. Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable in the open fourth quadrant and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open fourth
  quadrant for some `A`, `B`, and `c < 2`;
* `f` is equal to `g` on the boundary of the fourth quadrant.

Then `f` is equal to `g` on the closed fourth quadrant.  -/
PhragmenLindelof.eqOn_quadrant_IV : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
  DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Iio 0) →
        (∃ c < 2,
            ∃ B,
              g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
          (∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x) →
            (∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | 0 ≤ z.re ∧ z.im ≤ 0}
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.depth : Aesop.ExtResult → ℕ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instFaithfulMonForget₂Mon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.AddGrp.forget₂Mon C).Faithful
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcWireFormat.refFieldName : Lean.Lsp.RpcWireFormat → String
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_eq_of_dvd_dvd : ∀ {m n : ℤ}, m ∣ n → n ∣ m → m.natAbs = n.natAbs
-- Mathlib.RingTheory.Nilpotent.Defs
pos_nilpotencyClass_iff : ∀ {R : Type u_1} {x : R} [inst : MonoidWithZero R] [Nontrivial R], 0 < nilpotencyClass x ↔ IsNilpotent x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_eq_zero_of_irreducible_of_natDegree_ne_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  Irreducible p → p.natDegree ≠ 1 → p.roots = 0
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.brecOn.eq : ∀ {motive : Mathlib.Deriving.Encodable.S✝ → Sort u} (t : Mathlib.Deriving.Encodable.S✝)
  (F_1 : (t : Mathlib.Deriving.Encodable.S✝) → Mathlib.Deriving.Encodable.S.below✝ t → motive t),
  Mathlib.Deriving.Encodable.S.brecOn✝ t F_1 = F_1 t (Mathlib.Deriving.Encodable.S.brecOn.go✝ t F_1).2
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a sieve `S` on `X : C`, its associated cocone `S.cocone` is defined to be
the natural cocone over the diagram defined above with cocone point `X`.  -/
CategoryTheory.Presieve.cocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Presieve X) → CategoryTheory.Limits.Cocone S.diagram
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.coe_comp : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  [inst_4 : Monoid C] [inst_5 : Star C] (f : B →⋆* C) (g : A →⋆* B), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesLimitsOfShape_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sInfHomClass F α β] {J : Type w} [inst_4 : CategoryTheory.Category.{w', w} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (↑f).toFunctor
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.op_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y), φ.op.f = φ.f.op
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the reverse direction of `SimpleGraph.neighborSet_eq_compl_singleton`. -/
SimpleGraph.IsUniversal.neighborSet_eq : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, G.IsUniversal v → G.neighborSet v = {v}ᶜ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α}, m.getKey! a = m.getKeyD a default
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {Y : AlgebraicGeometry.Scheme}
  (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i),
  𝒰.glueMorphismsOfLocallyDirected g h = AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 g ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.map.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {G : Type u_7} [inst_4 : NormedAddCommGroup G]
  [inst_5 : InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G),
  b.map L = { repr := L.symm.trans b.repr }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.TreeMap.Raw.ofList l cmp)[k]? = none
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_toInt : ∀ (x : Int16), Int16.ofIntLE x.toInt ⋯ ⋯ = x
-- Mathlib.RingTheory.FractionalIdeal.Basic
IsFractional.sup : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : Submodule R P}, IsFractional S I → IsFractional S J → IsFractional S (I ⊔ J)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α σ : Type u} {x : StateT σ m α} {h : ε → StateT σ m α}
  [inst : Std.Do.WP m ps] [inst_1 : Monad m] [inst_2 : MonadExceptOf ε m]
  (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)),
  ⦃fun s => (Std.Do.wp (MonadExceptOf.tryCatch (x.run s) fun e => (h e).run s)).apply (fun xs => Q.1 xs.1 xs.2, Q.2)⦄
    MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.mk : {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₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁)) →
                  autoParam
                      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
                        CategoryTheory.CategoryStruct.comp (adj X₁).unit
                            (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
                          CategoryTheory.CategoryStruct.comp (adj Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op)))
                      CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map._autoParam →
                    (F ⊣₂ G)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g)
  {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (F.map g) (self.app b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
      (CategoryTheory.CategoryStruct.comp (self.naturality g).hom h)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.noConfusionType : Sort v✝ → FirstOrder.Field.FieldAxiom → FirstOrder.Field.FieldAxiom → Sort v✝
-- Init.Control.State
/-- Adds a mutable state of type `σ` to a monad.

Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
of a value and a state.
 -/
StateT : Type u → (Type u → Type v) → Type u → Type (max u v)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.neg_nat_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℕ), Function.Periodic f (-(↑n * c))
-- Aesop.BuiltinRules.DestructProducts
Aesop.BuiltinRules.destructProducts : Aesop.RuleTac
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.limMap_π_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_4 : CategoryTheory.ConcreteCategory C F_1]
  (x : carrier (CategoryTheory.Limits.limit F)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π G j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limMap α)) x) =
    (CategoryTheory.ConcreteCategory.hom (α.app j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_single : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {N : Type u_10}
  [inst_2 : IsStrictOrderedRing R] (x : M) (f : M → N),
  Convexity.StdSimplex.map f (Convexity.StdSimplex.single x) = Convexity.StdSimplex.single (f x)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.pos_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => max (f x) 0) p μ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_map_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₂ = f.f j
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldlM_eq_foldlM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.DTreeMap.foldlM f init t = List.foldlM (fun a b => f a b.1 b.2) init (Std.DTreeMap.Const.toList t)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.ins.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (t : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.root, t with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_1 t
-- Mathlib.Probability.ProductMeasure
MeasureTheory.lintegral_infinitePi_of_piFinset : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : DecidableEq ι] {s : Finset ι}
  {f : ((i : ι) → X i) → ENNReal},
  Measurable f →
    ∀ (x : (i : ι) → X i), ∫⁻ (y : (i : ι) → X i), f y ∂MeasureTheory.Measure.infinitePi μ = (∫⋯∫⁻_s, f ∂μ) x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.csinh : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => Complex.sinh (f x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isLE₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C),
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n : ℤ), t.IsLE T.obj₁ n → t.IsLE T.obj₃ n → t.IsLE T.obj₂ n
-- Mathlib.Analysis.Convex.Gauge
gauge_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 ≤ r → ∀ (x : E), gauge (Metric.closedBall 0 r) x = ‖x‖ / r
-- Mathlib.Order.Lattice.Congruence
LatticeCon.mk.injEq : ∀ {α : Type u_2} [inst : Lattice α] (toSetoid : Setoid α)
  (inf : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊓ y) (x ⊓ z))
  (sup : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊔ y) (x ⊔ z)) (toSetoid_1 : Setoid α)
  (inf_1 : ∀ {w x y z : α}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w ⊓ y) (x ⊓ z))
  (sup_1 : ∀ {w x y z : α}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w ⊔ y) (x ⊔ z)),
  ({ toSetoid := toSetoid, inf := inf, sup := sup } = { toSetoid := toSetoid_1, inf := inf_1, sup := sup_1 }) =
    (toSetoid = toSetoid_1)
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.convMul_comp_bialgHom_distrib : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Semiring C] [inst_4 : Bialgebra R C] [inst_5 : Algebra R A]
  [inst_6 : Bialgebra R B] (f g : WithConv (C →ₐ[R] A)) (h : B →ₐc[R] C),
  (f * g).ofConv.comp ↑h = (WithConv.toConv (f.ofConv.comp ↑h) * WithConv.toConv (g.ofConv.comp ↑h)).ofConv
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄}
  (f :
    (i₁ : ι₁) →
      (i₂ : ι₂) →
        (i₃ : ι₃) →
          c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A))
  (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h_1 : A ⟶ Z), ⋯ = ⋯