mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.closedIhom_obj_map : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F Y : CategoryTheory.Functor D C) {X Y_1 : D} (f : X ⟶ Y_1),
  (F.closedIhom.obj Y).map f =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.inv (F.map f))).app (Y.obj X))
      ((CategoryTheory.ihom (F.obj Y_1)).map (Y.map f))
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.comp_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
  (p : Submodule R₃ M₃) (h : ∀ (b : M₂), g b ∈ p),
  LinearMap.codRestrict p g h ∘ₛₗ f = LinearMap.codRestrict p (g ∘ₛₗ f) ⋯
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.CommMonCat.Hom.mk.sizeOf_spec : ∀ {A B : CommMonCat} (hom' : ↑A →* ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.iteratedDeriv_odd_cos : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Complex.cos = (-1) ^ (n + 1) * Complex.sin
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_coe : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {F : Type u_14} [inst_6 : FunLike F M M₃] [inst_7 : SemilinearMapClass F σ M M₃] {f : F}, ⇑↑f = ⇑f
-- Mathlib.NumberTheory.ModularForms.NormTrace
/-- The norm of a modular form, as a modular form.  -/
ModularForm.norm : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F →
        [inst : FunLike F UpperHalfPlane ℂ] →
          {k : ℤ} →
            [𝒢.IsFiniteRelIndex ℋ] →
              [ℋ.HasDetPlusMinusOne] → [ModularFormClass F 𝒢 k] → ModularForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.fromThinSkeleton_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : Quiver.IsThin C]
  (a : Quotient (CategoryTheory.isIsomorphicSetoid C)), (CategoryTheory.ThinSkeleton.fromThinSkeleton C).obj a = a.out
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flippingEquiv_symm_apply_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) {X Y : C} (f : X ⟶ Y) (j : D),
  ((CategoryTheory.Functor.flippingEquiv.symm F).map f).app j = (F.obj j).map f
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.card_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Nat.card α = 4 → Nat.card ↥(alternatingGroup α) = 12
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite_one : Polynomial.hermite 1 = Polynomial.X
-- Init.Data.Array.Lemmas
Array.getElem!_set!_self : ∀ {α : Type u_1} [inst : Inhabited α] (xs : Array α) (i : ℕ) (x : α), i < xs.size → (xs.set! i x)[i]! = x
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
EuclideanSpace.volume_ball : ∀ (ι : Type u_1) [Nonempty ι] [inst : Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ),
  MeasureTheory.volume (Metric.ball x r) =
    ENNReal.ofReal r ^ Fintype.card ι *
      ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.add_eq_add : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanHom 2 A B f → ∀ {a b c d : α}, a ∈ A → b ∈ A → c ∈ A → d ∈ A → a + b = c + d → f a + f b = f c + f d
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
/-- The matrix $[a, -b; b, a]$ (inspired by multiplication by a complex number); it is an element of
$GL_2(R)$ if `a ^ 2 + b ^ 2` is nonzero.  -/
Matrix.planeConformalMatrix : {R : Type u_1} → [inst : Field R] → (a b : R) → a ^ 2 + b ^ 2 ≠ 0 → GL (Fin 2) R
-- Mathlib.Algebra.Order.Ring.Pow
/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.

This is a version for a linear ordered semiring.  -/
Commute.pow_add_mul_le_add_pow : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {a b : R},
  Commute a b → 0 ≤ a → 0 ≤ 2 * a + b → ∀ (n : ℕ), a ^ n + ↑n * a ^ (n - 1) * b ≤ (a + b) ^ n
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility : ∀ {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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  [inst_6 : CategoryTheory.HasWeakSheafify J A] [inst_7 : CategoryTheory.HasWeakSheafify K A]
  (F : CategoryTheory.Functor Dᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (G.op.comp F))
      ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom =
    G.op.whiskerLeft (CategoryTheory.toSheafify K F)
-- Mathlib.Geometry.Manifold.Submersion
/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `(u,v) ↦ u`.
This version does not assume that `f` maps `φ.source` to `ψ.source`,
but that `f` is continuous at `x`.  -/
Manifold.IsSubmersionAtOfComplement.mk_of_continuousAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M},
  ContinuousAt f x →
    ∀ (equiv : E ≃L[𝕜] E'' × F) (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
      x ∈ domChart.source →
        f x ∈ codChart.source →
          domChart ∈ IsManifold.maximalAtlas I n M →
            codChart ∈ IsManifold.maximalAtlas J n N →
              Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv)
                  (domChart.extend I).target →
                Manifold.IsSubmersionAtOfComplement F I J n f x
-- Mathlib.Order.OrderIsoNat
/-- An order embedding from `ℕ` to itself with a specified range  -/
Nat.orderEmbeddingOfSet : (s : Set ℕ) → [Infinite ↑s] → [DecidablePred fun x => x ∈ s] → ℕ ↪o ℕ
-- Mathlib.Condensed.Discrete.Module
/-- Auxiliary definition for `functorIsoDiscrete`.  -/
CondensedMod.LocallyConstant.functorIsoDiscreteComponents : (R : Type (u + 1)) →
  [inst : Ring R] →
    (M : ModuleCat R) → (Condensed.discrete (ModuleCat R)).obj M ≅ (CondensedMod.LocallyConstant.functor R).obj M
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- Use `Algebra.QuasiFinite.of_restrictScalars` instead for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.of_restrictScalars : ∀ (R : Type u_1) (S : Type u_2) {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal T)
  [inst_7 : q.IsPrime] [Algebra.WeaklyQuasiFiniteAt R q], Algebra.WeaklyQuasiFiniteAt S q
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_id : ∀ {Z : AlgebraicGeometry.Scheme} (I : Z.IdealSheafData), I.comap (CategoryTheory.CategoryStruct.id Z) = I
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramState.mk.inj : ∀ {sub : String} {embeds : Std.HashMap String (String × ProofWidgets.Html)} {sub_1 : String}
  {embeds_1 : Std.HashMap String (String × ProofWidgets.Html)},
  { sub := sub, embeds := embeds } = { sub := sub_1, embeds := embeds_1 } → sub = sub_1 ∧ embeds = embeds_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Lift an `add_monoid_hom` to `Finset` via `image`  -/
Finset.imageAddMonoidHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : DecidableEq α] →
        [inst_1 : DecidableEq β] →
          [inst_2 : AddZeroClass α] →
            [inst_3 : AddZeroClass β] → [inst_4 : FunLike F α β] → [AddMonoidHomClass F α β] → F → Finset α →+ Finset β
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_of : ∀ {α : Type u_1} (x : α), FreeMonoid.toList (FreeMonoid.of x) = [x]
-- Mathlib.Topology.Constructions.SumProd
/-- If `Sum.elim f g` is inducing, `closure (range f)` and `range g` must be disjoint.
This is an auxiliary result towards proving `isInducing_sumElim`.  -/
Topology.IsInducing.disjoint_of_sumElim_aux : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsInducing (Sum.elim f g) → Disjoint (closure (Set.range f)) (Set.range g)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of a set of congruence relations is the same as the smallest congruence relation
containing the supremum of the set's image under the map to the underlying binary relation.  -/
Con.sSup_def : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), sSup S = conGen (sSup (DFunLike.coe '' S))
-- Mathlib.CategoryTheory.ConnectedComponents
/-- The connected component of an object in a category.  -/
CategoryTheory.ConnectedComponents.mk : {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → J → CategoryTheory.ConnectedComponents J
-- Init.Data.Nat.Lemmas
Nat.mod_add_mod : ∀ (m n k : ℕ), (m % n + k) % n = (m + k) % n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
trapezoidal_error.eq_1 : ∀ (f : ℝ → ℝ) (N : ℕ) (a b : ℝ), trapezoidal_error f N a b = trapezoidal_integral f N a b - ∫ (x : ℝ) in a..b, f x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOnFilter.inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α},
  TendstoUniformlyOnFilter f g l l' → TendstoUniformlyOnFilter f⁻¹ g⁻¹ l l'
-- Mathlib.Data.Nat.Choose.Central
/-- An exponential lower bound on the central binomial coefficient.
This bound is of interest because it appears in
[Tochiori's refinement of Erdős's proof of Bertrand's postulate](tochiori_bertrand).
 -/
Nat.four_pow_lt_mul_centralBinom : ∀ (n : ℕ), 4 ≤ n → 4 ^ n < n * n.centralBinom
-- Mathlib.Computability.EpsilonNFA
εNFA.evalFrom_nil : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ), M.evalFrom S [] = M.εClosure S
-- Mathlib.Data.Fintype.Card
Fintype.card_fin_lt_of_le : ∀ {m n : ℕ}, m ≤ n → Fintype.card { i // ↑i < m } = m
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.Nonsingular.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (x y : R),
  W.Nonsingular x y =
    (W.Equation x y ∧ (Polynomial.evalEval x y W.polynomialX ≠ 0 ∨ Polynomial.evalEval x y W.polynomialY ≠ 0))
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] {g : BoundedOrderHom β γ}
  {f₁ f₂ : BoundedOrderHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restriction_d : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (x x_1 : ι),
  (K.restriction e).d x x_1 = K.d (e.f x) (e.f x_1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : SizeOf C] (X : C) [addGrp : CategoryTheory.AddGrpObj X],
  sizeOf { X := X, addGrp := addGrp } = 1 + sizeOf X + sizeOf addGrp
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyEtale.of_comp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.FormallyUnramified → (g.comp f).FormallyEtale → g.FormallyEtale
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Algebra.IsAlgebraic.isTranscendenceBasis_of_lift_le_trdeg : ∀ {ι : Type u} (R : Type u_1) {A : Type w} (x : ι → A) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [NoZeroDivisors A] [FaithfulSMul R A] [Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A],
  Algebra.trdeg R A < Cardinal.aleph0 →
    Cardinal.lift.{w, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, w} (Algebra.trdeg R A) → IsTranscendenceBasis R x
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
/-- The category of algebras over an additive monad on a preadditive category is preadditive.  -/
CategoryTheory.Monad.algebraPreadditive : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (T : CategoryTheory.Monad C) → [T.Additive] → CategoryTheory.Preadditive T.Algebra
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inter_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)], (E.inter F).I₀ = (E.I₀ × F.1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.SetTheory.Cardinal.Order
/-- A variant of `Cardinal.lift_mk_le` with specialized universes.
Because Lean often cannot realize it should use this specialization itself,
we provide this statement separately so you don't have to solve the specialization problem either.
 -/
Cardinal.lift_mk_le' : ∀ {α : Type u} {β : Type v},
  Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ↪ β)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsLimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.ReflectsLimitsOfShape J F)
      CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsLimitsOfShape._autoParam →
    CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.EvalTacticFailure.mk.inj : ∀ {exception : Lean.Exception} {state : Lean.Elab.Tactic.SavedState} {exception_1 : Lean.Exception}
  {state_1 : Lean.Elab.Tactic.SavedState},
  { exception := exception, state := state } = { exception := exception_1, state := state_1 } →
    exception = exception_1 ∧ state = state_1
-- Mathlib.Algebra.Opposites
MulOpposite.op_injective : ∀ {α : Type u_1}, Function.Injective MulOpposite.op
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.typelessBinder? : Lean.Syntax → Option (Array Lean.Ident × Lean.BinderInfo)
-- Std.Tactic.BVDecide.Syntax
/-- Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the
Lean process.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.graphviz : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
le_mulRothNumber_product : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Monoid α] [inst_2 : DecidableEq β] [inst_3 : Monoid β]
  (s : Finset α) (t : Finset β), mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)
-- Mathlib.Data.List.Duplicate
List.Mem.duplicate_cons_self : ∀ {α : Type u_1} {l : List α} {x : α}, x ∈ l → List.Duplicate x (x :: l)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [Finite ι], Nat.card σ ≤ Nat.card ι
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₁ = CategoryTheory.Limits.biprod.inl
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
  {g : E → F →L[𝕜] G} {g' : E →L[𝕜] F →L[𝕜] G} {s : Set E} {x : E} [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  HasFDerivWithinAt f f' s x →
    HasFDerivWithinAt g g' s x →
      HasFDerivWithinAt (fun x => (f x).compContinuousLinearMap (g x))
        (ContinuousAlternatingMap.compContinuousLinearMapCLM (g x) ∘SL f' +
          (f x).fderivCompContinuousLinearMap (g x) ∘SL g')
        s x
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bindOnSupport_bindOnSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : (a : α) → a ∈ p.support → PMF β)
  (g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ),
  (p.bindOnSupport f).bindOnSupport g = p.bindOnSupport fun a ha => (f a ha).bindOnSupport fun b hb => g b ⋯
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableAt.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) → DifferentiableAt 𝕜 (fun x => ∏ i ∈ u, f i x) x
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.le_def : ∀ {E : Type u_3} [inst : Group E] {p q : GroupNorm E}, p ≤ q ↔ ⇑p ≤ ⇑q
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz' : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  (self : Derivation R A M) (a b : A), ↑self (a * b) = a • ↑self b + b • ↑self a
-- Mathlib.Analysis.Normed.Operator.Extend
/-- Extension of a linear map `f : E →ₛₗ[σ₁₂] F` to a continuous linear map `Eₗ →SL[σ₁₂] F`,
where `E` is a normed space and `F` a complete normed space, using a dense map `e : E →ₗ[𝕜] Eₗ`
together with a bound `‖f x‖ ≤ C * ‖e x‖` for all `x : E`.  -/
LinearMap.extendOfNorm : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          [inst : NormedDivisionRing 𝕜] →
            [inst_1 : NormedDivisionRing 𝕜₂] →
              {σ₁₂ : 𝕜 →+* 𝕜₂} →
                [inst_2 : AddCommGroup E] →
                  [inst_3 : SeminormedAddCommGroup Eₗ] →
                    [inst_4 : NormedAddCommGroup F] →
                      [inst_5 : Module 𝕜 E] →
                        [inst_6 : Module 𝕜₂ F] →
                          [IsBoundedSMul 𝕜₂ F] →
                            [inst_8 : Module 𝕜 Eₗ] →
                              [IsBoundedSMul 𝕜 Eₗ] → [CompleteSpace F] → (E →ₛₗ[σ₁₂] F) → (E →ₗ[𝕜] Eₗ) → Eₗ →SL[σ₁₂] F
-- Mathlib.Algebra.Notation.Prod
Prod.one_eq_mk : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N], 1 = (1, 1)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ), Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.num k) = k
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sign_touchpointWeights : ∀ {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 →
    ∀ {i j : Fin (n + 1)},
      i ≠ j → SignType.sign (s.touchpointWeights signs i j) = SignType.sign (s.excenterWeights signs j)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₂ : Lean.ParserDescr
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailId : Lean.Order.MonadTail Id
-- Lean.Elab.Term.TermElabM
/-- Metavariable represents a hole whose elaboration has been postponed.  -/
Lean.Elab.Term.SyntheticMVarKind.postponed : Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.card_pairSet_le : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T],
  1 < a → ↑(PairReduction.pairSet J a c).card ≤ a * ↑J.card
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_sSup_iff : ∀ {α : Type u_1} [inst : LE α] {S : Set (UpperSet α)} {a : α}, a ∈ sSup S ↔ ∀ s ∈ S, a ∈ s
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Let `E` be a real, finite-dimensional, inner product space and `x` be a point of `E`. A function `f`
on `E` is harmonic at `x` if it is two times continuously `ℝ`-differentiable and if its Laplacian
vanishes in a neighborhood of `x`.
 -/
InnerProductSpace.HarmonicAt : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] → {F : Type u_2} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (E → F) → E → Prop
-- Mathlib.Algebra.Group.Defs
InvOneClass.toInv : {G : Type u_2} → [self : InvOneClass G] → Inv G
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.tendsto_inv₀_cobounded' : ∀ {α : Type u_1} [inst : NormedDivisionRing α], Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.trans_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)}
  (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) (x : ↑unitInterval × X),
  (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)