mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.shift_counit_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (Y : D) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y)) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app (G.obj Y))
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Functor.commShiftIso G a).inv.app Y))
        (CategoryTheory.CategoryStruct.comp (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj Y)) h))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_add_right_eq_map : ∀ {m n : ℤ}, (m<...m + 1 + n).toArray = Array.map (fun x => x + m + 1) (0...n).toArray
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_apply_prime_pow : ∀ {p k : ℕ}, Nat.Prime p → k ≠ 0 → ArithmeticFunction.cardDistinctFactors (p ^ k) = 1
-- Init.Data.Nat.Basic
Nat.ne_add_one : ∀ (n : ℕ), n ≠ n + 1
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.quasiIso_descShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)},
  S.ShortExact → QuasiIso (CochainComplex.mappingCone.descShortComplex S)
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function is non-negative.
 -/
ValueDistribution.logCounting_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {r : ℝ} {f : 𝕜 → E} {e : WithTop E},
  1 ≤ r → 0 ≤ ValueDistribution.logCounting f e r
-- Mathlib.RingTheory.Ideal.Operations
Ideal.eq_span_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] {x : R} (I J : Ideal R),
  I = Ideal.span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
-- Batteries.Data.Fin.Coding
Fin.getRepr_equiv : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (x : Fin n), s (Fin.getRepr s x) x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.iterOfTree : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Std.Iter ((a : α) × β a)
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction_def_odd : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ →
    ∀ (s : ℂ),
      ZMod.completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.completedHurwitzZetaOdd (ZMod.toAddCircle j) s
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∐ I.left ⟶ ∐ I.right` via `I.snd` for colimiting cofans.  -/
CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (d : CategoryTheory.Limits.Cofan I.right) → CategoryTheory.Limits.IsColimit c → (c.pt ⟶ d.pt)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.remainingBytes.match_1.eq_1 : ∀ (motive : String.Legacy.Iterator → Sort u_1) (s : String) (i : String.Pos.Raw)
  (h_1 : (s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }),
  (match { s := s, i := i } with
    | { s := s, i := i } => h_1 s i) =
    h_1 s i
-- Mathlib.CategoryTheory.Opposites
/-- The isomorphism between `F.rightOp.leftOp` and `F`.  -/
CategoryTheory.Functor.rightOpLeftOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor Cᵒᵖ D) → F.rightOp.leftOp ≅ F
-- Mathlib.Data.Sym.NatCard
/-- Type **stars and bars** for the case `n = 2`.  -/
Sym2.natCard : ∀ (α : Type u_1), Nat.card (Sym2 α) = (Nat.card α + 1).choose 2
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.unit_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.unit R).val = PresheafOfModules.unit R.obj
-- Mathlib.Data.Nat.DvdSequence
Nat.IsStrongDvdSequence.isDvdSequence : ∀ {f : ℕ → ℕ}, Nat.IsStrongDvdSequence f → IsDvdSequence f
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- A generalization of the fixed point lemma for normal functions: any family of normal functions
has an unbounded set of common fixed points.  -/
Ordinal.not_bddAbove_fp_family : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) → ¬BddAbove (⋂ i, Function.fixedPoints (f i))
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrInvMem.mk : ∀ {S : Type u_3} {G : Type u_4} [inst : Inv G] [inst_1 : SetLike S G] {s : S},
  (∀ (a : G), a ∈ s ∨ a⁻¹ ∈ s) → HasMemOrInvMem s
-- Mathlib.Algebra.Group.ULift
ULift.vadd : {α : Type u} → {β : Type v} → [VAdd β α] → VAdd β (ULift.{u_1, u} α)
-- Mathlib.Order.Lattice
Pi.instSemilatticeSup : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → SemilatticeSup (α' i)] → SemilatticeSup ((i : ι) → α' i)
-- Mathlib.Data.Countable.Basic
Option.instCountable : ∀ {α : Type u} [Countable α], Countable (Option α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    ∀ {P' X' Y' Z' : C} {fst' : P' ⟶ X'} {snd' : P' ⟶ Y'} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (e₁ : P ≅ P') (e₂ : X ≅ X')
      (e₃ : Y ≅ Y') (e₄ : Z ≅ Z'),
      CategoryTheory.CategoryStruct.comp fst e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom fst' →
        CategoryTheory.CategoryStruct.comp snd e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom snd' →
          CategoryTheory.CategoryStruct.comp f e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom f' →
            CategoryTheory.CategoryStruct.comp g e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom g' →
              CategoryTheory.IsPullback fst' snd' f' g'
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_3.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (lls : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_3 : (x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x),
  (match Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_1 lls k v l r lrs lrk lrv lrl lrr
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l r
    | Std.DTreeMap.Internal.Impl.leaf, x => h_3 x) =
    h_3 x
-- Init.Tactics
/-- `trace msg` displays `msg` in the info view. 

Extensions:

 * `msg` can be a literal string, or a term that evaluates to a string. -/
Lean.Parser.Tactic.traceMessage : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.mergeWith : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {f : (a : α) → x a → x a → x a} {h : t₁.Balanced}
  [inst_1 : Std.LawfulEqOrd α] (a : t₁.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t₁ a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_le_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N}
  {J : AddSubgroup (G × N)},
  H.prod K ≤ J ↔ AddSubgroup.map (AddMonoidHom.inl G N) H ≤ J ∧ AddSubgroup.map (AddMonoidHom.inr G N) K ≤ J
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- Complementary statement to `proximity_top_eq_circleAverage_circleAverage`, providing circle
integrability of the integrand.
 -/
ValueDistribution.circleIntegrable_circleAverage_log_norm_sub : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f → CircleIntegrable (fun a => Real.circleAverage (fun x => Real.log ‖f x - a‖) 0 R) 0 1
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ker_naive : ∀ {R : Type u} [inst : CommRing R] {σ : Type u_8} {I : Ideal (MvPolynomial σ R)}
  (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x),
  (Algebra.Generators.naive s hs).ker = I
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The bicategory that has the same objects as a bicategory `B`, in which `1`-morphisms
are adjunctions (in the same direction as the left adjoints),
and `2`-morphisms are tuples of mate maps between the left and right
adjoints (where the map between right adjoints is in the opposite direction).
 -/
CategoryTheory.Bicategory.Adj : (B : Type u) → [CategoryTheory.Bicategory B] → Type u
-- Mathlib.Order.Hom.WithTopBot
InfHom.withBot'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β]
  (f : InfHom α β) (a : WithBot α), f.withBot' a = Option.elim a ⊥ ⇑f
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.not_irreducible_of_aleph0_le : ∀ {a : Cardinal.{u}}, Cardinal.aleph0 ≤ a → ¬Irreducible a
-- Mathlib.Order.UpperLower.CompleteLattice
/-- The complement of an upper set as a lower set.  -/
UpperSet.compl : {α : Type u_1} → [inst : LE α] → UpperSet α → LowerSet α
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.pred_eq_of_covBy`.

---

See also `Order.pred_le_of_wcovBy`.  -/
CovBy.pred_eq : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α}, b ⋖ a → Order.pred a = b
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_of_forks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {cg : CategoryTheory.Limits.KernelFork S.g}
  (hg : CategoryTheory.Limits.IsLimit cg) {cf : CategoryTheory.Limits.CokernelCofork S.f}
  (hf : CategoryTheory.Limits.IsColimit cf),
  S.Exact ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι cg) (CategoryTheory.Limits.Cofork.π cf) = 0
-- Mathlib.CategoryTheory.Shift.Basic
/-- When shifts are indexed by an additive commutative monoid, then shifts commute.  -/
CategoryTheory.shiftFunctorComm : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (i j : A) →
            (CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j) ≅
              (CategoryTheory.shiftFunctor C j).comp (CategoryTheory.shiftFunctor C i)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKey!_eq_getKey!ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α), m.getKey! a = m.getKey!ₘ a
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.functorπ_app : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (f : α → C),
  (CategoryTheory.Limits.Pi.functorπ a).app f = CategoryTheory.Limits.Pi.π f a
-- Mathlib.Order.Lattice
right_eq_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b = a ⊔ b ↔ a ≤ b
-- Mathlib.Data.Set.Countable
Set.countable_of_injective_of_countable_image : ∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → (f '' s).Countable → s.Countable
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_div_add : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (x / c + d) = c • ∫ (x : ℝ) in a / c + d..b / c + d, f x
-- Mathlib.Order.RelIso.Basic
RelIso.mk : {α : Type u_5} →
  {β : Type u_6} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → (toEquiv : α ≃ β) → (∀ {a b : α}, s (toEquiv a) (toEquiv b) ↔ r a b) → r ≃r s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.irreducible_pow_sup`. -/
irreducible_pow_sup : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ →
    Irreducible J → ∀ (n : ℕ), J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n
-- Mathlib.Order.Bounds.Basic
Set.Nonempty.bddBelow_upperBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.Nonempty → BddBelow (upperBounds s)
-- Lean.Elab.Tactic.Induction
/-- Elaborates the targets (`Lean.Parser.Tactic.elimTarget`),
generalizing them if requested or if otherwise necessary.

Returns
1. the targets as fvars and
2. an array of identifier/fvarid pairs so that the `induction`/`cases` tactic can
   annotate any user-supplied target hypothesis names using `Term.addLocalVarInfo`.

Modifies the current goal when generalizing.
 -/
Lean.Elab.Tactic.elabElimTargets : Array Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Expr × Array (Lean.Ident × Lean.FVarId))
-- Std.Http.Data.Chunk
Std.Http.Chunk.instEncodeV11 : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Chunk
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.restrictScalars : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] {A : Type u_5}
  [inst_2 : CommSemiring A] [inst_3 : Algebra R A] [inst_4 : Module R M] (S : Submonoid R) [inst_5 : Module A M]
  {N : Type u_6} [inst_6 : AddCommMonoid N] [inst_7 : Module R N] [inst_8 : Module A N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (f : M →ₗ[A] N) [h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f],
  IsLocalizedModule S (↑R f)
-- Lean.Server.Completion.CompletionInfoSelection
_private.Lean.Server.Completion.CompletionInfoSelection.0.Lean.Server.Completion.filterDuplicateCompletionInfos : Array Lean.Server.Completion.ContextualizedCompletionInfo → Array Lean.Server.Completion.ContextualizedCompletionInfo
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDTreeMap.ofList l cmp).getKey! k = default
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instCommSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalCommSemiring A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → CommSemiring (Unitization R A)
-- Lean.Attributes
Lean.ParametricAttributeImpl.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (toAttributeImplCore : Lean.AttributeImplCore)
  (getParam : Lean.Name → Lean.Syntax → Lean.AttrM α) (afterSet : Lean.Name → α → Lean.AttrM Unit)
  (preserveOrder : Bool) (filterExport : Lean.Environment → Lean.Name → α → Bool),
  sizeOf
      { toAttributeImplCore := toAttributeImplCore, getParam := getParam, afterSet := afterSet,
        preserveOrder := preserveOrder, filterExport := filterExport } =
    1 + sizeOf toAttributeImplCore + sizeOf preserveOrder
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.boundedFormula₁.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (r : L.Relations 1) (t : L.Term (α ⊕ Fin n)),
  r.boundedFormula₁ t = r.boundedFormula ![t]
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.Order.RelSeries
RelSeries.smash_castLE : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin (p.length + 1)),
  (p.smash q h).toFun (Fin.castLE ⋯ i) = p.toFun i
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.inc_other : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x), G.Inc e h.other
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.anyM_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Std.Iter β} {f : β → m β'}
  {p : β' → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.Iter.mapM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        p __do_lift)
      (Std.Iter.mapM pure it)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_replaceConsts : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b) (a' : G)
  (b' : H) (ha : a = a') (hb : b = b'), ⇑(f.replaceConsts a' b' ha hb) = ⇑f
-- Init.Data.SInt.Lemmas
ISize.toInt16_add : ∀ (a b : ISize), (a + b).toInt16 = a.toInt16 + b.toInt16
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_one : ∀ {x : ℝ}, √x = 1 ↔ x = 1
-- Mathlib.RepresentationTheory.Coinvariants
Representation.toCoinvariants_mk : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal] (g : G) (x : V),
  ((ρ.toCoinvariants S) g) ((Representation.Coinvariants.mk (MonoidHom.comp ρ S.subtype)) x) =
    (Representation.Coinvariants.mk (MonoidHom.comp ρ S.subtype)) ((ρ g) x)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D'),
  (CategoryTheory.CostructuredArrow.prodEquivalence S S' T T').counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.CostructuredArrow.prodInverse S S' T T').comp
                (CategoryTheory.CostructuredArrow.prodFunctor S S' T T')).obj
            f))
      ⋯
-- Plausible.Shrinkable
Plausible.UInt8.shrinkable : Plausible.Shrinkable UInt8
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring bracket is additive in its second component.  -/
LieRing.lie_add : ∀ {L : Type v} [self : LieRing L] (x y z : L), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_insert_of_notMem' : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α) (f : α → β)
  (comm : (↑(insert a s)).Pairwise (Function.onFun AddCommute f)),
  a ∉ s → (insert a s).noncommSum f comm = s.noncommSum f ⋯ + f a
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_bot : ∀ {M : Type u_2} [inst : Add M], ⊥.unop = ⊥
-- Mathlib.Topology.Order.ScottTopology
/-- A recursor for `WithScott`. Use as `induction x`.  -/
Topology.WithScott.rec : {α : Type u_1} →
  {β : Topology.WithScott α → Sort u_3} →
    ((a : α) → β (Topology.WithScott.toScott a)) → (a : Topology.WithScott α) → β a
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_zero_left : ∀ {α : Type u_1} {E' : Type u_6} {F'' : Type u_10} [inst : SeminormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F'']
  {g'' : α → F''} {l : Filter α}, (fun x => 0) =Θ[l] g'' ↔ g'' =ᶠ[l] 0
-- Init.Data.UInt.Bitwise
UInt64.and_comm : ∀ (a b : UInt64), a &&& b = b &&& a
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_eq_ascFactorialBinary : Nat.ascFactorial = Nat.ascFactorialBinary
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.of_limitPresentation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {X : C} {a : α}
  (pres : CategoryTheory.Limits.LimitPresentation (J a) X),
  (∀ (j : J a), P.limitsClosure J (pres.diag.obj j)) → P.limitsClosure J X
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.typeUnknown : Lean.Expr → Lean.MetaM Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKey!_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).isEmpty = false →
        ((Std.DTreeMap.Raw.Const.alter t k f).maxKey! = k ↔
          (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.nsmul_le_nsmul_of_le_of_le_of_nonneg : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.NatModule M] [Lean.Grind.OrderedAdd M]
  {k₁ k₂ : ℕ} {x y : M}, k₁ ≤ k₂ → x ≤ y → 0 ≤ x → k₁ • x ≤ k₂ • y
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.iUnion_openCell_eq_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C],
  ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n j = C
-- Init.PropLemmas
forall_or_eq_imp : ∀ {α : Sort u_1} {a' : α} {P Q : α → Prop}, (∀ (a : α), Q a ∨ a = a' → P a) ↔ (∀ (a : α), Q a → P a) ∧ P a'
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.isColoop_iff_sdiff_not_spanning`. -/
Matroid.isColoop_iff_diff_not_spanning : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instFullLocalizedFunctorOfIsLocalizedFullyFaithful : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] [Φ.IsLocalizedFullyFaithful], (Φ.localizedFunctor L₁ L₂).Full
-- Mathlib.Algebra.GCDMonoid.Basic
NormalizedGCDMonoid.mk : {α : Type u_2} →
  [inst : CommMonoidWithZero α] →
    [toNormalizationMonoid : NormalizationMonoid α] →
      [toGCDMonoid : GCDMonoid α] →
        (∀ (a b : α), normalize (gcd a b) = gcd a b) →
          (∀ (a b : α), normalize (lcm a b) = lcm a b) → NormalizedGCDMonoid α
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.equivMapDomain_single : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddCommMonoid k] (f : G ≃ H) (a : G) (b : k),
  SkewMonoidAlgebra.equivMapDomain f (SkewMonoidAlgebra.single a b) = SkewMonoidAlgebra.single (f a) b