mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.glue.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (sz : ℕ) →
      (k : α) →
        (v : β k) →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                (r : Std.DTreeMap.Internal.Impl α β) →
                  r.Balanced →
                    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                        r.size →
                      Sort u_3) →
              (r : Std.DTreeMap.Internal.Impl α β) →
                (hr : r.Balanced) →
                  (hlr :
                      Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                        r.size) →
                    ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalancedAtRoot
                              (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                              Std.DTreeMap.Internal.Impl.leaf.size) →
                          motive Std.DTreeMap.Internal.Impl.leaf hr hlr) →
                      ((sz' : ℕ) →
                          (k' : α) →
                            (v' : β k') →
                              (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                                (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalancedAtRoot
                                        (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                                        (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size) →
                                    motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') hr hlr) →
                        motive r hr hlr
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instNeg.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Neg (G i)], Pi.instNeg = { neg := fun f i => -f i }
-- Mathlib.Tactic.Ring.Common
/-- Divides two polynomials `va, vb` to get a normalized result polynomial.

* `a / b = a * b⁻¹`
 -/
Mathlib.Tactic.Ring.Common.evalDiv : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              (rα : Q(Semifield «$α»)) →
                Option Q(CharZero «$α») →
                  Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                    Mathlib.Tactic.Ring.Common.ExSum bt sα b →
                      Mathlib.Tactic.AtomM
                        (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» / «$b»))
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpToOn_top_iff_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  ↑⊤ ≤ N → ∀ (k : ℕ), HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.functor_additive : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions], L.Additive
-- Mathlib.RingTheory.Ideal.Prod
/-- Ideals of `R × S` are in one-to-one correspondence with pairs of ideals of `R` and ideals of
`S`.  -/
Ideal.idealProdEquiv : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → Ideal (R × S) ≃o Ideal R × Ideal S
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.IsColimit.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {K : CategoryTheory.Limits.Multicofork I}
  (hK : CategoryTheory.Limits.IsColimit K) {T : C} (k : (a : J.R) → I.right a ⟶ T)
  (hk :
    ∀ (b : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst b) (k (J.fst b)) =
        CategoryTheory.CategoryStruct.comp (I.snd b) (k (J.snd b)))
  (a : J.R) {Z : C} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.π a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.IsColimit.desc hK k hk) h) =
    CategoryTheory.CategoryStruct.comp (k a) h
-- Init.Data.BitVec.Lemmas
BitVec.and_or_distrib_left : ∀ {w : ℕ} {x y z : BitVec w}, x &&& (y ||| z) = x &&& y ||| x &&& z
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), γ.neg.φH = -γ.φH
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inr_iso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z : D} (h : CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g)) h
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_union_le_encard_add_eRk : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (X ∪ Y) ≤ X.encard + M.eRk Y
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- `Matrix.conjTranspose` as a `LinearMap`  -/
Matrix.conjTransposeLinearEquiv : (m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_7) →
      (α : Type v) →
        [inst : CommSemiring R] →
          [inst_1 : StarRing R] →
            [inst_2 : AddCommMonoid α] →
              [inst_3 : StarAddMonoid α] → [inst_4 : Module R α] → [StarModule R α] → Matrix m n α ≃ₗ⋆[R] Matrix n m α
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObj_tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).tgt = (X.tgt ⨯ Y.tgt)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAtFilter_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {L : Filter (E × E)} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}
  {Φ' : E →L[𝕜] (i : ι) → F' i},
  HasFDerivAtFilter Φ Φ' L ↔ ∀ (i : ι), HasFDerivAtFilter (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') L
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSFiniteOfNatMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α}, MeasureTheory.SFinite 0
-- Mathlib.NumberTheory.Divisors
Int.mem_divisors_self : ∀ {z : ℤ}, z ≠ 0 → z ∈ z.divisors
-- Mathlib.NumberTheory.Bertrand
/-- A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime
factorization of the central binomial coefficient only has factors at most `2 * n / 3 + 1`.
 -/
centralBinom_factorization_small : ∀ (n : ℕ),
  2 < n →
    (∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p) →
      n.centralBinom = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.readRequestAs : String → (α : Type) → [Lean.FromJson α] → Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Request α)
-- Mathlib.Topology.Semicontinuity.Basic
/-- A lower semicontinuous function attains its lower bound on a nonempty compact set.  -/
LowerSemicontinuousOn.exists_isMinOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : LinearOrder β] {s : Set α},
  s.Nonempty → IsCompact s → LowerSemicontinuousOn f s → ∃ a ∈ s, IsMinOn f s a
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncContext.descr : Lean.AsyncContext✝ → String
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)}, (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_updateCell : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α}
  {f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)}
  {l : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced),
  l.Ordered → (Std.DTreeMap.Internal.Impl.updateCell k f l hlb).impl.Ordered
-- Lean.MetavarContext
/-- Given a sequence of delayed assignments
```
mvarId₁ := fun ... => mvarId₂;
...
mvarIdₙ := fun ... => mvarId_root  -- where `mvarId_root` is not delayed assigned
```
in `mctx`, `getDelayedRoot mctx mvarId₁` return `mvarId_root`.
If `mvarId₁` is not delayed assigned then return `mvarId₁`  -/
Lean.getDelayedMVarRoot : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Lean.MVarId
-- Init.Core
DoResultPR.return.sizeOf_spec : ∀ {α β σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (a : β) (a_1 : σ),
  sizeOf (DoResultPR.return a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
cardinal_lt_aleph0_of_finiteDimensional : ∀ (K : Type u) (V : Type v) [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Finite K] [Module.Free K V] [Module.Finite K V], Cardinal.mk V < Cardinal.aleph0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), f.domain ≤ f.toRationalMap.domain
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_nonneg`.  -/
Right.add_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.mk : Lean.Name → (Lean.Name → Bool) → (Lean.LMVarId → Bool) → Lean.MetavarContext.LevelMVarToParam.Context
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') x
-- Init.Grind.AC
Lean.Grind.AC.Seq.beq'.eq_1 : ∀ (s₁ : Lean.Grind.AC.Seq),
  s₁.beq' =
    Lean.Grind.AC.Seq.rec (motive := fun x => Lean.Grind.AC.Seq → Bool)
      (fun x s₂ => Lean.Grind.AC.Seq.rec (fun y => Nat.beq x y) (fun x x_1 x_2 => false) s₂)
      (fun x x_1 ih s₂ => Lean.Grind.AC.Seq.rec (fun x => false) (fun y s₂ x_2 => (Nat.beq x y).and' (ih s₂)) s₂) s₁
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
/-- If `X` is a simplicial object in a preadditive category and `f : X _⦋n⦌ ⟶ T`
is a morphism, we say that is vanishes on degeneracies if `n = 0` or if
maps `X.σ i ≫ f` all vanish.  -/
AlgebraicTopology.DoldKan.DegeneraciesVanish : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} → {n : ℕ} → {T : C} → (X.obj (Opposite.op { len := n }) ⟶ T) → Prop
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.Prod.upAddHom.eq_1 : ∀ (G : Type u) (H : Type v) [inst : Add G] [inst_1 : Add H],
  Prod.upAddHom✝ G H = { toFun := fun x t => Bool.rec { down := x.1 } { down := x.2 } t, map_add' := ⋯ }
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.leftInverse : ∀ {𝕜 : 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),
  Function.LeftInverse ↑I.symm ↑I
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.append.eq_def : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly),
  p₁.append p₂ =
    match p₁ with
    | Lean.Grind.Linarith.Poly.nil => p₂
    | Lean.Grind.Linarith.Poly.add k x p₁ => Lean.Grind.Linarith.Poly.add k x (p₁.append p₂)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic at `x`, convert `f` to normal form at `x` by changing its value at `x`.
Otherwise, returns the 0 function.  -/
toMeromorphicNFAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → 𝕜 → E
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.match_1.splitter : (motive : List String → Sort u_1) →
  (x : List String) → (Unit → motive []) → ((a : String) → (as : List String) → motive (a :: as)) → motive x
-- Mathlib.Analysis.Fourier.AddCircle
/-- Express Fourier coefficients of `f` on an interval in terms of those of its derivative.  -/
fourierCoeffOn_of_hasDerivAt_Ioo : ∀ {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ},
  n ≠ 0 →
    ContinuousOn f (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b →
          fourierCoeffOn hab f n =
            1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
              ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
-- Mathlib.Tactic.SudoSetOption
/-- The command `sudo set_option name val` is similar to `set_option name val`,
but it also allows to set undeclared options.
 -/
commandSudoSet_option___ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The clifford algebras over `CliffordAlgebraComplex.Q` is isomorphic as an `ℝ`-algebra to `ℂ`.  -/
CliffordAlgebraComplex.equiv : CliffordAlgebra CliffordAlgebraComplex.Q ≃ₐ[ℝ] ℂ
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Pre-compose an internal hom with an external hom.  -/
CategoryTheory.MonoidalClosed.pre : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : C} →
        [inst_2 : CategoryTheory.Closed A] →
          [inst_3 : CategoryTheory.Closed B] → (B ⟶ A) → (CategoryTheory.ihom A ⟶ CategoryTheory.ihom B)
-- Mathlib.GroupTheory.SemidirectProduct
/-- Define a map from `N₁ ⋊[φ₁] G₁` to `N₂ ⋊[φ₂] G₂` given maps `N₁ →* N₂` and `G₁ →* G₂` that
satisfy a commutativity condition `∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n)`.  -/
SemidirectProduct.map : {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₁} →
                  {φ₂ : G₂ →* MulAut N₂} →
                    (fn : N₁ →* N₂) →
                      (fg : G₁ →* G₂) →
                        (∀ (g : G₁),
                            fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn) →
                          N₁ ⋊[φ₁] G₁ →* N₂ ⋊[φ₂] G₂
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.multipliable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  MultipliableLocallyUniformlyOn f s → x ∈ s → Multipliable fun x_1 => f x_1 x
-- Aesop.Forward.State
/-- Update a cluster change, adding any enqueued hypotheses. This may result in
new complete matches.  -/
Aesop.ClusterState.update : Aesop.ClusterState → Aesop.ClusterState.AddM Aesop.ClusterState
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_eq_getD_get? : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α}, m.getD a fallback = (m.get? a).getD fallback
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.instFullProdUncurry : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E], CategoryTheory.Functor.uncurry.Full
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveOn.continuousWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ} {t₀ : ℝ}, IsMIntegralCurveOn γ v s → t₀ ∈ s → ContinuousWithinAt γ s t₀
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.mk.injEq : ∀ (matcher : Lean.Expr) (counterExamples : Array Lean.Meta.Match.CounterExample) (unusedAltIdxs : List ℕ)
  (addMatcher : Lean.MetaM Unit) (matcher_1 : Lean.Expr) (counterExamples_1 : Array Lean.Meta.Match.CounterExample)
  (unusedAltIdxs_1 : List ℕ) (addMatcher_1 : Lean.MetaM Unit),
  ({ matcher := matcher, counterExamples := counterExamples, unusedAltIdxs := unusedAltIdxs,
        addMatcher := addMatcher } =
      { matcher := matcher_1, counterExamples := counterExamples_1, unusedAltIdxs := unusedAltIdxs_1,
        addMatcher := addMatcher_1 }) =
    (matcher = matcher_1 ∧
      counterExamples = counterExamples_1 ∧ unusedAltIdxs = unusedAltIdxs_1 ∧ addMatcher = addMatcher_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ),
  (Polynomial.C a * Polynomial.X ^ n).toFinsupp = AddMonoidAlgebra.single n a
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.run_pure : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type w} {x : α}, (pure x).run = pure x
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuous.lowerHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuous f → ∀ (s : Set α) (x : α), LowerHemicontinuousWithinAt f s x
-- Mathlib.Topology.Compactification.StoneCech
/-- The basic open sets for the topology on ultrafilters are open.  -/
ultrafilter_isOpen_basic : ∀ {α : Type u} (s : Set α), IsOpen {u | s ∈ u}
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, (m.insert k v).contains a = (k == a || m.contains a)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasDerivAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {f' : ℂ} {x : 𝕜},
  HasDerivAt f f' x → HasDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x
-- Mathlib.Algebra.Group.Ext
AddCommGroup.toAddGroup_injective : ∀ {G : Type u_1}, Function.Injective (@AddCommGroup.toAddGroup G)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.w_prod_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') {A B : CategoryTheory.CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) {Z : D'} (h : T' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S'.map f.left.2) (CategoryTheory.CategoryStruct.comp B.hom.2 h) =
    CategoryTheory.CategoryStruct.comp A.hom.2 h
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- **Alias** of `Ideal.finite_setOfPred_absNorm_le`. -/
Ideal.finite_setOf_absNorm_le : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  [CharZero S] (n : ℕ), {I | Ideal.absNorm I ≤ n}.Finite
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_dite`. -/
Set.restrict_dite : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : (x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β)
  (g : (a : α) → a ∉ s → β), (s.domRestrict fun a => if h : a ∈ s then f a h else g a h) = fun a => f ↑a ⋯
-- Mathlib.Algebra.Azumaya.Defs
/-- `A` as a `A ⊗[R] Aᵐᵒᵖ`-module (or equivalently, an `A`-`A` bimodule).  -/
instModuleTensorProductMop : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Module (TensorProduct R A Aᵐᵒᵖ) A
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
IsPrimitiveRoot.toInteger_cube_eq_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3), hζ.toInteger ^ 3 = 1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Balls defined using the distance or the edistance coincide  -/
Metric.eball_ofReal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.eball x (ENNReal.ofReal ε) = Metric.ball x ε
-- Mathlib.Topology.Compactification.StoneCech
instTopologicalSpaceStoneCech : {α : Type u} → [inst : TopologicalSpace α] → TopologicalSpace (StoneCech α)
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.ofNSMul.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : n • x = ↑u),
  u.ofNSMul x hn hu = u.leftOfAdd x ((n - 1) • x) ⋯ ⋯
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.congr_right : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → v =ᶠ[l] w → Asymptotics.IsEquivalent l u w
-- Mathlib.Order.Rel.GaloisConnection
SetRel.rightDual_leftDual_le_of_le : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) {J J' : Set α},
  J' ∈ R.leftFixedPoints → J ⊆ J' → R.rightDual (R.leftDual J) ⊆ J'
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Surjective.instSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective f],
  AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Data.Finmap
Finmap.replace_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : AList β),
  Finmap.replace a b s.toFinmap = (AList.replace a b s).toFinmap
-- Init.Data.SInt.Lemmas
Int16.toInt64_div_of_ne_right : ∀ (a b : Int16), b ≠ -1 → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.X_sub_C_mul_removeFactor : ∀ {K : Type v} [inst : Field K] (f : Polynomial K),
  f.natDegree ≠ 0 →
    (Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor)) * f.removeFactor =
      Polynomial.map (AdjoinRoot.of f.factor) f
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_id : ∀ {ι : Type u} {β₁ : ι → Type v₁} [inst : (i : ι) → Zero (β₁ i)] (h : optParam (∀ (i : ι), id 0 = 0) ⋯)
  (g : Π₀ (i : ι), β₁ i), DFinsupp.mapRange (fun i => id) h g = g
-- Init.Data.Repr
ReprTuple : Type u → Type u
-- Std.Http.Data.Request
/-- Sets the headers for the request being built
 -/
Std.Http.Request.Builder.headers : Std.Http.Request.Builder → Std.Http.Headers → Std.Http.Request.Builder
-- Init.Data.Fin.Lemmas
Fin.val_natAdd : ∀ (n : ℕ) {m : ℕ} (i : Fin m), ↑(Fin.natAdd n i) = n + ↑i