mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.pentagon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (W X Y Z : CategoryTheory.Arrow C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_trailingDegree_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), ↑n ≤ (Polynomial.C a * Polynomial.X ^ n).trailingDegree
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_le_of_eventually_le : ∀ {u v : ℕ → EReal} {b : EReal},
  b ≠ ⊤ → (∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n + b) → LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthInf v
-- Lean.Server.References
/-- Collects `ImportInfo` for all import statements in `headerStx`.  -/
Lean.Server.collectImports : Lean.Elab.HeaderSyntax → Array Lean.Lsp.ImportInfo
-- Mathlib.Logic.Relation
Relation.join_le_of_equivalence_of_le : ∀ {α : Type u_1} {r r' : α → α → Prop}, Equivalence r → r' ≤ r → Relation.Join r' ≤ r
-- Mathlib.Data.Multiset.Sort
/-- `sort s` constructs a sorted list from the multiset `s`.
(Uses merge sort algorithm.)  -/
Multiset.sort : {α : Type u_1} →
  Multiset α →
    (r : autoParam (α → α → Prop) Multiset.sort._auto_1) →
      [DecidableRel r] → [IsTrans α r] → [Std.Antisymm r] → [Std.Total r] → List α
-- Mathlib.Topology.Algebra.Group.Torsor
Filter.Tendsto.sdiv : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P] {l : Filter α} {f g : α → P} {x y : P},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f /ₛ g) l (nhds (x /ₛ y))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_union : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S T : Set E},
  IntermediateField.adjoin F (S ∪ T) = IntermediateField.adjoin F S ⊔ IntermediateField.adjoin F T
-- Mathlib.LinearAlgebra.QuadraticForm.Real
QuadraticMap.basisRepr.congr_simp : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_8} [inst_5 : Finite ι] (Q Q_1 : QuadraticMap R M N),
  Q = Q_1 → ∀ (v v_1 : Module.Basis ι R M), v = v_1 → Q.basisRepr v = Q_1.basisRepr v_1
-- Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
SymmetricAlgebra.instBialgebra : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_2) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Bialgebra R (SymmetricAlgebra R M)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The single functors `C ⥤ DerivedCategory.Plus C` for all `n : ℤ` along with
their compatibilities with shifts.  -/
DerivedCategory.Plus.singleFunctors : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.SingleFunctors C (DerivedCategory.Plus C) ℤ
-- Init.Data.SInt.Bitwise
ISize.shiftLeft_zero : ∀ {a : ISize}, a <<< 0 = a
-- Mathlib.RingTheory.FreeCommRing
/-- The coercion defined by the canonical ring homomorphism from the free ring generated by `α` to
the free commutative ring generated by `α`.  -/
FreeRing.castFreeCommRing : {α : Type u_1} → FreeRing α → FreeCommRing α
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
Real.posLog_one : Real.posLog 1 = 0
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.mk.inj : ∀ {declName oldArg : Lean.Name} {newArg? : Option Lean.Name} {text? since? : Option String}
  {declName_1 oldArg_1 : Lean.Name} {newArg?_1 : Option Lean.Name} {text?_1 since?_1 : Option String},
  { declName := declName, oldArg := oldArg, newArg? := newArg?, text? := text?, since? := since? } =
      { declName := declName_1, oldArg := oldArg_1, newArg? := newArg?_1, text? := text?_1, since? := since?_1 } →
    declName = declName_1 ∧ oldArg = oldArg_1 ∧ newArg? = newArg?_1 ∧ text? = text?_1 ∧ since? = since?_1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sup : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l l' : Filter α}, f =o[l] g → f =o[l'] g → f =o[l ⊔ l'] g
-- Mathlib.Data.Set.Basic
Set.univ_subset_iff : ∀ {α : Type u} {s : Set α}, Set.univ ⊆ s ↔ s = Set.univ
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Ico : ∀ {a b : ℝ}, MeasureTheory.volume.real (Set.Ico a b) = max (b - a) 0
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f : ∀ {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.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁) (i₂ : I₂),
  ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.prod : ∀ {α : Type u_2} {β : Type u_3} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] {t : Set β},
  CountableSupClosed s → CountableSupClosed t → CountableSupClosed (s ×ˢ t)
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- If `P` holds for `f` restricted to `Uᵢ` for all `i`, it also holds for `f : X ⟶ Y` for any
`K`-cover `R` of `Y`.  -/
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_forall_pullbackSnd : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtTarget K] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X →
    (∀ {U : C} {g : U ⟶ X} [inst_1 : CategoryTheory.Limits.HasPullback f g],
        R g → P (CategoryTheory.Limits.pullback.snd f g)) →
      P f
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint, and if they are free `R`-modules, then `A ⊔ B` is also a free `R`-module.  -/
Subalgebra.LinearDisjoint.sup_free_of_free : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S}, A.LinearDisjoint B → ∀ [Module.Free R ↥A] [Module.Free R ↥B], Module.Free R ↥(A ⊔ B)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_inv_sqrt_three : Real.arctan (√3)⁻¹ = Real.pi / 6
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], (Std.DHashMap.Const.toArray m).size = m.size
-- Mathlib.RingTheory.WittVector.IsPoly
/-- A binary function `f : Π R, 𝕎 R → 𝕎 R → 𝕎 R` on Witt vectors
is said to be *polynomial* if there is a family of polynomials `φₙ` over `ℤ` such that the `n`th
coefficient of `f x y` is given by evaluating `φₙ` at the coefficients of `x` and `y`.

See also `WittVector.IsPoly` for the unary variant.

The `ghost_calc` tactic makes use of the `IsPoly` and `IsPoly₂` typeclass and its instances.
(In Lean 3, there was an `@[is_poly]` attribute to manage these instances,
because typeclass resolution did not play well with function composition.
This no longer seems to be an issue, so that such instances can be defined directly.)
 -/
WittVector.IsPoly₂ : (p : ℕ) → (⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R) → Prop
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b) (r : R), (v.adicAbv hb) ((algebraMap R K) r) = 1 ↔ r ∉ v.asIdeal
-- Mathlib.Algebra.GCDMonoid.Nat
Int.normalize_of_nonpos : ∀ {z : ℤ}, z ≤ 0 → normalize z = -z
-- Mathlib.Algebra.Order.Monoid.Units
Units.instPreorder : {α : Type u_1} → [inst : Monoid α] → [Preorder α] → Preorder αˣ
-- Mathlib.RingTheory.Perfectoid.BDeRham
/-- The de Rham period ring $\mathbb{B}_{dR}^+$ for general perfectoid ring.
It is the completion of `𝕎 R♭` inverting `p` with respect to the kernel of
the Fontaine's θ map. When $R = \mathcal{O}_{\mathbb{C}_p}$, it coincides
with the classical de Rham period ring. Note that if `p = 0` in `R`,
then this
definition is the zero ring.
 -/
BDeRhamPlus : (R : Type u) →
  [inst : CommRing R] →
    (p : ℕ) → [Fact (Nat.Prime p)] → [Fact ¬IsUnit ↑p] → [IsAdicComplete (Ideal.span {↑p}) R] → Type u
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instIsEquivalenceRestrictScalarsToRingHomSymm : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  (AlgCat.restrictScalars e.symm.toRingHom).IsEquivalence
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.biSup : ∀ {G : Type u_3} [inst : AddGroup G] {ι : Type u_5} {s : Set ι},
  s.Finite → ∀ (P : ι → AddSubgroup G), (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.contains.loop : ByteSlice → UInt8 → ℕ → Bool
-- Init.Data.UInt.Lemmas
UInt64.pos_iff_ne_zero : ∀ {a : UInt64}, 0 < a ↔ a ≠ 0
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars.orderIso_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (E : { E // F ≤ E }), (IntermediateField.extendScalars.orderIso F) E = IntermediateField.extendScalars ⋯
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.orderDualEquivalence_functor_map : ∀ (X : Type u) [inst : Preorder X] {X_1 Y : Xᵒᵈ} (f : X_1 ⟶ Y),
  (CategoryTheory.orderDualEquivalence X).functor.map f = (CategoryTheory.homOfLE ⋯).op
-- Init.Data.UInt.Bitwise
UInt32.toUInt16_xor : ∀ (a b : UInt32), (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
-- Mathlib.Order.Heyting.Basic
himp_inf_himp_cancel : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, b ≤ a → c ≤ b → (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tensorRight : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_9)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid R) [IsLocalization M A],
  IsLocalization (Algebra.algebraMapSubmonoid S M) (TensorProduct R A S)
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofFin : ∀ (n : Fin UInt16.size), (UInt16.ofFin n).toUInt8 = UInt8.ofNat ↑n
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_σ_self'_assoc : ∀ {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    ∀ {Z : SimplexCategory} (h : { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) =
        h
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- In a locally path connected space, each path component is a clopen set.  -/
IsClopen.pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X), IsClopen (pathComponent x)
-- Mathlib.Data.FunLike.Group
FunLike.subNegMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : Neg F] [inst_5 : Sub F] [inst_6 : SMul ℤ F] [inst_7 : SubNegMonoid β]
  [inst_8 : IsZeroApply F α β] [inst_9 : IsAddApply F α β] [inst_10 : IsNegApply F α β] [inst_11 : IsSubApply F α β]
  [inst_12 : IsSMulApply ℕ F α β] [inst_13 : IsSMulApply ℤ F α β],
  FunLike.subNegMonoid = Function.Injective.subNegMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Core.transform.visit : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.CoreM m] →
      [MonadControlT Lean.CoreM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            (x : STWorld IO.RealWorld m) →
              MonadLiftT (ST IO.RealWorld) m → Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
continuous_sigmoid : Continuous Real.sigmoid
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_le_im : ∀ (a : ℝ), frontier {z | a ≤ z.im} = {z | z.im = a}
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  QuadraticAlgebra.trace (star z) = QuadraticAlgebra.trace z
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_measure_zero : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} [inst : NormedAddCommGroup E] (f : α → E),
  MeasureTheory.lpNorm f p 0 = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ [Inhabited α] {k fallback : α} {f : β → β}, (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.pairwise_disjoint_of_mem_zpowers : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  Pairwise fun i j => ∀ (x y : Equiv.Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → x.Disjoint y
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm : ∀ {S' : Type u_2} [inst : SeminormedAddGroup S'], (∀ (x y : S'), ‖x + y‖ ≤ max ‖x‖ ‖y‖) → IsUltrametricDist S'
-- Mathlib.Data.List.Basic
List.dropLast_append_getLast? : ∀ {α : Type u} {l : List α}, ∀ a ∈ l.getLast?, l.dropLast ++ [a] = l
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instSMul : {𝕜 : 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] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → SMul 𝕜 (ContMDiffSection I F n V)
-- Aesop.Tree.Data
Aesop.GoalData : Type → Type → Type
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.objEquiv_δ_apply : ∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n + 1 }))
  (i : Fin (n + 2)) (j : Fin (n + 1)),
  (SSet.prodStdSimplex.objEquiv
        ((CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.SimplicialObject.δ
              (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
                (SSet.stdSimplex.obj { len := q }))
              i))
          x))
      j =
    (SSet.prodStdSimplex.objEquiv x) (i.succAbove j)
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
/-- Given a prepartition `π` of a box `I` and a function `r : ℝⁿ → (0, ∞)`, `π.toSubordinate r`
is a tagged partition `π'` such that

* each box of `π'` is included in some box of `π`;
* `π'` is a Henstock partition;
* `π'` is subordinate to `r`;
* `π'` covers exactly the same part of `I` as `π`;
* the distortion of `π'` is equal to the distortion of `π`.
 -/
BoxIntegral.Prepartition.toSubordinate : {ι : Type u_1} →
  [Fintype ι] →
    {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → ((ι → ℝ) → ↑(Set.Ioi 0)) → BoxIntegral.TaggedPrepartition I
-- Mathlib.Algebra.Order.Group.Cone
/-- A (positive) cone in an abelian group is a submonoid that
does not contain both `a` and `-a` for any nonzero `a`.
This is equivalent to being the set of non-negative elements of
some order making the group into a partially ordered group.  -/
AddGroupCone : (G : Type u_1) → [AddCommGroup G] → Type u_1
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_mem_smul_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s : Finset β}
  {b : β} (a : α), a • b ∈ a • s ↔ b ∈ s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k k' : α},
  cmp k k' = Ordering.eq → t.get! k = t.get! k'
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.uniqueRingEquiv_symm_apply : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M] (r : R),
  (MonoidAlgebra.uniqueRingEquiv M).symm r = MonoidAlgebra.single 1 r
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.toLimitFun.eq_1 : ∀ (P : ProfiniteAddGrp.{u}), P.toLimitFun = { toFun := fun p => ⟨fun x => ↑p, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r : X) (s : ↥S), r /ₒ s = Quotient.mk' (r, s)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_restrictVarLeft : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : DecidableEq α]
  {γ : Type u_4} {t : L.Term (α ⊕ γ)} {f : ↥t.varFinsetLeft → β} {xs : β ⊕ γ → M} (xs' : α → M),
  (∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a) →
    FirstOrder.Language.Term.realize xs (t.restrictVarLeft f) =
      FirstOrder.Language.Term.realize (Sum.elim xs' (xs ∘ Sum.inr)) t
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Given maps `f`, `g` from a manifold into a field `𝕜` and `𝕜`-vector space `V`, respectively, the
formula for the `mfderiv` (differential) of their scalar multiplication `f • g` in the direction of
the tangent vector `v`.

Mathematically speaking the formula is `d(f • g)(v) = f • dg(v) + df(v) • g`, but to get it to
typecheck we need a phrasing involving the canonical identification `NormedSpace.fromTangentSpace`
between the vector space `V` and the tangent space to this vector space at any point. This is
because two different tangent spaces (at `(f • g) x` and `g x`) appear in the equation.

This is a defeq variant of the main lemma `fromTangentSpace_mfderiv_smul_apply`, in which we work in
the tangent space at `f x • g x` (the simp-normal form) rather than at `(f • g) x`.  -/
_private.Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.0.fromTangentSpace_mfderiv_smul_apply' : ∀ {𝕜 : 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] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
  MDiffAt f x →
    MDiffAt g x →
      ∀ (v : TangentSpace I x),
        (NormedSpace.fromTangentSpace (f x • g x)) ((mfderiv% (f • g) x) v) =
          f x • (NormedSpace.fromTangentSpace (g x)) ((mfderiv% g x) v) +
            (NormedSpace.fromTangentSpace (f x)) ((mfderiv% f x) v) • g x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.isBounded_range : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  (f : ZeroAtInftyContinuousMap α β), Bornology.IsBounded (Set.range ⇑f)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- `f` composed with `rightRetraction` is `leftRetraction` composed with `ι`  -/
CategoryTheory.IsSplitEqualizer.top_rightRetraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι),
  CategoryTheory.CategoryStruct.comp f self.rightRetraction = CategoryTheory.CategoryStruct.comp self.leftRetraction ι
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.instHasColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CosimplicialObject.Truncated C n)
-- Lean.Meta.WHNF
Lean.Meta.unfoldDefinition : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.add_bind : ∀ {α β : Type u} (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α), x + y >>= f = (x >>= f) + (y >>= f)
-- Lean.Structure
_private.Lean.Structure.0.Lean.getStructureFieldsFlattenedAux : Lean.Environment → Lean.Name → Array Lean.Name → Bool → Array Lean.Name
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `F` preserves the terminal object and binary products then it preserves finite products.  -/
CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal : ∀ {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.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.HasFiniteProducts C], CategoryTheory.Limits.PreservesFiniteProducts F
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_map_hom_hom : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X Y : CategoryTheory.AddGrp C} (f : X ⟶ Y),
  (F.mapAddGrp.map f).hom.hom = F.map f.hom.hom