mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_eq_lift : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p],
  CategoryTheory.Limits.biproduct.fromSubtype f p =
    CategoryTheory.Limits.biproduct.lift fun j =>
      if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0
-- Mathlib.Tactic.DeriveCountable
/-- Encode a `Countable` type into the natural numbers using the witness produced by
`Countable.exists_injective_nat`. Used internally by the `Countable` deriving handler.  -/
Mathlib.Deriving.Countable.encode : {α : Sort u_1} → [Countable α] → α → ℕ
-- Mathlib.Data.Int.Bitwise
/-- `m <<< n` produces an integer whose binary representation
is obtained by left-shifting the binary representation of `m` by `n` places  -/
Int.instShiftLeft_mathlib : ShiftLeft ℤ
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.Basis.toCentralizer.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis),
  a.toCentralizer = { toFun := fun τ => ⟨a.ofPermHom τ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- The map on objects underlying the Yoneda embedding. It sends an object `x` to
the pseudofunctor defined by:
* Objects: `a ↦ (a ⟶ x)`
* Higher morphisms get sent to the corresponding "precomposing" operation.

This is only used for defining `yoneda`, after which `Bicategory.yoneda.obj` should be preferred.  -/
CategoryTheory.Bicategory.yoneda₀ : {B : Type u} → [inst : CategoryTheory.Bicategory B] → B → CategoryTheory.Pseudofunctor Bᵒᵖ CategoryTheory.Cat
-- Lean.Data.Options
Lean.Options.instEmptyCollection : EmptyCollection Lean.Options
-- Mathlib.Order.UpperLower.Closure
gc_upperClosure_coe : ∀ {α : Type u_1} [inst : Preorder α],
  GaloisConnection (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} (h : F = G), (CategoryTheory.eqToHom h).toNatTrans = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.Nat.Cast.Basic
ext_nat : ∀ {R : Type u_3} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : FunLike F ℕ R] [RingHomClass F ℕ R] (f g : F),
  f = g
-- Mathlib.Analysis.CStarAlgebra.Basic
StarSubalgebra.to_cstarRing : ∀ {R : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : NormedRing A] [inst_3 : StarRing A]
  [CStarRing A] [inst_5 : Algebra R A] [inst_6 : StarModule R A] (S : StarSubalgebra R A), CStarRing ↥S
-- Mathlib.Analysis.Convex.BetweenList
List.wbtw_pair : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), List.Wbtw R [p₁, p₂]
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)),
  (I.ofPiForkFunctor hd).obj a = CategoryTheory.Limits.Multifork.ofPiFork a
-- Lean.Elab.PreDefinition.Structural.FindRecArg
_private.Lean.Elab.PreDefinition.Structural.FindRecArg.0.Lean.Elab.Structural.allCombinations.go : {α : Type u_1} → Array (Array α) → ℕ → Array α → Array (Array α)
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instAddAction : {G : Type u_1} → {α : Type u_3} → {β : Type u_4} → [inst : AddGroup G] → [AddAction G β] → AddAction G (α ↪ β)
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_eq_univ_sdiff : ∀ {α : Type u_1} (s : Set α), sᶜ = Set.univ \ s
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- The bounded linear map of considering a bounded continuous function on a finite-measure space
as an element of `Lp`.  -/
BoundedContinuousFunction.toLp : {α : Type u_1} →
  {E : Type u_2} →
    {m0 : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : TopologicalSpace α] →
            [BorelSpace α] →
              [inst_2 : NormedAddCommGroup E] →
                [SecondCountableTopologyEither α E] →
                  [MeasureTheory.IsFiniteMeasure μ] →
                    (𝕜 : Type u_3) →
                      [inst_5 : Fact (1 ≤ p)] →
                        [inst_6 : NormedRing 𝕜] →
                          [inst_7 : Module 𝕜 E] →
                            [inst_8 : IsBoundedSMul 𝕜 E] → BoundedContinuousFunction α E →L[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Init.Data.List.Basic
List.length.eq_2 : ∀ {α : Type u_1} (head : α) (tail : List α), (head :: tail).length = tail.length + 1
-- Mathlib.Order.Defs.LinearOrder
compare_gt_iff_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, compare a b = Ordering.gt ↔ b < a
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_add_symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C}
  (n m a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'')
  (x :
    Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶
      (CategoryTheory.shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)),
  (CategoryTheory.ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm x =
    (CategoryTheory.ShiftedHom.opEquiv' m a' a'' ha'').symm
      (Quiver.Hom.op
        ((CategoryTheory.ShiftedHom.opEquiv' n a a' ha').symm
          (CategoryTheory.CategoryStruct.comp x ((CategoryTheory.shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)))))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jmp.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {fvarId_1 : Lean.FVarId} {args_1 : Array (Lean.Compiler.LCNF.Arg pu)},
  Lean.Compiler.LCNF.Code.jmp fvarId args = Lean.Compiler.LCNF.Code.jmp fvarId_1 args_1 →
    fvarId = fvarId_1 ∧ args = args_1
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_comp_map : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn),
  SemidirectProduct.rightHom.comp (SemidirectProduct.map fn fg h) = fg.comp SemidirectProduct.rightHom
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier_subset_intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, intrinsicFrontier 𝕜 s ⊆ intrinsicClosure 𝕜 s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.unitOfList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α},
  Std.TreeMap.unitOfList (hd :: tl) cmp = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
-- Init.Data.Array.Lemmas
Array.filter_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {g : α → Array β} {f : β → Bool},
  Array.filter f (Array.flatMap g xs) = Array.flatMap (fun a => Array.filter f (g a)) xs
-- Init.Data.List.Perm
List.Perm.flatten : ∀ {α : Type u_1} {l₁ l₂ : List (List α)}, l₁.Perm l₂ → l₁.flatten.Perm l₂.flatten
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.maxDiff : String → String → Array (Lean.Diff.Action × String)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- UV-compressing `a` means removing `v` from it and adding `u` if `a` and `u` are disjoint and
`v ≤ a` (it replaces the `v` part of `a` by the `u` part). Else, UV-compressing `a` doesn't do
anything. This is most useful when `u` and `v` are disjoint finsets of the same size.  -/
UV.compress : {α : Type u_1} → [inst : GeneralizedBooleanAlgebra α] → [DecidableRel Disjoint] → [DecidableLE α] → α → α → α → α
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.instNeg : Neg Float.Model.UnpackedFloat.Sign
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.reindex_refl : ∀ {ι : 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)],
  PiTensorProduct.reindex R s (Equiv.refl ι) = LinearEquiv.refl R (PiTensorProduct R fun i => s i)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- [Stacks Tag 00EC](https://stacks.math.columbia.edu/tag/00EC) -/
PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem : ∀ {R : Type u} [inst : CommRing R] (e : R),
  IsIdempotentElem e → ↑(PrimeSpectrum.basicOpen e) = PrimeSpectrum.zeroLocus {1 - e}
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_mul_natCast : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ) (n : ℕ), x ^ (y * ↑n) = (x ^ y) ^ n
-- Mathlib.Analysis.Seminorm
Seminorm.smul_closedBall_preimage : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜),
  a ≠ 0 → (fun x => a • x) ⁻¹' p.closedBall y r = p.closedBall (a⁻¹ • y) (r / ‖a‖)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxBraidedMonMapMon.eq_1 : ∀ {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} [inst_4 : CategoryTheory.SymmetricCategory C]
  [inst_5 : CategoryTheory.SymmetricCategory D] [inst_6 : F.LaxBraided],
  CategoryTheory.Functor.instLaxBraidedMonMapMon = { toLaxMonoidal := F.instLaxMonoidalMonMapMon, braided := ⋯ }
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ico_add_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (a : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ico (a + ↑n) (a + ↑n + 1))
-- Mathlib.GroupTheory.Finiteness
Group.FG.out : ∀ {G : Type u_3} {inst : Group G} [self : Group.FG G], ⊤.FG
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The localized tensor product, as a bifunctor.  -/
CategoryTheory.Localization.Monoidal.tensorBifunctor : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.Functor (CategoryTheory.LocalizedMonoidal L W ε)
                        (CategoryTheory.Functor (CategoryTheory.LocalizedMonoidal L W ε)
                          (CategoryTheory.LocalizedMonoidal L W ε))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {f g : M₁ ⟶ M₂}, f = g ↔ ∀ (X : Cᵒᵖ), f.app X = g.app X
-- Mathlib.RingTheory.Noetherian.Basic
Module.IsNoetherian.finite : ∀ (R : Type u_1) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M],
  Module.Finite R M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β k}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert! k v t) = true},
  (Std.DTreeMap.Internal.Impl.insert! k v t).getKey a h₁ = if h₂ : compare k a = Ordering.eq then k else t.getKey a ⋯
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprCutsatConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.CutsatConfig
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesColimits_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sSupHomClass F α β], CategoryTheory.Limits.PreservesColimits (↑f).toFunctor
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.mk : {α : Type u_7} →
  (MeasurableSet' : Set α → Prop) →
    MeasurableSet' ∅ →
      (∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ) →
        (∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)) → MeasurableSpace α
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_one : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1], ⇑1 = id
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.mem_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} {h : ↥K}, h ∈ H.addSubgroupOf K ↔ ↑h ∈ H
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.smallHomMap'_comp : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {X Y Z : C₁}
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ Y Z]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Z] {X' Y' Z' : C₂}
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' X']
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ Y' Y']
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ Z' Z']
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' Y']
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ Y' Z']
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' Z'] (eX : Φ.functor.obj X ≅ X')
  (eY : Φ.functor.obj Y ≅ Y') (eZ : Φ.functor.obj Z ≅ Z') (f : CategoryTheory.Localization.SmallHom W₁ X Y)
  (g : CategoryTheory.Localization.SmallHom W₁ Y Z),
  Φ.smallHomMap' eX eZ (f.comp g) = (Φ.smallHomMap' eX eY f).comp (Φ.smallHomMap' eY eZ g)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.getUElimPos? : List Lean.Level → Lean.Level → Lean.MetaM (Option ℕ)
-- Mathlib.Geometry.Manifold.DerivationBundle
instCommRingPointedContMDiffMap : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_2) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → (n : WithTop ℕ∞) → (x : M) → CommRing (PointedContMDiffMap 𝕜 I M n x)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
CovariantDerivative.derivMetricTensor.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov cov_1 : CovariantDerivative I F V),
  cov = cov_1 →
    ∀ [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
      [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F] (x : M),
      cov.derivMetricTensor x = cov_1.derivMetricTensor x
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.ensureNoMinIndexable : Bool → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.tensorObj.inv_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : C} [inst_3 : CategoryTheory.GrpObj G]
  [inst_4 : CategoryTheory.GrpObj H],
  CategoryTheory.GrpObj.inv =
    CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv
-- Mathlib.Order.Filter.Map
Filter.seq_mem_seq : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {s : Set (α → β)} {t : Set α},
  s ∈ f → t ∈ g → s.seq t ∈ f.seq g
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality_assoc : ∀ {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] {d d' : D} (f : d ⟶ d') {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d' ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d').inv h)
-- Mathlib.Algebra.Order.Pi
/-- The product of a family of ordered commutative monoids is an ordered commutative monoid.  -/
Pi.isOrderedMonoid : ∀ {ι : Type u_6} {Z : ι → Type u_7} [inst : (i : ι) → CommMonoid (Z i)] [inst_1 : (i : ι) → Preorder (Z i)]
  [∀ (i : ι), IsOrderedMonoid (Z i)], IsOrderedMonoid ((i : ι) → Z i)
-- Aesop.Script.OptimizeSyntax
_private.Aesop.Script.OptimizeSyntax.0.Aesop.optimizeInitialRenameI.tacsToTacticSeq : {m : Type → Type} →
  [Monad m] → [Lean.MonadQuotation m] → Array (Lean.TSyntax `tactic) → m (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
-- Mathlib.Algebra.Order.Field.Basic
Mathlib.Meta.Positivity.zpow_zero_pos : ∀ {α : Type u_5} [inst : Semifield α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (a : α), 0 < a ^ 0
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_eq_truncTotal_sum_subst_truncTotal_of_le : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {x : σ → ℕ} {k : ℕ},
  MvPowerSeries.HasSubst a →
    (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
      (∀ (i : σ), k ≤ x i) →
        (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
          (MvPowerSeries.truncTotal k)
            (∑ i ∈ Finset.range k,
              MvPowerSeries.subst (fun i => ↑((MvPowerSeries.truncTotal (x i)) (a i)))
                ((MvPowerSeries.homogeneousComponent i) f))
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Build the `rw` discrimination tree?  -/
Mathlib.Tactic.ClickSuggestions.Choice.rw : Mathlib.Tactic.ClickSuggestions.Choice → Bool
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesOfIsCycle₁_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (x : G →₀ A) (hx : groupHomology.IsCycle₁ x),
  ↑(groupHomology.cyclesOfIsCycle₁ x hx) = x
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- An open subset of a charted space is naturally a charted space.  -/
TopologicalSpace.Opens.instChartedSpace : {H : Type u} →
  {M : Type u_2} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → (s : TopologicalSpace.Opens M) → ChartedSpace H ↥s
-- Lean.Meta.Basic
Lean.Meta.map1MetaM : {m : Type → Type u_1} →
  {β : Sort u_2} →
    [MonadControlT Lean.MetaM m] →
      [Monad m] → ({α : Type} → (β → Lean.MetaM α) → Lean.MetaM α) → {α : Type} → (β → m α) → m α
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_comp_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (a : E),
  DifferentiableWithinAt 𝕜 (fun x => f (a + x)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastShiftLeft : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ArbitraryShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft
-- Mathlib.LinearAlgebra.Dual.Basis
/-- Maps a basis for `V` to a basis for the dual space.  -/
Module.Basis.dualBasis : {R : Type uR} →
  {M : Type uM} →
    {ι : Type uι} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [DecidableEq ι] → Module.Basis ι R M → [Finite ι] → Module.Basis ι R (Module.Dual R M)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toIsOrderedMonoid : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α], IsOrderedMonoid α
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
RingCat.moduleCatRestrictScalarsPseudofunctor_obj : ∀ (b : CategoryTheory.LocallyDiscrete RingCatᵒᵖ),
  RingCat.moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as))
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.eq_4 : ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize✝ ByteArray.utf8DecodeChar?.FirstByte.twoMore = 3
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.eq_zero_of_mem_of_neg_mem' : ∀ {R : Type u_1} [inst : Ring R] (self : RingCone R) {a : R}, a ∈ self.carrier → -a ∈ self.carrier → a = 0
-- Init.Data.SInt.Basic
instLEISize : LE ISize
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommGroup.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : IsTopologicalGroup G],
  SeparationQuotient.instCommGroup = { toGroup := SeparationQuotient.instGroup, mul_comm := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
LinearOrderedRing.orderOf_le_two : ∀ {G : Type u_1} [inst : Ring G] [inst_1 : LinearOrder G] [IsStrictOrderedRing G] {x : G}, orderOf x ≤ 2
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.mk.sizeOf_spec : ∀ {A : Type u_6} {B : Type u_7} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] [inst_4 : SizeOf A]
  [inst_5 : SizeOf B] (toMulEquiv : A ≃* B)
  (map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)),
  sizeOf { toMulEquiv := toMulEquiv, map_star' := map_star' } = 1 + sizeOf toMulEquiv
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F],
  IsClosed (Set.range ContinuousAlternatingMap.toContinuousMultilinearMap)