mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Util.ProofWanted
/-- If `true`, the recorded statement must be a `Prop` (the placeholder is ascribed `: Prop`,
and `theorem` is used for the "Try this:" fallback).  -/
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.requireProp : WantedCmdKind✝ → Bool
-- Init.Data.Array.Basic
/-- Applies the monadic predicate `p` on every element in the array in reverse order, from right to
left, and returns those elements for which `p` returns `true`. The elements of the returned list are
in the same order as in the input list.

Only elements from `start` (exclusive) to `stop` (inclusive) are considered. Elements outside that
range are discarded. Because the array is examined in reverse order, elements are only examined when
`start > stop`. By default, the entire array is considered.

Example:
```lean example
#eval #[1, 2, 5, 2, 7, 7].filterRevM fun x => do
  IO.println s!"Checking {x}"
  return x < 3
```
```output
Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1
```
```output
#[1, 2, 2]
```
 -/
Array.filterRevM : {m : Type → Type u_1} →
  {α : Type} → [Monad m] → (α → m Bool) → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → m (Array α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.size ≤ (t.erase k).size + 1
-- Init.Data.String.Lemmas.Intercalate
String.intercalate_append_of_ne_nil : ∀ {l m : List String} {s : String}, l ≠ [] → m ≠ [] → s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m
-- Init.Data.Option.Lemmas
Option.pmap_eq_map : ∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (o : Option α) (H : ∀ (a : α), o = some a → p a),
  Option.pmap (fun a x => f a) o H = Option.map f o
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.map : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {pa qa : Set α → Prop},
  μ.InnerRegularWRT pa qa →
    ∀ {f : α → β},
      AEMeasurable f μ →
        ∀ {pb qb : Set β → Prop},
          (∀ (U : Set β), qb U → qa (f ⁻¹' U)) →
            (∀ (K : Set α), pa K → pb (f '' K)) →
              (∀ (U : Set β), qb U → MeasurableSet U) → (MeasureTheory.Measure.map f μ).InnerRegularWRT pb qb
-- Mathlib.Order.Preorder.Chain
/-- Reinterpret a maximal chain as a flag.  -/
Flag.ofIsMaxChain : {α : Type u_1} → [inst : LE α] → (c : Set α) → IsMaxChain (fun x1 x2 => x1 ≤ x2) c → Flag α
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The naturality condition.  -/
CategoryTheory.Lax.OplaxTrans.Modification.naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Lax.OplaxTrans.Modification η θ) {a b : B}
  (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b)) (θ.naturality f) =
    CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide locally around `x`, except maybe at a point `y`, then their
preimage under `extChartAt x` coincide locally, except maybe at `extChartAt I x x`.  -/
preimage_extChartAt_eventuallyEq_compl_singleton : ∀ {𝕜 : 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] {x : M} {s t : Set M} (y : M),
  s =ᶠ[nhdsWithin x {y}ᶜ] t →
    ↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhdsWithin (↑(extChartAt I x) x) {↑(extChartAt I x) x}ᶜ]
      ↑(extChartAt I x).symm ⁻¹' t ∩ Set.range ↑I
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.sup_mul_le_mul_sup_of_nonneg : ∀ {ι : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [inst_1 : SemilatticeSup M₀]
  [inst_2 : OrderBot M₀] [PosMulMono M₀] [MulPosMono M₀],
  (∀ i ∈ s, 0 ≤ a i) → (∀ i ∈ s, 0 ≤ b i) → s.sup (a * b) ≤ s.sup a * s.sup b
-- Mathlib.Order.Hom.CompleteLattice
map_iInf : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [inst : FunLike F α β] [inst_1 : InfSet α]
  [inst_2 : InfSet β] [sInfHomClass F α β] (f : F) (g : ι → α), f (⨅ i, g i) = ⨅ i, f (g i)
-- Mathlib.Data.Finset.Union
_private.Mathlib.Data.Finset.Union.0.Finset.pairwiseDisjoint_fibers : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β},
  (↑t).PairwiseDisjoint fun a => {x ∈ s | f x = a}
-- Mathlib.Order.Fin.Tuple
Fin.consOrderIso_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (f : α 0 × ((i : Fin n) → α i.succ))
  (i : Fin (n + 1)), (Fin.consOrderIso α) f i = Fin.cons f.1 f.2 i
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (i : Set α),
  MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i =
    if hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i then Classical.choose ⋯
    else ∅
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.ne_add_utf8Size_add_self : ∀ {i n : ℕ} {c : Char}, i ≠ n + c.utf8Size + i
-- Mathlib.Algebra.Group.Prod
AddCommute.prod : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] {x y : M × N},
  AddCommute x.1 y.1 → AddCommute x.2 y.2 → AddCommute x y
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α}
  [inst : Inhabited β], (List.map Prod.fst l).contains k = false → (Std.HashMap.ofList l)[k]! = default
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_left_injective_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {b : α}, b ≠ ⊤ → Function.Injective fun x => x - b
-- Mathlib.Data.Rel
SetRel.image_subset_image : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → R.image s₁ ⊆ R.image s₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_hom_app : ∀ (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ),
  CategoryTheory.Limits.walkingSpanOpEquiv.unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mk.sizeOf_spec : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} [inst_3 : SizeOf A] [inst_4 : SizeOf B] [inst_5 : SizeOf T] (left : A) (right : B)
  (hom : L.obj left ⟶ R.obj right),
  sizeOf { left := left, right := right, hom := hom } = 1 + sizeOf left + sizeOf right + sizeOf hom
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.isDominant_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.IsDominant f ↔ DenseRange ⇑f
-- Mathlib.Computability.NFA
NFA.Path.supp.eq_def : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} [inst : DecidableEq σ] {s t : σ} {x : List α} (x_1 : M.Path s t x),
  x_1.supp =
    match x, t, s, x_1 with
    | .([]), s, .(s), NFA.Path.nil .(s) => {s}
    | .(a :: x), t, s, NFA.Path.cons t_1 .(s) .(t) a x a_1 p => {s} ∪ p.supp
-- Mathlib.Algebra.Group.EvenFunction
Function.Odd.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] [inst_1 : SubtractionCommMonoid β] {f g : α → β},
  Function.Odd f → Function.Odd g → Function.Odd (f + g)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_enorm_rpow' : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [MeasureTheory.IsFiniteMeasure μ] {f : α → ε} {p : ENNReal},
  MeasureTheory.MemLp f p μ → MeasureTheory.Integrable (fun x => ‖f x‖ₑ ^ p.toReal) μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Order.Filter.Basic
Filter.Eventually.bot_lt_of_ne : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] [inst_1 : OrderBot β] {l : Filter α} {f : α → β},
  (∀ᶠ (x : α) in l, f x ≠ ⊥) → ∀ᶠ (x : α) in l, ⊥ < f x
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `coeq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
`f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
 -/
CategoryTheory.IsFiltered.coeq_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j j' : C}
  (f f' : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeqHom f f') =
    CategoryTheory.CategoryStruct.comp f' (CategoryTheory.IsFiltered.coeqHom f f')
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.trunc_derivative : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
  (PowerSeries.trunc n) ((PowerSeries.derivative R) f) = Polynomial.derivative ((PowerSeries.trunc (n + 1)) f)
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.instHashableSparseCasesOnKey : Hashable Lean.Meta.SparseCasesOnKey✝
-- Lean.LocalContext
/-- Return all of the free variables in the given context.  -/
Lean.LocalContext.getFVars : Lean.LocalContext → Array Lean.Expr
-- Mathlib.Logic.Basic
dite_ne_right_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {b : α} {A : P → α}, (dite P A fun x => b) ≠ b ↔ ∃ (h : P), A h ≠ b
-- Mathlib.Data.Finset.Card
Finset.card_pair_eq_one_or_two : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], {a, b}.card = 1 ∨ {a, b}.card = 2
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.MulSaturated.top : ∀ {M : Type u_1} [inst : MulOneClass M], ⊤.MulSaturated
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of limits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesLimits_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_commute : ∀ {α : Type u_3} [inst : Monoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (y : α),
  (∀ x ∈ s, Commute y x) → Commute y (s.noncommProd comm)
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.instEssFiniteTypeQuotientIdeal : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (I : Ideal S), Algebra.EssFiniteType R (S ⧸ I)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.markMatcherLike : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Order.Atoms
/-- **Alias** of the forward direction of `bot_covBy_iff`. -/
CovBy.is_atom : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ ⋖ a → IsAtom a
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.WhiskerLeft → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
    ((t : Mathlib.Tactic.BicategoryLike.WhiskerLeft) → Mathlib.Tactic.BicategoryLike.WhiskerLeft.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.WhiskerLeft.below t
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_sliceFrom_eq_iff_exists_splits : ∀ {s : String.Slice} {p : s.Pos} {t₂ : String}, (s.sliceFrom p).copy = t₂ ↔ ∃ t₁, p.Splits t₁ t₂
-- Mathlib.Order.Heyting.Basic
hnot_sdiff : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), ￢a \ a = ￢a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (n : ℕ), (Polynomial.X ^ n).support = {n}
-- Mathlib.Data.Num.Lemmas
Num.add_succ : ∀ (m n : Num), m + n.succ = (m + n).succ
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Suggestion.mk.sizeOf_spec : ∀ (name : Lean.Name) (score : Float) (flag : Option String),
  sizeOf { name := name, score := score, flag := flag } = 1 + sizeOf name + sizeOf score + sizeOf flag
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o o_1 : Orientation ℝ E (Fin n)), o = o_1 → o.volumeForm = o_1.volumeForm
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- A `PartialEquiv` which is continuous on its source and has open forward map (on its source)
and open source is an `OpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.ofContinuousOpenRestrict : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : PartialEquiv X Y) →
          ContinuousOn (↑e) e.source → IsOpenMap (e.source.domRestrict ↑e) → IsOpen e.source → OpenPartialHomeomorph X Y
-- Mathlib.Data.List.AList
AList.mem_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b' : β a'} (s : AList β),
  a ∈ AList.insert a' b' s ↔ a = a' ∨ a ∈ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k}
  {hc : k' ∈ Std.DTreeMap.Internal.Impl.modify k f t},
  (Std.DTreeMap.Internal.Impl.modify k f t).getKey k' hc = if compare k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_symm_some : ∀ {n : ℕ} (m : Fin n), (finSuccEquiv n).symm (some m) = m.succ
-- Lean.Elab.Quotation.Util
/-- Given an antiquotation like `$e:term` (i.e. `Syntax.antiquotKind?` returns `some`),
returns the `"term"` atom if present.
 -/
Lean.Elab.Term.Quotation.getAntiquotKindSpec? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_subset_Ioi_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi b ⊆ Set.Ioi a ↔ a ≤ b
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.Integrable.comp_snd_map_prod_id : ∀ {Ω : Type u_1} {F : Type u_2} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → F}
  [inst : NormedAddCommGroup F],
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map Function.diag μ)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First-Derivative Test from calculus, minima version,
expressed in terms of left and right filters.  -/
isLocalMin_of_deriv' : ∀ {f : ℝ → ℝ} {b : ℝ},
  ContinuousAt f b →
    (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), DifferentiableAt ℝ f x) →
      (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), DifferentiableAt ℝ f x) →
        (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), deriv f x ≤ 0) →
          (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), deriv f x ≥ 0) → IsLocalMin f b
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instAddMonoid : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → AddMonoid (AddMonoidAlgebra R M)
-- Mathlib.Topology.Algebra.UniformFilterBasis
/-- The uniform space structure associated to an abelian group filter basis via the associated
topological abelian group structure.  -/
AddGroupFilterBasis.uniformSpace : {G : Type u_1} → [inst : AddCommGroup G] → AddGroupFilterBasis G → UniformSpace G
-- Batteries.Data.List.Lemmas
List.countPBefore.go.eq_3 : ∀ {α : Type u_1} (p : α → Bool) (i s : ℕ), List.countPBefore.go p [] i s = s
-- Mathlib.Data.Int.Init
Int.le_iff_pos_of_dvd : ∀ {a b : ℤ}, 0 < a → a ∣ b → (a ≤ b ↔ 0 < b)
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNumExt.mk : Bool →
  Bool →
    ({u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)) →
      autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam → Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.BitVec.Lemmas
BitVec.toInt_mul_of_not_smulOverflow : ∀ {w : ℕ} {x y : BitVec w}, ¬x.smulOverflow y = true → (x * y).toInt = x.toInt * y.toInt
-- Init.Data.Int.Lemmas
Int.subNatNat_of_sub_eq_succ : ∀ {m n k : ℕ}, n - m = k.succ → Int.subNatNat m n = Int.negSucc k
-- Mathlib.Data.Multiset.Basic
/-- Suppose that, given that `p t` can be defined on all supersets of `s` of cardinality less than
`n`, one knows how to define `p s`. Then one can inductively define `p s` for all multisets `s` of
cardinality less than `n`, starting from multisets of card `n` and iterating. This
can be used either to define data, or to prove properties.  -/
Multiset.strongDownwardInduction : {α : Type u_1} →
  {p : Multiset α → Sort u_3} →
    {n : ℕ} →
      ((t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) →
        (s : Multiset α) → s.card ≤ n → p s
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some '' Set.Ioi a = Set.Ioi ↑a
-- Mathlib.Order.SetAccumulate
Set.accumulate_zero_nat : ∀ {β : Type u_2} (s : ℕ → Set β), Set.accumulate s 0 = s 0
-- Mathlib.Order.CompleteLattice.Defs
iInf_le_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteSemilatticeInf α] {a : α} {s : ι → α},
  iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a
-- Mathlib.Order.Types.Defs
/-- An order type lifted to the zero universe equals itself.  -/
OrderType.lift_uzero : ∀ (o : OrderType.{u}), OrderType.lift.{0, u} o = o
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.instUnique : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.RightHomologyData) →
            (h₂ : S₂.RightHomologyData) → Unique (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
-- Mathlib.Data.Finsupp.Weight
Finsupp.range_single_one : ∀ {σ : Type u_1}, (Set.range fun a => fun₀ | a => 1) = {d | Finsupp.degree d = 1}
-- Lean.Meta.Basic
Lean.Meta.getNumPostponed : Lean.MetaM ℕ
-- Mathlib.Topology.Sets.Closeds
/-- The complement of a closed set as an open set.  -/
TopologicalSpace.Closeds.compl : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Closeds α → TopologicalSpace.Opens α
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.residueFieldMap.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.residueFieldMap f x =
    CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)))
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- An inductive type representing all monoid expressions (without relations)
on a collection of types indexed by the objects of `J`.
 -/
MonCat.Colimits.Prequotient : {J : Type v} → [inst : CategoryTheory.Category.{u, v} J] → CategoryTheory.Functor J MonCat → Type v
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instReprExtTheorem.repr : Lean.Meta.Ext.ExtTheorem → ℕ → Std.Format
-- Mathlib.Data.Set.Sups
Set.mem_sups : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α} {c : α}, c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_single_of_pos : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] {a : α} {b : M},
  p a → (Finsupp.filter p fun₀ | a => b) = fun₀ | a => b
-- Mathlib.RingTheory.Flat.Equalizer
Module.Flat.eqLocus_lTensor_eq : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) [Module.Flat R M],
  ((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) g) =
    ((TensorProduct.AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype).range
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul_iff_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b c : α},
  a * b ≤ a * c ↔ b ≤ c
-- Std.Http.Data.Status
Std.Http.Status.httpVersionNotSupported.sizeOf_spec : sizeOf Std.Http.Status.httpVersionNotSupported = 1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.mk.inj : ∀ {lhs rhs : Lean.Grind.AC.Seq} {h : Lean.Meta.Grind.AC.DiseqCnstrProof} {lhs_1 rhs_1 : Lean.Grind.AC.Seq}
  {h_1 : Lean.Meta.Grind.AC.DiseqCnstrProof},
  { lhs := lhs, rhs := rhs, h := h } = { lhs := lhs_1, rhs := rhs_1, h := h_1 } → lhs = lhs_1 ∧ rhs = rhs_1 ∧ h = h_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_2 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_2 ()
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed.insertWff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : Type u_2} {t : Lean.PrefixTreeNode α x cmp} {k : List α} {val : x},
  Lean.PrefixTreeNode.WellFormed cmp t → Lean.PrefixTreeNode.WellFormed cmp (Lean.PrefixTreeNode.insert cmp t k val)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceLast : Lean.Meta.Simp.DSimproc
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_erase_le : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.comp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι] {t : ι → Ω → ι}
  [inst_3 : TopologicalSpace ι] [BorelSpace ι] [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f t →
      (∀ (i : ι) (ω : Ω), t i ω ≤ i) → MeasureTheory.IsStronglyProgressive f fun i ω => u (t i ω) ω
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Ici : ∀ {n : ℕ} (i : Fin n), Finset.map (Fin.succEmb n) (Finset.Ici i) = Finset.Ici i.succ
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.finite_real_spectrum : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n],
  (spectrum ℝ A).Finite