mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Core
/-- Non-dependent eliminator for `And`.  -/
And.elim : {a b : Prop} → {α : Sort u_1} → (a → b → α) → a ∧ b → α
-- Mathlib.Topology.UniformSpace.Equiv
/-- `{*} × α` is uniformly isomorphic to `α`.  -/
UniformEquiv.punitProd : (α : Type u) → [inst : UniformSpace α] → PUnit.{u_4 + 1} × α ≃ᵤ α
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.monoidWithZeroHom_ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] {f g : WithZero α →*₀ β},
  f = g ↔ (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_of_isGLB_of_le_one : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α),
  (∀ (i : ι), f i ≤ 1) → IsGLB (Set.range fun s => ∏ i ∈ s, f i) i → HasProd f i
-- Mathlib.Data.Vector3
/-- Unexpander for `Vector3.cons`  -/
Vector3.unexpandCons : Lean.PrettyPrinter.Unexpander
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_empty : ∀ {α : Type u_1} [inst : MeasurableSpace α], ↑∅ = ∅
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- There exists a non-null vector with respect to any symmetric, nonzero bilinear form `B`
on a module `M` over a ring `R` with invertible `2`, i.e. there exists some
`x : M` such that `B x x ≠ 0`.  -/
LinearMap.BilinForm.exists_bilinForm_self_ne_zero : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [htwo : Invertible 2] {B : LinearMap.BilinForm R M}, B ≠ 0 → LinearMap.IsSymm B → ∃ x, (B x) x ≠ 0
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.OldCollector.diff : List ℕ → Std.HashSet ℕ → List ℕ
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.mem_of_smul_add_smul_mem_right : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} {x y : M} {a b : R},
  F.IsFaceOf C → x ∈ C → y ∈ C → 0 < a → 0 < b → a • x + b • y ∈ F → y ∈ F
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeffAddEquiv_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (self : PolynomialModule R M), PolynomialModule.coeffAddEquiv self = self.coeff
-- Mathlib.Algebra.Group.Defs
CommSemigroup.toCommMagma : {G : Type u} → [self : CommSemigroup G] → CommMagma G
-- Mathlib.Data.Nat.PrimeFin
Nat.dvd_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → p ∣ n
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack.eq_def : ∀ (spec : Float.Model.Format) (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpack spec b =
    let mantissaVec := Float.Model.UnpackedFloat.unpackMantissa b;
    have exponentVec := Float.Model.UnpackedFloat.unpackExponent b;
    have exponent := ↑exponentVec.toNat - (↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit);
    have signVec := Float.Model.UnpackedFloat.unpackSign b;
    have sign := Float.Model.UnpackedFloat.Sign.ofBitVec signVec;
    if exponentVec = -1#spec.exponentBits then
      if mantissaVec = 0#spec.mantissaBitsWithoutImplicit then Float.Model.UnpackedFloat.infinity sign
      else Float.Model.UnpackedFloat.notANumber
    else
      if exponentVec = 0#spec.exponentBits then
        if h : mantissaVec = 0#spec.mantissaBitsWithoutImplicit then Float.Model.UnpackedFloat.zero sign
        else Float.Model.UnpackedFloat.finite sign mantissaVec.toNat (exponent + 1) ⋯
      else Float.Model.UnpackedFloat.finite sign (1#1 ++ mantissaVec).toNat exponent ⋯
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instNatCastCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → NatCast (CauSeq.Completion.Cauchy abv)
-- Batteries.Control.ForInStep.Basic
/-- Applies function `f` to each element of a list to accumulate a `ForInStep` value.  -/
ForInStep.bindList : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)
-- Mathlib.Order.Sublattice
/-- A sublattice of a distributive lattice inherits a distributive lattice structure.  -/
Sublattice.instDistribLatticeCoe : {α : Type u_5} → [inst : DistribLattice α] → (L : Sublattice α) → DistribLattice ↥L
-- Mathlib.CategoryTheory.Category.Cat
/-- The equivalence between the type of 1-morphisms in Cat between two objects
and the type of functors between the categories corresponding to those objects.
 -/
CategoryTheory.Cat.Hom.equivFunctor : (C D : CategoryTheory.Cat) → (C ⟶ D) ≃ CategoryTheory.Functor ↑C ↑D
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- An auxiliary lemma used twice in the proof of `PiLp.pseudoMetricAux` below. Not intended for
use outside this file.  -/
PiLp.iSup_edist_ne_top_aux : ∀ {ι : Type u_5} [Finite ι] {α : ι → Type u_6} [inst : (i : ι) → PseudoMetricSpace (α i)] (f g : PiLp ⊤ α),
  ⨆ i, edist (f.ofLp i) (g.ofLp i) ≠ ⊤
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- If a compact operator preserves a complete submodule, its restriction to that submodule is
compact.

Note that, following mathlib's convention in linear algebra, `restrict` designates the restriction
of an endomorphism `f : E →ₗ E` to an endomorphism `f' : ↥V →ₗ ↥V`. To prove that the restriction
`f' : ↥U →ₛₗ ↥V` of a compact operator `f : E →ₛₗ F` is compact, apply
`IsCompactOperator.codRestrict` to `f ∘ U.subtypeL`, which is compact by
`IsCompactOperator.comp_clm`.  -/
IsCompactOperator.restrict' : ∀ {R₂ : Type u_2} [inst : Semiring R₂] {M₂ : Type u_4} [inst_1 : UniformSpace M₂] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R₂ M₂] [T0Space M₂] {f : M₂ →ₗ[R₂] M₂},
  IsCompactOperator ⇑f →
    ∀ {V : Submodule R₂ M₂} (hV : ∀ v ∈ V, f v ∈ V) [hcomplete : CompleteSpace ↥V], IsCompactOperator ⇑(f.restrict hV)
-- Mathlib.RingTheory.Congruence.Defs
/-- Pulling back a `RingCon` across a ring homomorphism.
 -/
RingCon.comap : {R : Type u_2} →
  {R' : Type u_3} →
    {F : Type u_4} →
      [inst : Add R] →
        [inst_1 : Add R'] →
          [inst_2 : FunLike F R R'] →
            [AddHomClass F R R'] →
              [inst_4 : Mul R] → [inst_5 : Mul R'] → [MulHomClass F R R'] → RingCon R' → F → RingCon R
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Martingale f ℱ μ →
    (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
InnerProductSpace.volume_closedBall_of_dim_even : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [Nontrivial E] {k : ℕ},
  Module.finrank ℝ E = 2 * k →
    ∀ (x : E) (r : ℝ),
      MeasureTheory.volume (Metric.closedBall x r) =
        ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (Real.pi ^ k / ↑k.factorial)
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.IterStep.successor.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_ric : ∀ {α : Type u_1} {xs : List α} {hi : ℕ}, Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) xs.length
-- Mathlib.Topology.Order.IntermediateValue
/-- A continuous function which tends to `Filter.atTop` along `Filter.atTop` and to `Filter.atBot`
along `Filter.atBot` is surjective.  -/
Continuous.surjective : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ},
  Continuous f →
    Filter.Tendsto f Filter.atTop Filter.atTop → Filter.Tendsto f Filter.atBot Filter.atBot → Function.Surjective f
-- Init.Prelude
/-- Get the fresh scope of the current macro invocation  -/
Lean.MonadQuotation.getCurrMacroScope : {m : Type → Type} → [self : Lean.MonadQuotation m] → m Lean.MacroScope
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.ofTensorProductEquivOfFiniteNoetherian.congr_simp : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsNoetherianRing R] [inst_4 : Module.Finite R M],
  AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M = AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.coneOfHasLimitEval_pt_X : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] (n : ι),
  (HomologicalComplex.coneOfHasLimitEval F).pt.X n =
    CategoryTheory.Limits.limit (F.comp (HomologicalComplex.eval C c n))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {f : α → Bool}
  {k : α}, (Std.TreeSet.filter f t).get! k = (Option.filter f (t.get? k)).get!
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.PreprocessorBase.mk.injEq : ∀ (name : autoParam Lean.Name Mathlib.Tactic.Linarith.PreprocessorBase.name._autoParam) (description : String)
  (name_1 : autoParam Lean.Name Mathlib.Tactic.Linarith.PreprocessorBase.name._autoParam) (description_1 : String),
  ({ name := name, description := description } = { name := name_1, description := description_1 }) =
    (name = name_1 ∧ description = description_1)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.eq_bot_of_subsingleton : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) [Subsingleton ↥S], S = ⊥
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.finsetSup_mem : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C → ∀ {ι : Type u_2} {s : ι → Set α} {t : Finset ι}, (∀ i ∈ t, s i ∈ C) → t.sup s ∈ C
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x y : ↑(F.obj j)), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrict₂.eq_1 : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Module R M] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R M₃] (f : M₁ →ₗ[R] M₂ →ₗ[R] M)
  (i : M₃ →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range),
  f.codRestrict₂ i hi hf =
    { toFun := fun x => ↑(LinearEquiv.ofInjective i hi).symm ∘ₗ LinearMap.codRestrict i.range (f x) ⋯, map_add' := ⋯,
      map_smul' := ⋯ }
-- Std.Async.Basic
Std.Async.BaseAsync.instInhabited : {α : Type} → [Inhabited α] → Inhabited (Std.Async.BaseAsync α)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The object level part of the forward direction of `Comon (Mon C) ≌ Mon (Comon C)`  -/
CategoryTheory.Bimon.toMonComonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Bimon C → CategoryTheory.Mon (CategoryTheory.Comon C)
-- Mathlib.Control.Fold
Traversable.toList.eq_1 : ∀ {α : Type u} {t : Type u → Type u} [inst : Traversable t],
  Traversable.toList = List.reverse ∘ Traversable.foldl (flip List.cons) []
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOfSet.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] (s : Set X),
  ContinuousMap.idealOfSet R s = { carrier := {f | ∀ x ∈ sᶜ, f x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.Algebra.Module.NatInt
/-- Convert back any exotic `ℕ`-smul to the canonical instance. This should not be needed since in
mathlib all `AddCommMonoid`s should normally have exactly one `ℕ`-module structure by design.
 -/
nat_smul_eq_nsmul : ∀ {M : Type u_3} [inst : AddCommMonoid M] (h : Module ℕ M) (n : ℕ) (x : M), SMul.smul n x = n • x
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- The data of a basic constructible set `s` is a tuple `(f, g₁, ..., gₙ)`  -/
PrimeSpectrum.BasicConstructibleSetData : Type u_1 → Type u_1
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The lineality space of a cone `C` is the submodule given by `C ⊓ -C`.  -/
PointedCone.lineal : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Ring R] →
      [inst_1 : LinearOrder R] →
        [inst_2 : IsOrderedRing R] → [inst_3 : AddCommGroup E] → [inst_4 : Module R E] → PointedCone R E → Submodule R E
-- Std.Sync.CancellationContext
Std.CancellationContext.State.mk : Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare → UInt64 → Std.CancellationContext.State
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Order.Round
round_add_ofNat : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α) (n : ℕ)
  [inst_4 : n.AtLeastTwo], round (x + OfNat.ofNat n) = round x + OfNat.ofNat n
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsQuasiPreprimitive.isPretransitive_of_normal : ∀ {G : Type u_1} {X : Type u_2} {inst : Group G} {inst_1 : MulAction G X} [self : MulAction.IsQuasiPreprimitive G X]
  {N : Subgroup G} [N.Normal], MulAction.fixedPoints (↥N) X ≠ Set.univ → MulAction.IsPretransitive (↥N) X
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_prod_iff : ∀ {𝕜 : 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' : Type u_14}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_15} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {x : M} (f : M → M' × N'), MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x
-- Mathlib.Data.Set.Lattice.Image
Set.prod_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β},
  s ×ˢ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ×ˢ t i j
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `n`-th homology of the alternating constant complex is zero for odd `n`.  -/
ChainComplex.alternatingConstHomologyDataOdd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] →
        (X : C) → (n : ℕ) → Odd n → (HomologicalComplex.sc (ChainComplex.alternatingConst.obj X) n).HomologyData
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
/-- If a family of morphisms with fixed target, precomposed by a family of epis is
effective epimorphic, then the original family is as well.
 -/
CategoryTheory.effectiveEpiFamilyStructOfComp : {C : Type u_2} →
  [inst : CategoryTheory.Category.{v_2, u_2} C] →
    {I : Type u_3} →
      {Z Y : I → C} →
        {X : C} →
          (g : (i : I) → Z i ⟶ Y i) →
            (f : (i : I) → Y i ⟶ X) →
              [CategoryTheory.EffectiveEpiFamily Z fun i => CategoryTheory.CategoryStruct.comp (g i) (f i)] →
                [∀ (i : I), CategoryTheory.Epi (g i)] → CategoryTheory.EffectiveEpiFamilyStruct Y f
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor reflecting larger limits also reflects smaller limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.eval_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h : C}
  {η η' : g ⟶ h}
  {θ : CategoryTheory.MonoidalCategoryStruct.tensorObj f g ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj f h},
  η = η' →
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η' = θ →
      CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η = θ
-- Mathlib.Topology.MetricSpace.ProperSpace
instProperSpaceOrderDual : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [ProperSpace X], ProperSpace Xᵒᵈ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β}, m.contains a = false → Std.DHashMap.Const.getD m a fallback = fallback
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.rTensorOne_symm_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (m : ↥M), M.rTensorOne.symm m = m ⊗ₜ[R] 1
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The counit isomorphism of the equivalence `(C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D)`.  -/
CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso : (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] →
        ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C)
                    (CategoryTheory.Idempotents.Karoubi D)).obj
                (CategoryTheory.Idempotents.toKaroubi C)).comp
            (CategoryTheory.Idempotents.functorExtension₁ C D) ≅
          CategoryTheory.Functor.id
            (CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D))
-- Init.Data.Order.Ord
Std.TransCmp.congr_right : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α}, cmp b c = Ordering.eq → cmp a b = cmp a c
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.continuous_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜] [Finite ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜 F]
  {G : Type u_5} [inst_8 : AddCommGroup G] [inst_9 : TopologicalSpace G] [inst_10 : Module 𝕜 G]
  [inst_11 : ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F), Continuous fun p => (f p.1) p.2
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_eq_zero_of_not_isSelfAdjoint : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A}, ¬IsSelfAdjoint a → a⁺ = 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_eq_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, m.contains a = (m.get? a).isSome
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffWithinAt_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E} {t : Set H} {y : H},
  ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (f x).ofLp i) t y
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.TreeMap.getEntryLT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option (α × β)
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- An excenter of a simplex bisects the angle at a point shared between two faces, as measured
between that excenter and its touchpoints on those faces.  -/
Affine.Simplex.ExcenterExists.angle_excenter_touchpoint_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {p : P} {i₁ i₂ : Fin (n + 1)},
      p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points) →
        p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) →
          EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₁) =
            EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₂)
-- Mathlib.Data.Nat.Upto
/-- The "greater than" relation on `Upto p` is well founded if (and only if) there exists a value
satisfying `p`.  -/
Nat.Upto.wf : ∀ {p : ℕ → Prop}, (∃ x, p x) → WellFounded (Nat.Upto.GT p)
-- Mathlib.Algebra.Module.Hom
AddMonoidHom.coe_smul' : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑AddMonoidHom.smul = DistribSMul.toAddMonoidHom M
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withInDSimp : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two : ∀ {θ ψ : Real.Angle}, |θ.toReal| < Real.pi / 2 → |ψ.toReal| < Real.pi / 2 → (2 • θ = 2 • ψ ↔ θ = ψ)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_whiskerRight : ∀ {R : Type u} [inst : CommSemiring R] {L M : SemimoduleCat R} (f : L ⟶ M) (N : SemimoduleCat R),
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) =
    LinearMap.rTensor (↑N) (SemimoduleCat.Hom.hom f)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.coe_map : ∀ {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α), ↑(Ultrafilter.map m f) = Filter.map m ↑f