mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomRight : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f],
  CategoryTheory.inv (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f) =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x (CategoryTheory.inv f)
-- Aesop.Stats.File
Aesop.instToJsonStatsFileRecord : Lean.ToJson Aesop.StatsFileRecord
-- Mathlib.Topology.MetricSpace.Holder
Set.Subsingleton.holderOnWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {s : Set X},
  s.Subsingleton → ∀ (C r : NNReal) (f : X → Y), HolderOnWith C r f s
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDerivAux_le_one : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel η],
  κ ≤ η → ∀ {a : α}, κ.rnDerivAux η a ≤ᵐ[η a] 1
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- If `h` commutes with `f⁺ g` and `t` is another left Kan extension of `g` along `f`, then
`t.whisker h` is a left Kan extension of `g ≫ h` along `f`.  -/
CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            (t : CategoryTheory.Bicategory.LeftExtension f g) →
              t.IsKan → {x : B} → (h : c ⟶ x) → [CategoryTheory.Bicategory.Lan.CommuteWith f g h] → (t.whisker h).IsKan
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- We collect an integer part `b = ⌊v⌋` and fractional part `fr = v - ⌊v⌋` of a value `v` in a pair
`⟨b, fr⟩`.
 -/
GenContFract.IntFractPair : Type u_1 → Type u_1
-- Mathlib.Algebra.Group.Units.Hom
/-- If two homomorphism from an additive group to an additive monoid are equal at `x`,
then they are equal at `-x`.  -/
eq_on_neg : ∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : FunLike F G M]
  [AddMonoidHomClass F G M] (f g : F) {x : G}, f x = g x → f (-x) = g (-x)
-- Mathlib.Algebra.MonoidAlgebra.Opposite
/-- The opposite of a monoid algebra is equivalent as a ring to the opposite monoid algebra over the
opposite ring.  -/
AddMonoidAlgebra.opRingEquiv : {R : Type u_1} →
  {M : Type u_2} → [inst : Semiring R] → [inst_1 : Add M] → (AddMonoidAlgebra R M)ᵐᵒᵖ ≃+* AddMonoidAlgebra Rᵐᵒᵖ Mᵃᵒᵖ
-- Batteries.Data.List.Basic
/-- Right-biased version of `List.zipWith`. `zipWithRight f as bs` applies `f` to each
pair `aᵢ ∈ as` and `bᵢ ‌∈ bs`. If `as` is shorter than `bs`, `f` is applied to
`none` for the remaining `bᵢ`.
```
zipWithRight prod.mk [1, 2] ['a'] = [(some 1, 'a')]
zipWithRight prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipWithRight f as bs = (zipWithRight' f as bs).fst
```
 -/
List.zipWithRight : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (Option α → β → γ) → List α → List β → List γ
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposing₂_obj_naturality_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) {a_1 b_1 : Bᵒᵖ} (g : a_1 ⟶ b_1)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_1 ⟶ a))),
  (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).naturality g).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop X f).inv
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a
compact subset. See also `MeasurableSet.exists_isCompact_lt_add` and
`MeasurableSet.exists_lt_isCompact_of_ne_top`.  -/
MeasurableSet.exists_isCompact_sdiff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [OpensMeasurableSpace α] [T2Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₄_eq_some_iff_utf8EncodeChar_eq : ∀ {w x y z : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.threeMore ∧
      ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c ↔
    String.utf8EncodeChar c = [w, x, y, z]
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.whiskerLeft_η_commutator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G CategoryTheory.MonObj.one)
      (CategoryTheory.GrpObj.commutator G) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj G (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
      CategoryTheory.MonObj.one
-- Init.Data.Int.Lemmas
Int.sub_right_inj : ∀ {i j : ℤ} (k : ℤ), k - i = k - j ↔ i = j
-- Mathlib.Algebra.Order.Ring.Abs
abs_mul_abs_self : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a : α), |a| * |a| = a * a
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_expand : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α]
  {buckets : { d // 0 < d.size }},
  (Std.DHashMap.Internal.toListModel ↑(Std.DHashMap.Internal.Raw₀.expand buckets)).Perm
    (Std.DHashMap.Internal.toListModel ↑buckets)
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.of_vComp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : 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_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  [R₁.EssSurj] [w.GuitartExact] [(w.vComp w').GuitartExact], w'.GuitartExact
-- Mathlib.Computability.ContextFreeGrammar
/-- Add extra postfix to context-free deriving.  -/
ContextFreeGrammar.Derives.append_right : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
  g.Derives v w → ∀ (p : List (Symbol T g.NT)), g.Derives (v ++ p) (w ++ p)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the right commutative square of a morphism in `ShortComplex`  -/
CategoryTheory.ShortComplex.Hom.comm₂₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂) {Z : C} (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.τ₂ (CategoryTheory.CategoryStruct.comp S₂.g h) =
    CategoryTheory.CategoryStruct.comp S₁.g (CategoryTheory.CategoryStruct.comp self.τ₃ h)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- If `f` and `g` are homotopic relative to a pre-path object `P`, then `g` and `f`
are homotopic relative to `P.symm`  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} →
      {P : HomotopicalAlgebra.PrepathObject Y} →
        {X : C} → {f g : X ⟶ Y} → P.RightHomotopy f g → P.symm.RightHomotopy g f
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.isNontrivial_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation R Γ₀} {v' : Valuation R Γ'₀},
  v.IsEquiv v' → (v.IsNontrivial ↔ v'.IsNontrivial)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.le_ker_iff_comp_subtype_eq_zero : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂}, N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.add_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {x y : PreLp E} {i : α},
  (x + y) i = x i + y i
-- Mathlib.Util.TermReduce
/-- `delta% t` elaborates to a head-delta reduced version of `t`.  -/
Mathlib.Util.TermReduce.deltaStx : Lean.ParserDescr
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- A FinCategory `α` is equivalent to a category with objects in `Type`.  -/
CategoryTheory.FinCategory.ObjAsType : (α : Type u_1) → [Fintype α] → Type
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol of `p` and `a` is zero iff `p ∣ a`.  -/
legendreSym.eq_zero_iff : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ℤ), legendreSym p a = 0 ↔ ↑a = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F]
  (a : A),
  CategoryTheory.CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a))
      ((L.rightKanExtensionCounit (F.comp G)).app a) =
    G.map ((L.rightKanExtensionCounit F).app a)
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.erase : ∀ {α : Type u_1} [inst : LE α] {s : Set α} {a : α}, IsUpperSet s → (∀ b ∈ s, b ≤ a → b = a) → IsUpperSet (s \ {a})
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
_private.Mathlib.GroupTheory.SpecificGroups.Cyclic.0.card_addOrderOf_eq_totient_aux₁ : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | n • a = 0}.card ≤ n) →
    ∀ {d : ℕ}, d ∣ Fintype.card α → 0 < {a | addOrderOf a = d}.card → {a | addOrderOf a = d}.card = d.totient
-- Mathlib.Data.ENNReal.Basic
ENNReal.iSup_ennreal : ∀ {α : Type u_2} [inst : CompleteLattice α] {f : ENNReal → α}, ⨆ n, f n = (⨆ n, f ↑n) ⊔ f ⊤
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- A presheaf `F` of types is (strongly) a sheaf for a pre-`1`-hypercover if `F` is a sheaf for
both the `0` and the `1`-components.
This implies that the multiequalizer diagram attached to `E` is exact
(see `CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork`).
 -/
CategoryTheory.PreOneHypercover.IsStronglySheafFor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : C} → CategoryTheory.PreOneHypercover X → CategoryTheory.Functor Cᵒᵖ (Type u_3) → Prop
-- Mathlib.Data.Finset.Functor
Finset.map_traverse : ∀ {α β γ : Type u} {G : Type u → Type u} [inst : Applicative G] [inst_1 : CommApplicative G] (g : α → G β) (h : β → γ)
  (s : Finset α), Functor.map h <$> Finset.traverse g s = Finset.traverse (Functor.map h ∘ g) s
-- Mathlib.Dynamics.Transitive
/-- An action of a monoid `M` on `α` is topologically transitive if and only if for any nonempty
open subset `U` of `α` the union over the elements of `M` of images of `U` is dense in `α`.  -/
MulAction.isTopologicallyTransitive_iff_dense_iUnion : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α],
  MulAction.IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, m • U)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_X_add_C : ∀ {S : Type v} [inst : Semiring S] (r : S), (Polynomial.X + Polynomial.C r).leadingCoeff = 1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans'_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ)
  (h : e.target = e'.source), (e.trans' e' h).source = e.source
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
isometry_cfcHom : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : MetricSpace A] [inst_8 : Algebra R A] [inst_9 : IsometricContinuousFunctionalCalculus R A p] (a : A)
  (ha : autoParam (p a) isometry_cfcHom._auto_1), Isometry ⇑(cfcHom ⋯)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instAddGroupCarrierToAddGrp.eq_1 : ∀ (G : FiniteAddGrp.{u_1}), G.instAddGroupCarrierToAddGrp = G.toAddGrp.str
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mrevertPat.quot : Lean.ParserDescr
-- Mathlib.Data.NNReal.Basic
NNReal.sub_div : ∀ (a b c : NNReal), (a - b) / c = a / c - b / c
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_bot : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n], RingCon.matrix n ⊥ = ⊥
-- Mathlib.Tactic.Simps.Basic
/-- Syntax for making a projection default in `initialize_simps_projections`.  -/
Lean.Parser.Command.simpsRule.add : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
instContMDiffVectorBundleOfTopWithTopENat : ∀ {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
  [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  {a : WithTop ℕ∞} [ContMDiffVectorBundle ⊤ F E IB], ContMDiffVectorBundle a F E IB
-- Mathlib.Data.Seq.Parallel
Computation.parallel_congr_right : ∀ {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α},
  (∀ t ∈ T, t.Promises a) →
    Stream'.WSeq.LiftRel Computation.Equiv S T → (Computation.parallel S).Equiv (Computation.parallel T)
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_inv_le : ∀ {r : NNReal}, ↑r⁻¹ ≤ (↑r)⁻¹
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  (f : E →SL[σ] F) (hsurj : (↑f).range = ⊤), 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  hζ.integralPowerBasisOfPrimePow.dim = (p ^ k).totient
-- Mathlib.Algebra.Order.Group.Cone
AddGroupConeClass.eq_zero_of_mem_of_neg_mem : ∀ {S : Type u_1} {G : outParam (Type u_2)} {inst : AddCommGroup G} {inst_1 : SetLike S G} [self : AddGroupConeClass S G]
  {C : S} {a : G}, a ∈ C → -a ∈ C → a = 0
-- Mathlib.GroupTheory.GroupExtension.Defs
MulAut.conjNormal.congr_simp : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal], MulAut.conjNormal = MulAut.conjNormal
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (n : ℕ),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.ofOpSequence (CategoryTheory.Limits.SequentialProduct.functorMap f)).map
        (CategoryTheory.homOfLE ⋯).op)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) n)
        (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => if x : i < n + 1 then M i else N i) n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f n))
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.pairwise_div_notMem_range : ∀ {ι : Type u_1} {G : Type u_3} [inst : CommGroup G] [inst_1 : InvolutiveInv ι] (v : ι → G),
  (∀ (i : ι), v i ≠ 1) →
    (∀ (i : ι), v i⁻¹ = (v i)⁻¹) →
      ∀ (s t : Set ι),
        s ⊆ {i | IsMulIndecomposable v t i} →
          (∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t) → s.Pairwise fun i j => v i / v j ∉ Set.range v
-- Mathlib.Order.Defs.PartialOrder
Decidable.le_iff_lt_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} [DecidableLE α], a ≤ b ↔ a < b ∨ a = b
-- Init.Data.Array.Lex.Lemmas
List.lex_toArray : ∀ {α : Type u_1} [inst : BEq α] {lt : α → α → Bool} {l₁ l₂ : List α}, l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_eval_zero : ∀ (R : Type u) [inst : Ring R] {n : ℕ}, Polynomial.eval 0 (descPochhammer R n) = if n = 0 then 1 else 0
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionData.mk.injEq : ∀ (name : Lean.Name) (expr : Lean.Expr) (projNrs : List ℕ) (isDefault isPrefix : Bool) (name_1 : Lean.Name)
  (expr_1 : Lean.Expr) (projNrs_1 : List ℕ) (isDefault_1 isPrefix_1 : Bool),
  ({ name := name, expr := expr, projNrs := projNrs, isDefault := isDefault, isPrefix := isPrefix } =
      { name := name_1, expr := expr_1, projNrs := projNrs_1, isDefault := isDefault_1, isPrefix := isPrefix_1 }) =
    (name = name_1 ∧ expr = expr_1 ∧ projNrs = projNrs_1 ∧ isDefault = isDefault_1 ∧ isPrefix = isPrefix_1)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.done : Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Order.Partition.Finpartition
/-- Construct a `Finpartition s` from a finset of finsets `parts` such that each element of `s` is in
exactly one member of `parts`. This provides a converse to `Finpartition.subset`,
`Finpartition.not_empty_mem_parts` and `Finpartition.existsUnique_mem`.
 -/
Finpartition.ofExistsUnique : {α : Type u_1} →
  [inst : DecidableEq α] →
    {s : Finset α} →
      (parts : Finset (Finset α)) →
        (∀ p ∈ parts, p ⊆ s) → (∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t) → ∅ ∉ parts → Finpartition s
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.eraseIdx.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        ((x : ℕ) → motive [] x) →
          ((head : α) → (as : List α) → motive (head :: as) 0) →
            ((a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ) → motive x x_1
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsLT_inv : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iio a⁻¹)) (nhdsWithin a (Set.Ioi a))
-- Mathlib.Topology.Category.Profinite.Product
Profinite.IndexFunctor.map_comp_π_app : ∀ {ι : Type u} {X : ι → Type} [inst : (i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J K : ι → Prop}
  (h : ∀ (i : ι), J i → K i),
  ⇑(Profinite.IndexFunctor.map C h) ∘ ⇑(Profinite.IndexFunctor.π_app C K) = ⇑(Profinite.IndexFunctor.π_app C J)
-- Init.Data.UInt.Bitwise
UInt32.toBitVec_shiftRight : ∀ (a b : UInt32), (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 32)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Tensor product of algebras analogue of `mul_left_comm`.

This is the algebra version of `TensorProduct.leftComm`.  -/
Algebra.TensorProduct.leftComm : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (C : Type uC) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Semiring C] →
                    [inst_6 : Algebra R C] →
                      TensorProduct R A (TensorProduct R B C) ≃ₐ[R] TensorProduct R B (TensorProduct R A C)
-- Mathlib.Topology.ContinuousMap.StarOrdered
/-- `sqrt (a, b)` returns a value `s` such that `b = a + s * s` when `a ≤ b`.  -/
ContinuousSqrt.sqrt : {R : Type u_1} →
  {inst : LE R} → {inst_1 : NonUnitalSemiring R} → {inst_2 : TopologicalSpace R} → [self : ContinuousSqrt R] → R × R → R
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
/-- A map `f` is conformal if it's conformal at every point.  -/
Conformal : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : NormedAddCommGroup X] →
      [inst_1 : NormedAddCommGroup Y] → [NormedSpace ℝ X] → [NormedSpace ℝ Y] → (X → Y) → Prop
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mapsTo_vadd_orbit : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  Set.MapsTo (fun x => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
ContinuousLinearEquiv.integrable_comp_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜' E]
  [inst_5 : NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomIsometric σ] [RingHomIsometric σ']
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {φ : α → H} (L : H ≃SL[σ] E),
  MeasureTheory.Integrable (fun a => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) {K₂ L₂ : CochainComplex C₂ ℤ} (f₂ : K₂ ⟶ L₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F]
  [inst_9 : K₁.HasMapBifunctor L₂ F],
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁)
        ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).map f₂) F (ComplexShape.up ℤ))
      (K₁.mapBifunctorShift₂Iso L₂ F y).hom =
    CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₂Iso K₂ F y).hom
      ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
        (HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) f₂ F (ComplexShape.up ℤ)))
-- Mathlib.Algebra.Group.Defs
NegZeroClass.toZero : {G : Type u_2} → [self : NegZeroClass G] → Zero G