mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.mul_scalar : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {r s : R}, FreeAlgebra.Rel.below ⋯
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.operating.sizeOf_spec : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] [inst_1 : (a : String.Slice) → SizeOf (σ a)]
  [inst_2 : SizeOf ρ] (currPos : s.Pos) (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)),
  sizeOf (String.Slice.RevSplitIterator.operating currPos searcher) = 1 + sizeOf currPos + sizeOf searcher
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The Pell `x` sequence.  -/
Pell.xn : {a : ℕ} → 1 < a → ℕ → ℕ
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `ℓ¹(ι, E)` is the space of summable functions `ι → E`. To be more precise, it is the space
of functions whose *norms* are summable, but when `E` is complete these coincide.  -/
lp.«termℓ¹(_,_)» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f]
  (U : { U // ↑U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }),
  ↑((RelIso.symm (AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv f)) U) =
    (TopologicalSpace.Opens.map f.base).obj ↑↑U
-- Mathlib.Data.NNReal.Defs
Real.lt_toNNReal_iff_coe_lt : ∀ {r : NNReal} {p : ℝ}, r < p.toNNReal ↔ ↑r < p
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverse.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (f : ℕ → R) (hf : Invertible (f 1)),
  ArithmeticFunction.dirichletInverse f hf = { toFun := ArithmeticFunction.dirichletInverseFun f hf, map_zero' := ⋯ }
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_all_iff : ∀ {α β : Type u} {f : α → β} {p : β → Prop} {s : Stream'.Seq α}, (∀ x ∈ Stream'.Seq.map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x
-- Mathlib.MeasureTheory.Function.Egorov
/-- **Egorov's theorem**: If `f : ι → α → β` is a sequence of functions that
converges to `g : α → β` almost everywhere on a measurable set `s` of finite measure,
and the distance between `f n a` and `g a` is measurable for all `n`,
then for all `ε > 0`, there exists a subset `t ⊆ s` such that `μ t ≤ ε` and `f` converges to `g`
uniformly on `s \ t`. We require the index type `ι` to be countable, and usually `ι = ℕ`.

In other words, a sequence of almost everywhere convergent functions converges uniformly except on
an arbitrarily small set.  -/
MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β}
  {s : Set α},
  (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) →
    MeasurableSet s →
      μ s ≠ ⊤ →
        (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
          ∀ {ε : ℝ},
            0 < ε → ∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)
-- Init.Data.SInt.Lemmas
instCommutativeInt64HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.ext_ring : ∀ {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra S B] [inst_6 : Algebra R S]
  [inst_7 : Algebra R B] [inst_8 : IsScalarTower R S B] {f g : TensorProduct R S A →ₐ[S] B},
  (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight =
      (AlgHom.restrictScalars R g).comp Algebra.TensorProduct.includeRight →
    f = g
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Composition of adjunctions.  -/
CategoryTheory.Bicategory.Adjunction.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f₁ : a ⟶ b} →
        {g₁ : b ⟶ a} →
          {f₂ : b ⟶ c} →
            {g₂ : c ⟶ b} →
              CategoryTheory.Bicategory.Adjunction f₁ g₁ →
                CategoryTheory.Bicategory.Adjunction f₂ g₂ →
                  CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.comp f₁ f₂)
                    (CategoryTheory.CategoryStruct.comp g₂ g₁)
-- Mathlib.Order.WithBot
WithBot.decidableLE : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → DecidableLE (WithBot α)
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.cderiv_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {r : ℝ} {f g : ℂ → E},
  0 < r →
    ContinuousOn f (Metric.sphere z r) →
      ContinuousOn g (Metric.sphere z r) → Complex.cderiv r (f - g) z = Complex.cderiv r f z - Complex.cderiv r g z
-- Mathlib.Algebra.Category.Ring.FinitePresentation
/-- Given a filtered diagram `F` of rings over `R`, `S` a finitely presented `R`-algebra,
and a ring hom `g : S ⟶ colimit F` over `R`.
then there exists `i` such that `g` factors through `Fᵢ`.
In other words, the map `colimᵢ Hom_R(S, Fᵢ) ⟶ Hom_R(S, colim F)` is surjective.
 -/
RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit : ∀ {J : Type uJ} [inst : CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat)
  (F : CategoryTheory.Functor J CommRingCat) (α : (CategoryTheory.Functor.const J).obj R ⟶ F) {S : CommRingCat}
  (f : R ⟶ S) (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget CommRingCat)],
  (CommRingCat.Hom.hom f).FinitePresentation →
    ∀ (g : S ⟶ c.pt),
      (∀ (i : J), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp (α.app i) (c.ι.app i)) →
        ∃ i g',
          CategoryTheory.CategoryStruct.comp f g' = α.app i ∧ g = CategoryTheory.CategoryStruct.comp g' (c.ι.app i)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisNamedArg : Lean.Options → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.keyAtIdxD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : α}, t₁.Equiv t₂ → t₁.keyAtIdxD i fallback = t₂.keyAtIdxD i fallback
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- Circle integrability of the term `logCounting f · R` that appears in Cartan's formula.
 -/
ValueDistribution.circleIntegrable_logCounting : ∀ {f : ℂ → ℂ} {R : ℝ}, Meromorphic f → CircleIntegrable (fun x => ValueDistribution.logCounting f (↑x) R) 0 1
-- Aesop.RuleSet
Aesop.LocalRuleSet.empty : Aesop.LocalRuleSet
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Seminormed ring structure on the product of two seminormed rings,
using the sup norm.  -/
Prod.seminormedRing : {α : Type u_2} → {β : Type u_3} → [SeminormedRing α] → [SeminormedRing β] → SeminormedRing (α × β)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineEquiv.ofEq_rfl : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) [inst_4 : Nonempty ↥S₁],
  AffineEquiv.ofEq S₁ S₁ ⋯ = AffineEquiv.refl k ↥S₁
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The single object pre-`0`-hypercover obtained from taking the coproduct of the components.  -/
CategoryTheory.PreZeroHypercover.sigmaOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        {c : CategoryTheory.Limits.Cofan E.X} → CategoryTheory.Limits.IsColimit c → CategoryTheory.PreZeroHypercover S
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.le_rank_iff_exists_linearIndependent : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] {c : Cardinal.{v'}} {f : V →ₗ[K] V'},
  c ≤ f.rank ↔ ∃ s, Cardinal.lift.{v', v} (Cardinal.mk ↑s) = Cardinal.lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s
-- Init.Data.UInt.Lemmas
UInt16.toNat_mod : ∀ (a b : UInt16), (a % b).toNat = a.toNat % b.toNat
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.minKey? = none
-- Lean.Compiler.ExternAttr
Lean.getExternEntryFor : Lean.ExternAttrData → Lean.Name → Option Lean.ExternEntry
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.jmp.injEq : ∀ (ref : Lean.Syntax) (jpName : Lean.Name) (args : Array Lean.Syntax) (ref_1 : Lean.Syntax) (jpName_1 : Lean.Name)
  (args_1 : Array Lean.Syntax),
  (Lean.Elab.Term.Do.Code.jmp ref jpName args = Lean.Elab.Term.Do.Code.jmp ref_1 jpName_1 args_1) =
    (ref = ref_1 ∧ jpName = jpName_1 ∧ args = args_1)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.unitCompPartialBijective_symm_natural : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (A : C) {B B' : C} (h : B ⟶ B')
  (hB : i.essImage B) (hB' : i.essImage B') (f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ B),
  (CategoryTheory.unitCompPartialBijective A hB').symm (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB).symm f) h
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.simpleFunc_bot : ∀ {β : Type u_2} {α : Type u_5} (f : MeasureTheory.SimpleFunc α β) [Nonempty β], ∃ c, ∀ (x : α), f x = c
-- Init.Data.SInt.Lemmas
Int32.ofIntClamp.eq_1 : ∀ (i : ℤ),
  Int32.ofIntClamp i =
    if hl : Int32.minValue.toInt ≤ i then
      if hr : i ≤ Int32.maxValue.toInt then Int32.ofIntLE i hl hr else Int32.maxValue
    else Int32.minValue
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- A class of morphisms `W` in a monoidal category is monoidal if it is multiplicative
and stable under left and right whiskering. Under this condition, the localized
category can be equipped with a monoidal category structure, see `LocalizedMonoidal`.  -/
CategoryTheory.MorphismProperty.IsMonoidal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → [CategoryTheory.MonoidalCategory C] → Prop
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.InternalCombinators.map.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] (lift : ⦃α : Type w⦄ → m α → n α)
  [inst_1 : Std.Iterator α m β] (f : β → Std.Iterators.PostconditionT n γ) (it : Std.IterM m β),
  Std.IterM.InternalCombinators.map lift f it = { internalState := { inner := it } }
-- Mathlib.Tactic.Translate.Core
/-- Warn the user when the declaration has a parametric attribute.  -/
Mathlib.Tactic.Translate.warnParametricAttr : {β : Type} →
  [Inhabited β] →
    Lean.Syntax → Lean.ParametricAttribute β → Lean.Name → Lean.Name → Lean.Name → Lean.Name → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The pullback of a monomorphism along itself is isomorphic to the top object.  -/
CategoryTheory.MonoOver.pullbackSelf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {A B : C} →
        (f : A ⟶ B) →
          [inst_2 : CategoryTheory.Mono f] → (CategoryTheory.MonoOver.pullback f).obj (CategoryTheory.MonoOver.mk f) ≅ ⊤
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instMinSubtypeMem : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → Min ↥L
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMax_eq_insertMax! : ∀ {α : Type u} {β : α → Type v} [Ord α] {a : α} {b : β a} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced),
  (Std.DTreeMap.Internal.Impl.insertMax a b t htb).impl = Std.DTreeMap.Internal.Impl.insertMax! a b t
-- Lean.IdentifierSuggestion
/-- Given a name, find all the stored correct, existing identifiers that mention that name in a
`suggest_for` annotation.
 -/
Lean.getSuggestions : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Lean.NameSet
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
isAddFundamentalDomain_Ioc : ∀ {T : ℝ},
  0 < T →
    ∀ (t : ℝ) (μ : autoParam (MeasureTheory.Measure ℝ) isAddFundamentalDomain_Ioc._auto_1),
      MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T)) (Set.Ioc t (t + T)) μ
-- Mathlib.Analysis.Analytic.Inverse
/-- The right inverse does not depend on the zeroth coefficient of a formal multilinear
series.  -/
FormalMultilinearSeries.rightInv_removeZero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E), p.removeZero.rightInv i x = p.rightInv i x
-- Mathlib.Algebra.Star.Free
FreeAlgebra.star_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} (r : R),
  star ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)) r
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_iff_nonneg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) {b : α},
  a ≤ b + a ↔ 0 ≤ b
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.le_comap_of_map_le : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F},
  Submonoid.map f S ≤ T → S ≤ Submonoid.comap f T
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.toLinearMap_convMul : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A] (f g : WithConv (C →ₐ[R] A)),
  WithConv.toConv (f * g).ofConv.toLinearMap =
    WithConv.toConv f.ofConv.toLinearMap * WithConv.toConv g.ofConv.toLinearMap
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_mono_left : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup N),
  Monotone fun K => K.prod H
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.horn.spineId_vertex_coe : ∀ {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) (j : Fin (n + 2 + 1)),
  ↑((SSet.horn.spineId i h₀ hₙ).vertex j) = SSet.stdSimplex.const (n + 2) j (Opposite.op { len := 0 })
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- If `D` is a `V`-enriched category, then forgetting the enrichment and transporting the resulting
enriched ordinary category along a functor `F : V ⥤ W`, for which
`f ↦ Functor.LaxMonoidal.ε F ≫ F.map f` has an inverse, results in a category equivalent to
transporting along `F` and then forgetting about the resulting `W`-enrichment.  -/
CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {W : Type u''} →
        [inst_2 : CategoryTheory.Category.{v'', u''} W] →
          [inst_3 : CategoryTheory.MonoidalCategory W] →
            (F : CategoryTheory.Functor V W) →
              [inst_4 : F.LaxMonoidal] →
                (D : Type u) →
                  [inst_5 : CategoryTheory.EnrichedCategory V D] →
                    (e :
                        (v : V) →
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) →
                      (∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
                          (e v) f =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) →
                        (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D) ≌
                          CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D))
-- Mathlib.NumberTheory.SmoothNumbers
Nat.factoredNumbers_mono : ∀ {s t : Finset ℕ}, s ⊆ t → Nat.factoredNumbers s ⊆ Nat.factoredNumbers t
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkIrrelevance : Aesop.MVarClusterRef → Lean.CoreM Unit
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F], DifferentiableOn 𝕜 f s → ∀ (c : R), DifferentiableOn 𝕜 (c • f) s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) =
    f
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.pmul_apply : ∀ {R : Type u_1} [inst : MulZeroClass R] {f g : ArithmeticFunction R} {x : ℕ}, (f.pmul g) x = f x * g x
-- Init.Data.String.Basic
String.Slice.Pos.le_endPos : ∀ {s : String.Slice} (p : s.Pos), p ≤ s.endPos
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivWithinAt.smul` -/
HasDerivWithinAt.fun_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'}
  {c' : 𝕜'},
  HasDerivWithinAt c c' s x →
    HasDerivWithinAt f f' s x → HasDerivWithinAt (fun i => c i • f i) (c x • f' + c' • f x) s x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.algebraMap_injective : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R], Function.Injective ⇑(algebraMap R (QuaternionAlgebra R c₁ c₂ c₃))
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.add_tprodCoeff : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
  PiTensorProduct.tprodCoeff R z (Function.update f i m₁) + PiTensorProduct.tprodCoeff R z (Function.update f i m₂) =
    PiTensorProduct.tprodCoeff R z (Function.update f i (m₁ + m₂))
-- Mathlib.Order.Disjointed
biUnion_Iic_disjointed : ∀ {ι : Type u_2} [inst : PartialOrder ι] [inst_1 : LocallyFiniteOrderBot ι] {α : Type u_3} (f : ι → Set α) (n : ι),
  ⋃ i ∈ Finset.Iic n, disjointed f i = (partialSups f) n
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_toLp : ∀ (p : ENNReal) {V : Type u_4} (x : V), (WithLp.toLp p x).ofLp = x
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.categoryWithHomology_of_abelian : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.CategoryWithHomology C
-- Mathlib.LinearAlgebra.Span.TensorProduct
/-- If `A` is an `R`-algebra and `p` is an `R`-submodule of an `A`-module `M`, this is the natural
surjection `A ⊗[R] p → span A p`.

See also `Submodule.tensorEquivSpan`.  -/
Submodule.tensorToSpan : {R : Type u_1} →
  (A : Type u_2) →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] →
                  [IsScalarTower R A M] → (p : Submodule R M) → TensorProduct R A ↥p →ₗ[A] ↥(Submodule.span A ↑p)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [Inhabited α] {k k' : α} (h : (↑m).WF) {f : Option β → Option β}
  (hc : (Std.DHashMap.Internal.Raw₀.Const.alter m k f).contains k' = true),
  (Std.DHashMap.Internal.Raw₀.Const.alter m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors is π, the inner product equals the negative product
of the norms.  -/
InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = Real.pi → inner ℝ x y = -(‖x‖ * ‖y‖)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_toReal_of_lintegral_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → MeasureTheory.Integrable (fun x => (f x).toReal) μ
-- Mathlib.Algebra.Lie.Abelian
LieModule.maxTrivSubmodule.congr_simp : ∀ (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],
  LieModule.maxTrivSubmodule R L M = LieModule.maxTrivSubmodule R L M
-- Mathlib.Algebra.Module.Submodule.Basic
/-- Subspace of a vector space. Defined to equal `Submodule`.  -/
Subspace : (R : Type u) → (M : Type v) → [inst : DivisionRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Type v
-- Std.Data.ExtHashMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set
unchanged if a matching key is already present.
 -/
Std.ExtHashMap.insert : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → β → Std.ExtHashMap α β
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {y : N},
  y ∈ Subsemigroup.map f S ↔ ∃ x ∈ S, f x = y
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.surjective : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → Function.Surjective ⇑f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.foldM_eq_foldlM_keysArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  m.WF → Std.HashMap.Raw.foldM (fun d a x => f d a) init m = Array.foldlM f init m.keysArray