mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν], μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν
-- Mathlib.Data.Finset.Insert
/-- To prove a proposition about a nonempty `s : Finset α`, it suffices to show it holds for all
singletons and that if it holds for nonempty `t : Finset α`, then it also holds for the `Finset`
obtained by inserting an element in `t`.  -/
Finset.Nonempty.cons_induction : ∀ {α : Type u_3} {motive : (s : Finset α) → s.Nonempty → Prop},
  (∀ (a : α), motive {a} ⋯) →
    (∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯) →
      ∀ {s : Finset α} (hs : s.Nonempty), motive s hs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_empty : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty.minKey? = none
-- Lean.Data.RArray
Lean.RArray.size_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (h : 0 < n), (Lean.RArray.ofFn f h).size = n
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transposeOrderIso_apply : ∀ (μ : YoungDiagram), YoungDiagram.transposeOrderIso μ = μ.transpose
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- If `f : ℂ → E` is complex differentiable on an open disc of positive radius and is continuous
on its closure, then it is analytic on the open disc with coefficients of the power series given by
Cauchy integral formulas.  -/
DiffContOnCl.hasFPowerSeriesOnBall : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : NNReal} {c : ℂ}
  {f : ℂ → E}, DiffContOnCl ℂ f (Metric.ball c ↑R) → 0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context.mk : Lean.Syntax →
  Lean.Syntax → Array Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.ToTerm.Kind → Lean.Elab.Term.Do.ToTerm.Context
-- Mathlib.Topology.Order.LeftRightLim
continuousWithinAt_leftLim_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {a : α},
  Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds (Function.leftLim f a)) →
    ContinuousWithinAt (Function.leftLim f) (Set.Iic a) a
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- The object of the category of elements `shrinkYoneda.{w}.flip.obj (op X)`
corresponding to the identity of `X` is initial.  -/
CategoryTheory.Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      (X : C) →
        CategoryTheory.Limits.IsInitial
          ((CategoryTheory.shrinkYoneda.{w, v₁, u₁}.flip.obj (Opposite.op X)).elementsMk X
            (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X)))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_self_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (a : M) (haS : a ∈ S), Localization.mk a ⟨a, haS⟩ = 1
-- Init.Data.List.Find
List.lookup_append : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {l₁ l₂ : List (α × β)} {k : α},
  List.lookup k (l₁ ++ l₂) = (List.lookup k l₁).or (List.lookup k l₂)
-- Std.Data.TreeMap.Basic
Std.TreeMap.empty_eq_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.empty = ∅
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Formula for `Λ₀ 1`, where `Λ₀` is the entire function satisfying
`Λ₀ s = π ^ (-s / 2) Γ(s / 2) ζ(s) + 1 / s + 1 / (1 - s)` away from `s = 0, 1`.

Note that `s = 1` is _not_ a pole of `Λ₀`, so this statement (unlike `riemannZeta_one`) is
a mathematically meaningful statement and is not dependent on Mathlib's particular conventions for
division by zero.  -/
completedRiemannZeta₀_one : completedRiemannZeta₀ 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2 + 1
-- Mathlib.Topology.Order
Equiv.coinduced_symm : ∀ {α : Type u_4} {β : Type u_5} (e : α ≃ β), TopologicalSpace.coinduced ⇑e.symm = TopologicalSpace.induced ⇑e
-- Std.Internal.Do.ExceptPost
/-- The empty exception postcondition type, used when a monad has no exception layers.  -/
Std.Internal.Do.EPost.Nil : Type
-- Mathlib.Topology.Separation.Basic
t0Space_iff_nhds_injective : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ Function.Injective nhds
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.comp_sub : ∀ {𝕜 : 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 : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x → ∀ (y : E), HasFPowerSeriesAt (fun z => f (z - y)) p (x + y)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_ofHom : ∀ {M N : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N] (f : NormedAddGroupHom M N),
  SemiNormedGrp.Hom.hom (SemiNormedGrp.ofHom f) = f
-- Mathlib.Data.Set.Card
Set.ncard_eq_toFinset_card' : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], s.ncard = s.toFinset.card
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isCompact_subsets_of_isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : Set α}, IsCompact K → IsCompact {L | ↑L ⊆ K}
-- Mathlib.Algebra.Order.Group.Unbundled.Int
/-- **Alias** of `Int.le_self_sq`. -/
Int.le_self_pow_two : ∀ (b : ℤ), b ≤ b ^ 2
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.memLp_tilted_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (p : NNReal), MeasureTheory.MemLp X (↑p) (μ.tilted fun x => t * X x)
-- Mathlib.Data.Nat.Digits.Lemmas
/-- **Alias** of `Nat.length_digits`. -/
Nat.digits_len : ∀ (b n : ℕ), 1 < b → n ≠ 0 → (b.digits n).length = Nat.log b n + 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on simplicial objects.  -/
CategoryTheory.SimplicialObject.whiskering : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u_1) →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject D))
-- Mathlib.Combinatorics.Additive.Randomisation
/-- One can randomise by a function of dissociated support.  -/
AddDissociated.randomisation : ∀ {G : Type u_1} [inst : Fintype G] [inst_1 : AddCommGroup G] (c : AddChar G ℂ → ℝ) (d : AddChar G ℂ → ℂ),
  AddDissociated {ψ | d ψ ≠ 0} → (Finset.univ.expect fun a => ∏ ψ, (c ψ + (d ψ * ψ a).re)) = ∏ ψ, c ψ
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.Skeleton.one_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  1 = CategoryTheory.toSkeleton (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_pow : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ∀ {n : ℕ}, n ≠ 0 → T_gen✝ p F a ^ n < 1
-- Init.Data.Option.Lemmas
Option.or_assoc : ∀ {α : Type u_1} {o₁ o₂ o₃ : Option α}, (o₁.or o₂).or o₃ = o₁.or (o₂.or o₃)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.map_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y),
  (CategoryTheory.WithInitial.map F).map f =
    match X, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => PUnit.unit
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => PUnit.unit
-- Mathlib.Topology.Category.TopCat.EffectiveEpi
/-- The effective epimorphisms in `TopCat` are precisely the quotient maps.  -/
TopCat.effectiveEpi_iff_isQuotientMap : ∀ {B X : TopCat} (π : X ⟶ B),
  CategoryTheory.EffectiveEpi π ↔ Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom π)
-- Plausible.Random
/-- Generate a random value of type `α` between `x` and `y` inclusive.  -/
Plausible.Random.randBound : {m : Type u → Type u_1} →
  {g : Type} →
    (α : Type u) →
      [inst : LE α] →
        [Plausible.BoundedRandom m α] →
          (lo hi : α) → lo ≤ hi → [RandomGen g] → Plausible.RandGT g m { a // lo ≤ a ∧ a ≤ hi }
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.const.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.ElabRuleTerm.const decl = Aesop.ElabRuleTerm.const decl_1 → decl = decl_1
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Ici : ∀ {n : ℕ} (i : Fin n), Fin.succ '' Set.Ici i = Set.Ici i.succ
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState.mk.inj : ∀ {seen : Lean.ExprSet} {consts : Lean.NameSet} {seen_1 : Lean.ExprSet} {consts_1 : Lean.NameSet},
  { seen := seen, consts := consts } = { seen := seen_1, consts := consts_1 } → seen = seen_1 ∧ consts = consts_1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A}
  (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀) {Z : A}
  (h : F.obj.obj (Opposite.op (E.X i₀)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c)
      (CategoryTheory.CategoryStruct.comp (F.obj.map (E.f i₀).op) h) =
    CategoryTheory.CategoryStruct.comp (c.ι i₀) h
-- Mathlib.Algebra.Group.Action.Defs
/-- `•` is left commutative  -/
SMulCommClass.smul_comm : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} {inst : SMul M α} {inst_1 : SMul N α} [self : SMulCommClass M N α]
  (m : M) (n : N) (a : α), m • n • a = n • m • a
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Icc_of_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioo a b → x ∈ Set.Icc a b
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.opEquivOpUnder_functor_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : CategoryTheory.Over (Opposite.op X)),
  (CategoryTheory.Over.opEquivOpUnder X).functor.obj Y = Opposite.op (CategoryTheory.Under.mk Y.hom.unop)
-- Mathlib.GroupTheory.OrderOfElement
/-- `orderOf x` is the order of the element `x`, i.e. the `n ≥ 1`, s.t. `x ^ n = 1` if it exists.
Otherwise, i.e. if `x` is of infinite order, then `orderOf x` is `0` by convention.  -/
orderOf : {G : Type u_1} → [Monoid G] → G → ℕ
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜] [inst_2 : DecidableEq ι] (i : ι),
  (PiLp.basisFun p 𝕜 ι) i = PiLp.single p i 1
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.toSubtype'.match_1.splitter : (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) →
        (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
          (x : Fin2 n) → { x_1 // TypeVec.ofRepeat (p x (TypeVec.prod.mk x x_1.1 x_1.2)) } → Sort u_2) →
  (n : ℕ) →
    (α : TypeVec.{u_1} n) →
      (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
        (x : Fin2 n) →
          (x_1 : { x_1 // TypeVec.ofRepeat (p x (TypeVec.prod.mk x x_1.1 x_1.2)) }) →
            ((n : ℕ) →
                (α : TypeVec.{u_1} (n + 1)) →
                  (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
                    (i : Fin2 n) →
                      (x : { x // TypeVec.ofRepeat (p i.fs (TypeVec.prod.mk i.fs x.1 x.2)) }) →
                        motive (n + 1) α p i.fs x) →
              ((n : ℕ) →
                  (α : TypeVec.{u_1} (n + 1)) →
                    (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
                      (x : { x // TypeVec.ofRepeat (p Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) }) →
                        motive (n + 1) α p Fin2.fz x) →
                motive n α p x x_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceNeg : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Group.Action.Basic
MulAction.toPerm_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (a : α) (x : β),
  (MulAction.toPerm a) x = a • x
-- Mathlib.Data.Nat.Cast.Basic
Nat.castRingHom_nat : Nat.castRingHom ℕ = RingHom.id ℕ
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sub_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        ProbabilityTheory.covariance (X - Y) Z μ =
          ProbabilityTheory.covariance X Z μ - ProbabilityTheory.covariance Y Z μ
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjObj_w : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
  CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F x) (F.map f) =
    W.weightedLimObjObjπ F ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_singleton_iff : ∀ {k m n : ℤ}, (m...n).toArray = #[k] ↔ n = m + 1 ∧ m = k
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.distribHaarChar_pos : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] {g : G}, 0 < (MeasureTheory.distribHaarChar A) g
-- Mathlib.Topology.Algebra.Group.Basic
nhds_one_symm' : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G],
  Filter.map Inv.inv (nhds 1) = nhds 1
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.instInhabited.eq_1 : ∀ {G : Type u} [inst : Group G],
  GroupFilterBasis.instInhabited =
    { default := { sets := {{1}}, nonempty := ⋯, inter_sets := ⋯, one' := ⋯, mul' := ⋯, inv' := ⋯, conj' := ⋯ } }
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.finprod_finitePlace_pow_multiplicity : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {I : Ideal (NumberField.RingOfIntegers K)},
  I ≠ ⊥ → ∏ᶠ (v : NumberField.FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Mathlib.Topology.Bases
isTopologicalBasis_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {T : (i : ι) → Set (Set (X i))},
  (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) →
    TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A mixin for left cancellative multiplication by nonzero elements.  -/
IsLeftCancelMulZero : (M₀ : Type u) → [Mul M₀] → [Zero M₀] → Prop
-- Mathlib.Topology.MetricSpace.Thickening
IsCompact.exists_isCompact_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} [LocallyCompactSpace α],
  IsCompact s → ∃ δ, 0 < δ ∧ IsCompact (Metric.cthickening δ s)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (h : optParam (p ≤ Submodule.comap 0 q) ⋯), p.mapQ q 0 h = 0
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- The difference of the left morphisms factors through `hom`.  -/
CategoryTheory.Arrow.LeftHomotopy.comm : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (self : CategoryTheory.Arrow.LeftHomotopy f g),
  CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g = CategoryTheory.CategoryStruct.comp u.hom self.hom
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.addCommute_iff_add_neg_cancel_assoc : ∀ {M : Type u_1} [inst : AddMonoid M] {u : AddUnits M} {a : M}, AddCommute (↑u) a ↔ ↑u + (a + ↑(-u)) = a
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.of_exists_prime_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  (∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a) → UniqueFactorizationMonoid α
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.star_mul_self_of_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ pinGroup Q → star x * x = 1
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.mono_iff_injective : ∀ {A B : GrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Finset.sum_mul_sum_eq_sum_perm : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] {s : Finset ι} {σ : Equiv.Perm ι},
  σ.IsCycleOn ↑s →
    ∀ (f g : ι → α), (∑ i ∈ s, f i) * ∑ i ∈ s, g i = ∑ k ∈ Finset.range s.card, ∑ i ∈ s, f i * g ((σ ^ k) i)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.commGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : CommGroup G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [LieGroup I' n G] → CommGroup (ContMDiffMap I I' N G n)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.keep.inj : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ex ex_1 : Tactic.ComputeAsymptotics.BasisExtension basis_tl},
  Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex =
      Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex_1 →
    ex = ex_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toList.isEmpty = m.isEmpty
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.nsmul_vadd_eq_iff_period_dvd : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {n : ℕ} {m : M} {a : α},
  n • m +ᵥ a = a ↔ AddAction.period m a ∣ n
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.reflectsIsomorphisms_of_full_and_faithful : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful],
  F.ReflectsIsomorphisms
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f : E → F} {x : E}, s =ᶠ[nhds x] t → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.id.eq_1 : ∀ (M : Type u_1) [inst : Monoid M] {A : Type u_4} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A],
  DistribMulActionHom.id M = { toMulActionHom := MulActionHom.id M, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.get! (t.minD fallback) = t.minD fallback
-- Lean.Parser.Basic
Lean.Parser.strLitFnAux : String.Pos.Raw → optParam Bool true → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.incl_map : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) {X Y : C i}
  (a : X ⟶ Y), (CategoryTheory.Sigma.incl i).map a = CategoryTheory.Sigma.SigmaHom.mk a
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffAt_inv : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜'}, x ≠ 0 → ∀ {n : WithTop ℕ∞}, ContDiffAt 𝕜 n Inv.inv x
-- Mathlib.Order.Hom.Basic
OrderEmbedding.strictMono : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β), StrictMono ⇑f
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.natDegree_one_le : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.natDegree 1 ≤ 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instDecidableEqK' : DecidableEq Turing.PartrecToTM2.K'
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.le_sInf : ∀ {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α}, (∀ t' ∈ tt, t ≤ t') → t ≤ sInf tt
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.pderiv_zero_equivMvPolynomial : ∀ {R : Type u_2} [inst : CommRing R] (p : Polynomial (Polynomial R)),
  (MvPolynomial.pderiv 0) ((Polynomial.Bivariate.equivMvPolynomial R) p) =
    (Polynomial.Bivariate.equivMvPolynomial R)
      (PolynomialModule.equivPolynomialSelf (Polynomial.derivative'.mapCoeffs p))
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.Subcomplex.union : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C]
  {E : Topology.RelCWComplex.Subcomplex C}, ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = ↑E
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
/-- A club set is a set that is closed under suprema and that is cofinal.  -/
IsClub : {α : Type u_1} → [LinearOrder α] → Set α → Prop
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Composition of continuous linear maps.  -/
ContinuousLinearMap.«term_∘SL_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lift_tmul : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C)
  (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)) (a : A) (b : B),
  (Algebra.TensorProduct.lift f g hfg) (a ⊗ₜ[R] b) = f a * g b