mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_le_iff_le_comap : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (G' : SimpleGraph W),
  SimpleGraph.map (⇑f) G ≤ G' ↔ G ≤ SimpleGraph.comap (⇑f) G'
-- Mathlib.Algebra.Group.Embedding
addRightEmbedding.eq_1 : ∀ {G : Type u_1} [inst : Add G] [inst_1 : IsRightCancelAdd G] (g : G),
  addRightEmbedding g = { toFun := fun h => h + g, inj' := ⋯ }
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.str.sizeOf_spec : ∀ (s : String), sizeOf (Lean.JsonRpc.RequestID.str s) = 1 + sizeOf s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_rcc : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
        List.filter (fun e => decide ((compare e lowerBound).isGE = true ∧ (compare e upperBound).isLE = true)) t.keys
-- Mathlib.Topology.MetricSpace.Completion
/-- The distance on the completion is obtained by extending the distance on the original space,
by uniform continuity.  -/
UniformSpace.Completion.instDist : {α : Type u} → [inst : PseudoMetricSpace α] → Dist (UniformSpace.Completion α)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.funCongrLeft_comp : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} {p : Type u_11} (e₁ : m ≃ n) (e₂ : n ≃ p),
  LinearEquiv.funCongrLeft R M (e₁.trans e₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_real_iff_eq : ∀ {r s : ℝ}, (↑r).IsSt s ↔ r = s
-- Mathlib.Algebra.Group.Basic
eq_neg_iff_add_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a = -b ↔ a + b = 0
-- Mathlib.Analysis.Analytic.Basic
analyticOnNhd_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  IsOpen s → Set.EqOn f g s → (AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforwardIsoBind_inv_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (a : ((CategoryTheory.PreZeroHypercover.singleton f).bind fun x => E).I₀),
  (CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).inv.s₀ a = (Equiv.uniqueSigma fun i => E.I₀) a
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `AEMeasurable.mul` -/
AEMeasurable.fun_mul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableMul₂ M],
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i * g i) μ
-- Init.Data.Order.Lemmas
Std.instTransLeOfIsPreorder : {α : Type u} →
  [inst : LE α] → [Std.IsPreorder α] → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Divisibility.Units
/-- In a monoid, an element `a` divides an element `b` iff `a` divides all associates of `b`.  -/
Units.dvd_mul_right : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {u : αˣ}, a ∣ b * ↑u ↔ a ∣ b
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Precomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNorm_mul_linearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (f : E →L[𝕜] E) (e : E ≃ₗᵢ[𝕜] E), ‖f * ↑↑e‖ = ‖f‖
-- Mathlib.LinearAlgebra.AffineSpace.MidpointZero
lineMap_one_half : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing R] [inst_1 : CharZero R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (a b : P), (AffineMap.lineMap a b) (1 / 2) = midpoint R a b
-- Mathlib.NumberTheory.NumberField.DedekindZeta
NumberField.dedekindZeta_residue_def : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.dedekindZeta_residue K =
    2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          NumberField.Units.regulator K *
        ↑(NumberField.classNumber K) /
      (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|)
-- Mathlib.CategoryTheory.Endomorphism
/-- Assist the typechecker by expressing a morphism `X ⟶ X` as a term of `CategoryTheory.End X`.  -/
CategoryTheory.End.of : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → {X : C} → (X ⟶ X) → CategoryTheory.End X
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- **Bernoulli's inequality** for real exponents, non-strict version: for `1 ≤ p` and `-1 ≤ s`
we have `1 + p * s ≤ (1 + s) ^ p`.  -/
one_add_mul_self_le_rpow_one_add : ∀ {s : ℝ}, -1 ≤ s → ∀ {p : ℝ}, 1 ≤ p → 1 + p * s ≤ (1 + s) ^ p
-- Std.Http.Data.Headers.Name
/-- Standard Host header name
 -/
Std.Http.Header.Name.host : Std.Http.Header.Name
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The exceptional split Lie algebra of type g₂.  -/
LieAlgebra.g₂ : (R : Type u) → [CommRing R] → Type u
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X))
  (homEquiv_comp :
    autoParam
      (∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
        homEquiv (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g))
      CategoryTheory.Functor.RepresentableBy.homEquiv_comp._autoParam)
  (homEquiv_1 : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X))
  (homEquiv_comp_1 :
    autoParam
      (∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
        homEquiv_1 (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv_1 g))
      CategoryTheory.Functor.RepresentableBy.homEquiv_comp._autoParam),
  ({ homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } =
      { homEquiv := homEquiv_1, homEquiv_comp := homEquiv_comp_1 }) =
    (homEquiv = homEquiv_1)
-- Mathlib.Dynamics.OmegaLimit
/-- **Alias** of `mem_omegaLimit_singleton_iff_mapClusterPt`.

---

An element `y` is in the ω-limit of `x` w.r.t. `f` if the forward
images of `x` frequently (w.r.t. `f`) falls within an arbitrary neighbourhood of `y`.  -/
mem_omegaLimit_singleton_iff_map_cluster_point : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (x : α)
  (y : β), y ∈ omegaLimit f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.mono_radius : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε δ : NNReal} {s N : Set X},
  ε ≤ δ → Metric.IsCover ε s N → Metric.IsCover δ s N
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.ext : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m m' : MeasureTheory.AddContent G C},
  (∀ (s : Set α), m s = m' s) → m = m'
-- Init.Data.String.Basic
String.Pos.byte.eq_1 : ∀ {s : String} (pos : s.Pos) (h : pos ≠ s.endPos), pos.byte h = pos.toSlice.byte ⋯
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : Group N} {inst_1 : Group E} {inst_2 : Group G} {inl : N →* E}
  {rightHom : E →* G} {inl_injective : Function.Injective ⇑inl} {range_inl_eq_ker_rightHom : inl.range = rightHom.ker}
  {rightHom_surjective : Function.Surjective ⇑rightHom} {inl_1 : N →* E} {rightHom_1 : E →* G}
  {inl_injective_1 : Function.Injective ⇑inl_1} {range_inl_eq_ker_rightHom_1 : inl_1.range = rightHom_1.ker}
  {rightHom_surjective_1 : Function.Surjective ⇑rightHom_1},
  { inl := inl, rightHom := rightHom, inl_injective := inl_injective,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
      { inl := inl_1, rightHom := rightHom_1, inl_injective := inl_injective_1,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom_1, rightHom_surjective := rightHom_surjective_1 } →
    inl = inl_1 ∧ rightHom = rightHom_1
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_poly_eq_self : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s →
    ∀ {P : Polynomial F}, P.degree < ↑s.card → ((Lagrange.interpolate s v) fun i => Polynomial.eval (v i) P) = P
-- Mathlib.Data.Complex.Basic
Complex.div_im : ∀ (z w : ℂ), (z / w).im = z.im * w.re / Complex.normSq w - z.re * w.im / Complex.normSq w
-- Lean.MetavarContext
/-- Level metavariable declarations.  -/
Lean.MetavarContext.lDecls : Lean.MetavarContext → Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldr.eq_def : ∀ {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) (x : RBTree.RBNode α) (x_1 : σ),
  RBTree.RBNode.foldr f x x_1 =
    match x, x_1 with
    | RBTree.RBNode.nil, b => b
    | RBTree.RBNode.node c l v r, b => RBTree.RBNode.foldr f l (f v (RBTree.RBNode.foldr f r b))
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.const_smul₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddCommMonoid α]
  [inst_1 : DivisionSemiring γ] [inst_2 : Module γ α],
  Function.Periodic f c → ∀ (a : γ), Function.Periodic (fun x => f (a • x)) (a⁻¹ • c)
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.star_self_mem : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A), star x ∈ StarAlgebra.elemental R x
-- Mathlib.Algebra.Category.ModuleCat.AB
instAB5ModuleCat : ∀ (R : Type u) [inst : Ring R], CategoryTheory.AB5 (ModuleCat R)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_norm_norm`. -/
Asymptotics.IsLittleO.norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, f' =o[l] g' → (fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖
-- Lean.Util.LeanOptions
Lean.instHAppendLeanOptionsArrayLeanOption : HAppend Lean.LeanOptions (Array Lean.LeanOption) Lean.LeanOptions
-- Init.Data.SInt.Lemmas
Int64.mod_one : ∀ {a : Int64}, a % 1 = 0
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite_map : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] {n : ℕ} [inst_7 : NeZero n] (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂)
  (hf : Function.Injective ⇑f) (i : Fin (n + 1)), (s.map f hf).faceOpposite i = (s.faceOpposite i).map f hf
-- Mathlib.FieldTheory.Minpoly.Basic
/-- If a monic polynomial `p : A[X]` of degree `n` annihilates an element `x` in an `A`-algebra `B`,
such that `{xⁱ | 0 ≤ i < n}` is linearly independent over `A`, then `p` is the minimal polynomial
of `x` over `A`.  -/
minpoly.eq_of_linearIndependent : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic →
    (Polynomial.aeval x) p = 0 → ∀ (n : ℕ), p.degree = ↑n → (LinearIndependent A fun i => x ^ ↑i) → minpoly A x = p
-- Mathlib.CategoryTheory.Sites.Continuous
/-- To show a functor `F : C ⥤ D` is continuous for the topologies generated by
precoverage `J` and `K`, it suffices to show that the image of every `J`-covering
is a `K`-covering, if `F` preserves pairwise pullbacks of `J`-coverings.  -/
CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.Precoverage C) (K : CategoryTheory.Precoverage D)
  [J.IsStableUnderBaseChange] [J.HasPullbacks] [K.IsStableUnderBaseChange] [K.HasPullbacks] [J.PullbacksPreservedBy F],
  J ≤ CategoryTheory.Precoverage.comap F K → F.IsContinuous J.toGrothendieck K.toGrothendieck
-- Plausible.Testable
Plausible.PrintableProp.printProp : (p : Prop) → [self : Plausible.PrintableProp p] → String
-- Mathlib.Order.CompleteLattice.Lemmas
le_iSup_inf_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f g : ι → α), ⨆ i, f i ⊓ g i ≤ (⨆ i, f i) ⊓ ⨆ i, g i
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousAt.div'` -/
ContinuousAt.fun_div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun i => f i / g i) x
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_neg : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g : M → F} {x : M}, d% (-g) x = -d% g x
-- Mathlib.Algebra.Group.Defs
AddCommMagma.mk : {G : Type u} → [toAdd : Add G] → (∀ (a b : G), a + b = b + a) → AddCommMagma G
-- Aesop.Tree.State
Aesop.MVarClusterRef.markSubtreeIrrelevant : Aesop.MVarClusterRef → BaseIO Unit
-- Lean.Meta.Basic
/-- Return `mvarId` declaration in the current metavariable context.
Throw an exception if `mvarId` is not declared in the current metavariable context.
 -/
Lean.MVarId.getDecl : Lean.MVarId → Lean.MetaM Lean.MetavarDecl
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.isAdjMatrix_iff_hadamard : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq V] [inst_1 : MonoidWithZero α] [IsLeftCancelMulZero α]
  {A : Matrix V V α}, A.IsAdjMatrix ↔ A.hadamard A = A ∧ A.IsSymm ∧ Matrix.hadamard 1 A = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mk.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ μ_1 : MeasureTheory.Measure α}
  (e_μ : μ = μ_1) (f f_1 : α → β) (e_f : f = f_1) (hf : MeasureTheory.AEStronglyMeasurable f μ) (a a_1 : α),
  a = a_1 → MeasureTheory.AEStronglyMeasurable.mk f hf a = MeasureTheory.AEStronglyMeasurable.mk f_1 ⋯ a_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Ψ₂Sq_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 4 ≠ 0 → 0 < W.Ψ₂Sq.natDegree
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_eq_sum_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [inst_1 : ProbabilityTheory.IsSFiniteKernel η],
  κ.compProd η =
    ProbabilityTheory.Kernel.sum fun n => ProbabilityTheory.Kernel.sum fun m => (κ.seq n).compProd (η.seq m)
-- Std.Data.Iterators.Lemmas.Consumers.Set
_private.Std.Data.Iterators.Lemmas.Consumers.Set.0.Std.Iter.toHashSet.eq_1 : ∀ {α β : Type w} [inst : BEq β] [inst_1 : Hashable β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id Id]
  (it : Std.Iter β), it.toHashSet = it.toIterM.toHashSet.run
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.const_smul : ∀ {𝕜 : 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'] {f : M → E'} (s : 𝕜), MDiff f → MDiff (s • f)
-- Mathlib.Data.Nat.Factorial.BigOperators
Nat.monotone_factorial : Monotone Nat.factorial
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_zero : ∀ (n : ℕ), n.descFactorial 0 = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip)
  (X Y Z : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃ β).app X).app Y).app Z =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((β.hom.app X).app Z)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.toFun_eq_coe : ∀ {R : Type u_1} [inst : NonAssocRing R] (p : MulRingNorm R), p.toFun = ⇑p
-- Mathlib.Data.Fintype.Vector
Sym.Sym'.instFinite : ∀ {α : Type u_1} [Finite α] {n : ℕ}, Finite (Sym.Sym' α n)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_some : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut] {t : RBTree.RBSet α cmp},
  t.findP? cut = some y ↔ y ∈ t.toList ∧ cut y = Ordering.eq
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.eval.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N],
  MonoidHom.eval = (MonoidHom.id (M →* N)).flip
-- Mathlib.Control.Fold
Traversable.length_toList : ∀ {α : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {xs : t α},
  Traversable.length xs = (Traversable.toList xs).length
-- Lean.Util.LeanOptions
Lean.instCoeNatLeanOptionValue : Coe ℕ Lean.LeanOptionValue
-- Init.Data.SInt.Lemmas
Int64.ofInt_tdiv : ∀ {a b : ℤ},
  Int64.minValue.toInt ≤ a →
    a ≤ Int64.maxValue.toInt →
      Int64.minValue.toInt ≤ b → b ≤ Int64.maxValue.toInt → Int64.ofInt (a.tdiv b) = Int64.ofInt a / Int64.ofInt b
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_inv_inv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G),
  nndist a⁻¹ b⁻¹ = nndist a b
-- Init.Data.Vector.Basic
/-- The first element of a non-empty vector.   -/
Vector.head : {n : ℕ} → {α : Type u_1} → [NeZero n] → Vector α n → α
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.filterₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → Bool),
  m.filterₘ f =
    ⟨Std.DHashMap.Internal.withComputedSize
        (Std.DHashMap.Internal.updateAllBuckets (↑m).buckets fun l => Std.DHashMap.Internal.AssocList.filter f l),
      ⋯⟩
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- Return the rewrite tactic that performs the rewrite.  -/
_private.Mathlib.Tactic.ClickSuggestions.GRewrite.0.Mathlib.Tactic.ClickSuggestions.tacticSyntax : Mathlib.Tactic.ClickSuggestions.GrwLemma →
  Mathlib.Tactic.ClickSuggestions.GrwInfo →
    Lean.Expr → Bool → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.instFullSingle : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι} (j : ι),
  (HomologicalComplex.single V c j).Full
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.simpMatchTargetCore : Lean.MVarId → Lean.Name → Lean.Name → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {i : ℕ}
  {f g : E → F},
  ContDiff 𝕜 (↑i) f → ContDiff 𝕜 (↑i) g → iteratedFDeriv 𝕜 i (f + g) = iteratedFDeriv 𝕜 i f + iteratedFDeriv 𝕜 i g
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.recvReady' : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT (Std.CloseableChannel.Unbounded.State✝ α) m Bool
-- Mathlib.Order.Sublattice
Sublattice.mem_mk : ∀ {α : Type u_2} [inst : Lattice α] {s : Set α} {a : α} (h_sup : SupClosed s) (h_inf : InfClosed s),
  a ∈ { carrier := s, supClosed' := h_sup, infClosed' := h_inf } ↔ a ∈ s
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.match_5.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive Nat.zero) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | Nat.zero => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (ι : C → Type (max u v))
  (t : (X : C) → ι X → F.obj (Opposite.op X)) (x Y : C)
  (i : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y) (f : x ⟶ Y),
  CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t
      (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i) =
    do
    let __do_lift ← CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t i
    some ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) __do_lift)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
smoothRightMul.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] (g g_1 : G),
  g = g_1 → ∀ [inst_7 : ContMDiffMul I (↑⊤) G], smoothRightMul I g = smoothRightMul I g_1
-- Mathlib.Data.Finset.Card
Finset.card_eq_two : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.card = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instBEqCancelParams : BEq Lean.Lsp.CancelParams
-- Mathlib.Util.Superscript
/-- Parenthesizer for the script parser.  -/
Mathlib.Tactic.Superscript.scriptParser.parenthesizer : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.le_biUnionIndex : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, J ∈ π.biUnion πi → J ≤ π.biUnionIndex πi J
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.ext_of_integral_mul_prod_boundedContinuousFunction : ∀ {κ : Type u_2} {Z : Type u_3} {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)}
  [inst : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)]
  {mZ : MeasurableSpace Z} [inst_3 : TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] [inst_6 : Fintype κ]
  {μ ν : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ),
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
        ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν) →
    μ = ν
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom.mk.sizeOf_spec : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} [inst_1 : SizeOf B] {l : a ⟶ b} {r : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction l r),
  sizeOf { l := l, r := r, adj := adj } = 1 + sizeOf l + sizeOf r + sizeOf adj