mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_self : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  μ.rnDeriv μ =ᵐ[μ] fun x => 1
-- Lean.Data.NameTrie
Lean.NamePart.num.inj : ∀ {n n_1 : ℕ}, Lean.NamePart.num n = Lean.NamePart.num n_1 → n = n_1
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The order of the torsion subgroup.  -/
NumberField.Units.torsionOrder : (K : Type u_1) → [Field K] → ℕ
-- Mathlib.Order.Minimal
/-- **Alias** of `image_antitone_setOfPred_maximal`. -/
image_antitone_setOf_maximal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ x ≤ y)) →
    f '' {x | Maximal P x} = {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Mathlib.Order.OrderDual
OrderDual.ext_iff : ∀ {α : Type u_1} {a b : αᵒᵈ}, a = b ↔ OrderDual.ofDual a = OrderDual.ofDual b
-- Mathlib.Algebra.Group.Action.Units
Units.mulAction'.eq_1 : ∀ {G : Type u_1} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulAction G M]
  [inst_3 : SMulCommClass G M M] [inst_4 : IsScalarTower G M M],
  Units.mulAction' =
    { smul := fun g m => { val := g • ↑m, inv := g⁻¹ • ↑m⁻¹, val_inv := ⋯, inv_val := ⋯ }, mul_smul := ⋯,
      one_smul := ⋯ }
-- Std.Http.Data.Status
Std.Http.Status.unsupportedMediaType.sizeOf_spec : sizeOf Std.Http.Status.unsupportedMediaType = 1
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection in the `Submodule.map` of a subspace.  -/
Submodule.reflection_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E')
  (K : Submodule 𝕜 E) [inst_5 : K.HasOrthogonalProjection],
  (Submodule.map (↑f.toLinearEquiv) K).reflection = f.symm.trans (K.reflection.trans f)
-- Std.Data.DTreeMap.Internal.Def
/-- Computes the size of the tree. Used for verification of iterators.
 -/
Std.DTreeMap.Internal.Impl.treeSize : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ
-- Mathlib.Data.Set.Card
Set.encard_le_coe_iff_finite_ncard_le : ∀ {α : Type u_1} {s : Set α} {k : ℕ}, s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Finset.smul_prod' : ∀ {M : Type u_1} {N : Type u_2} {γ : Type u_3} [inst : Monoid M] [inst_1 : CommMonoid N]
  [inst_2 : MulDistribMulAction M N] {r : M} {f : γ → N} {s : Finset γ}, r • ∏ x ∈ s, f x = ∏ x ∈ s, r • f x
-- Init.Data.Nat.ToString
Nat.ofDigitChars_eq_ofDigitChars_zero : ∀ {l : List Char} {init : ℕ}, Nat.ofDigitChars 10 l init = 10 ^ l.length * init + Nat.ofDigitChars 10 l 0
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.mk : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y.toLocallyRingedSpace → X.Hom Y
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.instReflParallel : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Std.Refl AffineSubspace.Parallel
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_neg : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g : E → 𝕜},
  Function.HasTemperateGrowth g → SchwartzMap.smulLeftCLM F (-g) = -SchwartzMap.smulLeftCLM F g
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.whiskerTop_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {T' : CategoryTheory.Functor C₁ C₂}
  (w : CategoryTheory.TwoSquare T' L R B) (α : T ⟶ T') (X : C₁),
  (w.whiskerTop α).app X = CategoryTheory.CategoryStruct.comp (R.map (α.app X)) (w.natTrans.app X)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
ContinuousLinearMap.coe_smul' : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Lean.Meta.Basic
/-- Remark: we later define `getUnfoldableConst?` at `GetConst.lean` after we define `Instances.lean`.
This method is only used to implement `isClassQuickConst?`.
It is very similar to `getUnfoldableConst?`, but it returns none when `TransparencyMode.instances` and
`constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`.  -/
_private.Lean.Meta.Basic.0.Lean.Meta.getConstTemp? : Lean.Name → Lean.MetaM (Option Lean.ConstantInfo)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f₁ s →
    InnerProductSpace.HarmonicContOnCl f₂ s → InnerProductSpace.HarmonicContOnCl (f₁ + f₂) s
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- The left-inverse of `algebraMap`.  -/
SymmetricAlgebra.algebraMapInv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → SymmetricAlgebra R M →ₐ[R] R
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.Options.mk.inj : ∀ {recursive ignoreIfNotExists recursive_1 ignoreIfNotExists_1 : Bool},
  { recursive := recursive, ignoreIfNotExists := ignoreIfNotExists } =
      { recursive := recursive_1, ignoreIfNotExists := ignoreIfNotExists_1 } →
    recursive = recursive_1 ∧ ignoreIfNotExists = ignoreIfNotExists_1
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.exists_st_of_not_infinite : ∀ {x : ℝ*}, ¬x.Infinite → ∃ r, x.IsSt r
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_fdiv : ∀ {a b : ℤ}, a / b = a.fdiv b + if 0 ≤ b ∨ b ∣ a then 0 else 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_left_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A),
  φ.rightUnitor.inv.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- Send a nonzero ideal to the corresponding class in the class group.  -/
ClassGroup.mk0 : {R : Type u_1} →
  [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDedekindDomain R] → ↥(nonZeroDivisors (Ideal R)) →* ClassGroup R
-- Mathlib.RingTheory.RingHom.Finite
RingHom.finite_containsIdentities : RingHom.ContainsIdentities @RingHom.Finite
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_lt_of_inv_lt₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → a⁻¹ < b → b⁻¹ < a
-- Std.Data.ExtTreeMap.Lemmas
_private.Std.Data.ExtTreeMap.Lemmas.0.Std.ExtTreeMap.ext : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t t' : Std.ExtTreeMap α β cmp}, t.inner = t'.inner → t = t'
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
/-- A finite flat locally finitely presented morphism is an isomorphism if and only if
its rank is constant equal to `1`.  -/
AlgebraicGeometry.Scheme.Hom.isIso_iff_finrank_eq : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f],
  CategoryTheory.IsIso f ↔ AlgebraicGeometry.Scheme.Hom.finrank f = 1
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ofEq_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] [inst_6 : Nonempty ↥s₂] (h : s₁ = s₂),
  (AffineIsometryEquiv.ofEq s₁ s₂ h).symm = AffineIsometryEquiv.ofEq s₂ s₁ ⋯
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- **Alias** of `StrongDual.norm_extendRCLike_bound`.

---

The norm of the extension is bounded by `‖fr‖`.  -/
ContinuousLinearMap.norm_extendTo𝕜'_bound : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F),
  ‖fr.extendRCLike x‖ ≤ ‖fr‖ * ‖x‖
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyCell.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β)
  (f :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ),
  Std.DTreeMap.Internal.Impl.applyCell k l f =
    match l, f with
    | Std.DTreeMap.Internal.Impl.leaf, f => f Std.DTreeMap.Internal.Cell.empty ⋯
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, f =>
      match h : compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.applyCell k l fun c h_1 => f c ⋯
      | Ordering.eq => f (Std.DTreeMap.Internal.Cell.ofEq k' v' ⋯) ⋯
      | Ordering.gt => Std.DTreeMap.Internal.Impl.applyCell k r fun c h_1 => f c ⋯
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.ext_iff : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G},
  U = V ↔ ∀ (x : G), x ∈ U ↔ x ∈ V
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.of_le_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ {A' B' : Subalgebra R S}, A' ≤ A → B' ≤ B → ∀ [Module.Flat R ↥B] [Module.Flat R ↥A'], A'.LinearDisjoint B'
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.pow_def : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → Pow (M i) α] (f : (i : ι) → M i) (a : α),
  f ^ a = fun i => f i ^ a
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
/-- The isomorphism between `F` and its image `F.extendRight M` in `M`.  -/
IntermediateField.extendRightEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (F : IntermediateField K L) →
            (M : Type u_3) →
              [inst_3 : Field M] →
                [inst_4 : Algebra K M] →
                  [inst_5 : Algebra L M] → [inst_6 : IsScalarTower K L M] → ↥F ≃ₐ[K] ↥(F.extendRight M)
-- Init.Data.List.MinMaxOn
List.apply_maxOn_le_apply_maxOn_of_subset : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : ys ⊆ xs) (hys : ys ≠ []), f (List.maxOn f ys hys) ≤ f (List.maxOn f xs ⋯)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.Hom.comp`. -/
AlgebraicGeometry.Scheme.Cover.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} →
          {G : CategoryTheory.PreZeroHypercover S} → E.Hom F → F.Hom G → E.Hom G
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add : ∀ {α : Type u} [inst : Add α] {w x y z : WithTop α} [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α],
  x < z → y < w → x + y < z + w
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.dropPrefix?_char_eq_dropPrefix?_beq : ∀ {c : Char} {s : String.Slice}, s.dropPrefix? c = s.dropPrefix? fun x => x == c
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getMethods : Lean.Meta.SimpM Lean.Meta.Simp.Methods
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.add_point : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} (P Q : W.Point),
  (P + Q).point = W.addMap P.point Q.point
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.symm_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P), (LinearEquiv.rTensor M f).symm = LinearEquiv.rTensor M f.symm
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Extract a lean expression from an `Atom` expression.  -/
Mathlib.Tactic.BicategoryLike.Atom.e : Mathlib.Tactic.BicategoryLike.Atom → Lean.Expr
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- The root discriminant of a number field `K`.  -/
NumberField.rootDiscr : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℝ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.denseRange : ∀ (G : GrpCat), DenseRange (ProfiniteGrp.ProfiniteCompletion.etaFn G)
-- Mathlib.Algebra.Lie.TraceForm
/-- Given a bilinear form `B` on a representation `M` of a nilpotent Lie algebra `L`, if `B` is
invariant (in the sense that the action of `L` is skew-adjoint w.r.t. `B`) then components of the
Fitting decomposition of `M` are orthogonal w.r.t. `B`.  -/
LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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]
  [inst_7 : LieRing.IsNilpotent L] {B : LinearMap.BilinForm R M},
  (∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆) →
    ∀ {m₀ m₁ : M}, m₀ ∈ LieModule.genWeightSpace M 0 → m₁ ∈ LieModule.posFittingComp R L M → (B m₀) m₁ = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The underlying function between the affine spaces `P1` and `P2`.  -/
AffineMap.toFun : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → (P1 →ᵃ[k] P2) → P1 → P2
-- Mathlib.Logic.UnivLE
UnivLE.self : UnivLE.{u, u}
-- Batteries.Classes.Order
Std.LawfulCmp.toLawfulLECmp : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] {cmp : α → α → Ordering} [self : Std.LawfulCmp cmp], Std.LawfulLECmp cmp
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instInhabited : {α : Type} → Inhabited (Lean.Meta.DiscrTree α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = none ↔ t.contains k = false
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_id' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), logDeriv (fun x => x) x = 1 / x
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntryDₘ : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → (a : α) × β a → (a : α) × β a
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The increasing parameterization of each part  -/
OrderedFinpartition.emb : {n : ℕ} → (self : OrderedFinpartition n) → (m : Fin self.length) → Fin (self.partSize m) → Fin n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil_ne_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil ≠
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl
-- Mathlib.RingTheory.RingHomProperties
/-- Variant of `MorphismProperty.arrow_mk_iso_iff` specialized to morphism properties in
`CommRingCat` given by ring hom properties.  -/
RingHom.RespectsIso.arrow_mk_iso_iff : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ {A B A' B' : CommRingCat} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g),
      P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsPushout.isAlgebraic : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [inst_3 : CommRing R'] [inst_4 : Algebra R R'] [NoZeroDivisors R']
  [FaithfulSMul R R'] (S' : Type u_5) [inst_7 : CommRing S'] [inst_8 : Algebra R S'] [inst_9 : Algebra S S']
  [inst_10 : Algebra R' S'] [inst_11 : IsScalarTower R R' S'] [inst_12 : IsScalarTower R S S']
  [h : Algebra.IsPushout R S R' S'], Algebra.IsAlgebraic R' S'
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.left_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {x : X}, x ∈ e.source → ↑e.symm (↑e x) = x
-- Mathlib.Order.Lattice
sup_rotate : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = b ⊔ c ⊔ a
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- A morphism is a (locally-closed) immersion if and only if it can be factored into
a closed immersion followed by an open immersion.
 -/
AlgebraicGeometry.IsImmersion.isImmersion_iff_exists : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsImmersion f ↔
    ∃ Z g₁ g₂,
      AlgebraicGeometry.IsClosedImmersion g₁ ∧
        AlgebraicGeometry.IsOpenImmersion g₂ ∧ CategoryTheory.CategoryStruct.comp g₁ g₂ = f
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instZeroContMDiffAddMonoidMorphism : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {n : WithTop ℕ∞} →
      {H : Type u_2} →
        [inst_1 : TopologicalSpace H] →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {I : ModelWithCorners 𝕜 E H} →
                  {G : Type u_4} →
                    [inst_4 : AddMonoid G] →
                      [inst_5 : TopologicalSpace G] →
                        [inst_6 : ChartedSpace H G] →
                          {H' : Type u_5} →
                            [inst_7 : TopologicalSpace H'] →
                              {E' : Type u_6} →
                                [inst_8 : NormedAddCommGroup E'] →
                                  [inst_9 : NormedSpace 𝕜 E'] →
                                    {I' : ModelWithCorners 𝕜 E' H'} →
                                      {G' : Type u_7} →
                                        [inst_10 : AddMonoid G'] →
                                          [inst_11 : TopologicalSpace G'] →
                                            [inst_12 : ChartedSpace H' G'] →
                                              Zero (ContMDiffAddMonoidMorphism I I' n G G')
-- Mathlib.Order.CountableDenseLinearOrder
Order.exists_orderEmbedding_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [DenselyOrdered β] [NoMinOrder β]
  [NoMaxOrder β] [nonem : Nonempty β] (S : Finset α) (f : ↥S ↪o β) (a : α), ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.linearIndependent : ∀ (G : Type u_1) (R : Type u_3) [inst : AddCommGroup G] [inst_1 : RCLike R] [Finite G], LinearIndependent R DFunLike.coe
-- Mathlib.Topology.Connected.TotallyDisconnected
totallySeparatedSpace_iff_exists_isClopen : ∀ {α : Type u_3} [inst : TopologicalSpace α],
  TotallySeparatedSpace α ↔ Pairwise fun x1 x2 => ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
-- Init.Data.Float.Model.Format.Basic
Float.Model.Format.he : ∀ (self : Float.Model.Format), 0 < self.exponentBits
-- Lean.Util.Sorry
Lean.Expr.hasSorry : Lean.Expr → Bool
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.Quasicategory.mk : ∀ {S : SSet},
  (∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (SSet.horn (n + 2) i).toSSet ⟶ S),
      0 < i → i < Fin.last (n + 2) → ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn (n + 2) i).ι σ) →
    S.Quasicategory
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash : Lean.Grind.Linarith.Poly → UInt64
-- Mathlib.Algebra.Regular.SMul
/-- If an element `b` becomes `M`-regular after multiplying it on the left by an `M`-regular
element, then `b` is `M`-regular.  -/
IsSMulRegular.of_smul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {s : S} [inst : SMul R M] [inst_1 : SMul R S] [inst_2 : SMul S M]
  [IsScalarTower R S M] (a : R), IsSMulRegular M (a • s) → IsSMulRegular M s
-- Mathlib.Topology.Instances.AddCircle.Defs
continuousAt_toIcoMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → ContinuousAt (toIcoMod hp a) x
-- Mathlib.Order.Defs.LinearOrder
min_eq_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → min a b = b
-- Init.Prelude
/-- Retrieves the reader monad's local value. Typically accessed via `read`, or via `readThe` when more
than one local value is available.
 -/
ReaderT.read : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → ReaderT ρ m ρ
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.instMonoσ₀Iter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (hi : n + i = m), CategoryTheory.Mono (X.σ₀Iter i hi)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (Std.ExtDTreeMap.Const.ofList l cmp).size = l.length
-- Mathlib.Algebra.Star.Basic
star_inv : ∀ {R : Type u} [inst : Group R] [inst_1 : StarMul R] (x : R), star x⁻¹ = (star x)⁻¹
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Hom.of : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.StrongTrans.Modification η θ → CategoryTheory.Oplax.StrongTrans.Hom η θ
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- Base case: `T(n) > 0` whenever `n < n₀`  -/
AkraBazziRecurrence.T_gt_zero' : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r), ∀ n < self.n₀, 0 < T n
-- Std.Time.Format.Basic
Std.Time.instReprFormatPart : Repr Std.Time.FormatPart
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdParallelComp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} [ProbabilityTheory.IsZeroOrMarkovKernel κ]
  [ProbabilityTheory.IsZeroOrMarkovKernel η], ProbabilityTheory.IsZeroOrMarkovKernel (κ.parallelComp η)