mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mul_inl_eq_op_smul : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (r : R), x * TrivSqZeroExt.inl r = MulOpposite.op r • x
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.instIsSeparableQuotientIdealOfEssFiniteTypeOfIsPrime : ∀ (K : Type u_1) (A : Type u) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] [Algebra.EssFiniteType K A]
  [Algebra.FormallyEtale K A] (p : Ideal A) [p.IsPrime], Algebra.IsSeparable K (A ⧸ p)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.inl.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousMonoidHom.inl A B = (ContinuousMonoidHom.id A).prod 1
-- Init.Data.List.Lemmas
List.removeAll_nil : ∀ {α : Type u_1} [inst : BEq α] {xs : List α}, xs.removeAll [] = xs
-- Std.Time.Zoned.Database.TZdb
/-- Retrieves the timezone rules from the local timezone data file.
 -/
Std.Time.Database.TZdb.localRules : System.FilePath → IO Std.Time.TimeZone.ZoneRules
-- Mathlib.Analysis.Convex.Combination
Convex.sum_mem : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {s : Set E} {t : Finset ι} {w : ι → R} {z : ι → E} [inst_3 : LinearOrder R] [IsStrictOrderedRing R],
  Convex R s → (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ i ∈ t, z i ∈ s) → ∑ i ∈ t, w i • z i ∈ s
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_translationNumber_of_add_int_le : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, x + ↑m ≤ f x → ↑m ≤ f.translationNumber
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (m.insertMany l).size ≤ m.size + l.length
-- Init.Data.String.Iterate
String.Slice.instInhabitedByteIterator.default : String.Slice.ByteIterator
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given full range as a list in ascending order.
 -/
Std.Rii.toList : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] →
    [Std.PRange.Least? α] →
      Std.Rii α →
        [inst : Std.Iterator (Std.Rxi.Iterator α) Id α] → [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] → List α
-- Mathlib.Analysis.Convex.Strong
StrongConvexOn.strictConvexOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m : ℝ},
  StrongConvexOn s m f → 0 < m → StrictConvexOn ℝ s f
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The monoidal functor structure induced by a `Functor.CoreMonoidal` structure.  -/
CategoryTheory.Functor.CoreMonoidal.toMonoidal : {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} → F.CoreMonoidal → F.Monoidal
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorLeftUnitor : ∀ {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 : F.LaxMonoidal], CategoryTheory.NatTrans.IsMonoidal F.leftUnitor.hom
-- Lean.Level
Lean.Level.succ.sizeOf_spec : ∀ (a : Lean.Level), sizeOf a.succ = 1 + sizeOf a
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cones` is represented by `X`, the cone corresponding to a morphism `f : Y ⟶ X` is
the limit cone extended by `f`.  -/
CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cones.RepresentableBy X) {Y : C} (f : Y ⟶ X),
  CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h f = (CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h).extend f
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instMonoidalCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Grp.instMonoidalCategory =
    { toMonoidalCategoryStruct := CategoryTheory.Grp.instMonoidalCategoryStruct, tensorHom_def := ⋯,
      id_tensorHom_id := ⋯, tensorHom_comp_tensorHom := ⋯, whiskerLeft_id := ⋯, id_whiskerRight := ⋯,
      associator_naturality := ⋯, leftUnitor_naturality := ⋯, rightUnitor_naturality := ⋯, pentagon := ⋯,
      triangle := ⋯ }
-- Init.System.IO
IO.FS.Stream.Buffer.mk.sizeOf_spec : ∀ (data : ByteArray) (pos : ℕ), sizeOf { data := data, pos := pos } = 1 + sizeOf data + sizeOf pos
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A set `A` in the compact coherentification is open iff for all compact sets `K`,
the intersection `K ∩ A` is open in `K`.  -/
CompactCoherentification.isOpen_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Set (CompactCoherentification X)},
  IsOpen A ↔ ∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' ⇑(CompactCoherentification.mk X) ⁻¹' A)
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.separator.sizeOf_spec : sizeOf Lean.FuzzyMatching.CharType.separator = 1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_pow_iff_right₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀], 1 < a → (a ^ n < a ^ m ↔ n < m)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).minKey? = t.minKey?
-- Mathlib.Data.Nat.Cast.Commute
Commute.natCast_mul_natCast_mul : ∀ {α : Type u_1} [inst : Semiring α] {a b : α}, Commute a b → ∀ (m n : ℕ), Commute (↑m * a) (↑n * b)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.homEquiv_symm_apply : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} (f : { f // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }),
  Monoid.PushoutI.homEquiv.symm f = Monoid.PushoutI.lift (↑f).1 (↑f).2 ⋯
-- Lean.Elab.BuiltinCommand
/-- Produces a `Name` composed of the names of at most the innermost `n` scopes in `ss`, truncating if an
empty scope is reached (so that we do not suggest names like `Foo.«».Bar`).

If `n` is not specified, will use all scopes in `ss`.
 -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.nameOfScopes : (ss : List Lean.Elab.Command.Scope) → optParam ℕ ss.length → Lean.Name
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_iff_forall_isCompact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι} [LocallyCompactSpace α],
  IsOpen s → (TendstoLocallyUniformlyOn F f p s ↔ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn F f p K)
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulRightLinearEquiv_mul_apply : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (u v : Aˣ) (x : A),
  (Units.mulRightLinearEquiv R (u * v)) x = (Units.mulRightLinearEquiv R v) ((Units.mulRightLinearEquiv R u) x)
-- Batteries.Data.List.Lemmas
List.isChain_of_isChain_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → List.IsChain R l
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The object underlying `⊥ : Subobject B` is (up to isomorphism) the zero object.  -/
CategoryTheory.MonoOver.botCoeIsoZero : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → {B : C} → ⊥.obj.left ≅ 0
-- Mathlib.Data.Analysis.Filter
/-- Transfer a realizer along an equality of filter. This has better definitional equalities than
the `Eq.rec` proof.  -/
Filter.Realizer.ofEq : {α : Type u_1} → {f g : Filter α} → f = g → f.Realizer → g.Realizer
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.hasZeroObject_of_additive : ∀ {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.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive]
  [CategoryTheory.Limits.HasZeroObject C], CategoryTheory.Limits.HasZeroObject D
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.comp_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] (X Y Z : C)
  (f : X ⟶ Y) (g h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (g + h) =
    CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Topology.Irreducible
sUnion_irreducibleComponents : ∀ {X : Type u_1} [inst : TopologicalSpace X], ⋃₀ irreducibleComponents X = Set.univ
-- Mathlib.LinearAlgebra.Determinant
/-- Unfold lemma for `detAux`.

See also `detAux_def''` which allows you to vary the basis.
 -/
LinearMap.detAux_def' : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b : Module.Basis ι A M) (f : M →ₗ[A] M),
  (LinearMap.detAux (Trunc.mk b)) f = ((LinearMap.toMatrix b b) f).det
-- Mathlib.Data.ENNReal.Basic
ENNReal.top_ne_one : ⊤ ≠ 1
-- Init.Data.Array.Lex.Lemmas
Array.instTransLeOfLawfulOrderLTOfIsLinearOrder : {α : Type u_1} →
  [inst : LE α] →
    [inst_1 : LT α] →
      [Std.LawfulOrderLT α] →
        [Std.IsLinearOrder α] → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Batteries.Data.Nat.Lemmas
Nat.ofBits_zero : ∀ (f : Fin 0 → Bool), Nat.ofBits f = 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.SeparatingLeft.toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  M.SeparatingLeft → ((Matrix.toLinearMap₂ b₁ b₂) M).SeparatingLeft
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.hyp.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Mathlib.Tactic.ITauto.Proof.hyp n) = 1 + sizeOf n
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A functor `F : T ⥤ D` induces a functor `Under X ⥤ Under (F.obj X)` in the obvious way.  -/
CategoryTheory.Under.post : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          (F : CategoryTheory.Functor T D) →
            CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.Under (F.obj X))
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `simp_all` at every step in proofs, reporting where it succeeds.  -/
tryAtEachStepSimpAll : Mathlib.TacticAnalysis.Config
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_replicate : ∀ {i n w : ℕ} {x : BitVec w}, (BitVec.replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.mk : Option Std.Http.Body.Channel.Producer✝ →
  Option Std.Http.Body.Channel.Consumer✝ →
    Option (Std.Async.Waiter Bool) →
      Bool → Option Std.Http.Body.Length → Option Std.Http.Chunk → Std.Http.Body.Channel.State✝
-- Mathlib.Tactic.ApplyFun
/-- Apply a function to an equality or inequality in either a local hypothesis or the goal.

* If we have `h : a = b`, then `apply_fun f at h` will replace this with `h : f a = f b`.
* If we have `h : a ≤ b`, then `apply_fun f at h` will replace this with `h : f a ≤ f b`,
  and create a subsidiary goal `Monotone f`.
  `apply_fun` will automatically attempt to discharge this subsidiary goal using `mono`,
  or an explicit solution can be provided with `apply_fun f at h using P`, where `P : Monotone f`.
* If we have `h : a < b`, then `apply_fun f at h` will replace this with `h : f a < f b`,
  and create a subsidiary goal `StrictMono f` and behaves as in the previous case.
* If we have `h : a ≠ b`, then `apply_fun f at h` will replace this with `h : f a ≠ f b`,
  and create a subsidiary goal `Injective f` and behaves as in the previous two cases.
* If the goal is `a ≠ b`, `apply_fun f` will replace this with `f a ≠ f b`.
* If the goal is `a = b`, `apply_fun f` will replace this with `f a = f b`,
  and create a subsidiary goal `injective f`.
  `apply_fun` will automatically attempt to discharge this subsidiary goal using local hypotheses,
  or if `f` is actually an `Equiv`,
  or an explicit solution can be provided with `apply_fun f using P`, where `P : Injective f`.
* If the goal is `a ≤ b` (or similarly for `a < b`), and `f` is actually an `OrderIso`,
  `apply_fun f` will replace the goal with `f a ≤ f b`.
  If `f` is anything else (e.g. just a function, or an `Equiv`), `apply_fun` will fail.


Typical usage is:
```lean
open Function

example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : Injective <| g ∘ f) :
    Injective f := by
  intro x x' h
  apply_fun g at h
  exact H h
```

The function `f` is handled similarly to how it would be handled by `refine` in that `f` can contain
placeholders. Named placeholders (like `?a` or `?_`) will produce new goals.
 -/
Mathlib.Tactic.applyFun : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.hasFDerivAtFilter : ∀ {𝕜 : 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)
  {L : Filter (E × E)}, HasFDerivAtFilter (⇑f) f.contLinear L
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → X.Opens),
  iSup U = ⊤ → (P f ↔ ∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f))
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- The `positivity` extension which proves that `∏ i ∈ s, f i` is nonnegative if `f` is, and
positive if each `f i` is.

TODO: The following example does not work
```
example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.prod f := by positivity
```
because `compareHyp` can't look for assumptions behind binders.
 -/
Mathlib.Meta.Positivity.evalFinsetProd : Mathlib.Meta.Positivity.PositivityExt
-- Init.Ext
/-- Applies extensionality lemmas that are registered with the `@[ext]` attribute.
* `ext pat*` applies extensionality theorems as much as possible,
  using the patterns `pat*` to introduce the variables in extensionality theorems using `rintro`.
  For example, the patterns are used to name the variables introduced by lemmas such as `funext`.
* Without patterns,`ext` applies extensionality lemmas as much
  as possible but introduces anonymous hypotheses whenever needed.
* `ext pat* : n` applies ext theorems only up to depth `n`.

The `ext1 pat*` tactic is like `ext pat*` except that it only applies a single extensionality theorem.

Unused patterns will generate warning.
Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.
 -/
Lean.Elab.Tactic.Ext.ext : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Invmul-mul-mul version.  -/
Finset.ruzsa_triangle_inequality_invMul_mul_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  B.card * (A⁻¹ * C).card ≤ (B * A).card * (B * C).card
-- Mathlib.GroupTheory.OrderOfElement
Commute.orderOf_mul_dvd_lcm : ∀ {G : Type u_1} [inst : Monoid G] {x y : G}, Commute x y → orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)
-- Lean.Meta.Tactic.Simp.Types
/-- Helper function for `simpAppUsingCongr`  -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkCongr' : Lean.Expr → Lean.Meta.Simp.Result → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.im_smul : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane), (g • z).im = |(UpperHalfPlane.num g ↑z / UpperHalfPlane.denom g ↑z).im|
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] (φ : R →+* S) (a : σ → S) (r : R), MvPowerSeries.eval₂ φ a (MvPowerSeries.C r) = φ r
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.isOrdered_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t : RBTree.RBNode α},
  RBTree.RBNode.isOrdered cmp t = true ↔ RBTree.RBNode.Ordered cmp t
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_left_unitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Interpret a linear isometry as a continuous linear map.  -/
LinearIsometry.toContinuousLinearMap : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] →
                  [inst_4 : Module R E] → [inst_5 : Module R₂ E₂] → (E →ₛₗᵢ[σ₁₂] E₂) → E →SL[σ₁₂] E₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The natural isomorphism `F(A ⊗ -) ≅ FA ⊗ F-`, provided each `prodComparison F A B` is an
isomorphism (as `B` changes).  -/
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso : {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) →
              (A : C) →
                [∀ (B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] →
                  ((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp F ≅
                    F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).obj (F.obj A))
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.inclusion_injective : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} (h : N ≤ N'),
  Function.Injective ⇑(LieSubmodule.inclusion h)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_ofSnowflaking_eball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.eball x r = Metric.eball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_darts : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (h : G.Adj u' v'),
  h.toWalk.IsSubwalk p ↔ { fst := u', snd := v', adj := h } ∈ p.darts
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ⟶ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
        CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.div_rpow_of_nonneg : ∀ (x y : ENNReal) {z : ℝ}, 0 ≤ z → (x / y) ^ z = x ^ z / y ^ z
-- Lean.Elab.PreDefinition.WF.Unfold
Lean.Elab.WF.mkUnfoldEq : Lean.Elab.PreDefinition → Lean.Name → Lean.Meta.Simp.Result → Lean.MetaM Unit
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_iff_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  a ∈ t ↔ (t.get? a).isSome = true
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isLE_of_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n a n' : ℤ),
  autoParam (a + n' = n) CategoryTheory.Triangulated.TStructure.isLE_of_shift._auto_1 →
    ∀ [t.IsLE ((CategoryTheory.shiftFunctor C a).obj X) n'], t.IsLE X n
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
          Z)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y
              Z).hom
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
        h)
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.slope_le_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f x → slope f x y ≤ deriv f x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.of_epi_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f], f = 0 → CategoryTheory.Limits.IsZero Y
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- A type synonym for `C`, which should come equipped with a `Cat`-enriched category structure.
This converts it to a strict bicategory where `Category (X ⟶ Y)` is `(X ⟶[Cat] Y)`.  -/
CategoryTheory.CatEnriched : Type u_2 → Type u_2