mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_cons : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCancelCommMonoid μ]
  [inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] {i : ι} {s : Finset ι} (hi : i ∉ s) (n : μ),
  (Finset.cons i s hi).piAntidiag n =
    (Finset.HasAntidiagonal.antidiagonal n).disjiUnion
      (fun p => Finset.map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯
-- Mathlib.Data.PNat.Defs
Nat.toPNat'_zero : Nat.toPNat' 0 = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntry_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback) k).isLE = true
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- Given two elements `a`, `b` of a commutative cancellative `MonoidWithZero` and a nonzero
element `c`, `a*c` divides `b*c` iff `a` divides `b`.  -/
mul_dvd_mul_iff_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b c : α}, c ≠ 0 → (a * c ∣ b * c ↔ a ∣ b)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- Pointwise inversion of submonoids as an order isomorphism.  -/
Submonoid.invOrderIso : {G : Type u_2} → [inst : Group G] → Submonoid G ≃o Submonoid G
-- Std.Time.Date.Unit.Day
Std.Time.Day.instReprOrdinal : Repr Std.Time.Day.Ordinal
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.mul : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A A' : Matrix ι ι R} {f f' : Module.End R M},
  Matrix.Represents b A f → Matrix.Represents b A' f' → Matrix.Represents b (A * A') (f * f')
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
hasProd_pi_single : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : DecidableEq β] (b : β)
  (a : α), HasProd (Pi.mulSingle b a) a
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.ext : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₐc[R] B}, (∀ (x : A), φ₁ x = φ₂ x) → φ₁ = φ₂
-- Lean.Parser.Term
Lean.Parser.Term.whereFinallySubsection.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.homotopyUnop.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {f g : K ⟶ L}
  (h :
    Homotopy ((CochainComplex.opEquivalence C).functor.map f.op) ((CochainComplex.opEquivalence C).functor.map g.op)),
  CochainComplex.homotopyUnop h =
    {
      hom := fun p q =>
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K ⋯).hom
          (CategoryTheory.CategoryStruct.comp (h.hom (-q) (-p)).unop (HomologicalComplex.XIsoOfEq L ⋯).hom),
      zero := ⋯, comm := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Two Day convolution structures on the same functors gives an isomorphic functor.  -/
CategoryTheory.MonoidalCategory.DayConvolution.uniqueUpToIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {F G : CategoryTheory.Functor C V} →
              (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G) →
                CategoryTheory.MonoidalCategory.DayConvolution.convolution F G ≅
                  CategoryTheory.MonoidalCategory.DayConvolution.convolution F G
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- The spectrum of a selfadjoint is real  -/
selfAdjoint.val_re_map_spectrum : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : ↥(selfAdjoint A)),
  spectrum ℂ ↑a = Complex.ofReal ∘ Complex.re '' spectrum ℂ ↑a
-- Mathlib.Algebra.GroupWithZero.Regular
/-- A regular element of a `Nontrivial` `MulZeroClass` is non-zero.  -/
IsRegular.ne_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [Nontrivial R], IsRegular a → a ≠ 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  [inst_3 : Inhabited γ] {f : α → β → γ} {k : α}, m.WF → (Std.HashMap.Raw.map f m)[k]! = (Option.map (f k) m[k]?).get!
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.ext : ∀ {X Y : CategoryTheory.RelCat} (f g : X ⟶ Y), f.rel = g.rel → f = g
-- Mathlib.Order.WithBot
WithTop.semilatticeSup : {α : Type u_1} → [SemilatticeSup α] → SemilatticeSup (WithTop α)
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.NormCastExtension.mk : Lean.Meta.SimpExtension → Lean.Meta.SimpExtension → Lean.Meta.SimpExtension → Lean.Meta.NormCast.NormCastExtension
-- Init.Data.Int.Lemmas
Int.add_left_cancel : ∀ {a b c : ℤ}, a + b = a + c → b = c
-- Init.Data.Fin.Log2
/-- Logarithm base 2 for bounded numbers.

The resulting value is the same as that computed by `Nat.log2`. In particular, the result for `0` is
`0`.

Examples:
 * `(8 : Fin 10).log2 = (3 : Fin 10)`
 * `(7 : Fin 10).log2 = (2 : Fin 10)`
 * `(4 : Fin 10).log2 = (2 : Fin 10)`
 * `(3 : Fin 10).log2 = (1 : Fin 10)`
 * `(1 : Fin 10).log2 = (0 : Fin 10)`
 * `(0 : Fin 10).log2 = (0 : Fin 10)`
 -/
Fin.log2 : {m : ℕ} → Fin m → Fin m
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.inl_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.Limits.pushout.desc h k w) =
    h
-- Init.Data.List.Lemmas
List.contains_eq_any_beq : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α}, l.contains a = l.any fun x => a == x
-- Std.Internal.Parsec.ByteArray
/-- Skip a string by matching its UTF-8 bytes.
 -/
Std.Internal.Parsec.ByteArray.skipString : String → Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_lt_mk : ∀ {α : Type u} [Uncountable α], Cardinal.aleph0 < Cardinal.mk α
-- Mathlib.Algebra.Ring.CentroidHom
/-- The type of centroid homomorphisms from `α` to `α`.  -/
CentroidHom : (α : Type u_6) → [NonUnitalNonAssocSemiring α] → Type u_6
-- Mathlib.Data.PNat.Prime
PNat.Coprime.factor_eq_gcd_right : ∀ {a b m n : ℕ+}, m.Coprime n → a ∣ m → b ∣ n → a = (b * a).gcd m
-- Mathlib.CategoryTheory.Sites.Closed
/-- The closure of a sieve `S` is the largest closed sieve which contains `S` (justifying the name
"closure").
 -/
CategoryTheory.GrothendieckTopology.le_close_of_isClosed : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  {S T : CategoryTheory.Sieve X}, S ≤ T → J₁.IsClosed T → J₁.close S ≤ T
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.rank_baseChange : ∀ {R : Type u} {S : Type u'} {M' : Type v'} [inst : Semiring R] [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid M']
  [StrongRankCondition R] [StrongRankCondition S] [inst_5 : Module S M'] [Module.Free S M'] [inst_7 : Algebra S R],
  Module.rank R (TensorProduct S R M') = Cardinal.lift.{u, v'} (Module.rank S M')
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The pushforward of `R.over Y` along `Over.map f` is isomorphic to `R.over X`.  -/
SheafOfModules.overMapUnitIso : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      {R : CategoryTheory.Sheaf K RingCat} →
        {X Y : D} →
          (f : X ⟶ Y) →
            (SheafOfModules.overMap R f).obj (SheafOfModules.unit (R.over Y)) ≅ SheafOfModules.unit (R.over X)
-- Lean.Widget.InteractiveGoal
Lean.Widget.instRpcEncodableInteractiveTermGoal : Lean.Server.RpcEncodable Lean.Widget.InteractiveTermGoal
-- Mathlib.Topology.QuasiSeparated
isQuasiSeparated_iff_quasiSeparatedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α), IsOpen s → (IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s)
-- Lean.Elab.App
/-- Returns a named argument that depends on the next argument, otherwise `none`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.findNamedArgDependsOnCurrent? : Lean.Elab.Term.ElabAppArgs.M (Option Lean.Elab.Term.NamedArg)
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.instReprUnpackedFloat : Repr Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.representablyCoflat_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), CategoryTheory.RepresentablyCoflat F.op ↔ CategoryTheory.RepresentablyFlat F
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage_nonneg : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (U : SetRel X X), 0 ≤ Dynamics.coverEntropyInfEntourage T F U
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- compatibility condition  -/
CategoryTheory.Endofunctor.Coalgebra.Hom.h_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (self : V₀.Hom V₁) {Z : C} (h : F.obj V₁.V ⟶ Z),
  CategoryTheory.CategoryStruct.comp V₀.str (CategoryTheory.CategoryStruct.comp (F.map self.f) h) =
    CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp V₁.str h)
-- Mathlib.Analysis.Analytic.Order
/-- The order of an analytic function `f` at `z₀` is zero iff `f` does not vanish at `z₀`.  -/
AnalyticAt.analyticOrderAt_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, AnalyticAt 𝕜 f z₀ → (analyticOrderAt f z₀ = 0 ↔ f z₀ ≠ 0)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The infimum distance is invariant under isometries.  -/
Metric.infDist_image : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {t : Set α} {x : α} {Φ : α → β},
  Isometry Φ → Metric.infDist (Φ x) (Φ '' t) = Metric.infDist x t
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.separatingLeft_iff_separatingRight : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.SeparatingLeft ↔ M.SeparatingRight
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- The property of preserving equalizers expressed in terms of forks.  -/
CategoryTheory.Limits.isLimitForkMapOfIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            {f g : X ⟶ Y} →
              {h : Z ⟶ X} →
                (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) →
                  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι h w) →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map h) ⋯)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms],
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₂ → P T.obj₃ → P T.obj₁) →
    P.IsTriangulatedClosed₁
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_ne : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [inst : DecidableEq n]
  {j' : n}, j' ≠ j → M.updateCol j c i j' = M i j'
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.eq_def : ∀ (fuel : ℕ) (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.unionFuel fuel s₁ s₂ =
    match fuel with
    | 0 => s₁.concat s₂
    | fuel.succ =>
      match s₁, s₂ with
      | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ =>
        if Nat.blt x₁ x₂ = true then Lean.Grind.AC.Seq.cons x₁ (Lean.Grind.AC.Seq.var x₂)
        else Lean.Grind.AC.Seq.cons x₂ (Lean.Grind.AC.Seq.var x₁)
      | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => Lean.Grind.AC.Seq.insert x₁ s₂
      | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => Lean.Grind.AC.Seq.insert x₂ s₁
      | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ =>
        if Nat.blt x₁ x₂ = true then
          Lean.Grind.AC.Seq.cons x₁ (Lean.Grind.AC.Seq.unionFuel fuel s₁ (Lean.Grind.AC.Seq.cons x₂ s₂))
        else Lean.Grind.AC.Seq.cons x₂ (Lean.Grind.AC.Seq.unionFuel fuel (Lean.Grind.AC.Seq.cons x₁ s₁) s₂)
-- Mathlib.Data.FunLike.Group
FunLike.divisionMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Inv F] [inst_5 : Div F] [inst_6 : Pow F ℤ] [inst_7 : DivisionMonoid β]
  [inst_8 : IsOneApply F α β] [inst_9 : IsMulApply F α β] [inst_10 : IsInvApply F α β] [inst_11 : IsDivApply F α β]
  [inst_12 : IsPowApply ℕ F α β] [inst_13 : IsPowApply ℤ F α β],
  FunLike.divisionMonoid = Function.Injective.divisionMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.length_digitsAppend : ∀ {n b : ℕ}, 1 < b → ∀ (l : ℕ), n < b ^ l → (b.digitsAppend l n).length = l
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.IsPlausibleNthOutputStep.below.zero_yield : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive :
    (a : ℕ) →
      (a_1 : Std.IterM m β) →
        (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop}
  {it' : Std.IterM m β} {out : β} {it : Std.IterM m β} (a : it.IsPlausibleStep (Std.IterStep.yield it' out)),
  Std.IterM.IsPlausibleNthOutputStep.below ⋯
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_sdiff_left' : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), (s \ t) \ u = s \ t ∩ (s \ u)
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {b : R},
  AddMonoidHom.mulRight b = AddMonoidHom.mulLeft b ↔ ∀ (a : R), Commute a b
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- `λ` is the Carmichael function, also known as the reduced totient function,
defined as the exponent of the unit group of `ZMod n`.  -/
ArithmeticFunction.carmichael.«termλ» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.exists_lift_of_germInjective_aux : ∀ {X : AlgebraicGeometry.Scheme} {R A : CommRingCat} {U : X.Opens} {x : ↥X} (hxU : x ∈ U) (φ : A ⟶ X.presheaf.stalk x)
  (φRA : R ⟶ A) (φRX : R ⟶ X.presheaf.obj (Opposite.op U)),
  (CommRingCat.Hom.hom φRA).FiniteType →
    CategoryTheory.CategoryStruct.comp φRA φ = CategoryTheory.CategoryStruct.comp φRX (X.presheaf.germ U x hxU) →
      ∃ V,
        ∃ (hxV : x ∈ V), V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.finiteType_subcomplex_of_finiteType : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteType C] (E : Topology.RelCWComplex.Subcomplex C), Topology.RelCWComplex.FiniteType ↑E
-- Mathlib.Topology.Sets.Compacts
/-- The type of compact sets is inhabited, with default element the empty set.  -/
TopologicalSpace.Compacts.instInhabited : {α : Type u_1} → [inst : TopologicalSpace α] → Inhabited (TopologicalSpace.Compacts α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.get? k' =
    if h : compare k k' = Ordering.eq then cast ⋯ (f (t.get? k)) else t.get? k'
-- Mathlib.Data.Sym.Basic
/-- "Attach" a proof that `a ∈ s` to each element `a` in `s` to produce
an element of the symmetric power on `{x // x ∈ s}`.  -/
Sym.attach : {α : Type u_1} → {n : ℕ} → (s : Sym α n) → Sym { x // x ∈ s } n
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_rpow_of_log_le : ∀ {x y z : ℝ}, 0 < y → Real.log x ≤ z * Real.log y → x ≤ y ^ z
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing homogeneous binary bitvector operators.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceBin : Lean.Name → ℕ → ({n : ℕ} → BitVec n → BitVec n → BitVec n) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_nonneg : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω), 0 ≤ ProbabilityTheory.variance X μ
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.mk : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            (var : relations.G → M) →
              (∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0) → relations.Solution M
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set M} {x : M} {f : M → M'} {g : N → N'} {r : Set N} {y : N},
  MDiffAt[s] f x → MDiffAt[r] g y → MDiffAt[s ×ˢ r] (Prod.map f g) (x, y)
-- Mathlib.GroupTheory.QuotientGroup.Finite
Group.fintypeOfKerEqRange.eq_1 : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group F] [inst_1 : Group G] [inst_2 : Group H]
  [inst_3 : Fintype F] [inst_4 : Fintype H] (f : F →* G) (g : G →* H) (h : g.ker = f.range),
  Group.fintypeOfKerEqRange f g h = Group.fintypeOfKerLeRange f g ⋯
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.completedCosZeta_zero : ∀ (s : ℂ), HurwitzZeta.completedCosZeta 0 s = completedRiemannZeta s
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.algebra'' : {K : Type v} →
  [inst : Field K] → {n : ℕ} → {f : Polynomial K} → Algebra K (Polynomial.SplittingFieldAux n f.removeFactor)
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensorMk_apply : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A B : Rep.{u, u, v} k G} (a : ↑A) (b : ↑B),
  ((A.coinvariantsTensorMk B) a) b =
    (Representation.Coinvariants.mk
        (((CategoryTheory.MonoidalCategory.curriedTensor (Rep.{u, u, v} k G)).obj A).obj B).ρ)
      (a ⊗ₜ[k] b)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  (HomologicalComplex.homologyFunctor C c i).map f = HomologicalComplex.homologyMap f i
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.map_single : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R}
  [inst_2 : Zero S] (f : ZeroHom R S), ((HahnSeries.single a) r).map f = (HahnSeries.single a) (f r)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Finset.hasProd_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  {a : α} (s : Finset β), HasProd (fun x => f ↑x) a ↔ HasProd f (a * ∏ i ∈ s, f i)
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a complete nonarchimedean multiplicative abelian group. Then a function `f : α → G`
is unconditionally multipliable if and only if it tends to one on the filter of cofinite sets.  -/
NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G]
  [NonarchimedeanGroup G] [CompleteSpace G] (f : α → G), Multipliable f ↔ Filter.Tendsto f Filter.cofinite (nhds 1)
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.norm_eq_addGroupSeminorm : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S),
  ‖x‖ = QuotientAddGroup.addGroupSeminorm x
-- Mathlib.Data.DFinsupp.Defs
/-- Let `f i` be a binary operation `β₁ i → β₂ i → β i` such that `f i 0 0 = 0`.
Then `zipWith f hf` is a binary operation `Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i`.  -/
DFinsupp.zipWith : {ι : Type u} →
  {β : ι → Type v} →
    {β₁ : ι → Type v₁} →
      {β₂ : ι → Type v₂} →
        [inst : (i : ι) → Zero (β i)] →
          [inst_1 : (i : ι) → Zero (β₁ i)] →
            [inst_2 : (i : ι) → Zero (β₂ i)] →
              (f : (i : ι) → β₁ i → β₂ i → β i) →
                (∀ (i : ι), f i 0 0 = 0) → (Π₀ (i : ι), β₁ i) → (Π₀ (i : ι), β₂ i) → Π₀ (i : ι), β i
-- Mathlib.Analysis.Calculus.TangentCone.Real
/-- In a real vector space, a convex set with nonempty interior is a set of unique
differentiability at every point of its closure.  -/
uniqueDiffWithinAt_convex : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} [IsTopologicalAddGroup E],
  Convex ℝ s → (interior s).Nonempty → ∀ {x : E}, x ∈ closure s → UniqueDiffWithinAt ℝ s x
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_dvd_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [Nontrivial R] {i j : σ},
  MvPolynomial.X i ∣ MvPolynomial.X j ↔ i = j