mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M → M'} {x : M},
  ContMDiffAt (I.transContinuousLinearEquiv e) I' n f x ↔ ContMDiffAt I I' n f x
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.irq : Std.Internal.UV.System.CPUTimes → UInt64
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.forall : ∀ {P : UpperHalfPlane → Prop},
  (∀ (z : UpperHalfPlane), P z) ↔ ∀ (z : ℂ) (hz : 0 < z.im), P { coe := z, coe_im_pos := hz }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, (Std.ExtDTreeMap.map f t).contains k = t.contains k
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_zero : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Zero (γ a b)],
  Sigma.uncurry 0 = 0
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.setFinite_inter : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [ProperSpace E] [Finite ι] {s : Set E}, Bornology.IsBounded s → (s ∩ ↑(Submodule.span ℤ (Set.range ⇑b))).Finite
-- Init.Data.BitVec.Lemmas
BitVec.msb_udiv : ∀ {w : ℕ} (x y : BitVec w), (x / y).msb = (x.msb && y == 1#w)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint8.inj : ∀ {val val_1 : UInt8}, Lean.Compiler.LCNF.LitValue.uint8 val = Lean.Compiler.LCNF.LitValue.uint8 val_1 → val = val_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.Order.Basic
Preorder.ext : ∀ {α : Type u_2} {A B : Preorder α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.fromRows_one_isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq n] (A : Matrix m n R),
  (A.fromRows 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Mathlib.Analysis.Normed.Operator.Extend
ContinuousLinearMap.extend.eq_1 : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : AddCommGroup E]
  [inst_1 : UniformSpace E] [inst_2 : IsUniformAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : UniformSpace F]
  [inst_5 : IsUniformAddGroup F] [inst_6 : T0Space F] [inst_7 : AddCommMonoid Eₗ] [inst_8 : UniformSpace Eₗ]
  [inst_9 : ContinuousAdd Eₗ] [inst_10 : Semiring 𝕜] [inst_11 : Semiring 𝕜₂] [inst_12 : Module 𝕜 E]
  [inst_13 : Module 𝕜₂ F] [inst_14 : Module 𝕜 Eₗ] [inst_15 : ContinuousConstSMul 𝕜 Eₗ]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [inst_17 : CompleteSpace F] (e : E →L[𝕜] Eₗ),
  f.extend e =
    if h : DenseRange ⇑e ∧ IsUniformInducing ⇑e then
      have cont := ⋯;
      have eq := ⋯;
      { toFun := ⋯.extend ⇑f, map_add' := ⋯, map_smul' := ⋯, cont := cont }
    else 0
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation.eq_5 : ∀ (x n k : ℕ), hyperoperation n.succ x k.succ = hyperoperation n x (hyperoperation (n + 1) x k)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `x` is a conjugate root of some element `algebraMap R S r` in the image of the base ring, then
`x = algebraMap R S r`.
 -/
IsConjRoot.eq_algebraMap : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {r : K}
  {x : S}, IsConjRoot K ((algebraMap K S) r) x → x = (algebraMap K S) r
-- Mathlib.Order.ConditionallyCompleteLattice.Group
le_mul_ciInf : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Group α] [MulLeftMono α]
  {a g : α} {h : ι → α}, (∀ (j : ι), a ≤ g * h j) → a ≤ g * iInf h
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- Version of `MDifferentiableWithinAt.congr` where `x` need not be contained in `s`,
but `f` and `f₁` are equal on a set containing both.  -/
MDifferentiableWithinAt.congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s t : Set M},
  MDiffAt[s] f x → (∀ x ∈ t, f₁ x = f x) → s ⊆ t → x ∈ t → MDiffAt[s] f₁ x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] (k : α),
  t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
-- Lean.Data.NameMap.Basic
Lean.NameSSet.contains : Lean.NameSSet → Lean.Name → Bool
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instSemiring : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → Semiring (WithAbs v)
-- Mathlib.Data.TypeVec
TypeVec.const.eq_def : ∀ {β : Type u_1} (x : β) (x_1 : ℕ) (x_2 : TypeVec.{u_2} x_1) (x_3 : Fin2 x_1),
  TypeVec.const x x_2 x_3 =
    match (motive := (x : ℕ) → (x_4 : TypeVec.{u_2} x) → (x_5 : Fin2 x) → x_4 x_5 → TypeVec.repeat x β x_5) x_1, x_2,
      x_3 with
    | n.succ, α, a.fs => TypeVec.const x α.drop a
    | n.succ, x_4, Fin2.fz => fun x_5 => x
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
panicking if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyGT! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α → α
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_monotone : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n], Monotone (RingCon.matrix n)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.left_unitality_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X : C) {Z : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) h)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) h
-- Batteries.Data.List.Lemmas
List.idxsOf_map : ∀ {α : Type u_1} {β : Type u_2} {xs : List β} {x : α} {s : ℕ} [inst : BEq α] {f : β → α},
  List.idxsOf x (List.map f xs) s = List.findIdxs (fun x_1 => f x_1 == x) xs s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_13.eq_1 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w : ℕ) (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1)
  (aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (lhs : aig_1.RefVec w)
  (hlaig : aig.decls.size ≤ { aig := aig_1, vec := lhs }.aig.decls.size)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, vec := lhs }, hlaig⟩).aig)
  (h_1 :
    (aig_2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
      (lhs : aig_2.RefVec w) →
        (hlaig : aig.decls.size ≤ { aig := aig_2, vec := lhs }.aig.decls.size) →
          (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_2, vec := lhs }, hlaig⟩).aig) →
            motive { result := ⟨{ aig := aig_2, vec := lhs }, hlaig⟩, cache := cache }),
  (match { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache } with
    | { result := ⟨{ aig := aig_2, vec := lhs }, hlaig⟩, cache := cache } => h_1 aig_2 lhs hlaig cache) =
    h_1 aig_1 lhs hlaig cache
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.local.inj : ∀ {wi wi_1 : Lean.Widget.WidgetInstance},
  Lean.Widget.PanelWidgetsExtEntry.local wi = Lean.Widget.PanelWidgetsExtEntry.local wi_1 → wi = wi_1
-- Mathlib.Algebra.Order.Ring.Basic
pow_add_pow_le' : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b : R} {n : ℕ},
  0 ≤ a → 0 ≤ b → a ^ n + b ^ n ≤ 2 * (a + b) ^ n
-- Lean.Syntax
Lean.Syntax.instInhabitedRange.default : Lean.Syntax.Range
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mem_top : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (x : G), x ∈ ⊤
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertListₘ.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  (l : List (α × β)),
  Std.DHashMap.Internal.Raw₀.Const.insertListₘ m l =
    match l with
    | [] => m
    | hd :: tl => Std.DHashMap.Internal.Raw₀.Const.insertListₘ (m.insert hd.1 hd.2) tl
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.map.match_1.eq_1 : ∀ {α : Type u_1} (motive : Computation α → Sort u_2) (s : Stream' (Option α))
  (al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a)
  (h_1 : (s : Stream' (Option α)) → (al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a) → motive ⟨s, al⟩),
  (match ⟨s, al⟩ with
    | ⟨s, al⟩ => h_1 s al) =
    h_1 s al
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.ext : ∀ {R : Type u_1} {inst : CommRing R} {x y : LocalSubring R}, x.toSubring = y.toSubring → x = y
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_ofHamming : ∀ {ι : Type u_2} {β : ι → Type u_3} (x : Hamming β), Hamming.toHamming (Hamming.ofHamming x) = x
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.bufferOffset : Lean.CompactedRegion → USize
-- Init.Data.UInt.Lemmas
UInt64.ne_of_lt : ∀ {a b : UInt64}, a < b → a ≠ b
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances : Type
-- Mathlib.Analysis.Asymptotics.TVS
Filter.HasBasis.isBigOTVS_iff : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} {ιE : Sort u_7}
  {ιF : Sort u_8} {pE : ιE → Prop} {pF : ιF → Prop} {sE : ιE → Set E} {sF : ιF → Set F},
  (nhds 0).HasBasis pE sE →
    (nhds 0).HasBasis pF sF →
      (f =O[𝕜; l] g ↔ ∀ (i : ιE), pE i → ∃ j, pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x))
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a finite sum of field elements is at most
`totalWeight K * log n` plus the sum of the individual logarithmic heights,
where `n` is the number of terms.

(Note that here we do not need to assume that `s` is nonempty, due to the convenient
junk value `log 0 = 0`.)  -/
Height.logHeight₁_sum_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {α : Type u_2} (s : Finset α) (x : α → K),
  Height.logHeight₁ (∑ a ∈ s, x a) ≤ ↑(Height.totalWeight K) * Real.log ↑s.card + ∑ a ∈ s, Height.logHeight₁ (x a)
-- Plausible.Testable
/-- Configuration for testing a property.  -/
Plausible.Configuration : Type
-- Mathlib.Order.Prod.Lex.Hom
/-- `toLex` as an `OrderHom`.  -/
Prod.Lex.toLexOrderHom : {α : Type u_1} → {β : Type u_2} → [inst : PartialOrder α] → [inst_1 : Preorder β] → α × β →o Lex (α × β)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instHMulOfFintypeOfMulOfAddCommMonoid : {m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_5} →
      {l : Type u_7} →
        [Fintype m] → [Mul A] → [AddCommMonoid A] → HMul (CStarMatrix l m A) (CStarMatrix m n A) (CStarMatrix l n A)
-- Mathlib.Computability.Language
Language.mem_mul : ∀ {α : Type u_1} {l m : Language α} {x : List α}, x ∈ l * m ↔ ∃ a ∈ l, ∃ b ∈ m, a ++ b = x
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.coeff_expand_of_not_dvd : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) {m : ℕ},
  ¬p ∣ m → (PowerSeries.coeff m) ((PowerSeries.expand p hp) φ) = 0
-- Batteries.Data.MLList.Basic
/-- Gets the last element of a monadic lazy list, or the default value if the list is empty.
This will run forever if the list is infinite.  -/
MLList.getLast! : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → [Inhabited α] → MLList m α → m α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α), (t₁.insert k).Equiv (t₂.insert k)
-- Lean.Data.AssocList
Lean.AssocList.foldl : {α : Type u} → {β : Type v} → {δ : Type w} → (δ → α → β → δ) → δ → Lean.AssocList α β → δ
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.id_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.Hom.id sq).τ₃ = CategoryTheory.CategoryStruct.id sq.X₃
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.mk.inj : ∀ {α : Type} {tree : Lean.Meta.LazyDiscrTree.PreDiscrTree α} {errors : Array Lean.Meta.LazyDiscrTree.ImportFailure}
  {tree_1 : Lean.Meta.LazyDiscrTree.PreDiscrTree α} {errors_1 : Array Lean.Meta.LazyDiscrTree.ImportFailure},
  { tree := tree, errors := errors } = { tree := tree_1, errors := errors_1 } → tree = tree_1 ∧ errors = errors_1
-- Batteries.Data.List.Perm
List.Subperm.filter : ∀ {α : Type u_1} (p : α → Bool) ⦃l l' : List α⦄, l.Subperm l' → (List.filter p l).Subperm (List.filter p l')
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keys.isEmpty = m.isEmpty
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- The lift of a composition is homotopic to the composition of the lifts.  -/
CategoryTheory.ProjectiveResolution.liftCompHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            (P : CategoryTheory.ProjectiveResolution X) →
              (Q : CategoryTheory.ProjectiveResolution Y) →
                (R : CategoryTheory.ProjectiveResolution Z) →
                  Homotopy (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.comp f g) P R)
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q)
                      (CategoryTheory.ProjectiveResolution.lift g Q R))
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_sub : ∀ {R : Type u_1} {a b : R} (r1 r2 : R) [inst : SubNegZeroMonoid R],
  QuadraticAlgebra.C (r1 - r2) = QuadraticAlgebra.C r1 - QuadraticAlgebra.C r2
-- Mathlib.Topology.Separation.Basic
singleton_mem_nhdsWithin_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ {x : X}, x ∈ s → {x} ∈ nhdsWithin x s
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_sum_C_substInvFun_mul_X_pow_sub_X : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R),
  PowerSeries.constantCoeff P = 0 →
    ∀ [inst_1 : Invertible ((PowerSeries.coeff 1) P)] (n : ℕ),
      (PowerSeries.coeff n)
          (PowerSeries.subst (∑ i, PowerSeries.C (P.substInvFun ↑i) * PowerSeries.X ^ ↑i) P - PowerSeries.X) =
        0
-- Std.Data.DHashMap.Basic
/-- Equivalent to (but potentially faster than) calling `Const.get?` followed by `insertIfNew`.

Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.
 -/
Std.DHashMap.Const.getThenInsertIfNew? : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → α → β → Option β × Std.DHashMap α fun x => β
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNormedStarGroup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  [inst_2 : StarAddMonoid β] [inst_3 : NormedStarGroup β] [inst_4 : CompactSpace α], NormedStarGroup C(α, β)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C}
  (h : Opposite.unop (CategoryTheory.Limits.pullback f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.unop g.unop)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout f g).hom.unop h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g).unop h
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  (CategoryTheory.ShortComplex.opcyclesMapIso e).hom = CategoryTheory.ShortComplex.opcyclesMap e.hom
-- Mathlib.Analysis.Calculus.VectorField
/-- The differentiation operator along `[W, V]`
is the commutator of the differentiation operators along `W` and `V`.  -/
VectorField.fderivWithin_apply_lieBracket : ∀ {𝕜 : 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] {V W : E → E}
  {s : Set E} {x : E} {f : E → F} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x →
    minSmoothness 𝕜 2 ≤ n →
      UniqueDiffOn 𝕜 s →
        x ∈ closure (interior s) →
          x ∈ s →
            DifferentiableWithinAt 𝕜 W s x →
              DifferentiableWithinAt 𝕜 V s x →
                (fderivWithin 𝕜 f s x) (VectorField.lieBracketWithin 𝕜 V W s x) =
                  (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 f s x) (W x)) s x) (V x) -
                    (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 f s x) (V x)) s x) (W x)
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_union : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
  (s t : Set E), ProperCone.innerDual (s ∪ t) = ProperCone.innerDual s ⊓ ProperCone.innerDual t
-- Mathlib.Data.Fintype.Pi
Finset.piDiag_subset_piFinset : ∀ {α : Type u_1} {ι : Type u_3} [inst : DecidableEq (ι → α)] {s : Finset α} [inst_1 : DecidableEq ι]
  [inst_2 : Fintype ι], s.piDiag ι ⊆ Fintype.piFinset fun x => s
-- Mathlib.Topology.Algebra.Monoid
AddMonoid.continuousConstSMul_nat : ∀ {A : Type u_6} [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [ContinuousAdd A], ContinuousConstSMul ℕ A
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The `LinearEquiv` version of `LinearMap.dualMap`.  -/
LinearEquiv.dualMap : {R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : Module R M₁] →
            [inst_3 : AddCommMonoid M₂] →
              [inst_4 : Module R M₂] → (M₁ ≃ₗ[R] M₂) → Module.Dual R M₂ ≃ₗ[R] Module.Dual R M₁
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.homEquiv_extendScalarsId : ∀ {R : Type u₁} [inst : CommRing R] (M : ModuleCat R),
  ((ModuleCat.extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((CategoryTheory.Functor.id (ModuleCat R)).obj M))
      ((ModuleCat.extendScalarsId R).hom.app M) =
    (ModuleCat.restrictScalarsId R).inv.app M
-- Mathlib.Order.Category.Frm
/-- Construct a bundled `Frm` from the underlying type and typeclass.  -/
Frm.of : (carrier : Type u_1) → [str : Order.Frame carrier] → Frm
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instMin.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.instMin =
    {
      min := fun H₁ H₂ =>
        let __src := H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ } }
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isRat_lt_false : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ},
  Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (nb * ↑da ≤ na * ↑db) = true → ¬a < b
-- Mathlib.Data.Finset.Lattice.Fold
/-- Computing `sup` in a subtype (closed under `sup`) is the same as computing it in `α`.  -/
Finset.sup_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {P : α → Prop} {Pbot : P ⊥}
  {Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)} (t : Finset β) (f : β → { x // P x }), ↑(t.sup f) = t.sup fun x => ↑(f x)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr'_symm_apply_left : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂)
  (x : N₂ ⋊[(↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)] G₂),
  ((SemidirectProduct.congr' fn fg).symm x).left = fn.symm x.left
-- Mathlib.Algebra.DirectSum.Module
DirectSum.toAddMonoidHom_lmap : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i),
  (DirectSum.lmap f).toAddMonoidHom = DirectSum.map fun i => (f i).toAddMonoidHom
-- Mathlib.CategoryTheory.Sites.Closed
/-- The sieve `S` is in the topology iff its closure is the maximal sieve. This shows that the closure
operator determines the topology.
 -/
CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X), J₁.close S = ⊤ ↔ S ∈ J₁ X
-- Mathlib.Algebra.Lie.Graded
/-- If `L` is graded by `ι` with degree `i` component `ℒ i`, then it is isomorphic as
a Lie algebra to a direct sum of components.  -/
DirectSum.decomposeLieEquiv : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : CommRing R] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                (ℒ : ι → Submodule R L) → [inst_5 : GradedLieAlgebra ℒ] → L ≃ₗ⁅R⁆ DirectSum ι fun i => ↥(ℒ i)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.hasCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.Limits.HasCoproducts C