mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffAt.prodMap' : ∀ {𝕜 : 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_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {n : WithTop ℕ∞} {g : N → N'} {p : M × N},
  ContMDiffAt I I' n f p.1 → ContMDiffAt J J' n g p.2 → ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.sum.match_1.eq_2 : ∀ {α : Type u_2} (motive : (x : ℕ) → (Fin x → α) → Sort u_1) (v : Fin 1 → α) (h_1 : (x : Fin 0 → α) → motive 0 x)
  (h_2 : (v : Fin 1 → α) → motive 1 v) (h_3 : (n : ℕ) → (v : Fin (n + 2) → α) → motive n.succ.succ v),
  (match 1, v with
    | 0, x => h_1 x
    | 1, v => h_2 v
    | n.succ.succ, v => h_3 n v) =
    h_2 v
-- Mathlib.Algebra.Group.Even
Even.isSquare_zpow : ∀ {α : Type u_2} [inst : Group α] {n : ℤ}, Even n → ∀ (a : α), IsSquare (a ^ n)
-- Mathlib.Algebra.Module.RingHom
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →+* S`.

See also `Function.Surjective.mulActionLeft` and `Function.Surjective.distribMulActionLeft`.
 -/
Function.Surjective.moduleLeft : {R : Type u_5} →
  {S : Type u_6} →
    {M : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring S] →
              [inst_4 : SMul S M] →
                (f : R →+* S) → Function.Surjective ⇑f → (∀ (c : R) (x : M), f c • x = c • x) → Module S M
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_contract : ∀ {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α), (M.contract C₁).contract C₂ = M.contract (C₁ ∪ C₂)
-- Init.Data.Vector.Monadic
/-- We can express a for loop over a vector as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
 -/
Vector.forIn_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : α → β → m (ForInStep β)) (init : β),
  forIn xs init f =
    ForInStep.value <$>
      Vector.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) xs
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.of_sets : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {v : ι → Set X} (h_open : ∀ (i : ι), IsOpen (v i)),
  ⋃ i, v i = Set.univ → TopologicalSpace.IsOpenCover fun i => { carrier := v i, is_open' := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.below.mismatched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) → String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1 → Prop}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos} (a : startPos < endPos)
  (a_1 : ∀ (pos : s.Pos), startPos ≤ pos → pos < endPos → ¬String.Slice.Pattern.Model.MatchesAt pat pos)
  (a_2 : String.Slice.Pattern.Model.IsValidSearchFrom pat endPos l),
  String.Slice.Pattern.Model.IsValidSearchFrom.below a_2 →
    motive endPos l a_2 → String.Slice.Pattern.Model.IsValidSearchFrom.below ⋯
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
GroupLike.instGroup : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : HopfAlgebra R A] → Group (GroupLike R A)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
a cocone on `F` with cone point `W`.  -/
CategoryTheory.Limits.IsColimit.homIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t →
              (W : C) → ULift.{u₁, v₃} (t.pt ⟶ W) ≅ F ⟶ (CategoryTheory.Functor.const J).obj W
-- Init.Data.Order.Ord
Std.OrientedCmp.isLE_of_isGE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp b a).isGE = true → (cmp a b).isLE = true
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `mul_inv_le_iff₀'` for a version with multiplication on the other side.  -/
mul_inv_le_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (b * c⁻¹ ≤ a ↔ b ≤ a * c)
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α), M.transpose = Matrix.of fun x y => M y x
-- Mathlib.Algebra.Lie.Matrix
lieEquivMatrix'_apply : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f : Module.End R (n → R)), lieEquivMatrix' f = LinearMap.toMatrix' f
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `f` is strictly differentiable at `x` with derivative `f'`, then `f` is Lipschitz in a
neighborhood of `x`. See also `HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt` for a
more precise statement.  -/
HasStrictFDerivAt.exists_lipschitzOnWith : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → ∃ K, ∃ s ∈ nhds x, LipschitzOnWith K f s
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.presheafHom_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (M N : ↑(F.obj { as := Opposite.op S })) {T₁ T₂ : (CategoryTheory.Over S)ᵒᵖ} (p : T₁ ⟶ T₂),
  (F.presheafHom M N).map p =
    TypeCat.ofHom fun f =>
      CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom f (CategoryTheory.Over.Hom.left p.unop)
        (Opposite.unop T₂).hom (Opposite.unop T₂).hom ⋯ ⋯
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.succNthVal_spec : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
  (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot
    (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.isMittagLeffler_iff_subset_range_comp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J],
  F.IsMittagLeffler ↔
    ∀ (j : J),
      ∃ i f,
        ∀ ⦃k : J⦄ (g : k ⟶ i),
          Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⊆
            Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp g f)))
-- Mathlib.Data.Nat.Digits.Lemmas
List.consFixedLengthDigits_head : ∀ {b : ℕ} (hb : 1 < b) {l d : ℕ} {L : List ℕ} (hL : L ∈ List.consFixedLengthDigits hb l d), L.head ⋯ = d
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.sum_rpow_le_of_tendsto : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  {l : Filter ι} [l.NeBot] [_i : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ {C : ℝ} {F : ι → ↥(lp E p)},
      (∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) →
        ∀ {f : (a : α) → E a},
          Filter.Tendsto (id fun i => ↑(F i)) l (nhds f) → ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.completeSpace : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F]
  [CompleteSpace F] [ContinuousSMul 𝕜₁ E],
  Topology.IsCoherentWith {s | Bornology.IsVonNBounded 𝕜₁ s} → CompleteSpace (E →SL[σ] F)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any two morphisms to a terminal object are equal.  -/
CategoryTheory.Limits.IsTerminal.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X)
  (f g : Y ⟶ X), f = g
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.measure_mem_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
  ProbabilityTheory.IdentDistrib f g μ ν → ∀ {s : Set γ}, MeasurableSet s → μ (f ⁻¹' s) = ν (g ⁻¹' s)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.biSup_adjoin_simple : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  ⨆ x ∈ S, F⟮x⟯ = IntermediateField.adjoin F S
-- Mathlib.Analysis.Matrix.Normed
/-- This applies to the sup norm of L1 norm.  -/
Matrix.linftyOpIsBoundedSMul : ∀ {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedRing R] [inst_3 : SeminormedAddCommGroup α] [inst_4 : Module R α] [IsBoundedSMul R α],
  IsBoundedSMul R (Matrix m n α)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Standard formula, computing the Laplacian from any orthonormal basis.
 -/
InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F) {ι : Type u_5}
  [inst_5 : Fintype ι] (v : OrthonormalBasis ι ℝ E),
  Laplacian.laplacian f = fun x => ∑ i, (iteratedFDeriv ℝ 2 f x) ![v i, v i]
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.coe_restrictScalars : ∀ (R : Type uR) {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] {A : Type u_1} [inst_5 : Semiring A] [inst_6 : SMul R A] [inst_7 : (i : ι) → Module A (M₁ i)]
  [inst_8 : Module A M₂] [inst_9 : ∀ (i : ι), IsScalarTower R A (M₁ i)] [inst_10 : IsScalarTower R A M₂]
  (f : MultilinearMap A M₁ M₂), ⇑(MultilinearMap.restrictScalars R f) = ⇑f
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeMemValuationSubringValuationSubringAtPrime : {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) →
                Algebra R ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  {P : F.ObjectProperty}, (∀ (X : B), (P.prop X).IsClosedUnderIsomorphisms) → P.IsClosedUnderIsomorphisms
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.eventuallyEq_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) {ψ : F → G → E},
  (∀ᶠ (x : E) in nhds φ.pt, ψ (φ.leftFun x) (φ.rightFun x) = x) →
    Function.uncurry ψ =ᶠ[nhds (φ.prodFun φ.pt)] Function.uncurry φ.implicitFunction
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Alias** of `intervalIntegral.integral_deriv_smul_comp''`.

---

Change of variables for continuous integrands. If `f` is continuous on `[a, b]` and has
continuous right-derivative `f'` in `(a, b)`, and `g` is continuous on `f '' [a, b]` then we can
substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_comp_smul_deriv'' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn f' (Set.uIcc a b) →
        ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.GroupTheory.Order.Min
Monoid.minOrder_le_orderOf : ∀ {α : Type u_2} [inst : Monoid α] {a : α}, a ≠ 1 → IsOfFinOrder a → Monoid.minOrder α ≤ ↑(orderOf a)
-- Init.Prelude
/-- `` `null `` is the “fallback” kind, used when no other kind applies. Null nodes result from
repetition operators, and empty null nodes represent the failure of an optional parse.

The null kind is used for raw list parsers like `many`.
 -/
Lean.nullKind : Lean.SyntaxNodeKind
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_toUSize : ∀ (n : UInt16), n.toUSize.toUInt64 = n.toUInt64
-- Mathlib.RingTheory.Bialgebra.Basic
/-- If `R` is a commutative semiring and `A` is an `R`-algebra,
then `Bialgebra.ofAlgHom` consumes the counit and comultiplication
as algebra homomorphisms that satisfy the coalgebra axioms to define
a bialgebra structure on `A`.  -/
Bialgebra.ofAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          (comul : A →ₐ[R] TensorProduct R A A) →
            (counit : A →ₐ[R] R) →
              (↑(Algebra.TensorProduct.assoc R R R A A A)).comp
                    ((Algebra.TensorProduct.map comul (AlgHom.id R A)).comp comul) =
                  (Algebra.TensorProduct.map (AlgHom.id R A) comul).comp comul →
                (Algebra.TensorProduct.map counit (AlgHom.id R A)).comp comul = ↑(Algebra.TensorProduct.lid R A).symm →
                  (Algebra.TensorProduct.map (AlgHom.id R A) counit).comp comul =
                      ↑(Algebra.TensorProduct.rid R R A).symm →
                    Bialgebra R A
-- Mathlib.Topology.Order.MonotoneConvergence
/-- We say that `α` is an `InfConvergenceClass` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a greatest lower bound of `Set.range f`. Then `f x` tends to `𝓝 a`
as `x → -∞` (formally, at the filter `Filter.atBot`). We require this for `ι = (s : Set α)`,
`f = (↑)` in the definition, then prove it for any `f` in `tendsto_atBot_isGLB`.

This property holds for linear orders with order topology as well as their products.  -/
InfConvergenceClass : (α : Type u_3) → [Preorder α] → [TopologicalSpace α] → Prop
-- Mathlib.Logic.ExistsUnique
ExistsUnique.intro : ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → (∀ (y : α), p y → y = w) → ∃! x, p x
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Union of all boxes of a tagged prepartition.  -/
BoxIntegral.TaggedPrepartition.iUnion : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → Set (ι → ℝ)
-- Mathlib.Data.Fintype.Prod
infinite_prod : ∀ {α : Type u_1} {β : Type u_2}, Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
-- Mathlib.Logic.Function.Iterate
List.foldl_const : ∀ {α : Type u} {β : Type v} (f : α → α) (a : α) (l : List β), List.foldl (fun b x => f b) a l = f^[l.length] a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∈ t₂ → (t₁ ∩ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.CategoryTheory.Whiskering
/-- Auxiliary definition for `whiskeringLeft₃`.  -/
CategoryTheory.Functor.whiskeringLeft₃ObjMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    (C₃ : Type u_3) →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          (D₃ : Type u_6) →
            [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} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            (F₁ : CategoryTheory.Functor C₁ D₁) →
                              {F₂ F₂' : CategoryTheory.Functor C₂ D₂} →
                                (F₂ ⟶ F₂') →
                                  (CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂ ⟶
                                    CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂')
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.fieldEquivOfAlgEquivHom_apply : ∀ {A : Type u_8} {B : Type u_9} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (K : Type u_10)
  (L : Type u_11) [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : Algebra B L]
  [inst_7 : IsFractionRing A K] [inst_8 : IsFractionRing B L] [inst_9 : Algebra A L] [inst_10 : IsScalarTower A B L]
  [inst_11 : Algebra K L] [inst_12 : IsScalarTower A K L] (f : B ≃ₐ[A] B),
  (IsFractionRing.fieldEquivOfAlgEquivHom K L) f = IsFractionRing.fieldEquivOfAlgEquiv K L L f
-- Mathlib.Geometry.Euclidean.Altitude
/-- A vertex lies in the corresponding altitude.  -/
Affine.Simplex.mem_altitude : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)), s.points i ∈ s.altitude i
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSingletonClass α] (f : α → β) (g : ℕ → α)
  (n : ℕ),
  MeasureTheory.simpleFuncAux✝ f g n.succ =
    MeasureTheory.SimpleFunc.piecewise {g n} ⋯ (MeasureTheory.SimpleFunc.const α (f (g n)))
      (MeasureTheory.simpleFuncAux✝ f g n)
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_eq : ∀ (a b : UInt32), a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256
-- Lean.Environment
Lean.ConstantKind.induct : Lean.ConstantKind
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map : ∀ (X : CategoryTheory.Cat)
  {X_1 Y : ↑(CategoryTheory.Quiv.of (SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve ↑X))))}
  (a : X_1 ⟶ Y), (SSet.OneTruncation₂.ofNerve₂.natIso.hom.app X).map a = SSet.OneTruncation₂.nerveHomEquiv a
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- If a function is locally `r`-Hölder and locally `t`-Hölder,
then it is locally `s`-Hölder for `r ≤ s ≤ t`.  -/
HolderOnWith.exists_holderOnWith_of_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {s t : NNReal} {A : Set X},
  (∃ C, HolderOnWith C r f A) → (∃ C, HolderOnWith C t f A) → r ≤ s → s ≤ t → ∃ C, HolderOnWith C s f A
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank.eq_1 : ∀ {α : Type u_1} (M : Matroid α), M.eRank = ⨆ B, (↑B).encard
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInr_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : L'.Relations _n),
  FirstOrder.Language.LHom.sumInr.onRelation val = Sum.inr val
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.constantCoeff_exp : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℚ A], PowerSeries.constantCoeff (PowerSeries.exp A) = 1
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk_im : ∀ (z : ℂ) (h : 0 < z.im), { coe := z, coe_im_pos := h }.im = z.im
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
_private.Mathlib.RingTheory.Polynomial.UniqueFactorization.0.MvPolynomial.uniqueFactorizationMonoid_of_fintype : ∀ (σ : Type v) {D : Type u} [inst : CommRing D] [UniqueFactorizationMonoid D] [Finite σ],
  UniqueFactorizationMonoid (MvPolynomial σ D)
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_coeff_degree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {i : ℕ}, p.degree = ↑i → p.integralNormalization.coeff i = 1
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  {x y : A.Hom B}, x.val = y.val → x = y
-- Init.Data.List.Lemmas
List.tail_reverse : ∀ {α : Type u_1} {l : List α}, l.reverse.tail = l.dropLast.reverse
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  IsCompact (quasispectrum R a)
-- Mathlib.Order.RelSeries
RelSeries.apply_zero : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.toFun 0 = p.head
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.normedAddGroup : {E : Type u_1} → [inst : NormedAddGroup E] → {s : AddSubgroup E} → NormedAddGroup ↥s
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
given matrices `J`, `J₂`.  -/
pairSelfAdjointMatricesSubmodule : {R : Type u_1} →
  {n : Type u_11} →
    [inst : CommRing R] → [Fintype n] → Matrix n n R → Matrix n n R → [DecidableEq n] → Submodule R (Matrix n n R)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] [inst_3 : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)}
  {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ ↑(t.insertMany! l)},
  (↑(t.insertMany! l)).get k h' = t.get k ⋯
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.length_pos_iff : ∀ {n : ℕ} (c : Composition n), 0 < c.length ↔ 0 < n