mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insert_le_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t.isEmpty = false}, (cmp ((t.insert k v).minKey ⋯) (t.minKey he)).isLE = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {he : t ≠ ∅} {km : α}, t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.Data.Range.Polymorphic.RangeIterator
Std.IterM.IsPlausibleSkipSuccessorOf.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it' it : Std.IterM m β),
  it'.IsPlausibleSkipSuccessorOf it = it.IsPlausibleStep (Std.IterStep.skip it')
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.apply_union_le_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid β] [inst_1 : Preorder β] [AddLeftMono β]
  {f : Set α → β},
  f ∅ = 0 →
    (∀ {s t : Set α}, f (s ∪ t) ≤ f s + f t) → ∀ {s : ι → Set α} (t : Finset ι), f (⋃ i ∈ t, s i) ≤ ∑ i ∈ t, f (s i)
-- Mathlib.Data.NNReal.Defs
NNReal.instNoZeroDivisors : NoZeroDivisors NNReal
-- Mathlib.Analysis.Complex.Cardinality
/-- The cardinality of the complex numbers, as a set.  -/
Cardinal.mk_univ_complex : Cardinal.mk ↑Set.univ = Cardinal.continuum
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.cocones_obj_obj : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : (CategoryTheory.Functor J C)ᵒᵖ) (X : C),
  ((CategoryTheory.cocones J C).obj F).obj X = (Opposite.unop F ⟶ (CategoryTheory.Functor.const J).obj X)
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.polynomialEquiv_comp_D : ∀ (R : Type u) [inst : CommRing R],
  (KaehlerDifferential.polynomialEquiv R).compDer (KaehlerDifferential.D R (Polynomial R)) = Polynomial.derivative'
-- Mathlib.Order.TypeTags
WithTop.some.eq_1 : ∀ {α : Type u_1}, WithTop.some = some
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀),
  CategoryTheory.CategoryStruct.comp (E.forkOfIsColimit hc hd F).ι (F.map (c.inj i).op) = F.map (E.f i).op
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.edist_le_two : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → EDist (F i)] {x y : (i : ι) → F i},
  edist x y ≤ 2
-- Lean.Exception
Lean.Exception.internal.injEq : ∀ (id : Lean.InternalExceptionId) (extra : Lean.KVMap) (id_1 : Lean.InternalExceptionId) (extra_1 : Lean.KVMap),
  (Lean.Exception.internal id extra = Lean.Exception.internal id_1 extra_1) = (id = id_1 ∧ extra = extra_1)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_empty_union_closure_eq : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure ∅ ∪ M.closure X = M.closure X
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- `NonarchAddGroupSeminormClass F α` states that `F` is a type of nonarchimedean seminorms on
the additive group `α`.

You should extend this class when you extend `NonarchAddGroupSeminorm`.  -/
NonarchAddGroupSeminormClass : (F : Type u_6) → (α : outParam (Type u_7)) → [AddGroup α] → [FunLike F α ℝ] → Prop
-- Mathlib.Data.Num.ZNum
ZNum.pred.eq_1 : ZNum.zero.pred = ZNum.neg 1
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.iUnion_of_monotone_of_frequently : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_5} [inst_1 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {s : ι → Set α}, Monotone s → (∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i)) → MeasurableSet (⋃ i, s i)
-- Aesop.RuleTac.Cases
Aesop.CasesTarget.toCasesTarget' : Aesop.CasesTarget → Lean.MetaM Aesop.CasesTarget'
-- Mathlib.Data.Analysis.Filter
CFilter.toFilter.eq_1 : ∀ {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ),
  F.toFilter = { sets := {a | ∃ b, F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $(X_i)_{i \in \iota}$ are jointly Gaussian and uncorrelated, then they are independent.  -/
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDual : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {E : ι → Type u_3}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → MeasurableSpace (E i)]
  [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)]
  [inst_5 : (i : ι) → NormedSpace ℝ (E i)] {X : (i : ι) → Ω → E i},
  ProbabilityTheory.HasGaussianLaw (fun ω i => X i ω) P →
    (∀ (i j : ι),
        i ≠ j →
          ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
            ProbabilityTheory.covariance (⇑L₁ ∘ X i) (⇑L₂ ∘ X j) P = 0) →
      ProbabilityTheory.iIndepFun X P
-- Init.System.IO
/-- Runs an action with the specified stream `h` as standard output, restoring the original standard
output stream afterwards.
 -/
IO.withStdout : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT BaseIO m] → IO.FS.Stream → m α → m α
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul : ∀ {f : ℝ → ℝ},
  MeasurableEmbedding f →
    ∀ {s : Set ℝ},
      MeasurableSet s →
        ∀ {g : ℝ → ℝ},
          (∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x) →
            MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume →
              ∀ {f' : ℝ → ℝ},
                (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
                  (MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s =
                    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
-- Mathlib.Order.RelClasses
IsWellOrder.mk : ∀ {α : Type u} {r : α → α → Prop} [toIsWellFounded : IsWellFounded α r] [toTrichotomous : Std.Trichotomous r],
  IsWellOrder α r
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.coe_GL_coe_matrix : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (g : Matrix.SpecialLinearGroup n R), ↑(Matrix.SpecialLinearGroup.toGL g) = ↑g
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_C : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
  p.comp (Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.cpolynomialAt : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F)
  {x : (i : ι) → Em i}, CPolynomialAt 𝕜 (⇑f) x
-- Mathlib.Order.BooleanAlgebra.Basic
compl_le_of_compl_le : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], yᶜ ≤ x → xᶜ ≤ y
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_zero_atTop_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G),
  MapClusterPt 0 Filter.atTop fun x_1 => x_1 • x
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.map_sub_sprod_roots_eq_prod_map_eval : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (s : Multiset R) (g : Polynomial R),
  g.Monic →
    g.Splits →
      (Multiset.map (fun ij => ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x => Polynomial.eval x g) s).prod
-- Mathlib.Algebra.Free
FreeAddSemigroup.map_add' : ∀ {α β : Type u} (f : α → β) (x y : FreeAddSemigroup α), f <$> (x + y) = f <$> x + f <$> y
-- Init.Data.SInt.Bitwise
ISize.xor_right_inj : ∀ {a b : ISize} (c : ISize), c ^^^ a = c ^^^ b ↔ a = b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).getKey? k = t₁.getKey? k
-- Mathlib.GroupTheory.OrderOfElement
image_range_orderOf : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G} [inst_2 : DecidableEq G],
  Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (↑(Subgroup.zpowers x)).toFinset
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.addCommSemigroup.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommSemigroup α],
  Finset.addCommSemigroup = Function.Injective.addCommSemigroup SetLike.coe ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (lk : α) →
                  (lv : β lk) →
                    (size_1 : ℕ) →
                      (lrk : α) →
                        (lrv : β lrk) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                                (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r))) →
              ((size : ℕ) →
                  (lk : α) →
                    (lv : β lk) →
                      (size_1 : ℕ) →
                        (k : α) →
                          (v : β k) →
                            (l r : Std.DTreeMap.Internal.Impl α β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size lk lv
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k v l r) Std.DTreeMap.Internal.Impl.leaf)) →
                ((ls : ℕ) →
                    (lk : α) →
                      (lv : β lk) →
                        (size : ℕ) →
                          (k : α) →
                            (v : β k) →
                              (l r : Std.DTreeMap.Internal.Impl α β) →
                                (lrs : ℕ) →
                                  (k_1 : α) →
                                    (v_1 : β k_1) →
                                      (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                                        motive
                                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                            (Std.DTreeMap.Internal.Impl.inner size k v l r)
                                            (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1))) →
                  motive l
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
logDeriv_prod_sineTerm_eq_sum_cotTerm : ∀ {x : ℂ},
  x ∈ Complex.integerComplement →
    ∀ (n : ℕ), logDeriv (fun z => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_le_of_left_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.PartialOrder.rel P R → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R
-- Mathlib.RingTheory.Localization.NormTrace
/-- Let `S` be an extension of `R` and `Rₘ Sₘ` be localizations at `M` of `R S` respectively. Let
`b` be an `R`-basis of `S`. Then discriminant of the `Rₘ`-basis of `Sₘ` induced by `b` is the
discriminant of `b`.
 -/
Algebra.discr_localizationLocalization : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] (M : Submonoid R) [inst_5 : IsLocalization M Rₘ] (Sₘ : Type u_5)
  [inst_6 : CommRing Sₘ] [inst_7 : Algebra S Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [inst_10 : IsScalarTower R Rₘ Sₘ] [inst_11 : IsScalarTower R S Sₘ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {ι : Type u_6} [inst_13 : Fintype ι]
  [inst_14 : DecidableEq ι] (b : Module.Basis ι R S),
  Algebra.discr Rₘ ⇑(Module.Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (Algebra.discr R ⇑b)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equalizer inclusion for `(f, f)` is an isomorphism.  -/
CategoryTheory.Limits.equalizer.ι_of_self : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.ι f f)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_eq : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p), p.copy s hs = p
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_le_of_contravariant_eq_and_lt : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N] [ContravariantClass M N μ fun x1 x2 => x1 = x2]
  [ContravariantClass M N μ fun x1 x2 => x1 < x2], ContravariantClass M N μ fun x1 x2 => x1 ≤ x2
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Bundled graded (semi)ring homomorphisms. Use `GradedRingHom` for the namespace and other
identifiers, and `𝒜 →+*ᵍ ℬ` for the notation.  -/
«term_→+*ᵍ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.neg_top : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α], -⊤ = ⊤
-- Mathlib.Algebra.CharP.Defs
expChar_one : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] [CharZero R], ExpChar R 1
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EST.bind.eq_1 : ∀ {ε σ α β : Type} (x : EST ε σ α) (f : α → EST ε σ β) (s : Void σ),
  x.bind f s =
    match x s with
    | EST.Out.ok a s => f a s
    | EST.Out.error e s => EST.Out.error e s
-- Mathlib.Order.Hom.Basic
OrderHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), OrderHom.id.comp f = f
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- An enriched ordinary category is a category `C` that is also enriched
over a category `V` in such a way that morphisms `X ⟶ Y` in `C` identify
to morphisms `𝟙_ V ⟶ (X ⟶[V] Y)` in `V`.  -/
CategoryTheory.EnrichedOrdinaryCategory : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max (max u u') v) v')
-- Init.Data.UInt.Lemmas
UInt32.mul_zero : ∀ {a : UInt32}, a * 0 = 0
-- Mathlib.Tactic.Variable
/-- Strip off whitespace and comments.  -/
Mathlib.Command.Variable.cleanBinders : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder
-- Mathlib.Order.BoundedOrder.Lattice
max_top_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] (a : α), max a ⊤ = ⊤
-- Mathlib.Data.Rat.Defs
/-- **Alias** of `Rat.mkRat_self`. -/
Rat.mkRat_num_den' : ∀ (a : ℚ), mkRat a.num a.den = a
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_sSup : ∀ {M : Type u_2} [inst : MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)), (sSup S).unop = sSup (Submonoid.op ⁻¹' S)
-- Mathlib.ModelTheory.Substructures
/-- Reduces the language of a substructure along a language hom.  -/
FirstOrder.Language.LHom.substructureReduct : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      {L' : FirstOrder.Language} →
        [inst_1 : L'.Structure M] → (φ : L →ᴸ L') → [φ.IsExpansionOn M] → L'.Substructure M ↪o L.Substructure M
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.truncTotalAlgHom.congr_simp : ∀ (σ : Type u_3) (R : Type u_4) [inst : Finite σ] [inst_1 : CommRing R] (n : ℕ),
  MvPowerSeries.truncTotalAlgHom σ R n = MvPowerSeries.truncTotalAlgHom σ R n
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
/-- If `NormedSpace.exp R x.fst` converges to `e`
then `NormedSpace.exp R x` converges to `inl e + inr (e • x.snd)`.  -/
TrivSqZeroExt.hasSum_expSeries_of_smul_comm : ∀ (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field 𝕜] [CharZero 𝕜] [inst_2 : Ring R] [inst_3 : AddCommGroup M]
  [inst_4 : Algebra 𝕜 R] [inst_5 : Module 𝕜 M] [inst_6 : Module R M] [inst_7 : Module Rᵐᵒᵖ M]
  [inst_8 : SMulCommClass R Rᵐᵒᵖ M] [inst_9 : IsScalarTower 𝕜 R M] [inst_10 : IsScalarTower 𝕜 Rᵐᵒᵖ M]
  [inst_11 : TopologicalSpace R] [inst_12 : TopologicalSpace M] [inst_13 : IsTopologicalRing R]
  [inst_14 : IsTopologicalAddGroup M] [inst_15 : ContinuousSMul R M] [inst_16 : ContinuousSMul Rᵐᵒᵖ M]
  (x : TrivSqZeroExt R M),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd →
    ∀ {e : R},
      HasSum (fun n => (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) e →
        HasSum (fun n => (NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun x_1 => x)
          (TrivSqZeroExt.inl e + TrivSqZeroExt.inr (e • x.snd))
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_sub_of_add_le_left : ∀ {a b c : ENNReal}, a ≠ ⊤ → a + b ≤ c → b ≤ c - a
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatch_iff : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat
-- Mathlib.Algebra.Regular.Basic
/-- If a sum is add-regular, so is its left summand.  -/
IsAddRegular.of_add_left : ∀ {R : Type u_1} [inst : AddCommSemigroup R] {a b : R}, IsAddRegular (a + b) → IsAddRegular a
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If `η_A` is an isomorphism, then `A` is in the essential image of `i`.  -/
CategoryTheory.Adjunction.mem_essImage_of_unit_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (A : C)
  [CategoryTheory.IsIso (h.unit.app A)], R.essImage A
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.iSupLift_comp_inclusion : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] {ι : Sort u_1} [inst_7 : Nonempty ι] {K : ι → NonUnitalSubalgebra R A}
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A}
  {hT : T = iSup K} {i : ι} (h : K i ≤ T),
  (NonUnitalSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalSubalgebra.inclusion h) = f i
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_lt_disjSum_of_lt_of_le : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} {t₁ t₂ : Multiset β},
  s₁ < s₂ → t₁ ≤ t₂ → s₁.disjSum t₁ < s₂.disjSum t₂
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrLeftₐ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : CommSemiring R] [inst_3 : Semiring Z] [inst_4 : Algebra R Z] (e : X ≃ₜ Y) (g : LocallyConstant X Z) (a : Y),
  ((LocallyConstant.congrLeftₐ R e) g) a = g (e.symm a)
-- Init.Data.Float.Model.Float
Float.Model.instMin : Min Float.Model
-- Mathlib.Algebra.GroupWithZero.Defs
SemigroupWithZero.toMulZeroClass : {S₀ : Type u} → [self : SemigroupWithZero S₀] → MulZeroClass S₀
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doMatch; doElems`  -/
Lean.Elab.Term.Do.ToCodeBlock.doMatchToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Data.Set.Lattice
Set.sUnion_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α), ⋃₀ (f '' s) = ⋃ a ∈ s, f a
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {Y Y' : C} (g : Y ⟶ Y') (f : Opposite.unop X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g))
      (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm f) =
    CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.to_topologicalAddGroup : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R],
  IsTopologicalAddGroup R
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonzero, nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f` is nonzero.  -/
seminormFromBounded_nonzero : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  f ≠ 0 → 0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → seminormFromBounded' f ≠ 0
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul_of_lt_of_le' : ∀ {a c b d : ℕ}, a < c → b ≤ d → 0 < b → a * b < c * d
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.DTreeMap.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Const.get t k h) = true
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
/-- The first marginal of a product probability measure is the first probability measure.  -/
MeasureTheory.ProbabilityMeasure.map_fst_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β), (μ.prod ν).map ⋯ = μ