mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourierLp.congr_simp : ∀ {d : Type u_1} [inst : Fintype d] (p : ENNReal) [inst_1 : Fact (1 ≤ p)] (n n_1 : d → ℤ),
  n = n_1 → UnitAddTorus.mFourierLp p n = UnitAddTorus.mFourierLp p n_1
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integrableExpSet_fun_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, ProbabilityTheory.integrableExpSet (fun x => x) (ProbabilityTheory.gaussianReal μ v) = Set.univ
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_pow : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : ↥H) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.ext : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] {s t : ContMDiffSection I F n V},
  (∀ (x : M), s x = t x) → s = t
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom_assoc : ∀ {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] (t : CategoryTheory.Limits.Cone F) (w : F ≅ G) {Z : C}
  (h : CategoryTheory.Limits.limit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F t)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cone.postcompose w.hom).obj t)) h
-- Mathlib.Topology.Constructions
Topology.IsClosedEmbedding.uliftDown : ∀ {X : Type u} [inst : TopologicalSpace X], Topology.IsClosedEmbedding ULift.down
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instIsOrderedAddMonoid : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β],
  IsOrderedAddMonoid (CompactlySupportedContinuousMap α β)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.right_id.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : SizeOf J],
  sizeOf CategoryTheory.BiconeHom.right_id = 1
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The zero of the ring  -/
Zsqrtd.instZero : {d : ℤ} → Zero (ℤ√d)
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.getProofWithFreshMVarLevels : {α : Type} → [Lean.Meta.Grind.TheoremLike α] → α → Lean.MetaM Lean.Expr
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommGroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : CommGroup Y],
  LocallyConstant.instCommGroup = Function.Injective.commGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltRHS : Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y}
  {h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ X},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) W)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B Z W).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B h)
          (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Z W).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp h g))
        (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.eval_eq : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinPred.eq.eval = fun x1 x2 => x1 == x2
-- Mathlib.Algebra.Homology.Homotopy
CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive]
  (h : HomotopyEquiv C D), (F.mapHomotopyEquiv h).homotopyHomInvId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyHomInvId))
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.mem_of : ∀ {α : Type u_1} {c : Std.Sat.CNF.Clause α} {v : α} {p : Bool}, (v, p) ∈ c → Std.Sat.CNF.Clause.Mem v c
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_smul : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) {n : ℕ},
  a ∈ I → hI.dpow n (b • a) = b ^ n • hI.dpow n a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.maxD fallback ∈ t
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} {E : CategoryTheory.PreOneHypercover S} (P : CategoryTheory.Functor Cᵒᵖ A)
  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c)
  (d : CategoryTheory.Limits.Multifork (E.multicospanIndex P)),
  (CategoryTheory.PreOneHypercover.Hom.id E).mapMultiforkOfIsLimit P hc d =
    CategoryTheory.Limits.Multifork.IsLimit.lift hc d.ι ⋯
-- Mathlib.Analysis.RCLike.Basic
/-- Conjugation as a ring equivalence. This is used to convert the inner product into a
sesquilinear product.  -/
RCLike.conjToRingEquiv : (K : Type u_1) → [inst : RCLike K] → K ≃+* Kᵐᵒᵖ
-- Mathlib.RingTheory.Ideal.Cotangent
/-- In a Noetherian local ring,
the dimension of the cotangent space is equal to the span rank of the maximal ideal.
 -/
IsLocalRing.rank_cotangentSpace_eq_spanrank_maximalIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  Module.rank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) =
    Submodule.spanRank (IsLocalRing.maximalIdeal R)
-- Lean.Elab.MutualDef
Lean.Elab.DefViewElabHeader.mk.injEq : ∀ (toDefView : Lean.Elab.DefView) (toDefViewElabHeaderData : Lean.Elab.DefViewElabHeaderData)
  (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot))
  (bodySnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot)))
  (toDefView_1 : Lean.Elab.DefView) (toDefViewElabHeaderData_1 : Lean.Elab.DefViewElabHeaderData)
  (tacSnap?_1 : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot))
  (bodySnap?_1 : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot))),
  ({ toDefView := toDefView, toDefViewElabHeaderData := toDefViewElabHeaderData, tacSnap? := tacSnap?,
        bodySnap? := bodySnap? } =
      { toDefView := toDefView_1, toDefViewElabHeaderData := toDefViewElabHeaderData_1, tacSnap? := tacSnap?_1,
        bodySnap? := bodySnap?_1 }) =
    (toDefView = toDefView_1 ∧
      toDefViewElabHeaderData = toDefViewElabHeaderData_1 ∧ tacSnap? = tacSnap?_1 ∧ bodySnap? = bodySnap?_1)
-- Batteries.Data.AssocList
Batteries.AssocList.eraseP.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool),
  Batteries.AssocList.eraseP p Batteries.AssocList.nil = Batteries.AssocList.nil
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, we can construct a biproduct for `f : J → C` from
any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
 -/
CategoryTheory.Limits.isBilimitOfTotal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {J : Type u_1} →
        [inst_2 : Fintype J] →
          {f : J → C} →
            (b : CategoryTheory.Limits.Bicone f) →
              ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt →
                b.IsBilimit
-- Lean.Parser.Command
/-- `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions.  -/
Lean.Parser.Command.declModifiersT : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- The sieve of morphisms which factor through a morphism in a given family.
This is equal to `Sieve.generate (Presieve.ofArrows X π)`, but has
more convenient definitional properties.
 -/
CategoryTheory.Sieve.generateFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {B : C} → {α : Type u_1} → (X : α → C) → ((a : α) → X a ⟶ B) → CategoryTheory.Sieve B
-- Mathlib.CategoryTheory.Preadditive.Opposite
/-- `op` induces morphisms of monoids on hom groups of a preadditive category  -/
CategoryTheory.opHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (X Y : C) → (X ⟶ Y) →+ (Opposite.op Y ⟶ Opposite.op X)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment.eq_3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.hasNegAssignment = true
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The space of continuous affine maps between topological vector spaces is linearly isomorphic to
the product of the codomain with the space of linear maps, by taking the value of the affine map at
`(0 : V)` and the linear part.  -/
ContinuousAffineMap.decompLinearEquiv : (R : Type u_1) →
  (S : Type u_2) →
    (V : Type u_3) →
      (W : Type u_4) →
        [inst : Ring S] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module R V] →
                [inst_4 : TopologicalSpace V] →
                  [IsTopologicalAddGroup V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : Module R W] →
                        [inst_8 : TopologicalSpace W] →
                          [inst_9 : Module S W] →
                            [inst_10 : SMulCommClass R S W] →
                              [inst_11 : ContinuousConstSMul S W] →
                                [inst_12 : IsTopologicalAddGroup W] → (V →ᴬ[R] W) ≃ₗ[S] W × (V →L[R] W)
-- Mathlib.Combinatorics.Hall.Finite
HallMarriageTheorem.hall_cond_of_erase : ∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [inst_1 : Fintype ι] {x : ι} (a : α),
  (∀ (s : Finset ι), s.Nonempty → s ≠ Finset.univ → s.card < (s.biUnion t).card) →
    ∀ (s' : Finset ↑{x' | x' ≠ x}), s'.card ≤ (s'.biUnion fun x' => (t ↑x').erase a).card
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
tsum_comp_le_tsum_of_inj : ∀ {α : Type u_1} {β : Type u_4} {f : α → ℝ},
  Summable f → (∀ (a : α), 0 ≤ f a) → ∀ {i : β → α}, Function.Injective i → tsum (f ∘ i) ≤ tsum f
-- Lean.Parser.Do
Lean.Parser.Term.doCatchMatch.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_sub_iff_left : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {b c : α} (a : α),
  a - b < a - c ↔ c < b
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.toNat.match_1.eq_1 : ∀ (motive : WType WType.Natβ → Sort u_1) (f : WType.Natβ WType.Natα.zero → WType WType.Natβ)
  (h_1 : (f : WType.Natβ WType.Natα.zero → WType WType.Natβ) → motive (WType.mk WType.Natα.zero f))
  (h_2 : (f : WType.Natβ WType.Natα.succ → WType WType.Natβ) → motive (WType.mk WType.Natα.succ f)),
  (match WType.mk WType.Natα.zero f with
    | WType.mk WType.Natα.zero f => h_1 f
    | WType.mk WType.Natα.succ f => h_2 f) =
    h_1 f
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- An induction principle for closure membership. If `p` holds for `1` and all elements of
`k` and their inverse, and is preserved under multiplication, then `p` holds for all elements of
the closure of `k`.  -/
Subgroup.closure_induction'' : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (g : G) → g ∈ Subgroup.closure s → Prop},
  (∀ (x : G) (hx : x ∈ s), p x ⋯) →
    (∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯) →
      p 1 ⋯ →
        (∀ (x y : G) (hx : x ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯) →
          ∀ {x : G} (h : x ∈ Subgroup.closure s), p x h
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.star_eq_inv' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, star = Inv.inv
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The equality case of **Cauchy-Schwarz**.  -/
LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), x ≠ 0 → 0 < (B x) x) → ∀ (x y : M), (B x) y * (B y) x = (B x) x * (B y) y → ¬LinearIndependent R ![x, y]
-- Mathlib.Data.Seq.Basic
/-- Coinductive principle for `Pairwise`.  -/
Stream'.Seq.Pairwise.coind : ∀ {α : Type u} {R : α → α → Prop} {s : Stream'.Seq α} (motive : Stream'.Seq α → Prop),
  motive s →
    (∀ (hd : α) (tl : Stream'.Seq α), motive (Stream'.Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl) →
      Stream'.Seq.Pairwise R s
-- Init.Grind.ToInt
Lean.Grind.instBEqIntInterval.beq : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Bool
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.coe_mk : ∀ {α : Type u_1} (m : Set α → ENNReal) (h₁ : m ∅ = 0) (h₂ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → m s₁ ≤ m s₂)
  (h₃ : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)),
  ⇑{ measureOf := m, empty := h₁, mono := h₂, iUnion_nat := h₃ } = m
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.instCategoryObj : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (𝒳 : CategoryTheory.BasedCategory 𝒮) → CategoryTheory.Category.{v₂, u₂} 𝒳.obj
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.map_coe_nhdsGT : ∀ (x : NNReal), Filter.map NNReal.toReal (nhdsWithin x (Set.Ioi x)) = nhdsWithin (↑x) (Set.Ioi ↑x)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc : ∀ {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.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F] {Z : CategoryTheory.Functor A D}
  (h : L.comp ((L.pointwiseLeftKanExtension F).comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.pointwiseLeftKanExtensionUnit (F.comp G))
      (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.pointwiseLeftKanExtensionUnit F) G)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseLeftKanExtension F) G).hom h)
-- Mathlib.Order.CompleteLattice.Basic
iInf_inf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α},
  (⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whisker_exchange_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] (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)
  {Q X Y Z : CategoryTheory.LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z)
  {Z_1 : CategoryTheory.LocalizedMonoidal L W ε} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) h)
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.zsmul_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {n : ℤ} {x : PreLp E} {i : α},
  (n • x) i = n • x i
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (P P_1 : Ideal R) (e_P : P = P_1) [hp : P.IsPrime],
  Localization.AtPrime P = Localization.AtPrime P_1
-- Mathlib.Analysis.Calculus.Implicit
_private.Mathlib.Analysis.Calculus.Implicit.0.HasStrictFDerivAt.implicitFunctionDataOfComplemented.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (f : E → F) (f' : E →L[𝕜] F) {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  HasStrictFDerivAt.implicitFunctionDataOfComplemented f f' hf hf' hker =
    { leftFun := f, leftDeriv := f', rightFun := fun x => (Classical.choose hker) (x - a),
      rightDeriv := Classical.choose hker, pt := a, hasStrictFDerivAt_leftFun := hf, hasStrictFDerivAt_rightFun := ⋯,
      range_leftDeriv := hf', range_rightDeriv := ⋯, isCompl_ker := ⋯ }
-- Mathlib.Data.Sym.Basic
Sym.cons_equiv_eq_equiv_cons : ∀ (α : Type u_3) (n : ℕ) (a : α) (s : Sym α n), Sym.cons' a (Sym.symEquivSym' s) = Sym.symEquivSym' (a ::ₛ s)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `FunLike.coe_zero`. -/
MeasureTheory.OuterMeasure.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XIdeal.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x : R),
  WeierstrassCurve.Affine.CoordinateRing.XIdeal W' x = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.XClass W' x}
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addRight_bijective : ∀ {M : Type u_3} [inst : AddMonoid M] (a : AddUnits M), Function.Bijective fun x => x + ↑a
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
MulOpposite.comap_op_rightUniformSpace : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  UniformSpace.comap MulOpposite.op (IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.leftUniformSpace G
-- Init.Data.String.Defs
String.Pos.Raw.IsValidForSlice.le_utf8ByteSize : ∀ {s : String.Slice} {p : String.Pos.Raw}, String.Pos.Raw.IsValidForSlice s p → p.byteIdx ≤ s.utf8ByteSize
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- **Alias** of `dimH_finite`. -/
Set.Finite.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Finite → dimH s = 0
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : AddMonoid A] [inst_1 : GroupWithZero G₀] [inst_2 : DistribMulAction G₀ A]
  {a : G₀}, a ≠ 0 → ∀ (S : AddSubmonoid A) (x : A), x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Ric.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Ric α}, r.iter.toList = r.toList
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.unitOfList.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (l : List α),
  Std.DHashMap.Raw.Const.unitOfList l = Std.DHashMap.Raw.Const.insertManyIfNewUnit ∅ l
-- Init.Meta.Defs
/-- Creates an identifier that refers to a constant `c`. The identifier has no source position.

This variant of `mkIdent` makes sure that the identifier cannot accidentally be captured.
 -/
Lean.mkCIdent : Lean.Name → Lean.Ident
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_list_prod_le : ∀ {S : Type u_1} [inst : Semiring S] (l : List (Polynomial S)), l.prod.natDegree ≤ (List.map Polynomial.natDegree l).sum
-- Mathlib.Algebra.Group.Submonoid.Basic
AddMonoidHom.ofClosureMEqTopRight.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] {s : Set M} (f : M → N)
  (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y),
  AddMonoidHom.ofClosureMEqTopRight f hs h1 hmul = { toFun := f, map_zero' := h1, map_add' := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Banach
/-- An injective bounded linear operator between Banach spaces has closed range
iff it is anti-Lipschitz.  -/
ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  [CompleteSpace F] (f : E →L[𝕜] F), Function.Injective ⇑f → (IsClosed (Set.range ⇑f) ↔ ∃ K, AntilipschitzWith K ⇑f)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.symm : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle y x
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.isNonTrivialIsCharInst : Option (Lean.Expr × ℕ) → Bool
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} [inst_2 : SizeOf C] (toPrecylinder : HomotopicalAlgebra.Precylinder A)
  (weakEquivalence_π :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrecylinder.π)
      HomotopicalAlgebra.Cylinder.weakEquivalence_π._autoParam),
  sizeOf { toPrecylinder := toPrecylinder, weakEquivalence_π := weakEquivalence_π } =
    1 + sizeOf toPrecylinder + sizeOf weakEquivalence_π