mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Util.UnionFind
Aesop.UnionFind.addArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Aesop.UnionFind α → Aesop.UnionFind α
-- Init.Data.List.Nat.Sublist
List.prefix_take_le_iff : ∀ {α : Type u_1} {i j : ℕ} {xs : List α}, i < xs.length → (List.take i xs <+: List.take j xs ↔ i ≤ j)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject.HoCat C),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.HoCat.adj.unit.app X)
-- Lean.Parser.Basic
Lean.Parser.ParserState.keepPrevError : Lean.Parser.ParserState → ℕ → String.Pos.Raw → Option Lean.Parser.Error → ℕ → Lean.Parser.ParserState
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.brecOn : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  {motive : (a a_1 : (MvQPF.P F).W α) → MvQPF.WEquiv a a_1 → Prop} {a a_1 : (MvQPF.P F).W α} (t : MvQPF.WEquiv a a_1),
  (∀ (a a_2 : (MvQPF.P F).W α) (t : MvQPF.WEquiv a a_2), MvQPF.WEquiv.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioo_succ_right_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioo a (Order.succ b) = Set.Ioc a b
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.mulHom_apply : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (x y : GradedTensorProduct R 𝒜 ℬ),
  ((GradedTensorProduct.mulHom 𝒜 ℬ) x) y =
    (GradedTensorProduct.auxEquiv R 𝒜 ℬ).symm
      (((TensorProduct.gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) x))
        ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) y))
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.toDistribMulActionHom_eq_coe : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), f.toDistribMulActionHom = ↑f
-- Init.Prelude
/-- The notation typeclass for heterogeneous multiplication.
This enables the notation `a * b : γ` where `a : α`, `b : β`.
 -/
HMul : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Algebra.Jordan.Basic
commute_lmul_sq_rmul : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [IsJordan A] (a : A),
  Commute (AddMonoid.End.mulLeft (a * a)) (AddMonoid.End.mulRight a)
-- Mathlib.Order.Std
LinearOrder.OfStdArgs.toPartialOrderArgs : {α : Type u_1} → LinearOrder.OfStdArgs α → PartialOrder.OfStdArgs α
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.left_assoc' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (Bimod.TensorBimod.X P Q))
      (Bimod.TensorBimod.actLeft P Q) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator R.X R.X (Bimod.TensorBimod.X P Q)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.TensorBimod.actLeft P Q))
        (Bimod.TensorBimod.actLeft P Q))
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → FunLike (BoundedLatticeHom α β) α β
-- Mathlib.Data.SetLike.Basic
SetLike.forall : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : ↥p → Prop},
  (∀ (x : ↥p), q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, h⟩
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The **Lubell-Yamamoto-Meshalkin inequality**, also known as the **LYM inequality**.

If `𝒜` is an antichain, then the sum of `(#α.choose #s)⁻¹` over `s ∈ 𝒜` is less than `1`.  -/
Finset.lubell_yamamoto_meshalkin_inequality_sum_inv_choose : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : Fintype α] {𝒜 : Finset (Finset α)},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 → ∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ 1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_pp_pf_overlap : ∀ {R : Type u_1} [inst : CommSemiring R] {a₂ b₂ c : R} {ea eb e : ℕ} (x : R),
  ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.scalingScaleOf_pos : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] (K : ℝ), 0 < IsUnifLocDoublingMeasure.scalingScaleOf μ K
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- Given `x, y : E ⊗ F ⊗ G`, `x = y` iff `⟪a ⊗ₜ b ⊗ₜ c, x⟫ = ⟪a ⊗ₜ b ⊗ₜ c, y⟫` for all `a, b, c`.

See also `ext_iff_inner_left_threefold'` for when `x, y : E ⊗ (F ⊗ G)`.  -/
TensorProduct.ext_iff_inner_left_threefold : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G},
  x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) x = inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) y
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Constructor for morphisms from the point of a colimit cofan.  -/
CategoryTheory.Limits.Cofan.IsColimit.desc : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : β → C} →
        {c : CategoryTheory.Limits.Cofan F} →
          CategoryTheory.Limits.IsColimit c → {A : C} → ((i : β) → F i ⟶ A) → (c.pt ⟶ A)
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.DTreeMap.Raw.Const.unitOfList l cmp).WF
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_comp_neg_X : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
  (p.comp (-Polynomial.X)).roots = Multiset.map (fun x => -x) p.roots
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_snd : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2], ⇑AffineMap.snd = Prod.snd
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_injective_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f → Function.Injective (FirstOrder.Language.Substructure.map f)
-- Init.Data.String.PosRaw
String.Pos.Internal.subImpl : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Data.Seq.Defs
Stream'.Seq.omap.eq_1 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : β → γ), Stream'.Seq.omap f none = none
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_3.splitter : {w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    (motive : Option (aig.RefVec w) → Sort u_1) →
      (x : Option (aig.RefVec w)) → ((vec : aig.RefVec w) → motive (some vec)) → (Unit → motive none) → motive x
-- Mathlib.GroupTheory.Subgroup.Simple
MulEquiv.isSimpleGroup : ∀ {G : Type u_1} [inst : Group G] {H : Type u_3} [inst_1 : Group H] [IsSimpleGroup H] (e : G ≃* H), IsSimpleGroup G
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_insert : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℤ)
  (x : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
  k ≥ 0 →
    p.NonnegCoeffs →
      Lean.Grind.Linarith.Poly.denoteN ctx (Lean.Grind.Linarith.Poly.insert k x p) =
        k.toNat • Lean.Grind.Linarith.Var.denote ctx x + Lean.Grind.Linarith.Poly.denoteN ctx p
-- Mathlib.Algebra.Star.Conjneg
conjneg_bijective : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R],
  Function.Bijective conjneg
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The expression being certified.  -/
Mathlib.Tactic.Determinant.Cert.subject : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Cert rα → Q(«$α»)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instIsIsoHomFromCommaOfIsIso : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [inst_7 : CategoryTheory.IsIso i],
  CategoryTheory.IsIso (CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i)
-- Mathlib.Order.Interval.Set.LinearOrder
/-- We cannot replace `<` by `≤` in the hypotheses.
Otherwise for `b < a = d < c` the l.h.s. is `∅` and the r.h.s. is `{a}`.
 -/
Set.Icc_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  min a b < max c d → min c d < max a b → Set.Icc a b ∪ Set.Icc c d = Set.Icc (min a c) (max b d)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.lift_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (g : (i : ι) → G i →ₗ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} (x : G i),
  (Module.DirectLimit.lift R ι G f g Hg) ((Module.DirectLimit.of R ι G f i) x) = (g i) x
-- Lean.Parser.Term
/-- `let_fun x := v; b` is deprecated syntax sugar for `have x := v; b`.
 -/
Lean.Parser.Term.let_fun : Lean.Parser.Parser
-- Lean.Level
Lean.Level.param.injEq : ∀ (a a_1 : Lean.Name), (Lean.Level.param a = Lean.Level.param a_1) = (a = a_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey_modify_eq_maxKey : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : β → β}
  {he : (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false},
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey he = t.maxKey ⋯
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.of_subgroup_of_conjugate : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} {H : Subgroup G},
  MulAction.IsBlock (↥H) B →
    ∀ (g : G), MulAction.IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_of_le : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} (l : Filter α),
  (∀ (x : α), ‖f x‖ ≤ ‖g x‖) → f =O[l] g
-- Mathlib.FieldTheory.IsSepClosed
/-- If `k` is perfect, `K` is an algebraic closure of `k`,
then it is also a separable closure of `k`.  -/
IsSepClosure.of_isAlgClosure_of_perfectField : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra k K] [IsAlgClosure k K]
  [PerfectField k], IsSepClosure k K
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.spanFinBasis.span : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I),
  ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.spanFinBasis C s))
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Explicit bound on `HD (dist)`. This means that when looking for minimizers it will
be sufficient to look for functions with `HD(f)` bounded by this bound.  -/
GromovHausdorff.HD_candidatesBDist_le : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [inst_2 : CompactSpace X]
  [inst_3 : CompactSpace Y] [inst_4 : Nonempty X] [inst_5 : Nonempty Y],
  GromovHausdorff.HD (GromovHausdorff.candidatesBDist X Y) ≤ Metric.diam Set.univ + 1 + Metric.diam Set.univ
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.surjective_of_isDominant_of_isClosed_range : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f],
  IsClosed (Set.range ⇑f) → AlgebraicGeometry.Surjective f
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrowCone_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C}
  (c : CategoryTheory.Limits.Cone K) (F : CategoryTheory.Functor C D) {X : D} (f : X ⟶ F.obj c.pt) (j : J),
  (c.toStructuredArrowCone F f).π.app j = CategoryTheory.StructuredArrow.homMk (c.π.app j) ⋯
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_ne_zero`.  -/
hammingDist_ne_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  hammingDist x y ≠ 0 ↔ x ≠ y
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.toFun.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f f_1 : ContDiffBump c), f = f_1 → ∀ (a a_1 : E), a = a_1 → ↑f a = ↑f_1 a_1
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Asymptotics.IsEquivalent.summable_iff_nat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ℕ → E},
  Asymptotics.IsEquivalent Filter.atTop f g → (Summable f ↔ Summable g)
-- Init.Data.UInt.Bitwise
UInt16.toFin_xor : ∀ (a b : UInt16), (a ^^^ b).toFin = a.toFin ^^^ b.toFin
-- Mathlib.Order.Interval.Set.Image
MonotoneOn.image_Ici_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  MonotoneOn f (Set.Ici a) → f '' Set.Ici a ⊆ Set.Ici (f a)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE!_eq_get!_getKeyGE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} [inst_1 : Inhabited α],
  Std.DTreeMap.Internal.Impl.getKeyGE! k t = (Std.DTreeMap.Internal.Impl.getKeyGE? k t).get!
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_eq_flip_reflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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) (i : ι),
  P.coreflection i = P.flip.reflection i
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv_symm_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y) {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (t : P.obj X) {Z : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.shrinkYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (P.map f)) t)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYoneda.{w, v, u}.map f.unop)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaEquiv.symm t) h)
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- Composition in a bicategory is associative.  -/
CategoryTheory.Bicategory.Strict.assoc : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associator_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Except.toBool.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (a : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (a : ε) → motive (Except.error a)),
  (match Except.error a with
    | Except.ok a => h_1 a
    | Except.error a => h_2 a) =
    h_2 a
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.eval_typesGlue : ∀ {S : CategoryTheory.Functor Type uᵒᵖ (Type u)}
  {hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S} {α : Type u}
  (f : α → S.obj (Opposite.op PUnit.{u + 1})),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.eval S α (CategoryTheory.typesGlue S hs α f))) = f
-- Init.Data.SInt.Bitwise
Int8.or_comm : ∀ (a b : Int8), a ||| b = b ||| a
-- Mathlib.Probability.Process.Filtration
MeasureTheory.measurableSet_filtrationOfSet : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {s : ι → Set Ω}
  (hsm : ∀ (i : ι), MeasurableSet (s i)) (i : ι) {j : ι}, j ≤ i → MeasurableSet (s j)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
stabilizer_univ_eq_top : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α], MulAction.stabilizer G Set.univ = ⊤
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `p` is a prime and `n` is `p`-smooth, then `p` and `n` are coprime.  -/
Nat.Prime.smoothNumbers_coprime : ∀ {p n : ℕ}, Nat.Prime p → n ∈ p.smoothNumbers → p.Coprime n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.getKey?_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.Equiv m₂ → m₁.getKey? k = m₂.getKey? k
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeLspResponse : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.Response α → IO Unit
-- Aesop.Tree.Traversal
Aesop.TreeRef : Type
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orElim'.injEq : ∀ (p₁ : Mathlib.Tactic.ITauto.Proof) (x : Lean.Name) (p₂ p₃ p₁_1 : Mathlib.Tactic.ITauto.Proof) (x_1 : Lean.Name)
  (p₂_1 p₃_1 : Mathlib.Tactic.ITauto.Proof),
  (p₁.orElim' x p₂ p₃ = p₁_1.orElim' x_1 p₂_1 p₃_1) = (p₁ = p₁_1 ∧ x = x_1 ∧ p₂ = p₂_1 ∧ p₃ = p₃_1)
-- Mathlib.Order.Interval.Set.Infinite
Set.Ioc.infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → Infinite ↑(Set.Ioc a b)
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.ext_iff_measureReal_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] {μ1 μ2 : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ1] [MeasureTheory.SigmaFinite μ2], μ1 = μ2 ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}
-- Lean.Meta.WHNF
Lean.Meta.whnfHeadPred : Lean.Expr → (Lean.Expr → Lean.MetaM Bool) → Lean.MetaM Lean.Expr
-- Init.Data.SInt.Lemmas
Int8.ofInt_int64ToInt : ∀ (x : Int64), Int8.ofInt x.toInt = x.toInt8
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.go_decl_eq : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (↑(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).result).aig.decls.size),
  (↑(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).result).aig.decls[idx] = aig.decls[idx]
-- Mathlib.RingTheory.Polynomial.Quotient
/-- Split off from `quotientEquivQuotientMvPolynomial` for speed.  -/
MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] (I : Ideal R),
  Function.LeftInverse
    (MvPolynomial.eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯)
      fun i => (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i))
    ⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I)
        (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) ⋯)
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.instIsCharPFin : ∀ (n : ℕ) [inst : NeZero n], Lean.Grind.IsCharP (Fin n) n
-- Mathlib.Algebra.Order.Hom.Basic
MulRingSeminormClass.toRingSeminormClass : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : NonAssocRing α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [MulRingSeminormClass F α β], RingSeminormClass F α β
-- Plausible.Testable
Plausible.LE.printableProp : {α : Type u_1} → [Repr α] → [inst : LE α] → {x y : α} → Plausible.PrintableProp (x ≤ y)
-- Mathlib.Data.Finset.Max
Finset.isLUB_mem : ∀ {α : Type u_2} [inst : LinearOrder α] {i : α} (s : Finset α), IsLUB (↑s) i → s.Nonempty → i ∈ s
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- If the total masses of finite measures tend to zero, then the measures tend to
zero. This formulation concerns the associated functionals on bounded continuous
nonnegative test functions. See `MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass` for
a formulation stating the weak convergence of measures.  -/
MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3}
  {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto (fun i => (μs i).mass) F (nhds 0) →
    ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (nhds 0)
-- Init.Core
/-- Moves an cast using `Eq.rec` from the function to the argument.
Note: because the motive isn't reliably detected by unification,
it needs to be provided as an explicit parameter.
 -/
apply_eqRec : ∀ {β : Sort u_1} {α : Sort u} {a : α} (motive : (b : α) → a = b → Sort v) {b : α} {h : a = b} {c : motive a ⋯ → β}
  {d : motive b h},
  Eq.rec (motive := fun b h => motive b h → β) c h d =
    c
      ((fun h_1 =>
          Eq.ndrec (motive := fun {a} =>
            (motive : (b : α) → a = b → Sort v) → {h : a = b} → {c : motive a ⋯ → β} → {d : motive b h} → motive a ⋯)
            (fun motive {h} {c} {d} => d) h_1 motive)
        ⋯)