mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_X_sub_C_pow : ∀ {F : Type u} [inst : Field F] {x : F} {n : ℕ},
  ((Polynomial.X - Polynomial.C x) ^ n).natSepDegree = if n = 0 then 0 else 1
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.singleAddHom_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  (AddMonoidAlgebra.singleAddHom m) r = AddMonoidAlgebra.single m r
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `Relation.SymmGen.of_symmGen_of_antisymmRel`. -/
Relation.SymmGen.trans_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.hasMFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {x : E}, HasMFDerivAt% (⇑f) x f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_const : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {w : ℕ} {val : BitVec w},
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.const val) = val
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.of_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (X : C), P X → P.limitsClosure J X
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.pow_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → ∀ (n : ℕ), MonovaryOn f (g ^ n) s
-- Mathlib.Algebra.Order.ZeroLEOne
/-- See `zero_lt_one'` for a version with the type explicit.  -/
zero_lt_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1], 0 < 1
-- Init.Data.Int.Gcd
Int.gcd_pos_of_ne_zero_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → 0 < a.gcd b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.diff_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ \ m₃).Equiv (m₂ \ m₃)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.homTensorHomMap`  -/
TensorProduct.AlgebraTensorModule.homTensorHomMap : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (N : Type uN) →
          (P : Type uP) →
            (Q : Type uQ) →
              [inst : CommSemiring R] →
                [inst_1 : Semiring A] →
                  [inst_2 : Semiring B] →
                    [inst_3 : Algebra R A] →
                      [inst_4 : Algebra R B] →
                        [inst_5 : AddCommMonoid M] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module A M] →
                              [inst_8 : IsScalarTower R A M] →
                                [inst_9 : AddCommMonoid N] →
                                  [inst_10 : Module R N] →
                                    [inst_11 : AddCommMonoid P] →
                                      [inst_12 : Module R P] →
                                        [inst_13 : Module A P] →
                                          [inst_14 : IsScalarTower R A P] →
                                            [inst_15 : AddCommMonoid Q] →
                                              [inst_16 : Module R Q] →
                                                [inst_17 : Module B P] →
                                                  [inst_18 : IsScalarTower R B P] →
                                                    [inst_19 : SMulCommClass A B P] →
                                                      TensorProduct R (M →ₗ[A] P) (N →ₗ[R] Q) →ₗ[B]
                                                        TensorProduct R M N →ₗ[A] TensorProduct R P Q
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
/-- `IsLocalIso` is the weakest source-Zariski-local property containing identities.  -/
AlgebraicGeometry.IsLocalIso.eq_iInf : @AlgebraicGeometry.IsLocalIso = ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : AlgebraicGeometry.IsZariskiLocalAtSource P), P
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) self.map = g.map
-- Std.Sync.Channel
Std.instNonemptySync_1 : ∀ {α : Type}, Nonempty (Std.Channel.Sync α)
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
/-- `κ(p) ⊗[R] (R[X] ⧸ I) = κ(p)[X] / I`  -/
Polynomial.fiberEquivQuotient : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (f : Polynomial R →ₐ[R] S) →
            Function.Surjective ⇑f →
              (p : Ideal R) →
                [inst_3 : p.IsPrime] →
                  p.Fiber S ≃ₐ[p.ResidueField]
                    Polynomial p.ResidueField ⧸
                      Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C),
  EckmannHilton.IsUnital (fun x1 x2 => CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y x1 x2) 0
-- Init.Data.Fin.Lemmas
Fin.pos_iff_ne_zero : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, 0 < a ↔ a ≠ 0
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_spec : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  IsLocalization.mk' S x y * (algebraMap R S) ↑y = (algebraMap R S) x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_inv_left_fst_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : S.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom) T.hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom S.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) h)
-- Mathlib.Order.Completion
DedekindCut.principal_sInf_right : ∀ {α : Type u_1} [inst : CompleteLattice α] (A : DedekindCut α), DedekindCut.principal (sInf A.right) = A
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coe_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] [inst_3 : Nontrivial R]
  {x : ↑(Set.Ico 0 1)}, ↑x = 0 ↔ x = 0
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorAccess.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((next : α) → motive (some next)) → motive x
-- Mathlib.Data.Set.Finite.Lattice
/-- A decreasing union distributes over finite intersection.  -/
Set.iUnion_iInter_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [IsCodirectedOrder ι'] [Nonempty ι']
  {s : ι → ι' → Set α}, (∀ (i : ι), Antitone (s i)) → ⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonReferenceContext.toJson : Lean.Lsp.ReferenceContext → Lean.Json
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
SSet.stdSimplexToTop.eq_1 : SSet.stdSimplexToTop =
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerLeft SSet.stdSimplex sSetTopAdj.unit)
    (CategoryTheory.Functor.whiskerRight SSet.toTopSimplex.hom TopCat.toSSet)
-- LeanSearchClient.LoogleSyntax
/-- Search [Loogle](https://loogle.lean-lang.org/json) from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.


```lean
#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry

```

## Loogle Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring:
🔍 \"differ\"
finds all lemmas that have \"differ\" somewhere in their lemma name.

By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, \"two\", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have \"two\" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

You can modify the Loogle server URL by setting the `LEANSEARCHCLIENT_LOOGLE_API_URL` environment variable.
 -/
LeanSearchClient.just_loogle_cmd : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int16.ofIntTruncate_bitVecToInt : ∀ (n : BitVec 16), Int16.ofIntClamp n.toInt = Int16.ofBitVec n
-- Mathlib.Algebra.DirectSum.Ring
/-- The `Ring` derived from `GSemiring A`.  -/
DirectSum.ring : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommGroup (A i)] →
        [inst_1 : AddMonoid ι] → [DirectSum.GRing A] → Ring (DirectSum ι fun i => A i)
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreSetComm_oreSubtra : ∀ {R : Type u_2} [inst : AddCommMonoid R] (S : AddSubmonoid R) (r : R) (s : ↥S), AddOreLocalization.oreSubtra r s = s
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_neg : ∀ (x : ℂ), Complex.exp (-x) = (Complex.exp x)⁻¹
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_mul_eq_mul_denom_iff : ∀ {K : Type u} [inst : Field K] {x : RatFunc K} {p q : Polynomial K},
  q ≠ 0 →
    (x.num * q = p * x.denom ↔
      x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is Hölder over a bounded space, then it is bounded.  -/
HolderWith.holderWith_zero_of_bounded : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C D : NNReal}, (∀ (x y : X), edist x y ≤ ↑D) → HolderWith C r f → HolderWith (C * D ^ ↑r) 0 f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DTreeMap.filterMap f t).contains k = Option.any (fun x => (f k x).isSome) (t.get? k)
-- Mathlib.Data.ZMod.Basic
ZMod.instIsDomainOfNatNat : IsDomain (ZMod 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (v : β), (t₁.insertIfNew k v).Equiv (t₂.insertIfNew k v)
-- Mathlib.Data.Setoid.Basic
/-- Defining `≤` for equivalence relations.  -/
Setoid.instLE_mathlib : {α : Type u_1} → LE (Setoid α)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.symmetry : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.SymmetricCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.instNonemptyObjSimplexCategoryStdSimplex : ∀ (n : SimplexCategory), (SSet.stdSimplex.obj n).Nonempty
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.eval_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R], f.eval 0 = 0
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- Given a Type `R` with a `Language.ring.Structure R`, the instance given by
`addOfRingStructure` etc. are compatible with the `Language.ring.Structure` instance on `R`.

This definition is only to be used when `addOfRingStructure`, `mulOfRingStructure` etc
are local instances.
 -/
FirstOrder.Ring.compatibleRingOfRingStructure : (R : Type u_2) → [inst : FirstOrder.Language.ring.Structure R] → FirstOrder.Ring.CompatibleRing R
-- Mathlib.Order.Category.Frm
Frm.coe_of : ∀ (X : Type u) [inst : Order.Frame X], ↑{ carrier := X, str := inst } = X
-- Aesop.Tree.State
Aesop.GoalRef.checkAndMarkUnprovable : Aesop.GoalRef → BaseIO Unit
-- Mathlib.Logic.Equiv.Multiset
_private.Mathlib.Logic.Equiv.Multiset.0.instDecidableRelEnle : {α : Type u_1} → [inst : Encodable α] → DecidableRel enle✝
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_toContinuousLinearMap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E), (LinearMap.toContinuousLinearMap T).IsPositive ↔ T.IsPositive
-- Lean.Elab.Tactic.Omega.Frontend
/-- Process all the facts in a `MetaProblem`, returning the new problem, and the number of new facts.

This is partial because new facts may be generated along the way.
 -/
Lean.Elab.Tactic.Omega.MetaProblem.processFacts : Lean.Elab.Tactic.Omega.MetaProblem → Lean.Elab.Tactic.Omega.OmegaM (Lean.Elab.Tactic.Omega.MetaProblem × ℕ)
-- Mathlib.SetTheory.Cardinal.ToNat
/-- A `Cardinal.toNat` version of `eq_of_forall_le_iff`.
This is useful for proving equality of `Module.finrank`.  -/
Cardinal.toNat_eq_of_forall_le_iff : ∀ {c : Cardinal.{u}} {d : Cardinal.{v}}, (∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d) → Cardinal.toNat c = Cardinal.toNat d
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β}, m.WF → (m.alter k f)[k]? = f m[k]?
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalLeftDistrib.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C],
  autoParam
      (∀ (X : C),
        CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
          (CategoryTheory.MonoidalCategory.tensorLeft X))
      CategoryTheory.IsMonoidalLeftDistrib.preservesBinaryCoproducts_tensorLeft._autoParam →
    CategoryTheory.IsMonoidalLeftDistrib C
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, m.contains k = true → m.getKey? k = some k
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- A `BoxIntegral`, indexed by a positive integer `n` and `ν : ι → ℤ`, with corners `ν i / n`
and of side length `1 / n`.  -/
BoxIntegral.unitPartition.box : {ι : Type u_1} → (n : ℕ) → [NeZero n] → (ι → ℤ) → BoxIntegral.Box ι
-- Mathlib.Order.ModularLattice
/-- `a` and `b` both cover `a ⊓ b` if `a ⊔ b` covers either `a` or `b`  -/
IsLowerModularLattice.inf_covBy_of_covBy_sup : ∀ {α : Type u_2} {inst : Lattice α} [self : IsLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b
-- Mathlib.NumberTheory.Real.Irrational
Irrational.intCast_div : ∀ {x : ℝ}, Irrational x → ∀ {m : ℤ}, m ≠ 0 → Irrational (↑m / x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.contains (t.minKey he) = true
-- Mathlib.ModelTheory.LanguageMap
/-- The inclusion of the right factor into the sum of two languages.  -/
FirstOrder.Language.LHom.sumInr : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → L' →ᴸ L.sum L'
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicativeRight_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (f : α →* Multiplicative β)
  (a : Additive α), (AddMonoidHom.toMultiplicativeRight.symm f) a = Multiplicative.toAdd (f (Additive.toMul a))
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.trivialIsNilpotent : ∀ (L : Type v) (M : Type w) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [LieModule.IsTrivial L M], LieModule.IsNilpotent L M
-- Mathlib.Algebra.Group.Conj
IsConj.pow : ∀ {α : Type u} [inst : Monoid α] {a b : α} (n : ℕ), IsConj a b → IsConj (a ^ n) (b ^ n)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsTruncLENatIntEmbeddingDownNat : ComplexShape.embeddingDownNat.IsTruncLE
-- Mathlib.Data.List.Sort
List.SortedLT.getElem_lt_getElem_iff : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α],
  l.SortedLT → ∀ {i j : ℕ} {hi : i < l.length} {hj : j < l.length}, l[i] < l[j] ↔ i < j
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedCosZeta_eq : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.completedCosZeta a s = HurwitzZeta.completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)
-- Mathlib.Algebra.Group.Action.Defs
Function.Injective.mulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : SMul M β]
  (f : β → α) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c • x) = c • f x),
  Function.Injective.mulAction f hf smul = { toSMul := inst_2, mul_smul := ⋯, one_smul := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, (Std.DTreeMap.Const.getThenInsertIfNew? t k v).1 = Std.DTreeMap.Const.get? t k
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` have finite power series `q` and `p` respectively at `f x` and `x`,
then `g ∘ f` admits the finite power series `q.comp p` at `x`.  -/
HasFiniteFPowerSeriesAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [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] {m n : ℕ} {g : F → G} {f : E → F}
  {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFiniteFPowerSeriesAt g q (f x) m →
    HasFiniteFPowerSeriesAt f p x n → 0 < n → HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n)
-- Mathlib.Analysis.Convex.Quasiconvex
Convex.quasiconcaveOn_restrict : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} [inst_4 : Preorder β] {s : Set E} {f : E → β} {t : Set E},
  QuasiconcaveOn 𝕜 s f → t ⊆ s → Convex 𝕜 t → QuasiconcaveOn 𝕜 t f
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurable.congr : ∀ {α : Type u_2} {β : Type u_3} [m : MeasurableSpace α] [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {g : α → β},
  MeasureTheory.NullMeasurable f μ → f =ᵐ[μ] g → MeasureTheory.NullMeasurable g μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDHashMap.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => (f x_2 (m.get x_2 ⋯)).isSome
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_shiftRight : ∀ (a : BitVec 8), ∀ b < 8, { toBitVec := a >>> b } = { toBitVec := a } >>> UInt8.ofNat b
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_integral_tendsto_of_nonneg_ae : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} [l.NeBot]
  [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ℝ} (I : ℝ),
      (∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) →
        (∀ᵐ (x : α) ∂μ, 0 ≤ f x) →
          Filter.Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (nhds I) → MeasureTheory.Integrable f μ
-- Mathlib.Data.Multiset.Defs
Multiset.instHasSubset : {α : Type u_1} → HasSubset (Multiset α)
-- Mathlib.Data.Matrix.Mul
Matrix.ext_iff_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] {A B : Matrix m n α},
  A = B ↔ ∀ (v : m → α), Matrix.vecMul v A = Matrix.vecMul v B
-- Mathlib.Data.ENNReal.Operations
ENNReal.top_mul' : ∀ {a : ENNReal}, ⊤ * a = if a = 0 then 0 else ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.ext : ∀ {R : Type u} {x y : WeierstrassCurve R}, x.a₁ = y.a₁ → x.a₂ = y.a₂ → x.a₃ = y.a₃ → x.a₄ = y.a₄ → x.a₆ = y.a₆ → x = y
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.basis_repr_comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {V : Type u_3}
  [inst_3 : AddCommMonoid V] [inst_4 : Module R V] {W : Type u_4} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module S W] [inst_8 : IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V)
  (ibc : IsBaseChange S ε) (v : V) (i : ι), ((IsBaseChange.basis b ibc).repr (ε v)) i = (algebraMap R S) ((b.repr v) i)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_of_nonpos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, δ ≤ 0 → ∀ (E : Set α), Metric.cthickening δ E = closure E
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.nnnorm_ofSubsingleton_id : ∀ (𝕜 : Type u) (F : Type wF) {ι : Type v} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] [inst_4 : Subsingleton ι] [Nontrivial F] (i : ι),
  ‖(ContinuousAlternatingMap.ofSubsingleton 𝕜 F F i) (ContinuousLinearMap.id 𝕜 F)‖₊ = 1