mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_of_isUnit_left : ∀ {α : Type u_1} [inst : Monoid α] {a : α} (b : α), IsUnit a → ¬FiniteMultiplicity a b
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Context.mk.injEq : ∀ (config : Mathlib.Meta.FunProp.Config) (constToUnfold : Std.TreeSet Lean.Name Lean.Name.quickCmp)
  (disch : Lean.Expr → Lean.MetaM (Option Lean.Expr)) (transitionDepth : ℕ) (config_1 : Mathlib.Meta.FunProp.Config)
  (constToUnfold_1 : Std.TreeSet Lean.Name Lean.Name.quickCmp) (disch_1 : Lean.Expr → Lean.MetaM (Option Lean.Expr))
  (transitionDepth_1 : ℕ),
  ({ config := config, constToUnfold := constToUnfold, disch := disch, transitionDepth := transitionDepth } =
      { config := config_1, constToUnfold := constToUnfold_1, disch := disch_1,
        transitionDepth := transitionDepth_1 }) =
    (config = config_1 ∧ constToUnfold = constToUnfold_1 ∧ disch = disch_1 ∧ transitionDepth = transitionDepth_1)
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.setOfIdeal.eq_1 : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] (I : Ideal C(X, R)), ContinuousMap.setOfIdeal I = {x | ∀ f ∈ I, f x = 0}ᶜ
-- Std.Do.PredTrans
/-- Adds the ability to make assertions about exceptions of type `ε` to a predicate transformer with
postcondition shape `ps`, resulting in postcondition shape `.except ε ps`. This is done by
interpreting `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`.

This can be used for all kinds of exception-like effects, such as early termination, by interpreting
them as exceptions.
 -/
Std.Do.PredTrans.pushExcept : {ps : Std.Do.PostShape} →
  {α ε : Type u_1} → ExceptT ε (Std.Do.PredTrans ps) α → Std.Do.PredTrans (Std.Do.PostShape.except ε ps) α
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_ofNat : ∀ (n : ℕ) (h : System.Platform.numBits = 32), (OfNat.ofNat n).toBitVec32 h = BitVec.ofNat 32 n
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`, then
`f` grows at most as fast as `C * x` on `D`, i.e., `f y - f x ≤ C * (y - x)` whenever `x, y ∈ D`,
`x ≤ y`.  -/
Convex.image_sub_le_mul_sub_of_deriv_le : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          ∀ {C : ℝ}, (∀ x ∈ interior D, deriv f x ≤ C) → ∀ x ∈ D, ∀ y ∈ D, x ≤ y → f y - f x ≤ C * (y - x)
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Category structure on `ReflQuiv`  -/
CategoryTheory.ReflQuiv.category : CategoryTheory.LargeCategory CategoryTheory.ReflQuiv
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The underlying `NormedAddGroupHom`.  -/
SemiNormedGrp₁.Hom.hom' : {M N : SemiNormedGrp₁} → M.Hom N → NormedAddGroupHom M.carrier N.carrier
-- Init.Data.String.Lemmas.FindPos
String.Pos.posLE_offset : ∀ {s : String} {p : s.Pos}, s.posLE p.offset = p
-- Mathlib.RingTheory.Nullstellensatz
/-- Set of points that are zeroes of all polynomials in an ideal  -/
MvPolynomial.zeroLocus : {k : Type u_1} →
  (K : Type u_2) →
    [inst : Field k] → [inst_1 : Field K] → [Algebra k K] → {σ : Type u_3} → Ideal (MvPolynomial σ k) → Set (σ → K)
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation.C`. -/
FunctionField.inftyValuation.C : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {k : F},
  k ≠ 0 → (RatFunc.inftyValuation F) (RatFunc.C k) = 1
-- Lean.ResolveName
Lean.addAliasEntry : Lean.AliasState → Lean.AliasEntry → Lean.AliasState
-- Mathlib.Lean.Json
Lean.instToJsonSubtype_mathlib : {α : Type u} → [Lean.ToJson α] → (p : α → Prop) → Lean.ToJson (Subtype p)
-- Mathlib.MeasureTheory.Integral.Gamma
integral_rpow_mul_exp_neg_mul_rpow : ∀ {p q b : ℝ},
  0 < p →
    -1 < q →
      0 < b →
        ∫ (x : ℝ) in Set.Ioi 0, x ^ q * Real.exp (-b * x ^ p) = b ^ (-(q + 1) / p) * (1 / p) * Real.Gamma ((q + 1) / p)
-- Init.Data.List.Find
List.find?_eq_findSome?_guard : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.find? p l = List.findSome? (Option.guard p) l
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.inv : {α : Type u} → [Neg α] → Inv (Multiplicative α)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The bound that appears in **Minkowski Convex Body theorem**, see
`MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`. See
`NumberField.mixedEmbedding.volume_fundamentalDomain_idealLatticeBasis_eq` and
`NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis` for the computation of
`volume (fundamentalDomain (idealLatticeBasis K))`.  -/
NumberField.mixedEmbedding.minkowskiBound : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ → ENNReal
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.succ.congr_simp : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (self self_1 : F.WellOrderInductionData),
  self = self_1 →
    ∀ (j : J) (hj : ¬IsMax j) (x x_1 : F.obj (Opposite.op j)), x = x_1 → self.succ j hj x = self_1.succ j hj x_1
-- Mathlib.Analysis.Complex.CanonicalDecomposition
Complex.canonicalFactor.eq_1 : ∀ (R : ℝ) (w z : ℂ), Complex.canonicalFactor R w z = (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instWellFoundedLT : WellFoundedLT Cardinal.{u}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Init.Data.BitVec.Lemmas
BitVec.neg_inj : ∀ {w : ℕ} {x y : BitVec w}, -x = -y ↔ x = y
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      (motive : List α → List β → Array γ → Sort u_4) →
        (x : List α) →
          (x_1 : List β) →
            (x_2 : Array γ) →
              ((a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc) →
                ((x : List α) →
                    (x_3 : List β) →
                      (acc : Array γ) →
                        (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_3 = b :: bs → False) →
                          motive x x_3 acc) →
                  motive x x_1 x_2
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
stronglyMeasurable_derivWithin_Ioi : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F],
  MeasureTheory.StronglyMeasurable fun x => derivWithin f (Set.Ioi x) x
-- Lean.Syntax
Lean.Syntax.MonadTraverser.getCur : {m : Type → Type} → [Monad m] → [t : Lean.Syntax.MonadTraverser m] → m Lean.Syntax
-- Mathlib.Order.SaddlePoint
isSaddlePointOn_iff' : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [inst : CompleteLinearOrder β]
  {a : E}, a ∈ X → ∀ {b : F}, b ∈ Y → (IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Linearization proof for `/`
- If `?y = some y`, then it is a proof for `a / b = y / k` where `c` is a proof that `b = k`
- If `?y = none`, then it is a proof for `a / b = a/k` where `c` is a proof that `b = k`. `a` is a numeral in this case.
 -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div : ℤ → Option Int.Internal.Linear.Var → Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_map_eq_charpoly : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] (x : L),
  Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ x)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (i : ℤ),
  (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv.f i =
    (CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).inv
-- Mathlib.RingTheory.Kaehler.Basic
/-- (Implementation) An `Equiv` version of `KaehlerDifferential.End_equiv_aux`.
Used in `KaehlerDifferential.endEquiv`.  -/
KaehlerDifferential.endEquivAuxEquiv : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          { f //
              (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f =
                IsScalarTower.toAlgHom R S
                  ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸
                    (KaehlerDifferential.ideal R S).cotangentIdeal) } ≃
            { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_sum : ∀ {α : Type u_5} {f : Filter α} {R : Type u_6} {κ : Type u_7} [inst : AddCommMonoid R] {r : R → R → Prop},
  (∀ (v₁ v₂ : α → R),
      Filter.IsBoundedUnder r f v₁ → Filter.IsBoundedUnder r f v₂ → Filter.IsBoundedUnder r f (v₁ + v₂)) →
    r 0 0 →
      ∀ {u : κ → α → R} (s : Finset κ),
        (∀ k ∈ s, Filter.IsBoundedUnder r f (u k)) → Filter.IsBoundedUnder r f (∑ k ∈ s, u k)
-- Init.GrindInstances.Ring.Fin
_private.Init.GrindInstances.Ring.Fin.0.Lean.Grind.Fin.neg_neg : ∀ {n : ℕ} [NeZero n] (a : Fin n), - -a = a
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instModule : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → Module 𝕜 (LeftInvariantDerivation I G)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.congr : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M}
  {n : WithTop ℕ∞}, ContMDiffOn I I' n f s → (∀ y ∈ s, f₁ y = f y) → ContMDiffOn I I' n f₁ s
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.sq_add : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] (a : R) {s : R}, IsSumSq s → IsSumSq (a * a + s)
-- Init.Data.Array.Find
Array.min_findIdx_findIdx : ∀ {α : Type u_1} {xs : Array α} {p q : α → Bool},
  min (Array.findIdx p xs) (Array.findIdx q xs) = Array.findIdx (fun a => p a || q a) xs
-- Mathlib.Algebra.GroupWithZero.Associated
prime_dvd_prime_iff_eq : ∀ {M : Type u_2} [inst : CommMonoidWithZero M] [IsCancelMulZero M] [Subsingleton Mˣ] {p q : M},
  Prime p → Prime q → (p ∣ q ↔ p = q)
-- Mathlib.Topology.Compactness.Lindelof
countable_cover_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X] {U : X → Set X},
  (∀ (x : X), U x ∈ nhds x) → ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = Set.univ
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.comp : ∀ {S : Type u_4} [inst : CommRing S] {υ : Type u_5} {T : Type u_6} [inst_1 : CommRing T] [inst_2 : Algebra S T]
  {a : PowerSeries S},
  PowerSeries.HasSubst a →
    ∀ {b : MvPowerSeries υ T} (hb : PowerSeries.HasSubst b), PowerSeries.HasSubst ((PowerSeries.substAlgHom hb) a)
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_finsupp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : DecidableEq ι],
  dualTensorHom R M (ι →₀ N) =
    LinearMap.finsuppLinearMap R ∘ₗ
      Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(TensorProduct.finsuppRight R R (Module.Dual R M) N ι)
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtypeNe_symm_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (Equiv.optionSubtypeNe a).symm a = none
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.toAlgHomMonoidHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (self : A →A[R] A), ContinuousAlgHom.toAlgHomMonoidHom self = ↑self
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
mem_pairSelfAdjointMatricesSubmodule' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n] (J J₃ A : Matrix n n R₂)
  [inst_2 : DecidableEq n], A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ J.IsAdjointPair J₃ A A
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isoClosure_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.isoClosure = P ↔ P.RespectsIso
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.instOplaxMonoidalProdProd : {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] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  {C' : Type u₁'} →
                    [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] →
                      (F : CategoryTheory.Functor C D) →
                        (G : CategoryTheory.Functor E C') →
                          [inst_7 : CategoryTheory.MonoidalCategory C'] →
                            [F.OplaxMonoidal] → [G.OplaxMonoidal] → (F.prod G).OplaxMonoidal
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.mapId_hom_app : ∀ (I : Type w₁) (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  (x : (i : I) × (fun i => C (id i)) i),
  (CategoryTheory.Sigma.mapId I C).hom.app x = CategoryTheory.CategoryStruct.id ⟨x.fst, x.snd⟩
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.mk : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {c₁ c₂ c₃ : R} →
            (i j k : A) →
              i * i = c₁ • 1 + c₂ • i →
                j * j = c₃ • 1 → i * j = k → j * i = c₂ • j - k → QuaternionAlgebra.Basis A c₁ c₂ c₃
-- Mathlib.Analysis.RCLike.Basic
_private.Mathlib.Analysis.RCLike.Basic.0.RCLike.termIR : Lean.ParserDescr
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f + g` is generated by `{s + t | s ∈ f, t ∈ g}` in scope `Pointwise`.  -/
Filter.instAdd : {α : Type u_2} → [Add α] → Add (Filter α)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.sorry.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.Proof.sorry = 1
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.det_scalar : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (u : Rˣ),
  Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.scalar n) u) = u ^ Fintype.card n
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The `Subsemiring` generated by a multiplicative submonoid coincides with the
`Subsemiring.closure` of the submonoid itself .  -/
Submonoid.subsemiringClosure_eq_closure : ∀ {R : Type u} [inst : NonAssocSemiring R] (M : Submonoid R), M.subsemiringClosure = Subsemiring.closure ↑M
-- Init.System.IO
/-- The stream should be empty.  -/
IO.Process.Stdio.null : IO.Process.Stdio
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Coercion of an element of `WithVal (v.valuation K)` into the adic completion.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoeWithValWithZeroMultiplicativeIntValuation : {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) →
                Coe (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))
                  (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRightIso_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.whiskerRightIso (F.mapId a) (F.map f) =
    (F.mapComp (CategoryTheory.CategoryStruct.id a) f).symm ≪≫
      F.map₂Iso (CategoryTheory.Bicategory.leftUnitor f) ≪≫ (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.mk : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The generalized eigenspace of an eigenvalue has positive dimension for positive exponents.  -/
Module.End.pos_finrank_genEigenspace_of_hasEigenvalue : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {f : Module.End K V} {k : ℕ} {μ : K}, f.HasEigenvalue μ → 0 < k → 0 < Module.finrank K ↥((f.genEigenspace μ) ↑k)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformContinuousOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {s : Set α},
  UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε
-- Mathlib.LinearAlgebra.Determinant
AlternatingMap.map_basis_ne_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [Finite ι] (e : Module.Basis ι R M) (f : M [⋀^ι]→ₗ[R] R), f ⇑e ≠ 0 ↔ f ≠ 0
-- Init.Data.List.MinMaxOn
List.get_maxOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  (List.maxOn? f xs).get ⋯ = List.maxOn f xs h
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- Construct limit data for a product in `ModuleCat R`, using `ModuleCat.of R (∀ j, F.obj j)`.
 -/
ModuleCat.HasLimit.productLimitCone : {R : Type u} →
  [inst : Ring R] →
    {J : Type w} → (f : J → ModuleCat R) → CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
-- Mathlib.Topology.Closure
interior_eq_compl_closure_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s = (closure sᶜ)ᶜ
-- Mathlib.NumberTheory.DirichletCharacter.Bounds
/-- The values of a Dirichlet character with target a normed field have norm bounded by `1`.  -/
DirichletCharacter.norm_le_one : ∀ {F : Type u_1} [inst : NormedField F] {n : ℕ} (χ : DirichletCharacter F n) (a : ZMod n), ‖χ a‖ ≤ 1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.of_const_mul_right : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {c : R}, (f =o[l] fun x => c * g x) → f =o[l] g
-- Mathlib.RingTheory.MvPowerSeries.Restricted
/-- Restricted power series as a subring of `MvPowerSeries σ R`.  -/
MvPowerSeries.IsRestricted.subring : {R : Type u_1} → [inst : NormedRing R] → {σ : Type u_2} → [IsUltrametricDist R] → (σ → ℝ) → Subring (MvPowerSeries σ R)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p.degrees = p.support.sup fun s => Finsupp.toMultiset s
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The left commuting triangle of the factorization morphism.  -/
CategoryTheory.Factorisation.Hom.ι_h_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  (self : d.Hom e) {Z : C} (h : e.mid ⟶ Z),
  CategoryTheory.CategoryStruct.comp d.ι (CategoryTheory.CategoryStruct.comp self.h h) =
    CategoryTheory.CategoryStruct.comp e.ι h
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.uniqueRight : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → [Subsingleton N] → Unique (TensorProduct R M N)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.takeWhile.eq_1 : ∀ (x : Char → Bool) (s : String) (b e : String.Pos.Raw),
  { str := s, startPos := b, stopPos := e }.takeWhile x =
    { str := s, startPos := b, stopPos := Substring.Raw.takeWhileAux s e x b }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiff.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → ContDiff ℝ n fun x => Real.sinh (f x)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.corootSpanMem_reflectionPerm_self : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S N] (i : ι), P.corootSpanMem S ((P.reflectionPerm i) i) = -P.corootSpanMem S i
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.toAddCommMonoid.eq_1 : ∀ {M : Type u_5} [inst : AddCommMonoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M]
  (S : A), AddSubmonoidClass.toAddCommMonoid S = { toAddMonoid := AddSubmonoidClass.toAddMonoid S, add_comm := ⋯ }
-- Mathlib.Topology.Covering.Quotient
isAddQuotientCoveringMap_iff_isCoveringMap_and : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  IsAddQuotientCoveringMap f G ↔
    IsCoveringMap f ∧
      Function.Surjective f ∧
        ContinuousConstVAdd G E ∧ IsCancelVAdd G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂
-- Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
/-- If observables  `φ` and `ψ` are `μ`-a.e. equal then the corresponding `birkhoffSum` are
`μ`-a.e. equal.  -/
MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq : ∀ {α : Type u_1} {M : Type u_2} [inst : MeasurableSpace α] [inst_1 : AddCommMonoid M] {f : α → α}
  {μ : MeasureTheory.Measure α} {φ ψ : α → M},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ → φ =ᵐ[μ] ψ → ∀ (n : ℕ), birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n
-- Std.Data.Iterators.Producers.Monadic.Empty
Std.Iterators.Types.Empty.instFinite : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m], Std.Iterators.Finite (Std.Iterators.Types.Empty m β) m
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.contains t.minKey! = true