mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.HomogeneousLocalization.awayMapAux.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f x : A} (hx : f ∣ x),
  HomogeneousLocalization.awayMapAux✝ 𝒜 hx =
    (Localization.awayLift (algebraMap A (Localization.Away x)) f ⋯).comp
      (algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f))
-- Std.Sat.AIG.CNF
/-- Project the atom assignment out of a CNF assignment
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.projectLeftAssign : Std.Sat.AIG ℕ → (ℕ → Bool) → ℕ → Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuousAt_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {a : α},
  ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
-- Mathlib.Algebra.Colimit.Finiteness
Module.fgSystem.equiv.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq (Submodule R M)],
  Module.fgSystem.equiv R M =
    LinearEquiv.ofBijective
      (Module.DirectLimit.lift R { N // N.FG } (fun x => ↥↑x) (Module.fgSystem R M) (fun x => (↑x).subtype) ⋯) ⋯
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- An additive action is preprimitive if it is pretransitive and
the only blocks are the trivial ones  -/
AddAction.IsPreprimitive : (G : Type u_1) → (X : Type u_2) → [VAdd G X] → Prop
-- Mathlib.Data.ENNReal.Inv
ENNReal.mulLeftOrderIso_toEquiv : ∀ (a : ENNReal) (ha : IsUnit a), (a.mulLeftOrderIso ha).toEquiv = ha.unit.mulLeft
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_one_smul_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε} (c : ENNReal),
  MeasureTheory.eLpNorm f 1 (c • μ) = c * MeasureTheory.eLpNorm f 1 μ
-- Std.Http.Data.Status
/-- 300 Multiple Choices
 -/
Std.Http.Status.multipleChoices : Std.Http.Status
-- Mathlib.Data.TypeVec
TypeVec.append_prod_appendFun : ∀ {n : ℕ} {α α' β β' : TypeVec.{u} n} {φ φ' ψ ψ' : Type u} {f₀ : α.Arrow α'} {g₀ : β.Arrow β'} {f₁ : φ → φ'}
  {g₁ : ψ → ψ'}, (TypeVec.prod.map f₀ g₀ ::: Prod.map f₁ g₁) = TypeVec.prod.map (f₀ ::: f₁) (g₀ ::: g₁)
-- Mathlib.Order.Bounds.Image
BddBelow.bddBelow_image2_of_bddAbove : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)
-- Mathlib.Algebra.Central.Defs
Algebra.IsCentral.mk : ∀ {K : Type u} [inst : CommSemiring K] {D : Type v} [inst_1 : Semiring D] [inst_2 : Algebra K D],
  Subalgebra.center K D ≤ ⊥ → Algebra.IsCentral K D
-- Mathlib.Algebra.Category.Grp.Ulift
AddGrpCat.uliftFunctor_preservesLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J AddGrpCat.uliftFunctor
-- Mathlib.Algebra.Module.Injective
/-- Since every nonempty chain has a maximal element, by Zorn's lemma, there is a maximal
`extension_of i f`.  -/
Module.Baer.extensionOfMax : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) → (f : M →ₗ[R] Q) → [Fact (Function.Injective ⇑i)] → Module.Baer.ExtensionOf i f
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_range_update_sub_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_8}
  [inst_3 : DecidableEq ι] {i j : ι},
  i ≠ j →
    ∀ (v : ι → M) (r : R),
      Submodule.span R (Set.range (Function.update v j (v j - r • v i))) = Submodule.span R (Set.range v)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.rangeS_subtype : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), s.subtype.rangeS = s
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the array of values of the map.  -/
RBTree.RBMap.valuesArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Array β
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) {α : Type u_22} (s : Finset α)
  (n : α → N), m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a
-- Mathlib.RingTheory.SimpleRing.Matrix
IsSimpleRing.matrix : ∀ (ι : Type u_1) (A : Type u_2) [inst : Ring A] [inst_1 : Fintype ι] [Nonempty ι] [IsSimpleRing A],
  IsSimpleRing (Matrix ι ι A)
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.iff_isSquare_of_isInt_rat : ∀ (a : ℚ) (n : ℕ), Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → (n = 0 ↔ IsSquare a)
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.condition : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C))
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i) (CategoryTheory.Limits.chosenCoend.ι F i) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (CategoryTheory.Limits.chosenCoend.ι F j)
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot_atBot_of_monotone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → (∀ (b : β), ∃ a, f a ≤ b) → Filter.Tendsto f Filter.atBot Filter.atBot
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mul_inv_cancel : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {x : CauSeq.Completion.Cauchy abv},
  x ≠ 0 → x * x⁻¹ = 1
-- Mathlib.Algebra.Algebra.Basic
algebraMap.coe_prod : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {ι : Type u_3}
  {s : Finset ι} (a : ι → R), ↑(∏ i ∈ s, a i) = ∏ i ∈ s, ↑(a i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.cos_eq_neg_one_iff : ∀ {x : ℝ}, Real.cos x = -1 ↔ ∃ k, Real.pi + ↑k * (2 * Real.pi) = x
-- Mathlib.Topology.MetricSpace.Gluing
/-- Define a predistance on `X ⊕ Y`, for which `Φ p` and `Ψ p` are at distance `ε`  -/
Metric.glueDist : {X : Type u} →
  {Y : Type v} → {Z : Type w} → [MetricSpace X] → [MetricSpace Y] → (Z → X) → (Z → Y) → ℝ → X ⊕ Y → X ⊕ Y → ℝ
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The center of isomorphic (not necessarily unital or associative) rings are isomorphic.  -/
NonUnitalSubring.centerCongr : {R : Type u} →
  [inst : NonUnitalNonAssocRing R] →
    {S : Type u_1} →
      [inst_1 : NonUnitalNonAssocRing S] → R ≃+* S → ↥(NonUnitalSubring.center R) ≃+* ↥(NonUnitalSubring.center S)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_iff_omega0_dvd : ∀ {a : Ordinal.{u_4}}, Order.IsSuccLimit a ↔ a ≠ 0 ∧ Ordinal.omega0 ∣ a
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_neg : ∀ (b : BitVec 64), { toBitVec := -b } = -{ toBitVec := b }
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivAt.neg` -/
HasDerivAt.fun_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → HasDerivAt (fun i => -f i) (-f') x
-- Init.Data.Array.Lemmas
Array.sum_empty : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α], #[].sum = 0
-- Mathlib.Analysis.Seminorm
Seminorm.smul_sup : ∀ {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  [inst_3 : SMul R ℝ] [inst_4 : SMul R NNReal] [inst_5 : IsScalarTower R NNReal ℝ] (r : R) (p q : Seminorm 𝕜 E),
  r • (p ⊔ q) = r • p ⊔ r • q
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.BoundaryGE.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (j : ι),
  e.BoundaryGE j = (c'.Rel (c'.prev (e.f j)) (e.f j) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j))
-- Init.Tactics
/-- Like `rcases`, but operating on stateful `Std.Do.SPred` goals.
Example: Given a goal `h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R`,
`mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩` will yield two goals:
`(hq : Q, hqr : Q → R) ⊢ₛ R` and `(hr : R) ⊢ₛ R`.

That is, `mcases h with pat` has the following semantics, based on `pat`:
* `pat=□h'` renames `h` to `h'` in the stateful context, regardless of whether `h` is pure
* `pat=⌜h'⌝` introduces `h' : φ`  to the pure local context if `h : ⌜φ⌝`
  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`)
* `pat=h'` is like `pat=⌜h'⌝` if `h` is pure
  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`), otherwise it is like `pat=□h'`.
* `pat=_` renames `h` to an inaccessible name
* `pat=-` discards `h`
* `⟨pat₁, pat₂⟩` matches on conjunctions and existential quantifiers and recurses via
  `pat₁` and `pat₂`.
* `⟨pat₁ | pat₂⟩` matches on disjunctions, matching the left alternative via `pat₁` and the right
  alternative via `pat₂`.
 -/
Lean.Parser.Tactic.mcasesMacro : Lean.ParserDescr
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box_index_tag_eq_self : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] {B I : BoxIntegral.Box ι},
  I ∈ (BoxIntegral.unitPartition.prepartition n B).boxes →
    BoxIntegral.unitPartition.box n
        (BoxIntegral.unitPartition.index n ((BoxIntegral.unitPartition.prepartition n B).tag I)) =
      I
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2ComputableInPolyTime : Inhabited (Turing.TM2ComputableInPolyTime Computability.encodeBool Computability.encodeBool id)
-- Mathlib.RingTheory.Localization.Defs
/-- If `CommSemiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`.  -/
IsLocalization.map_comp_map : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T) {A : Type u_5} [inst_8 : CommSemiring A] {U : Submonoid A} {W : Type u_6}
  [inst_9 : CommSemiring W] [inst_10 : Algebra A W] [inst_11 : IsLocalization U W] {l : P →+* A}
  (hl : T ≤ Submonoid.comap l U),
  (IsLocalization.map W l hl).comp (IsLocalization.map Q g hy) = IsLocalization.map W (l.comp g) ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {l : List ((a : α) × β a)},
  l.isEmpty = true → Std.Internal.List.maxKey? l = none
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `x ↦ x / a` as an order isomorphism.  -/
OrderIso.divRight : {α : Type u} → [inst : Group α] → [inst_1 : LE α] → [MulRightMono α] → α → α ≃o α
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.nsmul_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x : R}, x ∈ s → ∀ (n : ℕ), n • x ∈ s
-- Mathlib.Data.Matrix.Diagonal
Matrix.instNatCastOfZero : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [Zero α] → [NatCast α] → NatCast (Matrix n n α)
-- Lean.Parser.Basic
/-- Parses a string quotation after a `\`.
- `isQuotable` determines which characters are valid escapes
- `inString` enables features that are only valid within strings,
  in particular `"\" newline whitespace*` gaps.
 -/
Lean.Parser.quotedCharCoreFn : (Char → Bool) → Bool → Lean.Parser.ParserFn
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsSmallJ : CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} SSet.modelCategoryQuillen.J
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.preimage_image_mk_eq_add : ∀ {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α),
  QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' s = s + ↑N
-- Init.Data.Vector.Perm
Vector.perm_iff_toList_perm : ∀ {α : Type u_1} {n : ℕ} {as bs : Vector α n}, as.Perm bs ↔ as.toList.Perm bs.toList
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- If this relation is well-founded, then `IterM.toArray`, `IterM.toList` and `IterM.toListRev` are
guaranteed to finish after finitely many steps. If all of the iterator's steps terminate
individually, `IterM.toArray` is guaranteed to terminate.
 -/
Std.IterM.toArray.RecursionRel : {α β : Type w} →
  {m : Type w → Type w'} →
    [Std.Iterator α m β] → {γ : Type w} → (_ : Std.IterM m β) ×' Array γ → (_ : Std.IterM m β) ×' Array γ → Prop
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {x y : E.Hom F}, x.s₀ = y.s₀ → x.h₀ ≍ y.h₀ → x = y
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- Let `S` be a short complex in an abelian category. Let `kf` be a
limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`.
Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`.
This is the left homology data expressing `H` as the homology of `S`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        {kf : CategoryTheory.Limits.KernelFork S.g} →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} →
            CategoryTheory.Limits.IsLimit kf →
              CategoryTheory.Limits.IsColimit cc →
                {H : C} →
                  {π : kf.pt ⟶ H} →
                    {ι : H ⟶ cc.pt} →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
                            (CategoryTheory.Limits.Cofork.π cc) =
                          CategoryTheory.CategoryStruct.comp π ι →
                        [CategoryTheory.Epi π] → [CategoryTheory.Mono ι] → S.LeftHomologyData
-- Mathlib.Data.Set.Lattice
Set.iInter_eq_univ : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α}, ⋂ i, s i = Set.univ ↔ ∀ (i : ι), s i = Set.univ
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.getFVarId : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.FVarId
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_univ : ∀ {α : Type u_2} [inst : Inv α], Set.univ⁻¹ = Set.univ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.dropPrefix?_string_empty : ∀ {s : String.Slice}, s.dropPrefix? "" = some s
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.condExp_ae_le : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Supermartingale f ℱ μ → ∀ {i j : ι}, i ≤ j → μ[f j | ↑ℱ i] ≤ᵐ[μ] f i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The singleton operation as an `AddHom`.  -/
Set.singletonAddHom : {α : Type u_2} → [inst : Add α] → α →ₙ+ Set α
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- The cardinality of an algebraically closed `R`-algebra is less than or equal to
the maximum of the cardinality of `R`, the cardinality of a transcendence basis and
`ℵ₀`

A less-universe polymorphic, but simpler statement of
`IsAlgClosed.cardinal_le_max_transcendence_basis`  -/
IsAlgClosed.cardinal_le_max_transcendence_basis' : ∀ {R : Type u} [inst : CommRing R] {K' : Type u} [inst_1 : Field K'] [inst_2 : Algebra R K'] [IsAlgClosed K']
  {ι' : Type u} (v' : ι' → K'),
  IsTranscendenceBasis R v' → Cardinal.mk K' ≤ max (max (Cardinal.mk R) (Cardinal.mk ι')) Cardinal.aleph0
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.brecOn.go : {C : Type u} →
  {motive : CategoryTheory.FreeMonoidalCategory C → Sort u_1} →
    (t : CategoryTheory.FreeMonoidalCategory C) →
      ((t : CategoryTheory.FreeMonoidalCategory C) → CategoryTheory.FreeMonoidalCategory.below t → motive t) →
        motive t ×' CategoryTheory.FreeMonoidalCategory.below t
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.filterM.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [inst_1 : Monad n]
  [inst_2 : MonadAttach n] [inst_3 : MonadLiftT m n] (f : β → n (ULift.{w, 0} Bool)) (it : Std.IterM m β),
  Std.IterM.filterM f it =
    Std.IterM.filterMapWithPostcondition
      (fun b =>
        Std.Iterators.PostconditionT.map (fun x => if x.down = true then some b else none)
          (Std.Iterators.PostconditionT.attachLift (f b)))
      it
-- Init.Data.Dyadic.Basic
Dyadic.add.eq_1 : ∀ (y : Dyadic), Dyadic.zero.add y = y
-- Std.Http.Internal.ChunkedBuffer
/-- An empty `ChunkedBuffer`.
 -/
Std.Http.Internal.ChunkedBuffer.empty : Std.Http.Internal.ChunkedBuffer
-- Mathlib.Algebra.Group.Subgroup.Finite
AddMonoidHom.decidableMemRange : {G : Type u_1} →
  [inst : AddGroup G] →
    {N : Type u_3} →
      [inst_1 : AddGroup N] → (f : G →+ N) → [Fintype G] → [DecidableEq N] → DecidablePred fun x => x ∈ f.range
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_vsub_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (S : Set (Set β)) (t : Set β), ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t
-- Mathlib.Algebra.Order.SuccPred
Order.lt_one_iff : ∀ {α : Type u_1} {x : α} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α]
  [NeZero 1], x < 1 ↔ x = 0
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go.eq_def : ∀ (q a a_1 : ℕ),
  LucasLehmer.norm_num_ext.sModNatTR.go✝ q a a_1 =
    match a, a_1 with
    | 0, acc => acc
    | n.succ, acc => LucasLehmer.norm_num_ext.sModNatTR.go✝ q n ((acc ^ 2 + (q - 2)) % q)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.instDecompositionMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α], DecompositionMonoid α
-- Init.Data.UInt.Lemmas
UInt64.mod_zero : ∀ {a : UInt64}, a % 0 = a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  {Z : ModuleCat k} (h : ModuleCat.of k ↥(groupHomology.cycles₁ C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupHomology.mapCycles₁ (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ (MonoidHom.id G) φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ (MonoidHom.id G) ψ) h)
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
/-- The abelian image in a functor category can be calculated componentwise.  -/
CategoryTheory.Abelian.FunctorCategory.imageObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type w} →
      [inst_1 : CategoryTheory.Category.{z, w} D] →
        [inst_2 : CategoryTheory.Abelian D] →
          {F G : CategoryTheory.Functor C D} →
            (α : F ⟶ G) → (X : C) → (CategoryTheory.Abelian.image α).obj X ≅ CategoryTheory.Abelian.image (α.app X)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.length_bypass_le_length`. -/
SimpleGraph.Walk.length_bypass_le : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.length ≤ p.length
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.coe_withBotCongr : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), ⇑e.withBotCongr = WithBot.map ⇑e
-- Std.Internal.UV.TCP
/-- Enables TCP keep-alive for a socket. If delay is less than 1 then UV_EINVAL is returned.
 -/
Std.Internal.UV.TCP.Socket.keepAlive : Std.Internal.UV.TCP.Socket → Int8 → UInt32 → IO Unit
-- Init.Data.Float.Model.Format.Valid
/-- Predicate asserting that the bit representation of a float is valid according to the given
format. By 'valid' we mean that `NaN` is encoded using the canonical `NaN`.
 -/
Float.Model.Format.Valid : (spec : Float.Model.Format) → BitVec spec.numBits → Prop
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.mk : Lean.MVarId → Std.HashSet Lean.MVarId → Aesop.GoalWithMVars
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_erase_right : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b : α),
  (Finset.Ioc a b).erase b = Finset.Ioo a b
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_preΨ' : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℕ),
  (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.pow_mul_m_le_card_part : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {u : Finset α},
  P.IsEquipartition →
    u ∈ P.parts → 4 ^ P.parts.card * ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) ≤ ↑u.card
-- Lean.Language.Basic
Lean.Language.SnapshotTask.instInhabitedReportingRange : Inhabited Lean.Language.SnapshotTask.ReportingRange
-- Mathlib.Tactic.Algebra.Basic
/-- Evaluates a numeric literal in the algebra `A` by lifting it through the base ring `R`.  -/
Mathlib.Tactic.Algebra.evalCast : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            {a : Q(«$A»)} →
              Mathlib.Tactic.Algebra.Cache q(«$sR») →
                Mathlib.Tactic.Algebra.Cache q(«$sA») →
                  Mathlib.Meta.NormNum.Result a →
                    Option (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Algebra.ExSum sAlg) q(«$a»))
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.primeFactorsPiBij_surj : ∀ (d n : ℕ),
  Squarefree n →
    ∀ t ∈ d.finMulAntidiag n,
      ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => Finset.univ), Nat.primeFactorsPiBij✝ d n g hg = t
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitCoconeComp_cocone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.ColimitCocone G),
  (CategoryTheory.Functor.Final.colimitCoconeComp F t).cocone = CategoryTheory.Limits.Cocone.whisker F t.cocone
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.ext_iff : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {f g : ContIntertwiningMap π₁ π₂},
  f = g ↔ f.toContinuousLinearMap = g.toContinuousLinearMap
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.trans : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
-- Init.Core
PUnit.ext : ∀ (a b : PUnit.{u_1}), a = b