mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Optimization.ValuedCSP
Function.HasMaxCutProperty.forbids_commutativeFractionalPolymorphism : ∀ {D : Type u_1} {C : Type u_3} [inst : AddCommMonoid C] [inst_1 : PartialOrder C] [IsOrderedCancelAddMonoid C]
  {f : (Fin 2 → D) → C},
  Function.HasMaxCutProperty f →
    ∀ {ω : FractionalOperation D 2}, ω.IsValid → ω.IsSymmetric → ¬Function.AdmitsFractional f ω
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.atomToCNF.eq_1 : ∀ {α : Type u_1} (output atom : α),
  Std.Sat.AIG.Decl.atomToCNF✝ output atom =
    Std.Sat.CNF.add [(output, false), (atom, true)] (Std.Sat.CNF.add [(output, true), (atom, false)] Std.Sat.CNF.empty)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.below.of_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure' x → Prop} {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W f)
  (hg : W.multiplicativeClosure' g),
  CategoryTheory.MorphismProperty.multiplicativeClosure'.below hg →
    motive g hg → CategoryTheory.MorphismProperty.multiplicativeClosure'.below ⋯
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_whiskerRight_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : Bᵒᵖ} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRight η h).unop2 = CategoryTheory.Bicategory.whiskerLeft h.unop η.unop2
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_toMatrix'_iff : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {B : LinearMap.BilinForm R₂ (ι → R₂)}, (LinearMap.BilinForm.toMatrix' B).Nondegenerate ↔ B.Nondegenerate
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_eq_default : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], a ∉ m → m.get! a = default
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_transpose : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype m] (M : Matrix m n R),
  M.transpose.mulVecLin = M.vecMulLinear
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.of_subsingleton : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Subsingleton α], p.IsHamiltonian
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofSums_parts : ∀ (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n), (Nat.Partition.ofSums n l hl).parts = Multiset.filter (fun x => x ≠ 0) l
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.basisDeriv_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (i j : σ),
  P.basisDeriv i j = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roo.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roo α},
  r.toList = (Std.Roo.Internal.iter r).toList
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {kf : CategoryTheory.Limits.KernelFork S.g}
  (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom (CategoryTheory.CategoryStruct.comp S.iCycles h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) h
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range.mk : Lean.Lsp.Position → Lean.Lsp.Position → Lean.Lsp.Range
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- A commutative additive group object is an additive group object in the category of
additive group objects.  -/
CategoryTheory.AddGrp.instAddGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {H : CategoryTheory.AddGrp C} → [CategoryTheory.IsCommAddMonObj H.X] → CategoryTheory.AddGrpObj H
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.Primes.coe_prodNatEquiv_apply : ∀ (p : Nat.Primes) (k : ℕ), ↑(Nat.Primes.prodNatEquiv (p, k)) = ↑p ^ (k + 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  [inst : Inhabited γ] {f : α → β → γ} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.map f m) k = (Option.map (f k) (Std.DHashMap.Const.get? m k)).get!
-- Mathlib.GroupTheory.Subgroup.Saturated
Subgroup.saturated_iff_zpow : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.PowSaturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.biUnion_uIoc_subset_of_mem_disjWithin : ∀ {a b : ℝ} {n : ℕ} {I : ℕ → ℝ × ℝ},
  (n, I) ∈ AbsolutelyContinuousOnInterval.disjWithin a b → ⋃ i ∈ Finset.range n, Set.uIoc (I i).1 (I i).2 ⊆ Set.uIoc a b
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instAddCommMonoid : {α : Type u_1} → {x : MeasurableSpace α} → AddCommMonoid (MeasureTheory.Measure α)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.mem_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ∈ Set.uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instElemOrbit.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {a : α},
  MulAction.instElemOrbit =
    { smul := fun m => Set.MapsTo.restrict (fun x => m • x) (MulAction.orbit M a) (MulAction.orbit M a) ⋯,
      mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.BisimO.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) (a : α) (s : Stream'.Seq α)
  (a' : α) (s' : Stream'.Seq α) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s')))
  (h_3 : (x x_1 : Option (Stream'.Seq1 α)) → motive x x_1),
  (match some (a, s), some (a', s') with
    | none, none => h_1 ()
    | some (a, s), some (a', s') => h_2 a s a' s'
    | x, x_1 => h_3 x x_1) =
    h_2 a s a' s'
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_self : ∀ {x : NNReal}, x.agm x = x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.map_pre' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] (F : CategoryTheory.Functor J C)
  {E₁ E₂ : CategoryTheory.Functor K J} (α : E₁ ⟶ E₂),
  CategoryTheory.Limits.limit.pre F E₂ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E₁)
      (CategoryTheory.Limits.lim.map (CategoryTheory.Functor.whiskerRight α F))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.keys_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} (h : (↑m).WF),
  (↑(Std.DHashMap.Internal.Raw₀.filter f m)).keys.Perm
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (m.get x ⋯))
        (↑m).keys.attach).unattach
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The global state that is shared between all threads.  -/
Mathlib.Tactic.ClickSuggestions.State : Type
-- Mathlib.Topology.Neighborhoods
Filter.EventuallyEq.tendsto : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X},
  (f =ᶠ[l] fun x_1 => x) → Filter.Tendsto f l (nhds x)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnit_of_mem_nonZeroDivisors_of_mulOpposite : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing Rᵐᵒᵖ] {a : R}, a ∈ nonZeroDivisors R → IsUnit a
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toOrderHom : α →o β)
  (map_top' : toOrderHom.toFun ⊤ = ⊤) (map_bot' : toOrderHom.toFun ⊥ = ⊥),
  sizeOf { toOrderHom := toOrderHom, map_top' := map_top', map_bot' := map_bot' } =
    1 + sizeOf toOrderHom + sizeOf map_top' + sizeOf map_bot'
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- On local sites, the constant sheaf functor is fully faithful.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulConstantSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [CategoryTheory.LocallySmall.{w, v, u} C] →
        [J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [CategoryTheory.Limits.HasProducts A] →
                  [inst_6 : CategoryTheory.HasWeakSheafify J A] → (CategoryTheory.constantSheaf J A).FullyFaithful
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_eq_zero_of_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ≤ a → Multiset.Ico a b = 0
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- The measure induced for `Real`-linear positive functional `Λ`, defined through `toNNRealLinear`
and the `NNReal`-version of `rieszContent`. This is under the namespace `RealRMK`, while
`rieszMeasure` without namespace is for `NNReal`-linear `Λ`.  -/
RealRMK.rieszMeasure : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [T2Space X] →
      [inst_2 : MeasurableSpace X] →
        [BorelSpace X] →
          (CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) → [LocallyCompactSpace X] → MeasureTheory.Measure X
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableWithinAt.continuousAlternatingMap_apply_const : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  [Finite ι], DifferentiableWithinAt 𝕜 c s x → ∀ (u : ι → F), DifferentiableWithinAt 𝕜 (fun y => (c y) u) s x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The derivative of `polarCoordReal.symm`, see `hasFDerivAt_polarCoordReal_symm`.
 -/
NumberField.mixedEmbedding.FDerivPolarCoordRealSymm : (K : Type u_1) →
  [inst : Field K] →
    NumberField.mixedEmbedding.realMixedSpace K →
      NumberField.mixedEmbedding.realMixedSpace K →L[ℝ] NumberField.mixedEmbedding.realMixedSpace K
-- Mathlib.CategoryTheory.Action.Basic
/-- A homomorphism of `Action V G`s is a morphism between the underlying objects,
commuting with the action of `G`.
 -/
Action.Hom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → Action V G → Action V G → Type v_1
-- Mathlib.Tactic.FunProp.Core
/-- Prove function property of using *transition theorems*.  -/
Mathlib.Meta.FunProp.applyTransitionRules : Lean.Expr →
  (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
    Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_sphere_sphere_sphere : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
-- Init.Data.Bool
Bool.min_eq_and : min = and
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.Linarith.Poly) (strict : Bool) (h : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof),
  sizeOf { p := p, strict := strict, h := h } = 1 + sizeOf p + sizeOf strict + sizeOf h
-- Mathlib.Topology.Homotopy.Contractible
ContinuousMap.Nullhomotopic.comp_right : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)}, f.Nullhomotopic → ∀ (g : C(Y, Z)), (g.comp f).Nullhomotopic
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.AddMon C)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- Functor translating a comonoid object in a functor category
to a functor into the category of comonoid objects.
 -/
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor (CategoryTheory.Comon (CategoryTheory.Functor C D))
            (CategoryTheory.Functor C (CategoryTheory.Comon D))
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.dvd_smul_X_iff_exists : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {i : σ} {r : R},
  r ≠ 0 → (p ∣ r • MvPolynomial.X i ↔ ∃ s, s ∣ r ∧ (p = MvPolynomial.C s ∨ p = s • MvPolynomial.X i))
-- Mathlib.Data.Matrix.Composition
Matrix.comp_one : ∀ {I : Type u_1} {J : Type u_2} {R : Type u_5} [inst : DecidableEq I] [inst_1 : DecidableEq J] [inst_2 : Zero R]
  [inst_3 : One R], (Matrix.comp I I J J R) 1 = 1
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.attrKind : Lean.Meta.InstanceEntry → Lean.AttributeKind
-- Mathlib.Algebra.Order.SuccPred
PredSubOrder.mk : {α : Type u_1} →
  [inst : Preorder α] →
    [inst_1 : Sub α] →
      [inst_2 : One α] → [toPredOrder : PredOrder α] → (∀ (x : α), PredOrder.pred x = x - 1) → PredSubOrder α
-- Mathlib.Order.CompactlyGenerated.Basic
Directed.iSup_inf_eq : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α},
  Directed (fun x1 x2 => x1 ≤ x2) f → (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The coefficient of `n.some` in the `n none`-th coefficient of `optionEquivLeft R S₁ f`
equals the coefficient of `n` in `f`  -/
MvPolynomial.optionEquivLeft_coeff_some_coeff_none : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (n : Option S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R),
  MvPolynomial.coeff n.some (((MvPolynomial.optionEquivLeft R S₁) f).coeff (n none)) = MvPolynomial.coeff n f
-- Mathlib.Algebra.Order.Group.PosPart
one_lt_oneLePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, 1 < a → 1 < a⁺ᵐ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- Given a graded ring `A` and a map `f : A →+* Γ(X, ⊤)`,
for each homogeneous `t` of positive degree, it induces a map from `D(f(t)) ⟶ D₊(t)`.  -/
AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              {X : AlgebraicGeometry.Scheme} →
                (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) →
                  {x : ↑(X.presheaf.obj (Opposite.op ⊤))} →
                    {t : A} →
                      {d : ℕ} → f t = x → 0 < d → t ∈ 𝒜 d → (↑(X.basicOpen x) ⟶ ↑(AlgebraicGeometry.Proj.basicOpen 𝒜 t))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.map_mul : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (f g : X ⟶ M), F.map (f * g) = F.map f * F.map g
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightEq_inv_app_right : ∀ {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) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r')
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightEq L r r' h hr).inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Differentiable.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.cosh (f x)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.orderEmbeddingToFun_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → LE (α i)] {f : Π₀ (i : ι), α i}
  {i : ι}, DFinsupp.orderEmbeddingToFun f i = f i
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `add_apply`. -/
GroupNorm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.p2.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g],
  AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g =
    CategoryTheory.Limits.Multicoequalizer.desc (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram Y
      (fun i => CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) ⋯
-- Init.Data.Array.MapIdx
Array.toList_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α},
  (Array.mapIdx f xs).toList = List.mapIdx (fun i a => f i a) xs.toList
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
exists_isTranscendenceBasis : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  ∃ s, IsTranscendenceBasis R Subtype.val
-- Mathlib.Algebra.Group.End
Equiv.swap_mul_eq_mul_swap : ∀ {α : Type u_4} [inst : DecidableEq α] (f : Equiv.Perm α) (x y : α),
  Equiv.swap x y * f = f * Equiv.swap (f⁻¹ x) (f⁻¹ y)
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instιScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y), AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.equalizer.ι f g)
-- Mathlib.Data.Nat.Log
Nat.clog_monotone : ∀ (b : ℕ), Monotone (Nat.clog b)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_zpow : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → Group (f i)] (i : I) (x : f i) (n : ℤ),
  Pi.mulSingle i (x ^ n) = Pi.mulSingle i x ^ n
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_pos : ∀ {o : Ordinal.{u_1}}, 0 < o.cof ↔ 0 < o
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.aeval_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra S T] (f : σ → T) (g : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R),
  (MvPolynomial.aeval f) ((MvPolynomial.bind₂ g) φ) = (MvPolynomial.eval₂Hom ((↑(MvPolynomial.aeval f)).comp g) f) φ
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.eq_of_forall_toMeasure_apply_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω),
  (∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s) → μ = ν
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_concat : ∀ {V : Type u_1} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w), p.IsSubwalk (p.concat h)
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isPreconnected_setOfPred_wSameSide`. -/
AffineSubspace.isPreconnected_setOf_wSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.WSameSide x y}
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Nat.instMeasurableSpace : MeasurableSpace ℕ
-- Mathlib.Topology.UniformSpace.Compact
lebesgue_number_lemma_nhdsWithin : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {U : α → Set α},
  IsCompact K → (∀ x ∈ K, U x ∈ nhdsWithin x K) → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ y, UniformSpace.ball x V ∩ K ⊆ U y
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- A Hadamard matrix with constant row sum `s` has order `star s * s`, provided the order
is regular in `R`. This generalizes [Theorem 2.3.7][deLauneyFlannery2011].  -/
Matrix.IsHadamard.card_eq_star_mul_of_const_row_sum : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R} {s : R},
  A.IsHadamard → IsRegular ↑(Fintype.card n) → (∀ (i : n), ∑ j, A i j = s) → ↑(Fintype.card n) = star s * s
-- Init.Data.UInt.Lemmas
UInt16.lt_iff_toNat_lt : ∀ {a b : UInt16}, a < b ↔ a.toNat < b.toNat
-- Init.Data.Char.Lemmas
Char.le_refl : ∀ (a : Char), a ≤ a
-- Aesop.Util.UnorderedArraySet
_private.Aesop.Util.UnorderedArraySet.0.Aesop.UnorderedArraySet.rep : {α : Type u_1} → [inst : BEq α] → Aesop.UnorderedArraySet α → Array α
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.cast_card_eq_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K], ↑(Fintype.card K) = 0
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Fin (addOrderOf a)` and
`AddSubmonoid.multiples a`, sending `i` to `i • a`  -/
finEquivMultiples : {G : Type u_1} → [inst : AddMonoid G] → {x : G} → IsOfFinAddOrder x → Fin (addOrderOf x) ≃ ↥(AddSubmonoid.multiples x)
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableOn.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableOn 𝕜 (f i) s) → DifferentiableOn 𝕜 (∏ i ∈ u, f i) s
-- Lean.Data.Lsp.Internal
/-- Position information for a declaration. Inlined to reduce memory consumption.  -/
Lean.Lsp.DeclInfo : Type
-- Mathlib.Combinatorics.Additive.Energy
Finset.le_mulEnergy_self : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s : Finset α}, s.card ^ 2 ≤ s.mulEnergy s