mathlib-initiative/mathlib-types huggingface dataset:
-- Init.RCases
/-- The `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.

```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```

If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.

If `type` is omitted, `:= proof` is required.
 -/
Lean.Parser.Tactic.obtain : Lean.ParserDescr
-- Init.Internal.Order.Lemmas
Array.anyM.loop.induct : ∀ {α : Type u} (as : Array α),
  ∀ stop ≤ as.size,
    ∀ (motive : ℕ → Prop),
      (∀ x < stop, x < as.size → motive (x + 1) → motive x) → (∀ (x : ℕ), ¬x < stop → motive x) → ∀ (j : ℕ), motive j
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.skipWhile.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (nextCurr : s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none),
  (match some nextCurr with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_1 nextCurr
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The trifunctor `F - ⊗ F (- ⊗ -)`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPrePost : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory D] →
            CategoryTheory.Functor C D →
              CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Mathlib.Data.List.Permutation
List.permutations_take_two : ∀ {α : Type u_1} (x y : α) (s : List α), List.take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} [inst_2 : Inhabited (β a)],
  (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[R] Nₛ`.  -/
IsLocalizedModule.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M'] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M'] →
                  (f : M →ₗ[R] M') →
                    [IsLocalizedModule S f] →
                      {N : Type u_6} →
                        {N' : Type u_7} →
                          [inst_6 : AddCommMonoid N] →
                            [inst_7 : AddCommMonoid N'] →
                              [inst_8 : Module R N] →
                                [inst_9 : Module R N'] →
                                  (g : N →ₗ[R] N') → [IsLocalizedModule S g] → (M →ₗ[R] N) →ₗ[R] M' →ₗ[R] N'
-- Init.Data.SInt.Bitwise
ISize.ofBitVec_intMax : ISize.ofBitVec (BitVec.intMax System.Platform.numBits) = ISize.maxValue
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEmbedding_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α ↪ β} {I : Set β},
  (M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ Set.range ⇑f
-- Lean.Elab.DefView
Lean.Elab.DefKind.theorem : Lean.Elab.DefKind
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_isize : ∀ (x : ISize), ↑x = x.toInt
-- Lean.ResolveName
/-- Check whether `ns ++ id` is a valid namespace name and/or there are aliases names `ns ++ id`.  -/
_private.Lean.ResolveName.0.Lean.ResolveName.resolveQualifiedName : Lean.Environment → Lean.Options → Lean.Name → Lean.Name → List Lean.Name
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.equivFnOfDiscrete_symm_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : DiscreteTopology α]
  (f : α → β) (a : α), (ContinuousMap.equivFnOfDiscrete.symm f) a = f a
-- Mathlib.Data.EReal.Operations
EReal.add_ne_bot_iff : ∀ {x y : EReal}, x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal`.

---

The property of posets in `CardinalDirectedPoset κ` that are
of cardinality `< κ` and have terminal object.  -/
CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminal : (κ : Cardinal.{u}) → [inst : Fact κ.IsRegular] → CategoryTheory.ObjectProperty (CategoryTheory.CardinalDirectedPoset κ)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.id_toOrderHom : ∀ (a : SimplexCategory), SimplexCategory.Hom.toOrderHom (CategoryTheory.CategoryStruct.id a) = OrderHom.id
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Algebra.forget_additive : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive], (CategoryTheory.Endofunctor.Algebra.forget F).Additive
-- Init.Data.Ord.Basic
List.isLE_compareLex_nil_right : ∀ {α : Type u_1} {cmp : α → α → Ordering} {xs : List α}, (List.compareLex cmp xs []).isLE = true ↔ xs = []
-- Mathlib.Logic.Basic
forall_true_iff : ∀ {α : Sort u_1}, (∀ (a : α), True) ↔ True
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- An element in SL₂(F) induced by a diagonal matrix with `a`, `a⁻¹` on
positition `0` and `1` respectively.  -/
Matrix.SpecialLinearGroup.diag2 : {F : Type u_1} → [inst : Field F] → (a : F) → a ≠ 0 → Matrix.SpecialLinearGroup (Fin 2) F
-- Mathlib.Data.Fin.Rev
Fin.rev_le_iff : ∀ {n : ℕ} {i j : Fin n}, i.rev ≤ j ↔ j.rev ≤ i
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.inclusion.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M} (h : p ≤ p'), Submodule.inclusion h = Submodule.inclusion h
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.associativity_inv : ∀ {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 Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- The complement of a measurable set is a measurable set. Use `MeasurableSet.compl` instead.  -/
MeasurableSpace.measurableSet_compl : ∀ {α : Type u_7} (self : MeasurableSpace α) (s : Set α),
  MeasurableSpace.MeasurableSet' self s → MeasurableSpace.MeasurableSet' self sᶜ
-- Mathlib.Algebra.Group.Shrink
Shrink.instMulAction : {M : Type u_1} →
  {α : Type u_2} → [inst : Small.{v, u_2} α] → [inst_1 : Monoid M] → [MulAction M α] → MulAction M (Shrink.{v, u_2} α)
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.toByteArray_eq_left : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → t₁.toByteArray = s.toByteArray.extract 0 p.offset.byteIdx
-- Mathlib.Order.ModularLattice
infIccOrderIsoIccSup'_symm_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (a_1 : ↑(Set.Icc a (a ⊔ b))),
  ↑((RelIso.symm (infIccOrderIsoIccSup' a b)) a_1) =
    ↑((infIccOrderIsoIccSup b a).symm ((OrderIso.setCongr (Set.Icc a (b ⊔ a)) (Set.Icc a (a ⊔ b)) ⋯).symm a_1))
-- Mathlib.Order.Heyting.Basic
/-- Construct a co-Heyting algebra from the difference and Heyting negation alone.  -/
CoheytingAlgebra.ofHNot : {α : Type u_2} →
  [inst : DistribLattice α] →
    [BoundedOrder α] → (hnot : α → α) → (∀ (a b c : α), a ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) → CoheytingAlgebra α
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Init.Data.String.Basic
/-- Given a position in `s` that is at least `p₀`, obtain the corresponding position in
`s.sliceFrom p₀`.  -/
String.Pos.sliceFrom : {s : String} → (p₀ pos : s.Pos) → p₀ ≤ pos → (s.sliceFrom p₀).Pos
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, DifferentiableAt 𝕜 f x → HasFDerivAt f (fderiv 𝕜 f x) x
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ : ∀ {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.Monoidal] (X Y : C) (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) T)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) T) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T)
-- Mathlib.Analysis.Quaternion
Quaternion.nnnorm_star : ∀ (a : Quaternion ℝ), ‖star a‖₊ = ‖a‖₊
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.monadLift_refl : ∀ {m : Type u → Type v} {α : Type u} (x : m α), monadLift x = x
-- Mathlib.Data.Finsupp.AList
AList.lookupFinsupp_eq_iff_of_ne_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] {l : AList fun _x => M} {a : α} {x : M},
  x ≠ 0 → (l.lookupFinsupp a = x ↔ x ∈ AList.lookup a l)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R}
  (h : S.moduleCatLeftHomologyData.K ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom h) =
    CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.f' h
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  φ.IsPrenex → ψ.IsPrenex → (φ.toPrenexImp ψ).IsPrenex
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.subset_Icc_csInf_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrder α] {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≥ x2) s →
    DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddBelow s → BddAbove s → s ⊆ Set.Icc (sInf s) (sSup s)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mk : ∀ {R : Type u} [inst : Lean.Grind.Semiring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPreorder R]
  [toOrderedAdd : Lean.Grind.OrderedAdd R],
  0 < 1 →
    (∀ {a b c : R}, a < b → 0 < c → c * a < c * b) →
      (∀ {a b c : R}, a < b → 0 < c → a * c < b * c) → Lean.Grind.OrderedRing R
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.mvfunctor : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → MvFunctor (MvQPF.Cofix F)
-- Init.Data.Nat.Fold
Nat.dfold_congr : ∀ {n m : ℕ} (w : n = m) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold_congr._auto_1 → Type u}
  (f : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯),
  n.dfold f init = cast ⋯ (m.dfold (fun i h => f i ⋯) init)
-- Mathlib.Data.Finset.Fold
Finset.fold_op_rel_iff_and : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {r : β → β → Prop},
  (∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z) → ∀ {c : β}, r c (Finset.fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x x_1 : List α) (h_1 : (acc : List α) → motive [] acc)
  (h_2 : (a : α) → (t acc : List α) → motive (a :: t) acc) (acc : List α),
  x = [] →
    x_1 = acc →
      (match x, x_1 with
        | [], acc => h_1 acc
        | a :: t, acc => h_2 a t acc) ≍
        h_1 acc
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_map : ∀ {α : Type u_1} {β : Type u_2} (f : α →₀ ℕ) (g : α → β),
  Multiset.map g (Finsupp.toMultiset f) = Finsupp.toMultiset (Finsupp.mapDomain g f)
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.comp_monotoneOn_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : LinearOrder β]
  [inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
  AntivaryOn f g s → MonotoneOn g' (g '' s) → AntivaryOn f (g' ∘ g) s
-- Mathlib.GroupTheory.GroupAction.ConjAct
MulAut.conjNormal_val : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] {h : ↥H}, MulAut.conjNormal ↑h = MulAut.conj h
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α}
  [CompleteSpace α], Summable f → ∀ (s : Set β), Summable (s.indicator f)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_diseq_subst1_cert : ℤ → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₂_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  CategoryTheory.Square.evaluation₂.map φ = φ.τ₂
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.unit_mem_leftInv : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : Mˣ), ↑x ∈ S → ↑x⁻¹ ∈ S.leftInv
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nonempty_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, (Metric.ball x ε).Nonempty ↔ 0 < ε
-- Mathlib.Algebra.GroupWithZero.Action.Defs
MulActionWithZero.toSMulWithZero : (M₀ : Type u_12) →
  (A : Type u_13) → {x : MonoidWithZero M₀} → {x_1 : Zero A} → [m : MulActionWithZero M₀ A] → SMulWithZero M₀ A
-- Mathlib.Topology.ContinuousMap.StarOrdered
ContinuousSqrt.continuousOn_sqrt : ∀ {R : Type u_1} {inst : LE R} {inst_1 : NonUnitalSemiring R} {inst_2 : TopologicalSpace R} [self : ContinuousSqrt R],
  ContinuousOn ContinuousSqrt.sqrt {x | x.1 ≤ x.2}
-- Mathlib.Topology.Algebra.Nonarchimedean.Completion
/-- The completion of a nonarchimedean ring is a nonarchimedean ring.  -/
instNonarchimedeanRingCompletion : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : UniformSpace R] [inst_2 : IsUniformAddGroup R]
  [inst_3 : NonarchimedeanRing R], NonarchimedeanRing (UniformSpace.Completion R)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.toHom (CochainComplex.HomComplex.CohomologyClass.mk x) = 0 ↔
    x ∈ CochainComplex.HomComplex.coboundaries K L n
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.dropSuffix?_string_eq_dropSuffix?_toSlice : ∀ {pat : String} {s : String.Slice}, s.dropSuffix? pat = s.dropSuffix? pat.toSlice
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae' : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : PseudoEMetricSpace E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f u g →
    ∃ ns,
      Filter.Tendsto ns Filter.atTop u ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => f (ns i) x) Filter.atTop (nhds (g x))
-- Mathlib.LinearAlgebra.Prod
Submodule.le_prod_iff : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)},
  q ≤ p₁.prod p₂ ↔ Submodule.map (LinearMap.fst R M M₂) q ≤ p₁ ∧ Submodule.map (LinearMap.snd R M M₂) q ≤ p₂
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The strict universal property of the localization with respect
to weak equivalences for the quotient functor
`toHoCat : BifibrantObject C ⥤ BifibrantObject.HoCat C`.  -/
HomotopicalAlgebra.BifibrantObject.strictUniversalPropertyFixedTargetToHoCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          CategoryTheory.Localization.StrictUniversalPropertyFixedTarget HomotopicalAlgebra.BifibrantObject.toHoCat
            (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C)) D
-- Mathlib.Topology.UniformSpace.Closeds
/-- The neighborhoods of a totally bounded set in the Hausdorff uniformity are neighborhoods in the
Vietoris topology.  -/
TotallyBounded.nhds_vietoris_le_nhds_hausdorff : ∀ {α : Type u_1} [inst : UniformSpace α] {s : Set α}, TotallyBounded s → nhds s ≤ nhds s
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_apply_le : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β) (i : ι), ‖x.ofLp i‖₊ ≤ ‖x‖₊
-- Lean.Meta.Tactic.Grind.AC.DenoteExpr
Lean.Meta.Grind.AC.EqCnstr.denoteExpr : {M : Type → Type} → [Monad M] → [Lean.Meta.Grind.AC.MonadGetStruct M] → Lean.Meta.Grind.AC.EqCnstr → M Lean.Expr
-- Lean.Elab.Tactic.Omega.Core
/-- Whether the elimination would be exact, because all of the upper bound coefficients are `±1`.
 -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.upperExact : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → Bool
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ : W.LeftFraction₂ X Y},
  CategoryTheory.MorphismProperty.LeftFraction₂Rel z₁ z₂ → CategoryTheory.MorphismProperty.LeftFractionRel z₁.fst z₂.fst
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.toList.eq_2 : ∀ {α : Type u} {β : α → Type v} (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  (Std.DHashMap.Internal.AssocList.cons a b es).toList = ⟨a, b⟩ :: es.toList
-- Lean.Meta.Tactic.LibrarySearch
/-- The maximum number of constants an individual task may perform.

The value was picked because it roughly corresponded to 50ms of work on the
machine this was developed on.  Smaller numbers did not seem to improve
performance when importing Std and larger numbers (<10k) seemed to degrade
initialization performance.
 -/
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.constantsPerImportTask : ℕ
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An `OrderIso` on `ArchimedeanClass` induces an `OrderIso` on `FiniteArchimedeanClass`.  -/
FiniteArchimedeanClass.congrOrderIso : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {N : Type u_2} →
          [inst_3 : AddCommGroup N] →
            [inst_4 : LinearOrder N] →
              [inst_5 : IsOrderedAddMonoid N] →
                ArchimedeanClass M ≃o ArchimedeanClass N → FiniteArchimedeanClass M ≃o FiniteArchimedeanClass N
-- Mathlib.Order.Filter.Basic
Filter.eventually_bot : ∀ {α : Type u} {p : α → Prop}, ∀ᶠ (x : α) in ⊥, p x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Squares between left adjoints can be composed "horizontally" by pasting.  -/
CategoryTheory.Bicategory.leftAdjointSquare.hcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f : B} →
      {g : a ⟶ d} →
        {h : b ⟶ e} →
          {k : c ⟶ f} →
            {l₁ : a ⟶ b} →
              {l₂ : d ⟶ e} →
                {l₃ : b ⟶ c} →
                  {l₄ : e ⟶ f} →
                    (CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h) →
                      (CategoryTheory.CategoryStruct.comp h l₄ ⟶ CategoryTheory.CategoryStruct.comp l₃ k) →
                        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp l₂ l₄) ⟶
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp l₁ l₃) k)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the 1-dimensional derivative.

Version for a general bilinear map.  -/
SchwartzMap.integral_bilinear_deriv_right_eq_neg_left : ∀ {E : Type u_5} {V : Type u_7} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedAddCommGroup V] [inst_5 : NormedSpace ℝ V]
  (f : SchwartzMap ℝ E) (g : SchwartzMap ℝ F) (L : E →L[ℝ] F →L[ℝ] V),
  ∫ (x : ℝ), (L (f x)) (deriv (⇑g) x) = -∫ (x : ℝ), (L (deriv (⇑f) x)) (g x)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.go.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (p : Lean.Grind.CommRing.Poly)
  (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0)) (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p))
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Poly),
  p = Lean.Grind.CommRing.Poly.add k m p_1 →
    (match p with
      | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
      | Lean.Grind.CommRing.Poly.num k => h_2 k
      | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) ≍
      h_3 k m p_1
-- Std.Time.Format.Modifier
Std.Time.Modifier.y.inj : ∀ {presentation presentation_1 : Std.Time.Year},
  Std.Time.Modifier.y presentation = Std.Time.Modifier.y presentation_1 → presentation = presentation_1
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is
invertible and to `0` otherwise.  This definition is somewhat ad hoc, but one needs a fully (rather
than partially) defined inverse function for some purposes, including for calculus.

Note that while this is in the `Ring` namespace for brevity, it requires the weaker assumption
`MonoidWithZero M₀` instead of `Ring M₀`.  -/
Ring.«term_⁻¹ʳ» : Lean.TrailingParserDescr