mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionOpcyclesIso.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j : ι) (hi : c.prev j = i) {i' j' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hi'' : c'.prev j' = i') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j],
  K.restrictionOpcyclesIso e i j hi hi' hj' hi'' =
    {
      hom :=
        (K.restriction e).descOpcycles
          (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom (K.pOpcycles j')) i hi ⋯,
      inv :=
        K.descOpcycles
          (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv ((K.restriction e).pOpcycles j)) i' hi'' ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Algebra.Algebra.IsSimpleRing
instFaithfulSMul_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [IsSimpleRing R]
  [Nontrivial A], FaithfulSMul R A
-- Mathlib.Algebra.CharP.Two
CharTwo.add_eq_zero : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] {a b : R}, a + b = 0 ↔ a = b
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.div_tendsto_atTop_zero_of_degree_lt`. -/
Polynomial.div_tendsto_zero_of_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree < Q.degree → Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.coe_val_mul_coe_inv_val : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : (↥S)ˣ}, ↑↑x * ↑↑x⁻¹ = 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.he : Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo → Lean.Expr
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.isBigO_comp : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [inst_3 : SeminormedAddCommGroup G] [inst_4 : Module 𝕜 G] {E : Type u_5} {g : F → G},
  IsBoundedLinearMap 𝕜 g → ∀ {f : E → F} (l : Filter E), (fun x' => g (f x')) =O[l] f
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.mem_compl : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α] {m : ℕ} {hm : m + n = Fintype.card α}
  {s : ↑(Set.powersetCard α n)} {a : α}, a ∈ (Set.powersetCard.compl hm) s ↔ a ∉ s
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.addLeft.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Equiv.addLeft a = (toAddUnits a).addLeft
-- Mathlib.Analysis.Normed.Module.Bases
/-- The `nnnorm` of any projection is bounded by the basis constant.  -/
SchauderBasis.nnnorm_proj_le_nnnormProjBound : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X] (n : ℕ), ‖b.proj n‖₊ ≤ b.nnnormProjBound
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- **Alias** of the forward direction of `Matrix.charmatrix_blockTriangular_iff`. -/
Matrix.BlockTriangular.of_charmatrix : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {α : Type u_5}
  [inst_3 : Preorder α] {M : Matrix n n R} {b : n → α}, M.charmatrix.BlockTriangular b → M.BlockTriangular b
-- Init.Data.List.Lemmas
List.getLast?_tail : ∀ {α : Type u_1} {l : List α}, l.tail.getLast? = if l.length = 1 then none else l.getLast?
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t t_1 : Std.TreeMap α β cmp) (e_t : t = t_1)
  (h : t.isEmpty = false), t.maxKey h = t_1.maxKey ⋯
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.evalSimp : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_posPart : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [inst_3 : HasSolidNorm β] [inst_4 : IsOrderedAddMonoid β] (f : BoundedContinuousFunction α β), ⇑f⁺ = (⇑f)⁺
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftComp_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (hl' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l'.app X.left) X.hom))
  (hll' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp l l').app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftComp R l l' hl hl' hll').inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Init.Data.Dyadic.Basic
Int.trailingZeros_zero : Int.trailingZeros 0 = 0
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.map_smul : ∀ {R₁ : Type u_2} {N₁ : Type u_12} {N₂ : Type u_13} [inst : Semiring R₁] [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] {module_N₁ : Module R₁ N₁} {module_N₂ : Module R₁ N₂} (e : N₁ ≃ₗ[R₁] N₂) (c : R₁)
  (x : N₁), e (c • x) = c • e x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.regularityReduced_adj : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] (ε δ : 𝕜) (a b : α),
  (SimpleGraph.regularityReduced P G ε δ).Adj a b =
    (G.Adj a b ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, a ∈ U ∧ b ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ ↑(G.edgeDensity U V))
-- Mathlib.Order.Notation
/-- Set / lattice complement 

Conventions for notations in identifiers:

 * The recommended spelling of `ᶜ` in identifiers is `compl`. -/
Compl.compl : {α : Type u_1} → [self : Compl α] → α → α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)}
  {toInsert : List (α × β)} {k : α},
  (List.map Prod.fst toInsert).contains k = false →
    Std.Internal.List.getValue! k (Std.Internal.List.insertListConst l toInsert) = Std.Internal.List.getValue! k l
-- Mathlib.Combinatorics.Quiver.Symmetric
_private.Mathlib.Combinatorics.Quiver.Symmetric.0.Quiver.Path.reverse.match_1.splitter : {V : Type u_2} →
  [inst : Quiver V] →
    {a : V} →
      (motive : (x : V) → Quiver.Path a x → Sort u_3) →
        (x : V) →
          (x_1 : Quiver.Path a x) →
            (Unit → motive a Quiver.Path.nil) →
              ((x b : V) → (p : Quiver.Path a b) → (e : b ⟶ x) → motive x (p.cons e)) → motive x x_1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] [inst_1 : CommSemiring β] (l : Filter α) (k f : α → β),
  Asymptotics.SuperpolynomialDecay l k f = ∀ (n : ℕ), Filter.Tendsto (fun a => k a ^ n * f a) l (nhds 0)
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- We relate a finite product over primes to an infinite sum over smooth numbers.  -/
EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖) →
        ∀ (N : ℕ), (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- The identity `StrictPseudofunctor`.  -/
CategoryTheory.StrictPseudofunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.StrictPseudofunctor B B
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ico_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x y : (i : ι) → α i) [Nonempty ι],
  (Set.univ.pi fun i => Set.Ico (y i) (x i)) ⊆ Set.Ico y x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.cosh` is real analytic.  -/
Real.analyticWithinAt_cosh : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.cosh s x
-- Batteries.Tactic.PrintDependents
/-- The monad used by `CollectDependents`.  -/
Batteries.Tactic.CollectDependents.M : Type → Type
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.rTensorEquivAlgEquiv.invFun.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : CommMonoid M],
  MonoidAlgebra.rTensorEquivAlgEquiv.invFun =
    MonoidAlgebra.liftNCAlgHom (Algebra.TensorProduct.map (AlgHom.id S A) MonoidAlgebra.singleOneAlgHom)
      ((↑Algebra.TensorProduct.includeRight.toRingHom).comp (MonoidAlgebra.of B M)) ⋯
-- Init.Data.BitVec.Lemmas
/-- `x ≤ y + z` if and only if `x - z ≤ y`
when `x - z` and `y + z` do not overflow.
 -/
BitVec.le_add_iff_sub_le : ∀ {w : ℕ} {x y z : BitVec w}, z ≤ x → y.toNat + z.toNat < 2 ^ w → (x ≤ y + z ↔ x - z ≤ y)
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Basic.0.Array.MergeSort.Internal.merge.go.congr_simp : ∀ {α : Type u_1} (le le_1 : α → α → Bool),
  le = le_1 →
    ∀ (xs xs_1 : Subarray α) (e_xs : xs = xs_1) (ys ys_1 : Subarray α) (e_ys : ys = ys_1) (hxs : 0 < Std.Slice.size xs)
      (hys : 0 < Std.Slice.size ys) (acc acc_1 : Array α),
      acc = acc_1 →
        Array.MergeSort.Internal.merge.go✝ le xs ys hxs hys acc =
          Array.MergeSort.Internal.merge.go✝ le_1 xs_1 ys_1 ⋯ ⋯ acc_1
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_empty_left_iff : ∀ {s : String.Slice} {p : s.Pos} {t : String}, p.Splits "" t ↔ p = s.startPos ∧ t = s.copy
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map_injective : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] {f : F},
  Function.Injective ⇑f → Function.Injective (NonUnitalStarSubalgebra.map f)
-- Mathlib.RingTheory.RootsOfUnity.Complex
IsPrimitiveRoot.arg_ext : ∀ {n m : ℕ} {ζ μ : ℂ}, IsPrimitiveRoot ζ n → IsPrimitiveRoot μ m → n ≠ 0 → m ≠ 0 → ζ.arg = μ.arg → ζ = μ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_none : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α}, a ∉ t → t.get? a = none
-- Mathlib.Data.Bundle
Bundle.pullbackTotalSpaceEmbedding.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (z : Bundle.TotalSpace F (f *ᵖ E)),
  Bundle.pullbackTotalSpaceEmbedding f z = (z.proj, ⟨f z.proj, z.snd⟩)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.toContinuousLinearMap_eq_iff_eq_toLinearMap : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] [inst_6 : T2Space E] [inst_7 : FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] E) (g : E →L[𝕜] E),
  LinearMap.toContinuousLinearMap f = g ↔ f = ↑g
-- Mathlib.Algebra.Lie.DirectSum
/-- See `DirectSum.lieRingOfIdeals` comment.  -/
DirectSum.lieAlgebraOfIdeals : {R : Type u} →
  {ι : Type v} →
    [inst : CommRing R] →
      {L : Type w} →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] → (I : ι → LieIdeal R L) → LieAlgebra R (DirectSum ι fun i => ↥(I i))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.of.sizeOf_spec : ∀ (carrier : Type u) [str : SeminormedAddCommGroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} {f : V₀.V ⟶ V₁.V}
  {h :
    autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map f) = CategoryTheory.CategoryStruct.comp f V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam}
  {f_1 : V₀.V ⟶ V₁.V}
  {h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map f_1) = CategoryTheory.CategoryStruct.comp f_1 V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam},
  { f := f, h := h } = { f := f_1, h := h_1 } → f = f_1
-- Mathlib.Data.ENat.Lattice
ENat.sub_iSup : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι], a ≠ ⊤ → a - ⨆ i, f i = ⨅ i, a - f i
-- Std.Do.Internal.Ensures.Lemmas
/-- Every value returned by `x` satisfies `MonadAttach.CanReturn x`.  -/
Std.Do.Internal.Ensures.canReturn : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m] [WeaklyLawfulMonadAttach m]
  {α : Type u_1} {x : m α}, Std.Do.Internal.Ensures (MonadAttach.CanReturn x) x
-- Mathlib.Data.Finsupp.Order
Finsupp.single_tsub : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [inst_4 : OrderedSub α] {i : ι} {a b : α}, (fun₀ | i => a - b) = (fun₀ | i => a) - fun₀ | i => b
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity follows from scaled distance. Backward direction of
`similar_iff_exists_dist_eq`.  -/
Similar.of_exists_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.ext_iff : ∀ {X : TopCat} {x y : ↑X} {x_1 y_1 : X.Path x y}, x_1 = y_1 ↔ x_1.hom = y_1.hom
-- Mathlib.Algebra.Ring.Nat
Nat.instAddMonoidWithOne : AddMonoidWithOne ℕ
-- Mathlib.Algebra.Group.Basic
sub_add_sub_cancel' : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a - b + (c - a) = c - b
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT'.eq_1 : ∀ {n : ℕ} (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' clause =
    Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray (List.toArray clause)
-- Lean.Parser.Command
Lean.Parser.Command.computedField.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The difference constant `σ[A]` of a finset `A` in a group is `|A - A| / |A|`.  -/
Combinatorics.Additive.«termδ[_]» : Lean.ParserDescr
-- Lean.Server.Requests
Lean.Server.RequestM.mapRequestTaskCheap : {α : Type u_1} →
  {β : Type} →
    Lean.Server.RequestTask α → (α → Lean.Server.RequestM β) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_le_omega0 : ∀ {a : Cardinal.{u_1}}, a.ord ≤ Ordinal.omega0 ↔ a ≤ Cardinal.aleph0
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalUnopUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.unopUnop C).Monoidal
-- Mathlib.Data.PNat.Xgcd
/-- `b = bp + 1`  -/
PNat.XgcdType.b : PNat.XgcdType → ℕ+
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`.  -/
ContMDiffOn.mlieBracketWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} [inst_6 : IsManifold I (minSmoothness 𝕜 2) M]
  [CompleteSpace E] {m n : ℕ∞} [IsManifold I (↑n + 1) M] {U V : (x : M) → TangentSpace I x},
  ContMDiffOn I I.tangent (↑n) (fun x => ⟨x, U x⟩) s →
    ContMDiffOn I I.tangent (↑n) (fun x => ⟨x, V x⟩) s →
      UniqueMDiff[s] →
        minSmoothness 𝕜 (↑m + 1) ≤ ↑n →
          ContMDiffOn I I.tangent (↑m) (fun x₀ => ⟨x₀, VectorField.mlieBracketWithin I U V s x₀⟩) s
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- **Alias** of the forward direction of `coplanar_iff_finrank_le_two`.

---

A set of points, whose `vectorSpan` is finite-dimensional, is coplanar if and only if their
`vectorSpan` has dimension at most `2`.  -/
Coplanar.finrank_le_two : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} [FiniteDimensional k ↥(vectorSpan k s)],
  Coplanar k s → Module.finrank k ↥(vectorSpan k s) ≤ 2
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.sub_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Sub γ] [MeasurableSub γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => f x - c) (fun x => g x - c) μ ν
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDeriv_clm_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {c : F} {x : E} {N : WithTop ℕ∞}
  {n : ℕ}, ContDiffAt 𝕜 N f x → ↑n ≤ N → ‖iteratedFDeriv 𝕜 n (fun y => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_eq_sq₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀],
  0 ≤ a → 0 ≤ b → (a ^ 2 = b ^ 2 ↔ a = b)
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The forget functor `CommGrpCat.{u} ⥤ Type u` is corepresentable.  -/
CommGrpCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (CommGrpCat.of (ULift.{u, 0} (Multiplicative ℤ)))) ≅
  CategoryTheory.forget CommGrpCat
-- Mathlib.Algebra.Order.Monovary
antivary_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Antivary f g⁻¹ ↔ Monovary f g
-- Mathlib.Algebra.Notation.Defs
neg_ite : ∀ {α : Type u_3} (P : Prop) [inst : Decidable P] [inst_1 : Neg α] (b c : α),
  (-if P then b else c) = if P then -b else -c
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) →
    (x : Option (Stream'.Seq1 (Option α))) →
      (Unit → motive none) →
        ((s' : Stream'.Seq (Option α)) → motive (some (none, s'))) →
          ((a : α) → (s' : Stream'.Seq (Option α)) → motive (some (some a, s'))) → motive x
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Push.instHasReverse : {V : Type u_2} →
  [inst : Quiver V] → {V' : Type u_4} → (σ : V → V') → [Quiver.HasReverse V] → Quiver.HasReverse (Quiver.Push σ)
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.below : {α : Type u_1} →
  {r : α → α → Prop} → {motive : (a : Set α) → ChainClosure r a → Prop} → {a : Set α} → ChainClosure r a → Prop
-- Mathlib.RingTheory.KrullDimension.Basic
ringKrullDim_lt_top : ∀ {R : Type u_1} [inst : CommSemiring R] [FiniteRingKrullDim R], ringKrullDim R < ⊤
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.not_isRightDescent_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  ¬cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) = cs.length w + 1
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.stateful.inj : ∀ {h h_1 : Lean.TSyntax `Lean.binderIdent},
  Lean.Parser.Tactic.MCasesPat.stateful h = Lean.Parser.Tactic.MCasesPat.stateful h_1 → h = h_1
-- Init.Data.List.Find
List.findIdx_eq_length_of_false : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, (∀ x ∈ xs, p x = false) → List.findIdx p xs = xs.length
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.map_i_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) (F : CategoryTheory.Functor C D),
  (h.map F).i.right = F.map (CategoryTheory.Arrow.Hom.right h.i)
-- Mathlib.Data.Nat.Bits
_private.Mathlib.Data.Nat.Bits.0.Nat.boddDiv2.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.eq_append_of_dropPrefix?_char_eq_some : ∀ {c : Char} {s res : String.Slice}, s.dropPrefix? c = some res → s.copy = String.singleton c ++ res.copy
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_min' : ∀ {G : Type u} [inst : Monoid G] (n : ℕ), 0 < n → (∀ (g : G), g ^ n = 1) → Monoid.exponent G ≤ n
-- Init.Data.Char.Lemmas
Char.isDigit.eq_1 : ∀ (c : Char), c.isDigit = (decide (c.val ≥ '0'.val) && decide (c.val ≤ '9'.val))
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The negative logarithmic derivative of `s ↦ (s - 1) * L χ s` for a trivial
Dirichlet character `χ` is continuous away from the zeros of `L χ` (including at `s = 1`).  -/
DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁ : ∀ (n : ℕ) [inst : NeZero n],
  ContinuousOn (fun s => -deriv (DirichletCharacter.LFunctionTrivChar₁ n) s / DirichletCharacter.LFunctionTrivChar₁ n s)
    {s | s = 1 ∨ DirichletCharacter.LFunctionTrivChar n s ≠ 0}
-- Std.Http.Data.Headers
/-- Like `getAll`, but returns `none` instead of requiring a membership proof.
Returns `none` if the header is absent.
 -/
Std.Http.Headers.getAll? : Std.Http.Headers → Std.Http.Header.Name → Option (Array Std.Http.Header.Value)
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyLE.isLocalMin : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  f ≤ᶠ[nhds a] g → f a = g a → IsLocalMin f a → IsLocalMin g a
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_eval_one_add : ∀ (n : ℕ) (x : ℚ),
  Polynomial.eval (1 + x) (Polynomial.bernoulli n) = Polynomial.eval x (Polynomial.bernoulli n) + ↑n * x ^ (n - 1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_comm : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (P Q : W'.Point), P.sym2x Q = Q.sym2x P
-- Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.VCGen.Config : Type
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.isInduced_iff_exists_eq_induce_top : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G'.IsInduced ↔ ∃ s, G' = ⊤.induce s
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.fst_isOpenEmbedding_of_right : ∀ {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S},
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))