mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- Auxiliary calculation for `mul_antipode`.

```
       |
       n
      /  \
     |   n
     |  / \
     |  S S
     |  \ /
     n   /
    / \ / \
    |  /  |
    \ / \ /
     v   v
     |   |
```

We move the leftmost multiplication up, so we can reassociate.
We then move the rightmost comultiplication under the strand,
and simplify using `antipode_right`.
 -/
CategoryTheory.HopfObj.mul_antipode₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
            (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)
                  A).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv A)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A) A)
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ A A).hom)
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HopfObj.antipode
                            CategoryTheory.HopfObj.antipode))
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.MonObj.mul)
                          CategoryTheory.MonObj.mul)))))))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        CategoryTheory.MonObj.one)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `lid_comp_map_assoc` that only fires when `g ≠ id`.  -/
CoassocSimps.lid_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation is a map that uniformly scales the edistance between any two points.  -/
Dilation : (α : Type u_1) → (β : Type u_2) → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.extendHom`.

---

There is a morphism from an extended cone to the original cone.  -/
CategoryTheory.Limits.Cones.extend : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) → {X : C} → (f : X ⟶ s.pt) → s.extend f ⟶ s
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeSRestrict_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  Function.Surjective ⇑f.rangeSRestrict
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.neg_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Neg (R i)] [inst_2 : ∀ (i : ι), NegMemClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (-x) i = -x i
-- Init.Data.Array.Lemmas
/-- Variant of `all_flatMap` with a side condition for the `stop` argument.  -/
Array.all_flatMap' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {xs : Array α} {f : α → Array β} {p : β → Bool},
  stop = (Array.flatMap f xs).size → (Array.flatMap f xs).all p 0 stop = xs.all fun a => (f a).all p
-- Mathlib.Order.SuccPred.Archimedean
Pred.rec_linear : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {p : α → Prop},
  (∀ (a : α), p a ↔ p (Order.pred a)) → ∀ (a b : α), p a ↔ p b
-- Mathlib.Order.Concept
Concept.isLowerSet_extent_lt : ∀ {α : Type u_6} [inst : PartialOrder α] (c : Concept α α fun x1 x2 => x1 < x2), IsLowerSet c.extent
-- Lean.Elab.Command
Lean.Elab.Command.CommandElabM : Type → Type
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.PreDiscrTree.modifyAt : {α : Type} →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
    Lean.Meta.RefinedDiscrTree.Key →
      (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α) → Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)) →
        Lean.Meta.RefinedDiscrTree.PreDiscrTree α
-- Init.Data.Array.Lemmas
Array.reflBEq_iff : ∀ {α : Type u_1} [inst : BEq α], ReflBEq (Array α) ↔ ReflBEq α
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. The number of elements in the heap.  -/
Batteries.BinomialHeap.size : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → ℕ
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.forkOfKernelFork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.KernelFork (f - g)), (CategoryTheory.Preadditive.forkOfKernelFork c).pt = c.pt
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_bisim_tail : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : List.Vector α n}
  {ys : List.Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ} {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂},
  (∃ R,
      R s₁ s₂ ∧
        ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) →
    (List.Vector.mapAccumr₂ f₁ xs ys s₁).2 = (List.Vector.mapAccumr₂ f₂ xs ys s₂).2
-- Mathlib.CategoryTheory.Category.Quiv
/-- The functor `free : Quiv ⥤ Cat` preserves composition up to natural isomorphism and in fact up
to equality.  -/
CategoryTheory.Cat.freeMapCompIso : {V₁ : Type u₁} →
  {V₂ : Type u₂} →
    {V₃ : Type u₃} →
      [inst : Quiver V₁] →
        [inst_1 : Quiver V₂] →
          [inst_2 : Quiver V₃] →
            (F : V₁ ⥤q V₂) →
              (G : V₂ ⥤q V₃) →
                CategoryTheory.Cat.freeMap (F ⋙q G) ≅ (CategoryTheory.Cat.freeMap F).comp (CategoryTheory.Cat.freeMap G)
-- Mathlib.Topology.Constructions.SumProd
/-- `(X × Y) × Z` is homeomorphic to `X × (Y × Z)`.  -/
Homeomorph.prodAssoc : (X : Type u) →
  (Y : Type v) →
    (Z : Type u_2) →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → (X × Y) × Z ≃ₜ X × Y × Z
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  (NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates K) ⟦a⟧ =
    ⟦NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a⟧
-- Mathlib.Order.SupIndep
sSupIndep_pair : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, a ≠ b → (sSupIndep {a, b} ↔ Disjoint a b)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingProd_cons : ∀ {G : Type u_7} [inst : CommGroup G] (a : G) (l : List G), (a :: l).alternatingProd = a / l.alternatingProd
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Given a theorem with proof `proof` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the pattern.
 -/
Lean.Meta.Grind.mkEMatchEqTheoremCore : Lean.Meta.Grind.Origin →
  Array Lean.Name → Lean.Expr → Bool → Bool → Bool → optParam Bool false → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A natural isomorphism `T ≅ T'` induces an equivalence
`StructuredArrow S T ≌ StructuredArrow S T'`.  -/
CategoryTheory.StructuredArrow.mapNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T T' : CategoryTheory.Functor C D} →
            (T ≅ T') → (CategoryTheory.StructuredArrow S T ≌ CategoryTheory.StructuredArrow S T')
-- Lean.Compiler.IR.Basic
Lean.IR.mkIndexSet : Lean.IR.Index → Lean.IR.IndexSet
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P.unop
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    ((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- Eta-expanded form of `MeasureTheory.IntegrableOn.sub` -/
MeasureTheory.IntegrableOn.fun_sub : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f g : α → E},
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ → MeasureTheory.IntegrableOn (fun i => f i - g i) s μ
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.containsThenInsert_fst_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α}
  {b : β a}, (m.containsThenInsert a b).1 = (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).1
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? Int16
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `|a|`.  -/
Mathlib.Meta.Positivity.evalAbs : Mathlib.Meta.Positivity.PositivityExt
-- Lean.Server.Utils
_private.Lean.Server.Utils.0.Lean.Server.externalNameToUri? : Lean.Name → Option Lean.Lsp.DocumentUri
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
/-- The right adjoint to the subdivision functor on simplicial sets.  -/
SSet.ex : CategoryTheory.Functor SSet SSet
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.Etale g],
  AlgebraicGeometry.Etale (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.neg_eq_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, -a = ⊤ ↔ a = ⊤
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.mk.injEq : ∀ {G : Type u_6} [inst : AddGroup G] (toAddGroupSeminorm : AddGroupSeminorm G)
  (eq_zero_of_map_eq_zero' : ∀ (x : G), toAddGroupSeminorm.toFun x = 0 → x = 0)
  (toAddGroupSeminorm_1 : AddGroupSeminorm G)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : G), toAddGroupSeminorm_1.toFun x = 0 → x = 0),
  ({ toAddGroupSeminorm := toAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }) =
    (toAddGroupSeminorm = toAddGroupSeminorm_1)
-- Mathlib.CategoryTheory.Pi.Basic
/-- An isomorphism between `I`-indexed objects gives an isomorphism between each
pair of corresponding components.  -/
CategoryTheory.Pi.isoApp : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → {X Y : (i : I) → C i} → (X ≅ Y) → (i : I) → X i ≅ Y i
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Consider a manifold in which the tangent spaces are already endowed with an inner product, and
the space is already endowed with an extended distance. We say that this is a Riemannian manifold
if the distance is given by the infimum of the lengths of `C^1` paths, measured using the norm in
the tangent spaces.

This is a `Prop`-valued typeclass, on top of existing data.

If you need to *construct* a distance using a Riemannian structure,
see `EMetricSpace.ofRiemannianMetric`.  -/
IsRiemannianManifold : {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] →
                [PseudoEMetricSpace M] →
                  [inst_5 : ChartedSpace H M] → [Bundle.RiemannianBundle fun x => TangentSpace I x] → Prop
-- Mathlib.Data.Fin.Basic
Fin.prop : ∀ {n : ℕ} (a : Fin n), ↑a < n
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Module.Basis.constrL_apply : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] {ι : Type u_2} [inst_12 : Fintype ι]
  (v : Module.Basis ι 𝕜 E) (f : ι → F) (e : E), (v.constrL f) e = ∑ i, v.equivFun e i • f i
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_strictAnti : StrictAnti Inv.inv
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ico_ae_eq_Ioc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α},
  μ {a} = 0 → μ {b} = 0 → Set.Ico a b =ᵐ[μ] Set.Ioc a b
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_ne_zero : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ}, 0 < p → ∀ {f : Polynomial R}, (Polynomial.expand R p) f ≠ 0 ↔ f ≠ 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Recursion principle for `Multiseries basis_hd basis_tl`. It is equivalent to
`Stream'.Seq.recOn` but provides some convenience.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.recOn : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    {motive : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Sort u_1} →
      (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
        motive Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil →
          ((exp : ℝ) →
              (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) →
                (tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
                  motive (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl)) →
            motive ms
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- A copy of `Finsupp.lsingle` for `MonoidAlgebra`.  -/
MonoidAlgebra.lsingle : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} → [inst : Semiring S] → [inst_1 : Semiring R] → [inst_2 : Module R S] → M → S →ₗ[R] MonoidAlgebra S M
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.hasNext.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.hasNext = decide (i.byteIdx < s.rawEndPos.byteIdx)
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- Composition of an additive group seminorm with an additive monoid homomorphism as
an additive group seminorm.  -/
AddGroupSeminorm.comp : {E : Type u_3} →
  {F : Type u_4} → [inst : AddGroup E] → [inst_1 : AddGroup F] → AddGroupSeminorm E → (F →+ E) → AddGroupSeminorm F
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  [inst_8 : (F.comp G).Monoidal] (X Y : C) {Z : E}
  (h : G.obj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X Y) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldl_eq_foldl_toArray : ∀ {α : Type u} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : δ → α → β → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldl f init t =
    Array.foldl (fun a b => f a b.1 b.2) init (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Std.Async.DNS
Std.Async.DNS.NameInfo.mk : String → String → Std.Async.DNS.NameInfo
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
a monoid homomorphism from `Mᵐᵒᵖ`.  -/
MonoidHom.fromOpposite : {M : Type u_3} →
  {N : Type u_4} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (f : M →* N) → (∀ (x y : M), Commute (f x) (f y)) → Mᵐᵒᵖ →* N
-- Mathlib.Algebra.Group.Action.Units
AddUnits.vaddCommClass_left : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} [inst : AddMonoid M] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddCommClass M N α], VAddCommClass (AddUnits M) N α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.continuousOn_tan_Ioo : ContinuousOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.isIntegral_coe : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.RingOfIntegers K),
  IsIntegral ℤ ((algebraMap (NumberField.RingOfIntegers K) K) x)
-- Lean.Elab.Quotation
/-- Pattern agrees with head check, remove and transform remaining alternative.
If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch.  -/
Lean.Elab.Term.Quotation.MatchResult.covered : (Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt) →
  Bool → Lean.Elab.Term.Quotation.MatchResult
-- Mathlib.Order.RelSeries
RelSeries.fromListIsChain_toFun : ∀ {α : Type u_1} {r : SetRel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x)
  (i : Fin (x.length - 1 + 1)), (RelSeries.fromListIsChain x x_ne_nil hx).toFun i = x[Fin.cast ⋯ i]
-- Mathlib.Order.Partition.Equipartition
Finpartition.indiscrete_isEquipartition : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) {hs : s ≠ ∅}, (Finpartition.indiscrete hs).IsEquipartition
-- Mathlib.LinearAlgebra.CliffordAlgebra.Star
CliffordAlgebra.star_def : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q), star x = CliffordAlgebra.reverse (CliffordAlgebra.involute x)
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.rotateL.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → α → Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : α) →
        (x_2 : Ordnode α) →
          ((l : Ordnode α) →
              (x : α) →
                (size : ℕ) → (m : Ordnode α) → (y : α) → (r : Ordnode α) → motive l x (Ordnode.node size m y r)) →
            ((l : Ordnode α) → (x : α) → motive l x Ordnode.nil) → motive x x_1 x_2
-- Aesop.Search.Expansion
Aesop.RuleResult.succeeded : Array Aesop.RappRef → Aesop.RuleResult
-- Mathlib.Data.ENNReal.Basic
ENNReal.instSub : Sub ENNReal
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis.eq_1 : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι], b.dualBasis = b.map b.toDualEquiv
-- Init.Data.Range.Polymorphic.Iterators
Std.Roo.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [DecidableLT α] [inst_3 : LT α]
  [inst_4 : DecidableLT α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {r : Std.Roo α} {a : α},
  (Std.Roo.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_none_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey? = none ↔ t = ∅
-- Mathlib.Algebra.Ring.Associator
/-- An a priori non-associative ring is associative iff the `AddMonoidHom` version of the
associator vanishes.  -/
AddMonoidHom.associator_eq_zero_iff_associative : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], AddMonoidHom.associator = 0 ↔ Std.Associative fun x y => x * y
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getEntry! : {α : Type u} →
  {β : α → Type v} → [BEq α] → α → [Inhabited ((a : α) × β a)] → Std.DHashMap.Internal.AssocList α β → (a : α) × β a
-- Mathlib.Topology.Closure
monotone_closure : ∀ (X : Type u_1) [inst : TopologicalSpace X], Monotone closure
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.card_algEquiv_extension : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n], Fintype.card Gal(FiniteField.Extension k p n/k) = n
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le : ∀ {α : Type u} {β : Type v} {c : Cardinal.{max u v}} (f : α → β),
  (∀ (b : β), Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' {b})) ≤ c) →
    Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) * c
-- Init.Data.UInt.Lemmas
UInt16.toUSize_mod_65536 : ∀ (n : UInt16), n.toUSize % 65536 = n.toUSize
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.hasLeftDerivedFunctor_of_hasPointwiseLeftDerivedFunctor : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (W : CategoryTheory.MorphismProperty C) [F.HasPointwiseLeftDerivedFunctor W],
  F.HasLeftDerivedFunctor W