mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv β γ)
  (e'' : PartialEquiv γ δ), (e.trans e').trans e'' = e.trans (e'.trans e'')
-- Std.Do.PostCond
Std.Do.PostShape.arg.inj : ∀ {σ : Type u} {a : Std.Do.PostShape} {σ_1 : Type u} {a_1 : Std.Do.PostShape},
  Std.Do.PostShape.arg σ a = Std.Do.PostShape.arg σ_1 a_1 → σ = σ_1 ∧ a = a_1
-- Mathlib.Algebra.Group.Hom.Defs
MulHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : FunLike F M N], (∀ (f : F) (x y : M), f (x * y) = f x * f y) → MulHomClass F M N
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The opposite of a binary bicone.  -/
CategoryTheory.Limits.BinaryBicone.op : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        CategoryTheory.Limits.BinaryBicone P Q → CategoryTheory.Limits.BinaryBicone (Opposite.op P) (Opposite.op Q)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_beq_zero : ∀ (a : BitVec 1), (!a == 0#1) = (a == 1#1)
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- Any continuous bijection of compact Hausdorff spaces is an isomorphism.  -/
CompHausLike.isIso_of_bijective : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y),
  Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.IsIso f
-- Init.Data.Ord.Basic
Ord.ext_iff : ∀ {α : Type u} {x y : Ord α}, x = y ↔ compare = compare
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticWithinAt.aeval_polynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {z : E} {s : Set E}
  [inst_4 : NormedRing B] [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {f : E → B},
  AnalyticWithinAt 𝕜 f s z → ∀ (p : Polynomial A), AnalyticWithinAt 𝕜 (fun x => (Polynomial.aeval (f x)) p) s z
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.mk.inj : ∀ {ref : Lean.Syntax} {term? : Option Lean.Term} {fixpointType : Lean.Elab.PartialFixpointType} {ref_1 : Lean.Syntax}
  {term?_1 : Option Lean.Term} {fixpointType_1 : Lean.Elab.PartialFixpointType},
  { ref := ref, term? := term?, fixpointType := fixpointType } =
      { ref := ref_1, term? := term?_1, fixpointType := fixpointType_1 } →
    ref = ref_1 ∧ term? = term?_1 ∧ fixpointType = fixpointType_1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u₁` and `u₂` are two uniform structures on `γ`, then
`𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂)`.  -/
UniformFun.inf_eq : ∀ {α : Type u_1} {γ : Type u_3} {u₁ u₂ : UniformSpace γ},
  UniformFun.uniformSpace α γ = UniformFun.uniformSpace α γ ⊓ UniformFun.uniformSpace α γ
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.mk.injEq : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (V : Type w) [hV1 : AddCommGroup V]
  [hV2 : Module k V] (ρ : Representation k G V) (V_1 : Type w) (hV1_1 : AddCommGroup V_1) (hV2_1 : Module k V_1)
  (ρ_1 : Representation k G V_1),
  ({ V := V, hV1 := hV1, hV2 := hV2, ρ := ρ } = { V := V_1, hV1 := hV1_1, hV2 := hV2_1, ρ := ρ_1 }) =
    (V = V_1 ∧ hV1 ≍ hV1_1 ∧ hV2 ≍ hV2_1 ∧ ρ ≍ ρ_1)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.η_ε_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (X : C)
  [inst_3 : F.Monoidal] {Z : C} (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X) h) =
    h
-- Init.Data.SInt.Basic
instModISize : Mod ISize
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates, as algebra, `R[M]`, then the set of supports of elements
of `S` generates `R[M]`.  -/
MonoidAlgebra.support_gen_of_gen : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] {S : Set (MonoidAlgebra R M)},
  Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⋃ f ∈ S, ⇑(MonoidAlgebra.of R M) '' ↑f.coeff.support) = ⊤
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDeg_eq : ∀ (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})]
  [IsCyclotomicExtension {n} ℚ K], n = p ^ (k + 1) * m → ¬p ∣ m → P.inertiaDeg ℤ = orderOf ↑p
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.instOrderHomClassReal : OrderHomClass CircleDeg1Lift ℝ ℝ
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centralizer_univ : ∀ {R : Type u_1} [inst : Ring R], Subring.centralizer Set.univ = Subring.center R
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.op_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.op.f = S.g.op
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.coe_smul_primesOver_mk_eq_map_galRestrict : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  (K : Type u_4) (L : Type u_5) [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K]
  [inst_6 : IsFractionRing A K] [inst_7 : Algebra B L] [inst_8 : Algebra K L] [inst_9 : Algebra A L]
  [inst_10 : IsScalarTower A B L] [inst_11 : IsScalarTower A K L] [inst_12 : IsIntegralClosure B A L]
  [inst_13 : FiniteDimensional K L] (σ : Gal(L/K)) (P : Ideal B) [inst_14 : P.IsPrime] [inst_15 : P.LiesOver p],
  ↑(σ • Ideal.primesOver.mk p P) = Ideal.map ((galRestrict A K L B) σ) P
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.config : Lean.Meta.ConfigWithKey
-- Std.Internal.Parsec.ByteArray
Std.Internal.Parsec.ByteArray.instInputIteratorUInt8Nat : Std.Internal.Parsec.Input ByteArray.Iterator UInt8 ℕ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₂ → (m₁ ∩ m₂)[k]! = default
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.mem_closure_X_union_C : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R), p ∈ Subring.closure (insert Polynomial.X {f | f.degree ≤ 0})
-- Mathlib.Topology.ExtendFrom
/-- Extend a function from a set `A`. The resulting function `g` is such that
at any `x₀`, if `f` converges to some `y` as `x` tends to `x₀` within `A`,
then `g x₀` is defined to be one of these `y`. Else, `g x₀` could be anything.  -/
extendFrom : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → Set X → (X → Y) → X → Y
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_findSomeM? : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m (Option β)) (xs : List α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => List.findSomeM? (f x) xs
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.realize_add : ∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
  [inst_5 : FirstOrder.Ring.CompatibleRing R] (x y : FirstOrder.Language.ring.Term α) (v : α → R),
  FirstOrder.Language.Term.realize v (x + y) =
    FirstOrder.Language.Term.realize v x + FirstOrder.Language.Term.realize v y
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.instInhabitedSlot : {a : Type} → Inhabited (Std.Slot✝ a)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_monotoneOn : ∀ {p t : ℝ}, p ∈ Set.Ioo 0 1 → 0 ≤ t → MonotoneOn (p.rpowIntegrand₀₁ t) (Set.Ici 0)
-- Mathlib.Algebra.Order.Floor.Ring
Mathlib.Meta.Positivity.int_floor_nonneg : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, 0 ≤ a → 0 ≤ ⌊a⌋
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- If `s : ι → Set α` is a countable family of pairwise a.e. disjoint sets, then there exists a
family of measurable null sets `t i` such that `s i \ t i` are pairwise disjoint.  -/
MeasureTheory.exists_null_pairwise_disjoint_sdiff : ∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
    ∃ t,
      (∀ (i : ι), MeasurableSet (t i)) ∧
        (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Function.onFun Disjoint fun i => s i \ t i)
-- Mathlib.Topology.UniformSpace.Basic
/-- Uniform space structure on `αᵒᵈ`.  -/
OrderDual.instUniformSpace : {α : Type ua} → [UniformSpace α] → UniformSpace αᵒᵈ
-- Mathlib.Topology.Order.LeftRightLim
Monotone.leftLim_eq_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α] [(nhdsWithin x (Set.Iio x)).NeBot],
      Function.leftLim f x = sSup (f '' Set.Iio x)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instAddCommGroup : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] → [inst_4 : Module A M] → [inst_5 : Module R M] → AddCommGroup (Derivation R A M)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instProjective : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], Module.Projective R M
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The inverse functor establishing the equivalence `CostructuredArrow.preEquivalence`.  -/
CategoryTheory.CostructuredArrow.preEquivalence.inverse : {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] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D E} →
                {e : E} →
                  (f : CategoryTheory.CostructuredArrow G e) →
                    CategoryTheory.Functor (CategoryTheory.CostructuredArrow F f.left)
                      (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f)
-- Mathlib.Order.Filter.Ultrafilter.Basic
Nat.hyperfilter_le_atTop : ↑(Filter.hyperfilter ℕ) ≤ Filter.atTop
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.HasLimit.productLimitCone_isLimit_lift : ∀ {R : Type u} [inst : Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f),
  (ModuleCat.HasLimit.productLimitCone f).isLimit.lift s = ModuleCat.HasLimit.lift f s
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mk.injEq : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] [inst_1 : Ring R]
  (toMonoidWithZeroHom : R →*₀ Γ₀)
  (map_add_le_max' :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom).toFun (x + y) ≤ max ((↑toMonoidWithZeroHom).toFun x) ((↑toMonoidWithZeroHom).toFun y))
  (toMonoidWithZeroHom_1 : R →*₀ Γ₀)
  (map_add_le_max'_1 :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom_1).toFun (x + y) ≤
        max ((↑toMonoidWithZeroHom_1).toFun x) ((↑toMonoidWithZeroHom_1).toFun y)),
  ({ toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom_1, map_add_le_max' := map_add_le_max'_1 }) =
    (toMonoidWithZeroHom = toMonoidWithZeroHom_1)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.eq_iff_sub_mem : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x y : G}, ↑x = ↑y ↔ x - y ∈ N
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB4StarOfSize_shrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  [CategoryTheory.AB4StarOfSize.{max w w', v, u} C], CategoryTheory.AB4StarOfSize.{w, v, u} C
-- Mathlib.Data.Finset.Filter
Set.pairwiseDisjoint_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Set β) (t : Finset α),
  s.PairwiseDisjoint fun x => {x_1 ∈ t | f x_1 = x}
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- In a space with `C^∞` bump functions, register some function that will be used as a basis
to construct bump functions of arbitrary size around any point.  -/
someContDiffBumpBase : (E : Type u_3) →
  [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → [hb : HasContDiffBump E] → ContDiffBumpBase E
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Ioi_eq_card_Ici_sub_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  (Finset.Ioi a).card = (Finset.Ici a).card - 1
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The numerator of the generator.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.f : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial K
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.expectedType : Lean.Elab.Term.ExtractMonadResult → Lean.Expr
-- Mathlib.Analysis.Matrix.Spectrum
/-- Unitary matrix whose columns are `Matrix.IsHermitian.eigenvectorBasis`.  -/
Matrix.IsHermitian.eigenvectorUnitary : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {n : Type u_4} →
      [inst_1 : Fintype n] → {A : Matrix n n 𝕜} → [inst_2 : DecidableEq n] → A.IsHermitian → ↥(Matrix.unitaryGroup n 𝕜)
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.instTransZagZigzag : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    Trans (fun x1 x2 => CategoryTheory.Zag x1 x2) (fun x1 x2 => CategoryTheory.Zigzag x1 x2) fun x1 x2 =>
      CategoryTheory.Zigzag x1 x2
-- Lean.Attributes
Lean.instInhabitedAttributeApplicationTime : Inhabited Lean.AttributeApplicationTime
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_add : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s₁ s₂ : Multiset α),
  (s₁ + s₂).lcm = lcm s₁.lcm s₂.lcm
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.mk.injEq : ∀ (params : Array Lean.Meta.Grind.TParam) (anchors : Array Lean.Meta.Grind.TAnchor✝) (hasSorry : Bool)
  (params_1 : Array Lean.Meta.Grind.TParam) (anchors_1 : Array Lean.Meta.Grind.TAnchor✝) (hasSorry_1 : Bool),
  ({ params := params, anchors := anchors, hasSorry := hasSorry } =
      { params := params_1, anchors := anchors_1, hasSorry := hasSorry_1 }) =
    (params = params_1 ∧ anchors = anchors_1 ∧ hasSorry = hasSorry_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert k v t₁ ⋯).impl.Equiv (Std.DTreeMap.Internal.Impl.insert k v t₂ ⋯).impl
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k : α} {v : β}, (m.insert k v).getKey k ⋯ = k
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ X₂ ⊗ (X₁ ⊗ X₃)`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of two points is the span of their difference (reversed).  -/
vectorSpan_pair_rev : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), vectorSpan k {p₁, p₂} = k ∙ (p₂ -ᵥ p₁)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The homotopy category functor preserves generic terminal objects.  -/
SSet.hoFunctor.terminalIso : SSet.hoFunctor.obj (⊤_ SSet) ≅ ⊤_ CategoryTheory.Cat
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the pure predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.
 -/
Std.Iter.any : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → (β → Bool) → Std.Iter β → Bool
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.instToMessageData : Lean.ToMessageData Aesop.IndexMatchLocation
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.unop_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.unop.h₀ = h.h₃.unop
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ),
  ↑(f.pair g) =ᵐ[μ] fun x => (↑f x, ↑g x)
-- Lean.Parser.Term
Lean.Parser.Term.matchExprAlt.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.hom_inv_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : E.I₀), CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (e.inv.h₀ (e.hom.s₀ i)) = CategoryTheory.eqToHom ⋯
-- Init.Data.AC
Lean.Data.AC.Expr.var.inj : ∀ {x x_1 : ℕ}, Lean.Data.AC.Expr.var x = Lean.Data.AC.Expr.var x_1 → x = x_1
-- Mathlib.Algebra.Category.Ring.EqualizerPushout
/-- If `f : R ⟶ S` is a faithfully flat map in `CommRingCat`, then the fork
```
        S ---inl---> pushout f f
R --f-->
        S ---inr---> pushout f f
```
is an equalizer diagram.  -/
CommRingCat.isLimitForkPushoutSelfOfFaithfullyFlat : {R S : CommRingCat} →
  (f : R ⟶ S) →
    (CommRingCat.Hom.hom f).FaithfullyFlat → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
_private.Std.Tactic.BVDecide.LRAT.Internal.Assignment.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_2 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_2 ()
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSetDivGcdEquiv_eq : ∀ (r : ℕ) [inst : NeZero r] (v : ↑(EisensteinSeries.gammaSet 1 r 0)),
  ↑((EisensteinSeries.gammaSetDivGcdEquiv r) v) = EisensteinSeries.divIntMap ↑r ↑v
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- If finite measures themselves converge weakly to a nonzero limit measure, then their
normalized versions also converge weakly.  -/
MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
  [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) → μ ≠ 0 → Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.RigidCategory.toLeftRigidCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.RigidCategory C] → CategoryTheory.LeftRigidCategory C
-- Mathlib.Data.Part
Part.toOption_eq_some_iff : ∀ {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] {a : α}, o.toOption = some a ↔ a ∈ o
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] {A : Type u_2} [inst_2 : NonUnitalRing A]
  [inst_3 : StarRing A] [inst_4 : Module ℝ A] (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A)
  (f : ContinuousMapZero X NNReal),
  φ.realContinuousMapZeroOfNNReal
      ({ toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe, map_zero' := ⋯ }.comp f) =
    φ f
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.continuous_univBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  Continuous ↑(OpenPartialHomeomorph.univBall c r)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.instIsContinuousOverLeftIteratedSliceBackwardOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (f : CategoryTheory.Over X), f.iteratedSliceBackward.IsContinuous (J.over f.left) ((J.over X).over f)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side.  -/
Orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
-- Init.Coe
/-- `CoeHead α β` is for coercions that are applied from left-to-right at most once
at beginning of the coercion chain.
 -/
CoeHead : Sort u → semiOutParam (Sort v) → Sort (max (max 1 u) v)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.add : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A A' : Matrix ι ι R} {f f' : Module.End R M},
  Matrix.Represents b A f → Matrix.Represents b A' f' → Matrix.Represents b (A + A') (f + f')
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.withNamespace : {α : Type} → Lean.Name → Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Real.cos_eq_tsum : ∀ (r : ℝ), Real.cos r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n) / ↑(2 * n).factorial
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_appLE : ∀ {R S : CommRingCat} (f : R ⟶ S) {U : (AlgebraicGeometry.Spec S).Opens} {V : (AlgebraicGeometry.Spec R).Opens}
  (e : U ≤ (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).base).obj V),
  AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Spec.map f) V U e =
    CommRingCat.ofHom (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) V U e)