mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Batteries.Recycling.RBTree.Basic
/-- The maximum element of a tree is the right-most value.  -/
RBTree.RBNode.max? : {α : Type u_1} → RBTree.RBNode α → Option α
-- Lean.Data.Json.Basic
Lean.Json.Structured.arr : Array Lean.Json → Lean.Json.Structured
-- Mathlib.Algebra.BigOperators.Finprod
/-- `∑ᶠ x, f x` is notation for `finsum f`. It is the sum of `f x`, where `x` ranges over the
support of `f`, if it's finite, zero otherwise. Taking the sum over multiple arguments or
conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x`  -/
«term∑ᶠ_,_» : Lean.ParserDescr
-- Mathlib.Order.Ideal
Order.Ideal.coe_toIdeal : ∀ {P : Type u_1} [inst : LE P] {I : Set P} (h : Order.IsIdeal I), ↑h.toIdeal = I
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_top : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, a ∈ ⊤
-- Init.Data.BitVec.Bitblast
BitVec.divRec_succ' : ∀ {w : ℕ} (m : ℕ) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w),
  BitVec.divRec (m + 1) args qr =
    have wn := qr.wn - 1;
    have wr := qr.wr + 1;
    have r' := qr.r.shiftConcat (args.n.getLsbD wn);
    have input :=
      if r' < args.d then { wn := wn, wr := wr, q := qr.q.shiftConcat false, r := r' }
      else { wn := wn, wr := wr, q := qr.q.shiftConcat true, r := r' - args.d };
    BitVec.divRec m args input
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.contains.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.contains a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => false
    | Std.DHashMap.Internal.AssocList.cons k value l => k == a || Std.DHashMap.Internal.AssocList.contains a l
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.liftOn.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (x : Localization S) (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d), x.liftOn f H = Localization.rec f ⋯ x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Order.Interval.Set.ProjIcc
Set.monotone_projIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Monotone (Set.projIcc a b h)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cocycle K (L⟦a⟧) n' → Cocycle K L n` when `n' + a = n`.  -/
CochainComplex.HomComplex.Cocycle.rightUnshift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n' a : ℤ} →
          CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n' →
            (n : ℤ) → n' + a = n → CochainComplex.HomComplex.Cocycle K L n
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Returns `.true` if `c` is satisfied by the current partial model,
`.undef` if `c` contains unassigned variables, and `.false` otherwise.
 -/
Lean.Meta.Grind.Arith.Linear.IneqCnstr.satisfied : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Lean.Meta.Grind.Arith.Linear.LinearM Lean.LBool
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRight_counitIso_inv_app : ∀ {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] (e : C ≌ D) (X : CategoryTheory.Functor E D),
  e.congrRight.counitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp X.rightUnitor.inv
      (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.inv) (X.associator e.inverse e.functor).inv)
-- Mathlib.RingTheory.Valuation.Quotient
AddValuation.self_le_supp_comap : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (J : Ideal R)
  (v : AddValuation (R ⧸ J) Γ₀), J ≤ (AddValuation.comap (Ideal.Quotient.mk J) v).supp
-- Mathlib.Data.ZMod.Basic
ZModModule.neg_eq_self : ∀ {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod 2) G] (x : G), -x = x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.isPullback_χ`.

---

The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
is a pullback square.
 -/
CategoryTheory.HasClassifier.isPullback_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.IsPullback m (⋯.some.χ₀ U) (CategoryTheory.HasSubobjectClassifier.χ m)
    (CategoryTheory.HasSubobjectClassifier.truth C)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.sum_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  [inst_1 : J.IsStableUnderSup] (E : J.ZeroHypercover S) (F : J.ZeroHypercover S),
  (E.sum F).toPreZeroHypercover = E.sum F.toPreZeroHypercover
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObj.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.yonedaAddMonObj M =
    { obj := fun X => AddMonCat.of (Opposite.unop X ⟶ M),
      map := fun {X Y₂} φ =>
        AddMonCat.ofHom
          { toFun := fun x => CategoryTheory.CategoryStruct.comp φ.unop x, map_zero' := ⋯, map_add' := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkPureUnitAction : Lean.MacroM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_add : ∀ (x y : NNReal), ↑(x + y) = ↑x + ↑y
-- Lean.Language.Basic
Lean.Language.SnapshotTask.ReportingRange.some.sizeOf_spec : ∀ (range : Lean.Syntax.Range), sizeOf (Lean.Language.SnapshotTask.ReportingRange.some range) = 1 + sizeOf range
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.new : {α : Type} → BaseIO (Std.CloseableChannel.Unbounded✝ α)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.prod_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'], ⊤.prod ⊤ = ⊤
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_functor_map_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {Y X : CategoryTheory.Comma L R₁} (f : Y ⟶ X),
  ((CategoryTheory.Comma.mapRightIso L i).functor.map f).left = f.left
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.toContinuousSMul : ∀ (R : Type u_1) [inst : TopologicalSpace R] (A : Type u_2) [inst_1 : Add A] [inst_2 : SMul R A]
  [inst_3 : TopologicalSpace A] [IsModuleTopology R A], ContinuousSMul R A
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_inf : ∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthInf (u ⊓ v) = min (ExpGrowth.expGrowthInf u) (ExpGrowth.expGrowthInf v)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.eq_def : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α),
  Std.DTreeMap.Internal.Impl.pruneLE✝ t lowerBound =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k v l r =>
      match compare lowerBound k with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k v (Std.DTreeMap.Internal.Impl.pruneLE✝ l lowerBound) r
      | Ordering.eq => Std.DTreeMap.Internal.Impl.inner sz k v Std.DTreeMap.Internal.Impl.leaf r
      | Ordering.gt => Std.DTreeMap.Internal.Impl.pruneLE✝ r lowerBound
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_add_left : ∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Add M] [IsIsometricVAdd M M] (a b c : M),
  nndist (a + b) (a + c) = nndist b c
-- Mathlib.Topology.Compactness.SigmaCompact
SigmaCompactSpace.of_countable : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
  S.Countable → (∀ s ∈ S, IsCompact s) → ⋃₀ S = Set.univ → SigmaCompactSpace X
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mk.congr_simp : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R']
  (toMonoidHom toMonoidHom_1 : R →* R') (e_toMonoidHom : toMonoidHom = toMonoidHom_1)
  (map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom).toFun a = 0),
  { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' } = { toMonoidHom := toMonoidHom_1, map_nonunit' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Icc_eq_integral_Ioo' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X},
  μ {x} = 0 → μ {y} = 0 → ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A too large block is equal to `univ`  -/
AddAction.IsBlock.eq_univ_of_card_lt : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X] {B : Set X}
  [hX : Finite X], AddAction.IsBlock G B → Nat.card X < B.ncard * 2 → B = Set.univ
-- Mathlib.Algebra.GroupWithZero.Action.Units
Units.smul_mk0 : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {α : Type u_6} [inst_1 : SMul G₀ α] {g : G₀} (hg : g ≠ 0) (a : α),
  Units.mk0 g hg • a = g • a
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.IsIdempotentElem.isTopCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f : M →L[R] M}, IsIdempotentElem f → Submodule.IsTopCompl (↑f).range (↑f).ker
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- Auxiliary lemma for `measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'`.  -/
MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α}
  [inst : MeasureTheory.IsFiniteMeasure ν], MeasurableSet s → s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ → ν s ≠ 0 → μ s = ⊤
-- Aesop.Forward.SlotIndex
Aesop.instHSubSlotIndexNat : HSub Aesop.SlotIndex ℕ Aesop.SlotIndex
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.needMoreData.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (size size_1 : Option ℕ),
  (Std.Http.Protocol.H1.Event.needMoreData size = Std.Http.Protocol.H1.Event.needMoreData size_1) = (size = size_1)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y} (hf : Φ.prop f), hf.arrowIso.inv.left = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W},
  f = g ↔
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g ∧
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g
-- Mathlib.Data.ENNReal.Inv
/-- Right multiplication by a nonzero finite `a` as an order isomorphism.  -/
ENNReal.mulRightOrderIso : (a : ENNReal) → IsUnit a → ENNReal ≃o ENNReal
-- Batteries.Recycling.RBTree.Basic
/-- Returns `true` iff every element of the tree satisfies `p`.  -/
RBTree.RBNode.all : {α : Type u_1} → (α → Bool) → RBTree.RBNode α → Bool
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G × G → A` satisfies the 2-coboundary condition if there's `x : G → A` such
that `g • x(h) - x(gh) + x(g) = f(g, h)` for all `g, h : G`.  -/
groupCohomology.IsCoboundary₂ : {G : Type u_1} → {A : Type u_2} → [Mul G] → [AddCommGroup A] → [SMul G A] → (G × G → A) → Prop
-- Mathlib.Tactic.DeriveTraversable
/-- Get `Expr`s of `FVarId`s which is not implementation details in the current context.  -/
Mathlib.Deriving.Traversable.getFVarsNotImplementationDetails : Lean.MetaM (List Lean.Expr)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_set_mk : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubsemigroup M} (h_zero : 0 ∈ s.carrier),
  ↑{ toAddSubsemigroup := s, zero_mem' := h_zero } = ↑s
-- Init.Data.Iterators.Basic
Std.Iterators.Finite.of_finitenessRelation : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (r : Std.Iterators.FinitenessRelation α m), Std.Iterators.Finite α m
-- Init.Data.List.SplitOn.Basic
/-- Tail recursive version of `splitOnP`.  -/
List.splitOnPTR : {α : Type u_1} → (α → Bool) → List α → List (List α)
-- Mathlib.RingTheory.RootsOfUnity.Complex
IsPrimitiveRoot.norm'_eq_one : ∀ {ζ : ℂ} {n : ℕ}, IsPrimitiveRoot ζ n → n ≠ 0 → ‖ζ‖ = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isExtrOn_T_real_iff : ∀ {n : ℕ},
  n ≠ 0 →
    ∀ {x : ℝ},
      x ∈ Set.Icc (-1) 1 →
        (IsExtrOn (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Set.Icc (-1) 1) x ↔
          ∃ k ≤ n, x = Real.cos (↑k * Real.pi / ↑n))
-- Mathlib.Order.SupClosed
/-- Every set in a join-semilattice generates a set closed under join.  -/
latticeClosure : {α : Type u_3} → [Lattice α] → ClosureOperator (Set α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.unitOfArray_eq_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (a : Array α),
  Std.DHashMap.Raw.Const.unitOfArray a = Std.DHashMap.Raw.Const.unitOfList a.toList
-- Mathlib.Analysis.Normed.Group.Hom
/-- Addition of normed group homs.  -/
NormedAddGroupHom.add : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → Add (NormedAddGroupHom V₁ V₂)
-- Mathlib.Data.Finset.Lattice.Basic
/-- `s ∪ t` is the set such that `a ∈ s ∪ t` iff `a ∈ s` or `a ∈ t`.  -/
Finset.instUnion : {α : Type u_1} → [DecidableEq α] → Union (Finset α)
-- Mathlib.GroupTheory.Perm.ClosureSwap
SubmonoidClass.swap_mem_trans : ∀ {α : Type u_2} [inst : DecidableEq α] {a b c : α} {C : Type u_3} [inst_1 : SetLike C (Equiv.Perm α)]
  [SubmonoidClass C (Equiv.Perm α)] (M : C), Equiv.swap a b ∈ M → Equiv.swap b c ∈ M → Equiv.swap a c ∈ M
-- Init.Data.BitVec.Lemmas
BitVec.getElem_shiftLeft' : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y : BitVec w₂} {i : ℕ} (h : i < w₁),
  (x <<< y)[i] = (!decide (i < y.toNat) && x[i - y.toNat])
-- Mathlib.Analysis.Fourier.AddCircle
AddCircle.instIsProbabilityMeasureRealHaarAddCircle : ∀ {T : ℝ} [hT : Fact (0 < T)], MeasureTheory.IsProbabilityMeasure AddCircle.haarAddCircle
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If the initial comparison map for `G` is an isomorphism, then `G` preserves initial objects.
 -/
CategoryTheory.Limits.PreservesInitial.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasInitial C]
  [inst_3 : CategoryTheory.Limits.HasInitial D] [i : CategoryTheory.IsIso (CategoryTheory.Limits.initialComparison G)],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.mem_maximalIdeal_iff_eval_one_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : IsLocalRing R]
  (x : AdicCompletion (IsLocalRing.maximalIdeal R) R),
  x ∈ IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R) ↔ ↑x 1 = 0
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        (countdown : ℕ) → Std.IterM m β → countdown > 0 ∨ Std.Iterators.Finite α m → Std.Iterators.Types.Take α m
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_merge_node : ∀ {α : Type u_1} (le : α → α → Bool) (a₁ : α) (c₁ s₁ : Batteries.PairingHeapImp.Heap α) (a₂ : α)
  (c₂ s₂ : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ s₁)
        (Batteries.PairingHeapImp.Heap.node a₂ c₂ s₂)).size =
    c₁.size + c₂.size + 2
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_trans : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] {φ ψ : G ≃ₜ+ G},
  MeasureTheory.addEquivAddHaarChar (ψ.trans φ) =
    MeasureTheory.addEquivAddHaarChar ψ * MeasureTheory.addEquivAddHaarChar φ
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Setoid.quotientKerEquivOfRightInverse` as a homeomorphism.  -/
Function.RightInverse.homeomorph : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f : C(X, Y)} → {f' : C(Y, X)} → Function.RightInverse ⇑f' ⇑f → Quotient (Setoid.ker ⇑f) ≃ₜ Y
-- Init.Control.StateCps
StateCpsT.runK_set : ∀ {σ : Type u} {m : Type u → Type v} {β : Type u} (s s' : σ) (k : PUnit.{u + 1} → σ → m β),
  (set s').runK s k = k PUnit.unit s'
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given a graph embedding, map paths to paths.  -/
SimpleGraph.Path.mapEmbedding : {V : Type u} →
  {V' : Type v} →
    {G : SimpleGraph V} → {G' : SimpleGraph V'} → (f : G ↪g G') → {u v : V} → G.Path u v → G'.Path (f u) (f v)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_ofEq_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] [inst_6 : Nonempty ↥s₂] (h : s₁ = s₂) (x : ↥s₁), ↑((AffineIsometryEquiv.ofEq s₁ s₂ h) x) = ↑x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRupCheck_insertRat : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.AssignmentsInvariant →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ),
      ((f.insertRatUnits c.negate).1.performRupCheck rupHints).2.2.1 = true →
        Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.neg (u • P) = u • W'.neg P
-- Mathlib.Data.Ordmap.Ordset
Ordnode.size_erase_of_mem : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] {x : α} {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α},
  Ordnode.Valid' a₁ t a₂ → x ∈ t → (Ordnode.erase x t).size = t.size - 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α] {l : ρ}, m.size ≤ (Std.DHashMap.Const.insertManyIfNewUnit m l).size
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.induction_on₃ : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Localization S → Localization S → Prop}
  (x y z : Localization S),
  (∀ (x y z : M × ↥S), p (Localization.mk x.1 x.2) (Localization.mk y.1 y.2) (Localization.mk z.1 z.2)) → p x y z
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_ofNat : ∀ (n : ℕ), Int8.ofBitVec (BitVec.ofNat 8 n) = Int8.ofNat n
-- Mathlib.Data.Set.Lattice.Image
Set.prod_eq_seq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = (Prod.mk '' s).seq t
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
/-- If `γ` is an integral curve at each `t ∈ s`, it is an integral curve on `s`.  -/
IsMIntegralCurveAt.isMIntegralCurveOn : ∀ {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 ∈ s, IsMIntegralCurveAt γ v t) → IsMIntegralCurveOn γ v s
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.mk : (carrier : Type u) → [str : AddGroup carrier] → AddGrpCat
-- Mathlib.Logic.Basic
imp_and_neg_imp_iff : ∀ (p q : Prop), (p → q) ∧ (¬p → q) ↔ q
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- `{v, w₁, w₂}` induces the single edge `w₁w₂`  -/
SimpleGraph.IsFiveWheelLike.isPathGraph3Compl : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsPathGraph3Compl v w₁ w₂
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonAssocCommSemiring` instance along a surjective function.  -/
Function.Surjective.nonAssocCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : NatCast S] →
                    [inst_6 : NonAssocCommSemiring R] →
                      f 0 = 0 →
                        f 1 = 1 →
                          (∀ (x y : R), f (x + y) = f x + f y) →
                            (∀ (x y : R), f (x * y) = f x * f y) →
                              (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → NonAssocCommSemiring S
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_presheaf : ∀ (R : CommRingCat), (AlgebraicGeometry.Spec R).presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).obj
-- Mathlib.GroupTheory.Coset.Basic
leftAddCoset_mem_leftAddCoset : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → a +ᵥ ↑s = ↑s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso C =
    CategoryTheory.NatIso.ofComponents
      (fun F => CategoryTheory.AddMon.mkIso (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F) ⋯ ⋯) ⋯