mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k} {h : k ∈ m.modify k f}, (m.modify k f).get k h = f (m.get k ⋯)
-- Mathlib.Analysis.Real.Cardinality
/-- `cantorFunction c (f : ℕ → Bool)` is `Σ n, f n * c ^ n`, where `true` is interpreted as `1` and
`false` is interpreted as `0`. It is implemented using `cantorFunctionAux`.  -/
Cardinal.cantorFunction : ℝ → (ℕ → Bool) → ℝ
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_sum : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (p : Polynomial R) (f : ℕ → R → Polynomial (Polynomial R)),
  Polynomial.evalEval x y (p.sum f) = p.sum fun n a => Polynomial.evalEval x y (f n a)
-- Mathlib.Probability.Density
MeasureTheory.pdf.hasFiniteIntegral_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsFiniteMeasure ℙ]
  {f : ℝ → ℝ} {g : ℝ → ENNReal},
  MeasureTheory.pdf X ℙ MeasureTheory.volume =ᵐ[MeasureTheory.volume] g →
    ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤ →
      MeasureTheory.HasFiniteIntegral (fun x => f x * (MeasureTheory.pdf X ℙ MeasureTheory.volume x).toReal)
        MeasureTheory.volume
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.g₃.eq_1 : ∀ (L : PeriodPair), L.g₃ = 140 * L.G 6
-- Batteries.Data.PairingHeap
/-- Amortized `O(log n)`. Get the tail of the pairing heap after removing the minimum element.  -/
Batteries.PairingHeapImp.Heap.tail? : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Option (Batteries.PairingHeapImp.Heap α)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.mul_compat_left : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X}
  (a_1 : FreeAlgebra.Rel R X a b), FreeAlgebra.Rel.below a_1 → motive a b a_1 → FreeAlgebra.Rel.below ⋯
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_iUnion : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Sort u_1} (s : ι → Set R),
  Subring.closure (⋃ i, s i) = ⨆ i, Subring.closure (s i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.DTreeMap.foldlM f init t = Array.foldlM (fun a b => f a b.1 b.2) init (Std.DTreeMap.Const.toArray t)
-- Mathlib.Algebra.Group.Units.Defs
Units.val_inv_eq_inv_val : ∀ {α : Type u} [inst : DivisionMonoid α] (u : αˣ), ↑u⁻¹ = (↑u)⁻¹
-- Mathlib.Data.List.Sections
List.mem_sections : ∀ {α : Type u_1} {L : List (List α)} {f : List α}, f ∈ L.sections ↔ List.Forall₂ (fun x1 x2 => x1 ∈ x2) f L
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd.eq_1 : ∀ {α : Type u_3} [inst : Monoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute),
  s.noncommProd comm = Multiset.noncommFold (fun x1 x2 => x1 * x2) s comm 1
-- Mathlib.RingTheory.PowerSeries.Ideal
/-- If `R` is principal then `R⟦X⟧` is a `UniqueFactorizationMonoid`. Note that `R` being a
`UniqueFactorizationMonoid` is not enough.  -/
PowerSeries.instUniqueFactorizationMonoidOfIsPrincipalIdealRingOfIsDomain : ∀ {R : Type u_1} [inst : CommRing R] [IsPrincipalIdealRing R] [IsDomain R], UniqueFactorizationMonoid (PowerSeries R)
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
CochainComplex.instFaithfulIntSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ), (CochainComplex.singleFunctor C n).Faithful
-- Mathlib.CategoryTheory.Action.Limits
Action.instSMulNatHom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Preadditive V] → {X Y : Action V G} → SMul ℕ (X ⟶ Y)
-- Mathlib.NumberTheory.ZetaValues
hasSum_zeta_four : HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90)
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instDivisionSemiring : {α : Type u_1} → [DivisionSemiring α] → DivisionSemiring αᵐᵒᵖ
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).obj₂ = (X₁ ⊞ X₂)
-- Mathlib.Logic.Function.Basic
/-- There is no surjection from `α : Type u` into `Type (max u v)`. This theorem
demonstrates why `Type : Type` would be inconsistent in Lean.  -/
Function.not_surjective_Type : ∀ {α : Type u} (f : α → Type (max u v)), ¬Function.Surjective f
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The "unlifted" version of addition in the colimit. To add two dependent pairs
`⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂`
(given by `IsFiltered.max`) and add them there.  -/
AddMonCat.FilteredColimits.colimitAddAux : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [CategoryTheory.IsFiltered J] → (j : J) × ↑(F.obj j) → (j : J) × ↑(F.obj j) → AddMonCat.FilteredColimits.M F
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.mk.inj : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_4} {inst : CommRing R} {inst_1 : CommRing A₁} {inst_2 : CommRing A₂}
  {inst_3 : Algebra R A₁} {inst_4 : Algebra R A₂} {σ : A₁ →ₐ[R] A₂} {L₁ : Type u_8} {L₂ : Type u_9}
  {inst_5 : LieRing L₁} {inst_6 : Module A₁ L₁} {inst_7 : LieRingModule L₁ A₁} {inst_8 : LieAlgebra R L₁}
  {inst_9 : LieRing L₂} {inst_10 : Module A₂ L₂} {inst_11 : LieRingModule L₂ A₂} {inst_12 : LieAlgebra R L₂}
  {toLieHom : L₁ →ₗ⁅R⁆ L₂} {map_smul_apply' : ∀ (a : A₁) (x : L₁), toLieHom (a • x) = σ a • toLieHom x}
  {apply_lie' : ∀ (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅toLieHom x, σ a⁆} {toLieHom_1 : L₁ →ₗ⁅R⁆ L₂}
  {map_smul_apply'_1 : ∀ (a : A₁) (x : L₁), toLieHom_1 (a • x) = σ a • toLieHom_1 x}
  {apply_lie'_1 : ∀ (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅toLieHom_1 x, σ a⁆},
  { toLieHom := toLieHom, map_smul_apply' := map_smul_apply', apply_lie' := apply_lie' } =
      { toLieHom := toLieHom_1, map_smul_apply' := map_smul_apply'_1, apply_lie' := apply_lie'_1 } →
    toLieHom = toLieHom_1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] (f : α → M) (l : FreeAddMonoid α),
  (FreeAddMonoid.lift f) l = (List.map f (FreeAddMonoid.toList l)).sum
-- Mathlib.Algebra.Group.Basic
sub_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b + c = a - (b - c)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.codeBlock.codeFrom : Lean.Doc.Parser.BlockCtxt → ℕ → ℕ → Lean.Parser.ParserFn
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_even : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.ψ (2 * m) * W.ψ₂ = W.ψ (m - 1) ^ 2 * W.ψ m * W.ψ (m + 2) - W.ψ (m - 2) * W.ψ m * W.ψ (m + 1) ^ 2
-- Mathlib.Order.Filter.Basic
Filter.mem_sdiff_iff_union : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f \ g ↔ ∀ t ∈ g, s ∪ t ∈ f
-- Std.Http.Data.Body.Empty
Std.Http.Body.Empty.noConfusionType : Sort v✝ → Std.Http.Body.Empty → Std.Http.Body.Empty → Sort v✝
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_insertNth : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (a : α p) (f : (i : Fin n) → α (p.succAbove i)),
  p.removeNth (p.insertNth a f) = f
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_union : ∀ {V : Type u} (s t : Set (Sym2 V)),
  SimpleGraph.fromEdgeSet (s ∪ t) = SimpleGraph.fromEdgeSet s ⊔ SimpleGraph.fromEdgeSet t
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.instIsRelationalEmpty : FirstOrder.Language.empty.IsRelational
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.natCast_card_filter : ∀ {ι : Type u_1} {R : Type u_4} [inst : AddCommMonoidWithOne R] (p : ι → Prop) [inst_1 : DecidablePred p]
  (s : Finset ι), ↑{x ∈ s | p x}.card = ∑ a ∈ s, if p a then 1 else 0
-- Lean.Server.Utils
_private.Lean.Server.Utils.0.Lean.Server.externalUriToName : Lean.Lsp.DocumentUri → Lean.Name
-- Mathlib.NumberTheory.ADEInequality
/-- `E6 := {2,3,3}` is a `Multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

This solution is related to the Dynkin diagrams $E_6$.  -/
ADEInequality.E6 : Multiset ℕ+
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ofLeftInverse_apply : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {g : N →+ G}
  (h : Function.LeftInverse ⇑g ⇑f) (x : G), ↑((AddMonoidHom.ofLeftInverse h) x) = f x
-- Mathlib.Data.Set.Countable
Set.Countable.preimage_of_injOn : ∀ {α : Type u} {β : Type v} {s : Set β}, s.Countable → ∀ {f : α → β}, Set.InjOn f (f ⁻¹' s) → (f ⁻¹' s).Countable
-- Mathlib.Computability.Partrec
Computable.unpair : Computable Nat.unpair
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.elementarilyEquivalent_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- `IteratorLoop α m` provides efficient implementations of loop-based consumers for `α`-based
iterators. The basis is a `ForIn`-style loop construct.

Its behavior for well-founded loops is fully characterized by the `LawfulIteratorLoop` type class.

This class is experimental and users of the iterator API should not explicitly depend on it.
They can, however, assume that consumers that require an instance will work for all iterators
provided by the standard library.
 -/
Std.IteratorLoop : (α : Type w) →
  (m : Type w → Type w') →
    {β : Type w} → [Std.Iterator α m β] → (Type x → Type x') → Type (max (max (max (w + 1) w') (x + 1)) x')
-- Lean.Compiler.InitAttr
Lean.isIOUnitInitFn : Lean.Environment → Lean.Name → Bool
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.lift_apply_apply : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G) (a : ι → H)
  (x : G), (b.lift a) x = (FreeGroup.lift a) (b.repr x)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (x : M), (TensorProduct.quotTensorEquivQuotSMul M I) (1 ⊗ₜ[R] x) = Submodule.Quotient.mk x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldl_eq_foldl_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.DTreeMap.foldl (fun d a x => f d a) init t = Array.foldl f init t.keysArray
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ici_subset_Ici : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], Finset.Ici a ⊆ Finset.Ici b ↔ b ≤ a
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.coe_pointwise_vadd : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (v : V) (s : AffineSubspace k P), ↑(v +ᵥ s) = v +ᵥ ↑s
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.cyclesMap'_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.cyclesMap' φ h₁.left h₂.left = γ.left.φK
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.bilinearComp_apply_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X Y Z : C) (a b c : ℕ) (h : a + b = c) (α : CategoryTheory.Abelian.Ext X Y a)
  (β : CategoryTheory.Abelian.Ext Y Z b), ((CategoryTheory.Abelian.Ext.bilinearComp X Y Z a b c h) α) β = α.comp β h
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- The morphism `t : 1 ⟶ Ω` which picks out the maximal sieve  -/
CategoryTheory.Sheaf.truth : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      CategoryTheory.Sheaf.terminal J CategoryTheory.Limits.Types.isTerminalPUnit ⟶ CategoryTheory.Sheaf.Ω J
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.one : ∀ (R : Type u_1) [inst : MulOneClass R] [inst_1 : StarMul R], IsSelfAdjoint 1
-- Lean.Meta.Tactic.Grind.Action
/-- ``TSyntax `grind`` => ``TSyntax `Lean.Parser.Tactic.Grind.grindStep``  -/
Lean.Meta.Grind.Action.mkGrindStep : Lean.Meta.Grind.TGrind → Lean.Meta.Grind.TGrindStep
-- Mathlib.Data.Setoid.Partition
/-- The equivalence relation associated to an indexed partition. Two
elements are equivalent if they belong to the same set of the partition.  -/
IndexedPartition.setoid : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → IndexedPartition s → Setoid α
-- Mathlib.Algebra.Order.Hom.Basic
AddGroupSeminormClass.toZeroHomClass : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupSeminormClass F α β], ZeroHomClass F α β
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.union.injEq : ∀ (leanTypeName : Lean.Name) (types : Array Lean.IR.IRType) (leanTypeName_1 : Lean.Name)
  (types_1 : Array Lean.IR.IRType),
  (Lean.IR.IRType.union leanTypeName types = Lean.IR.IRType.union leanTypeName_1 types_1) =
    (leanTypeName = leanTypeName_1 ∧ types = types_1)
-- Init.Prelude
instLEFin : {n : ℕ} → LE (Fin n)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.instCompOfCommShift : {C : Type u_1} →
  {D : Type u_2} →
    {A : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
            {π : CategoryTheory.Functor C D} →
              {H : CategoryTheory.Functor D A} →
                (M : Type u_4) →
                  [inst_3 : AddMonoid M] →
                    [inst_4 : CategoryTheory.HasShift C M] →
                      [inst_5 : CategoryTheory.HasShift D M] →
                        [π.CommShift M] → [H.ShiftSequence M] → (π.comp H).ShiftSequence M
-- Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
/-- Let `e : M ≃ N` be an additive isomorphism (therefore a `ℤ`-linear equiv).
Then an alternative way to compute the cardinality of the quotient `M ⧸ N` is given by taking
the determinant of `e`.
See `natAbs_det_basis_change` for a more familiar formulation of this result.  -/
Submodule.natAbs_det_equiv : ∀ {M : Type u_1} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) {E : Type u_2}
  [inst_3 : EquivLike E M ↥N] [inst_4 : AddEquivClass E M ↥N] (e : E),
  (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.map_zero : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂}, IsLinearMap R f → f 0 = 0
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : CommRing R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : LinearOrder α] [Invertible M],
  M.BlockTriangular b →
    ∀ (k : α), ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
-- Mathlib.Algebra.Order.Archimedean.Basic
WithZero.instMulArchimedean : ∀ (M : Type u_5) [inst : CommMonoid M] [inst_1 : PartialOrder M] [MulArchimedean M], MulArchimedean (WithZero M)
-- Mathlib.Order.SuccPred.Basic
Order.succ_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : OrderTop α], Order.succ ⊤ = ⊤
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.δ_eq_two : EisensteinSeries.δ✝ ![0, -1] = 2
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_incidenceSet : ∀ {V : Type u} {G H : SimpleGraph V}, (∀ (v : V), Disjoint (G.incidenceSet v) (H.incidenceSet v)) ↔ Disjoint G H
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- A Lipschitz function is continuous.  -/
LipschitzWith.continuous : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → Continuous f
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_add_right_of_ge' : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atBot → (∀ᶠ (x : α) in l, g x ≤ C) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_sup : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R), (I ⊔ J).radical = (I.radical ⊔ J.radical).radical
-- Mathlib.Algebra.Notation.Defs
ite_add : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a b c : α),
  (if P then a else b) + c = if P then a + c else b + c
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.forkMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X),
  CategoryTheory.Equalizer.forkMap P R = CategoryTheory.Limits.Pi.lift fun f => P.map (↑f.snd).op
-- Mathlib.Topology.Homotopy.Path
/-- The composition of path homotopy classes. This is `Path.trans` descended to the quotient.  -/
Path.Homotopic.Quotient.trans : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ x₂ : X} → Path.Homotopic.Quotient x₀ x₁ → Path.Homotopic.Quotient x₁ x₂ → Path.Homotopic.Quotient x₀ x₂
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_self : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, p.Monic → p %ₘ p = 0
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_one_left : ∀ {α : Type u_1} (f : Equiv.Perm α), Equiv.Perm.Disjoint 1 f
-- Mathlib.Order.Hom.Basic
/-- Converts a `RelIso (<) (<)` into an `OrderIso`.  -/
OrderIso.ofRelIsoLT : {α : Type u_6} →
  {β : Type u_7} →
    [inst : PartialOrder α] → [inst_1 : PartialOrder β] → ((fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2) → α ≃o β
-- Mathlib.Logic.Equiv.Sum
Equiv.sumAssoc_symm_apply_inr_inr : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ), (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
-- Lean.Meta.MkIffOfInductiveProp
/-- Generates existential form of a prop-valued inductive type and proves the equivalence.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.mkIffOfInductivePropImpl : Lean.InductiveVal → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.free_map : ∀ (R : Type u) [inst : CommRing R] {X Y : Type u} (f : X ⟶ Y),
  (AlgCat.free R).map f =
    AlgCat.ofHom ((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)))
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.eq_one_iff_conductor_eq_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} [NeZero n], χ = 1 ↔ χ.conductor = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Init.Data.List.Lemmas
List.any_filter : ∀ {α : Type u_1} {l : List α} {p q : α → Bool}, (List.filter p l).any q = l.any fun a => p a && q a
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalence_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂),
  (HomologicalComplex₂.flipEquivalence C c₁ c₂).inverse = HomologicalComplex₂.flipFunctor C c₂ c₁
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_neg_eq : ∀ {R : Type u_1} [inst : CommRing R] (a b : Polynomial R), -a.wronskian b = b.wronskian a
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_5 : ∀ (motive : Lean.Expr → Sort u_1) (declName : Lean.Name) (us : List Lean.Level)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.const declName us with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_5 declName us
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.

This function is deprecated. Instead of `it.allowNontermination.findSomeM?`, use `it.findSomeM?`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Std.Iter.Partial.findSomeM? : {α β : Type w} →
  {γ : Type x} →
    {m : Type x → Type w'} →
      [Monad m] →
        [inst : Std.Iterator α Id β] →
          [Std.IteratorLoop α Id m] → Std.Iter.Partial β → (β → m (Option γ)) → m (Option γ)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R S T : CategoryTheory.CommMon C} (f : R ⟶ S) (g : S ⟶ T),
  (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom