mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonUnitalSeminormedCommRing.mul_comm : ∀ {α : Type u_5} [self : NonUnitalSeminormedCommRing α] (a b : α), a * b = b * a
-- Mathlib.LinearAlgebra.Projection
Submodule.prodEquivOfIsCompl_symm_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) (x : ↥p), (p.prodEquivOfIsCompl q h).symm ↑x = (x, 0)
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.coe_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : CocompactMap β γ) (g : CocompactMap α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Order.ConditionallyCompleteLattice.Group
le_add_ciInf : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : AddGroup α]
  [AddLeftMono α] {a g : α} {h : ι → α}, (∀ (j : ι), a ≤ g + h j) → a ≤ g + iInf h
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.gc_lcs_ucs : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (k : ℕ),
  GaloisConnection (fun N => LieSubmodule.lcs k N) fun N => LieSubmodule.ucs k N
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.mk.injEq : ∀ (ref : Lean.Syntax) (expr : Lean.Expr) (ref_1 : Lean.Syntax) (expr_1 : Lean.Expr),
  ({ ref := ref, expr := expr } = { ref := ref_1, expr := expr_1 }) = (ref = ref_1 ∧ expr = expr_1)
-- Aesop.RuleSet
Aesop.LocalRuleSet.trace : Aesop.LocalRuleSet → Aesop.TraceOption → Lean.CoreM Unit
-- Init.Data.Float.Model.Unpacked.Operations.Div
/-- Returns the accuracy corresponding to the point `y + (num/den)ulp`.

Assumes `num < den`.
 -/
Float.Model.UnpackedFloat.accuracyOfFraction : ℕ → ℕ → Float.Model.UnpackedFloat.Accuracy
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_I_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K], (starRingEnd K) RCLike.I = -RCLike.I
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 g s → AnalyticOnNhd 𝕜 (f - g) s
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by applying the mod operation.
 -/
Std.Time.Internal.Bounded.LE.mod : {n num : ℤ} →
  Std.Time.Internal.Bounded.LE n num → (num : ℤ) → 0 < num → Std.Time.Internal.Bounded.LE (-(num - 1)) (num - 1)
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- The family of `ℂ`-linear combinations of `char he hL w, w : W`, is closed under `star`.  -/
BoundedContinuousFunction.star_mem_range_charAlgHom : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (hL : Continuous fun p => (L p.1) p.2)
  {x : BoundedContinuousFunction V ℂ},
  x ∈ (BoundedContinuousFunction.charAlgHom he hL).range → star x ∈ (BoundedContinuousFunction.charAlgHom he hL).range
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
/-- The `insert_cast_fun foo := ..., ...` command should be used when the translation of some
type `foo` is not definitionally equal to the translation of its value.
It requires a function from the translation of `foo` to the translation of the value of `foo`,
and a function in the opposite direction. For example,

```
to_dual_insert_cast_fun DecidableLE := fun inst a b ↦ inst b a, fun inst a b ↦ inst b a
```

The command internally generates these unfold/refold functions for `foo`, and their translations.
If type checking a term requires the definition `foo` to be unfolded, then before translating
that term, the unfold/refold function is inserted into the term.
As a result, type checking the term won't anymore require unfolding `foo`, so the term
can be safely translated. After translating, the unfold/refold functions are again unfolded.  -/
Mathlib.Tactic.Translate.elabInsertCastFun : Lean.Ident → Lean.Term → Lean.Term → Mathlib.Tactic.Translate.TranslateData → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_comap : ∀ {α : Type ua} {β : Type ub} {f : α → β} {u : UniformSpace β},
  (UniformSpace.comap f u).toTopologicalSpace = TopologicalSpace.induced f u.toTopologicalSpace
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.left_id.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : SizeOf J],
  sizeOf CategoryTheory.BiconeHom.left_id = 1
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.id_comp : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B),
  (StarAlgHom.id R B).comp f = f
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.Commutative ctx.op}
  (lhs rhs : Lean.Grind.AC.Expr) (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_ac_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs = Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' = Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.TransportEnrichment.eComp_eq : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {W : Type v'} [inst_3 : CategoryTheory.Category.{w', v'} W]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.LaxMonoidal]
  (X Y Z : CategoryTheory.TransportEnrichment F C),
  CategoryTheory.eComp W X Y Z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F (X ⟶[V] Y) (Y ⟶[V] Z))
      (F.map (CategoryTheory.eComp V X Y Z))
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Ici_castSucc : ∀ {n : ℕ} (i : Fin n), Fin.castSucc ⁻¹' Set.Ici i.castSucc = Set.Ici i
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.φ_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g)
      CategoryTheory.Limits.biprod.snd =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_map : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β β₂ γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_6 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β}
  {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)},
  forIn (Std.IterM.map f it) init g = forIn it init fun out acc => g (f out) acc
-- Mathlib.Combinatorics.Additive.Corner.Roth
cornersTheoremBound.eq_1 : ∀ (ε : ℝ), cornersTheoremBound ε = ⌊(SimpleGraph.triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ + 1
-- Mathlib.Algebra.DirectSum.Ring
/-- A graded version of `Semiring`.  -/
DirectSum.GSemiring : {ι : Type u_1} → (A : ι → Type u_2) → [AddMonoid ι] → [(i : ι) → AddCommMonoid (A i)] → Type (max u_1 u_2)
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center_eq_top_iff : ∀ {G : Type u_1} [inst : Group G], Subgroup.center G = ⊤ ↔ IsMulCommutative G
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β k}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.differentiableAt_rpow_of_ne : ∀ (p : ℝ × ℝ), p.1 ≠ 0 → DifferentiableAt ℝ (fun p => p.1 ^ p.2) p
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.pair.sizeOf_spec : ∀ {ι : Type v} [inst : SizeOf ι] (a a_1 : ι), sizeOf (CategoryTheory.Pairwise.pair a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- A choice of chart on the domain `M` of a local property of `f` at `x`:
w.r.t. this chart and `h.codChart`, `f` has the local property `P` at `x`.
The particular chart is arbitrary, but this choice matches the witness given by `h.codChart`.  -/
Manifold.LiftSourceTargetPropertyAt.domChart : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              {P :
                                                  (M → N) →
                                                    OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} →
                                                Manifold.LiftSourceTargetPropertyAt I J n f x P →
                                                  OpenPartialHomeomorph M H
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarLeft.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (N : Type u_4) [inst_1 : AddCommMonoid N] [inst_2 : Module R N] (ι : Type u_5)
  [inst_3 : DecidableEq ι],
  TensorProduct.finsuppScalarLeft R N ι =
    (TensorProduct.finsuppLeft R R R N ι).trans (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instLawfulForwardPatternForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.LawfulForwardPattern p
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The iterated derivative of the composition with a linear map on the left is
obtained by applying the linear map to the iterated derivative.  -/
ContinuousLinearMap.iteratedFDeriv_comp_left : ∀ {𝕜 : 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] {x : E} {n : WithTop ℕ∞} {f : E → F} (g : F →L[𝕜] G),
  ContDiffAt 𝕜 n f x →
    ∀ {i : ℕ}, ↑i ≤ n → iteratedFDeriv 𝕜 i (⇑g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the second morphism in a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂ → (T₁.obj₂ ⟶ T₂.obj₂)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_insert_perm : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β k},
      (↑(m.insert k v)).toList.Perm (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) (↑m).toList)
-- Mathlib.Topology.Constructible
Topology.IsConstructible.biInter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {f : ι → Set X} {t : Set ι},
  t.Finite → (∀ i ∈ t, Topology.IsConstructible (f i)) → Topology.IsConstructible (⋂ i ∈ t, f i)
-- Mathlib.Analysis.LocallyConvex.Basic
/-- The union of `{0}` with the interior of a balanced set is balanced.  -/
Balanced.zero_insert_interior : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E], Balanced 𝕜 A → Balanced 𝕜 (insert 0 (interior A))
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.range_mk' : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], (QuotientAddGroup.mk' N).range = ⊤
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.gc_map_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  GaloisConnection (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {f : β → α} {b : β},
  {b}.gcd f = normalize (f b)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `log_stirlingSeq` is bounded below for `n ≥ 1`.  -/
Stirling.log_stirlingSeq_bounded_by_constant : ∀ (n : ℕ), 1 - 12⁻¹ - Real.log 2 / 2 ≤ Real.log (Stirling.stirlingSeq (n + 1))
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_of_orderOf_eq_card : ∀ {α : Type u_1} [inst : Group α] [Finite α] (x : α), orderOf x = Nat.card α → IsCyclic α
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.prime_X : ∀ {R : Type u} [inst : CommRing R] [IsDomain R], Prime Polynomial.X
-- Mathlib.Order.Lex
instNontrivialLex : ∀ (α : Type u_2) [Nontrivial α], Nontrivial (Lex α)
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.ker_eq_bot_of_mono : ∀ {A B : CommGrpCat} (f : A ⟶ B) [CategoryTheory.Mono f], (CommGrpCat.Hom.hom f).ker = ⊥
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget₂AddGroup_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedMor₂ : Inhabited Mathlib.Tactic.BicategoryLike.Mor₂
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanLocationLink.mk.sizeOf_spec : ∀ (toLocationLink : Lean.Lsp.LocationLink) (ident? : Option Lean.Lsp.LeanDeclIdent) (isDefault : Bool),
  sizeOf { toLocationLink := toLocationLink, ident? := ident?, isDefault := isDefault } =
    1 + sizeOf toLocationLink + sizeOf ident? + sizeOf isDefault
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecomposition_spec : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [h : μ.HaveLebesgueDecomposition ν],
  Measurable (μ.rnDeriv ν) ∧ (μ.singularPart ν).MutuallySingular ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_mul_natCast : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_3} [inst : NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ)
  (p : ENNReal) (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (f * ↑n) p μ = MeasureTheory.lpNorm f p μ * ↑n
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_comp : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] {P'' : Type u_4} [inst_5 : CommRing P'']
  [inst_6 : Algebra R P''] (I : FractionalIdeal S P) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P''),
  FractionalIdeal.map (g'.comp g) I = FractionalIdeal.map g' (FractionalIdeal.map g I)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.diagramIsoCospan_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C) (X : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.diagramIsoCospan F).hom.app X = ((fun j => CategoryTheory.eqToIso ⋯) X).hom
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
instIsIntegralPolynomial : ∀ (R : Type u_1) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [int : Algebra.IsIntegral R S], Algebra.IsIntegral (Polynomial R) (Polynomial S)
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_guard : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.findSomeRev? (Option.guard p) = Fin.findRev? p
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.supClosure_apply : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent G C) {s : Set α} {J : Finset (Set α)},
  ↑J ⊆ C → (↑J).PairwiseDisjoint id → s = ⋃₀ ↑J → (m.supClosure hC) s = ∑ s ∈ J, m s
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.finrank_add_finrank_le_of_disjoint : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {s t : Submodule K V},
  Disjoint s t → Module.finrank K ↥s + Module.finrank K ↥t ≤ Module.finrank K V
-- Mathlib.Analysis.Analytic.OfScalars
/-- The radius of convergence of a scalar series is the inverse of the non-zero limit
`fun n ↦ ‖c n.succ‖ / ‖c n‖`.  -/
FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) [NormOneClass E] {r : NNReal},
  r ≠ 0 →
    Filter.Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds ↑r) →
      (FormalMultilinearSeries.ofScalars E c).radius = ↑r⁻¹
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instIsRightCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsRightCancelMulZero α], IsRightCancelMulZero (Lex α)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr : Lean.Meta.Simp.Arith.Nat.LinearExpr → Lean.Expr
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso_inv_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (G : CategoryTheory.Functor H D') {F' : CategoryTheory.Functor D H} (α : F ⟶ L.comp F') (X : D),
  (CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso G α).inv.right.app X =
    CategoryTheory.CategoryStruct.id (G.obj (F'.obj X))
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_four_eq : Real.log 4 = 2 * Real.log 2
-- Mathlib.Analysis.Convex.Function
ConvexOn.lt_left_of_right_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f y < f z → f z < f x
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasProd_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Fintype β] (f : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop], HasProd f (∏ b, f b) L
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The first projection in a product is `C^∞`.  -/
contDiff_fst : ∀ {𝕜 : 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] {n : WithTop ℕ∞},
  ContDiff 𝕜 n Prod.fst
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_toBitVec : ∀ (x : ISize), ISize.ofBitVec x.toBitVec = x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_mul_I : ∀ (x : ℂ), Complex.exp (x * Complex.I) = Complex.cos x + Complex.sin x * Complex.I
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_rci : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound : α),
      Std.Slice.toList (Std.Rci.Sliceable.mkSlice t lowerBound...*) =
        List.filter (fun e => (compare e.fst lowerBound).isGE) t.toList
-- Lean.Meta.Tactic.Grind.Arith.Insts
Lean.Meta.Grind.Arith.getNoZeroDivInst? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- `Abelian.image S.f` is the kernel of `kernel.ι S.g ≫ cokernel.π S.f`  -/
CategoryTheory.ShortComplex.abelianImageToKernelIsKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.abelianImageToKernel ⋯)
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.radical.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] (Q : QuadraticMap R M P),
  Q.radical = { carrier := {x | Q x = 0 ∧ Q.polarBilin x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.fst) = t.keys.forM f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_drop_of_length_le : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} {p : G.Walk u v}, p.length ≤ n → (p.drop n).Nil
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Numerator of the formula for a fractional linear transformation  -/
UpperHalfPlane.num : GL (Fin 2) ℝ → ℂ → ℂ
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashSet.emptyWithCapacity c).isEmpty = true
-- Lean.ProjFns
Lean.getAuxParentProjectionInfo? : {m : Type → Type} → [Lean.MonadEnv m] → [Monad m] → Lean.Name → m (Option Lean.AuxParentProjectionInfo)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis_empty : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {v : ι → F} {i : ι}, Lagrange.basis ∅ v i = 1