mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- All convergents of `0` are zero.  -/
Real.convergent_of_zero : ∀ (n : ℕ), Real.convergent 0 n = 0
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_fun_neg_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg F],
  (f =O[𝕜; l] fun x => -g x) ↔ f =O[𝕜; l] g
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.succ_fixpoint : ∀ {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : Set α},
  ChainClosure r c₁ → ChainClosure r c₂ → SuccChain r c₂ = c₂ → c₁ ⊆ c₂
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.perm_filter_self_iff_forall_containsKey : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).Perm l ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true),
        f (Std.Internal.List.getKey a l h) (Std.Internal.List.getValue a l h) = true)
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_neg : ∀ (a : UInt8), (-a).toUInt32 = -a.toUInt32 % 256
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- An infinite place of a number field `K` is a place associated to a complex embedding.  -/
NumberField.InfinitePlace : (K : Type u_1) → [Field K] → Type (max 0 u_1)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.Faithful
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.isAtom : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M}
  [IsSimpleModule R ↥m], IsAtom m
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The Fubini theorem for a functor `G : J × K ⥤ C`,
showing that the colimit of `G` can be computed as
the colimit of the colimits of the functors `G.obj (j, _)`.
 -/
CategoryTheory.Limits.colimitIsoColimitCurryCompColim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                [inst_4 :
                    CategoryTheory.Limits.HasColimit
                      ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] →
                  CategoryTheory.Limits.colimit G ≅
                    CategoryTheory.Limits.colimit
                      ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)
-- Init.Data.Format.Basic
/-- Starts a region tagged with `tag`.
 -/
Std.Format.MonadPrettyFormat.startTag : {m : Type → Type} → [self : Std.Format.MonadPrettyFormat m] → ℕ → m Unit
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.mapsTo_vadd_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G)
  (x : AddAction.orbitRel.Quotient G α), Set.MapsTo (fun x => g +ᵥ x) x.orbit x.orbit
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}
  {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β), ⇑(hnp.comp hmn) = ⇑hnp ∘ ⇑hmn
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.evalGrindTactic : Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp k ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The set of all arrows of a subgroupoid, as a set in `Σ c d : C, c ⟶ d`.  -/
CategoryTheory.Subgroupoid.toSet : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Set ((c : C) × (d : C) × (c ⟶ d))
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.pow_dvd_add_pow_of_pow_eq_zero_right : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Semiring R],
  n + m ≤ p + 1 → Commute x y → y ^ n = 0 → x ^ m ∣ (x + y) ^ p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.pentagon_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (W X Y Z : C) {Z_1 : C} (h : W ⨯ X ⨯ Y ⨯ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom
        (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W)
            (CategoryTheory.Limits.prod.associator X Y Z).hom)
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)},
  (t.alter k f).getD k fallback = (f (t.get? k)).getD fallback
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_Ioi_rpow_of_lt : ∀ {a : ℝ}, a < -1 → ∀ {c : ℝ}, 0 < c → ∫ (t : ℝ) in Set.Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The graph induced on `Set.univ` is isomorphic to the original graph.  -/
SimpleGraph.induceUnivIso : {V : Type u_1} → (G : SimpleGraph V) → SimpleGraph.induce Set.univ G ≃g G
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.op_commShiftIso_inv_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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ)
  (h : n + m = 0) {Z : Dᵒᵖ} (h_1 : F.op.obj ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).inv.app X) h_1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).hom.app (Opposite.op (F.obj (Opposite.unop X))))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F m).hom.app (Opposite.unop X)).op
        (CategoryTheory.CategoryStruct.comp
          (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).inv.app X).unop).op h_1))
-- Mathlib.Algebra.Ring.Subring.Defs
intCast_mem : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ),
  ↑n ∈ s
-- Init.Notation
/-- `#check_tactic t ~> r by commands` runs the tactic sequence `commands`
on a goal with `t` and sees if the resulting expression has reduced it
to `r`.
 -/
Lean.Parser.checkTactic : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodEquivProdPLift_apply : ∀ {α : Sort u_1} {β : Sort u_4} (a : α ×' β), Equiv.pprodEquivProdPLift a = ({ down := a.fst }, { down := a.snd })
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- If a functor `F : C ⥤ D` preserves exact sequences on the right-hand side (i.e.
if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then `F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact),
then it preserves epimorphisms.
 -/
CategoryTheory.Functor.preservesEpimorphisms_of_preserves_shortExact_right : ∀ {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] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  (∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g)) →
    F.PreservesEpimorphisms
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α)
  [inst_1 : DecidableEq β] {b : β}, (insert b s).sup' ⋯ f = f b ⊔ s.sup' H f
-- Init.PropLemmas
/-- Construct a non-Prop by cases on an `Or`, when the left conjunct is decidable.  -/
Or.by_cases : {p q : Prop} → [Decidable p] → {α : Sort u} → p ∨ q → (p → α) → (q → α) → α
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousAdd : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousAdd α]
  [WeaklyLocallyCompactSpace α], WeaklyLocallyCompactSpace (AddUnits α)
-- Mathlib.Tactic.Continuity
/-- `@[continuity]` adds the tagged definition to the set of lemmas used by the `continuity` tactic.
Lemmas are used without backtracking: when the conclusion of this lemma matches the goal, the lemma
is applied unconditionally. Thus a lemma should preserve provability: if the goal can be proven,
then after applying a `@[continuity]` lemma to it, the generated subgoals should remain provable.
 -/
attrContinuity : Lean.ParserDescr
-- Mathlib.CategoryTheory.Opposites
/-- Given a natural transformation `α : F.op ⟶ G.op`,
we can take the "unopposite" of each component obtaining a natural transformation `G ⟶ F`.
 -/
CategoryTheory.NatTrans.removeOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {F G : CategoryTheory.Functor C D} → (F.op ⟶ G.op) → (G ⟶ F)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_right_as : ∀ {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)
  (g : CategoryTheory.CostructuredArrow F f.left),
  ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.right.as = PUnit.unit
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.separable : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E] (x : E),
  IsSeparable F x
-- Mathlib.Data.Num.Lemmas
Num.to_nat_inj : ∀ {m n : Num}, ↑m = ↑n ↔ m = n
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- (Implementation) Auxiliary definition for `unitCompPartialBijective`.  -/
CategoryTheory.unitCompPartialBijectiveAux : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {i : CategoryTheory.Functor D C} →
          [inst_2 : CategoryTheory.Reflective i] →
            (A : C) → (B : D) → (A ⟶ i.obj B) ≃ (i.obj ((CategoryTheory.reflector i).obj A) ⟶ i.obj B)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.comp_id : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B), f.comp (MulDistribMulActionHom.id M) = f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.type.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (expr : Lean.Expr)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1),
  sizeOf (Lean.Compiler.LCNF.Arg.type expr h) = 1 + sizeOf expr + sizeOf h
-- Mathlib.Data.List.GetD
List.getElem?_getD_replicate_default_eq : ∀ {α : Type u} (d : α) (r n : ℕ), (List.replicate r d)[n]?.getD d = d
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false)
  {h : k ∈ m.insertMany l}, (m.insertMany l).get k h = m.get k ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_smulₛₗ : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E), e (c • x) = σ₁₂ c • e x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α}, a ∈ t → t.get? a = some (t.get! a)
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.mk : {R : Type u} →
  [inst : CommRing R] →
    (carrier : Type v) → [commRing : CommRing carrier] → [bialgebra : Bialgebra R carrier] → CommBialgCat R
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.toIsHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [self : p.IsStronglyCocartesian f φ],
  p.IsHomLift f φ
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup (Lex α)
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
/-- If an open subscheme `U` of `X` surjects onto `S` and `X` is geometrically irreducible over `S`,
then also `U` is geometrically irreducible over `S`.  -/
AlgebraicGeometry.instGeometricallyIrreducibleCompSchemeOfIsOpenImmersionOfSurjective : ∀ {X S U : AlgebraicGeometry.Scheme} {f : U ⟶ X} {g : X ⟶ S} [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.GeometricallyIrreducible g]
  [AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g)],
  AlgebraicGeometry.GeometricallyIrreducible (CategoryTheory.CategoryStruct.comp f g)
-- Std.Http.Protocol.H1.Writer
/-- Marks the body as closed, indicating no more user data will be added.
 -/
Std.Http.Protocol.H1.Writer.closeBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Mathlib.Data.Part
Part.mul_get_eq : ∀ {α : Type u_1} [inst : Mul α] (a b : Part α) (hab : (a * b).Dom), (a * b).get hab = a.get ⋯ * b.get ⋯
-- Mathlib.Combinatorics.KatonaCircle
Numbering.card_prefixed : ∀ {X : Type u_1} [inst : Fintype X] [inst_1 : DecidableEq X] (s : Finset X),
  (Numbering.prefixed s).card = s.card.factorial * (Fintype.card X - s.card).factorial
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.mk : {X Y : TopPair} →
  {f g : X ⟶ Y} →
    (fst : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g)) →
      (snd : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g)) →
        autoParam
            (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I) fst.h =
              CategoryTheory.CategoryStruct.comp snd.h TopPair.map)
            TopPair.Homotopy.w._autoParam →
          TopPair.Homotopy f g
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.isStableUnderShift_iff_shiftClosure_eq_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.IsClosedUnderIsomorphisms],
  P.IsStableUnderShift A ↔ P.shiftClosure A = P
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instNontrivial : Nontrivial Cardinal.{u}
-- Mathlib.CategoryTheory.Localization.LocallySmall
/-- If `L : C ⥤ D` is a localization functor for a class of morphisms
`W : MorphismProperty C`, and `D` is locally `w`-small, we may obtain
a `HasLocalization.{w} W` instance. This should be used only in the
unlikely situation where the types of objects of `C` and `D` are in
different universes. Otherwise, use `hasLocalizationOfLocallySmall`.  -/
CategoryTheory.MorphismProperty.hasLocalizationOfLocallySmall' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {D : Type u_3} →
        [inst_1 : CategoryTheory.Category.{u_4, u_3} D] →
          [CategoryTheory.LocallySmall.{u_5, u_4, u_3} D] →
            (L : CategoryTheory.Functor C D) → [L.IsLocalization W] → W.HasLocalization
-- Mathlib.Tactic.Widget.Calc
CalcParams.mk.sizeOf_spec : ∀ (toSelectInsertParams : SelectInsertParams) (isFirst : Bool) (indent : ℕ),
  sizeOf { toSelectInsertParams := toSelectInsertParams, isFirst := isFirst, indent := indent } =
    1 + sizeOf toSelectInsertParams + sizeOf isFirst + sizeOf indent
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodPUnit_apply : ∀ (M : Type u_1) [inst : AddMonoid M], ⇑(AddEquiv.coprodPUnit M) = ⇑AddMonoid.Coprod.fst
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- Convert a `Real.Angle` to a real number in the interval `Ioc (-π) π`.  -/
Real.Angle.toReal : Real.Angle → ℝ
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_union : ∀ {α : Type u} (s t : Set α) [Finite ↑s] [Finite ↑t], Finite ↑(s ∪ t)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
/-- `Real.cos` and `Real.arccos` as a (partial) equivalence from `[0, π]` to `[-1, 1]`  -/
Real.cosPartialEquiv : PartialEquiv ℝ ℝ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The maximal separated set is a cover.  -/
Metric.isCover_maximalSeparatedSet : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.packingNumber ε A ≠ ⊤ → Metric.IsCover ε A (Metric.maximalSeparatedSet ε A)
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.mem_closedBall₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (self : ODE.FunSpace t₀ x₀ r L), self.toFun t₀ ∈ Metric.closedBall x₀ ↑r
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_I : ↑UpperHalfPlane.I = Complex.I
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- `ball x ε` is the set of all points `y` with `dist y x < ε`  -/
Metric.ball : {α : Type u} → [PseudoMetricSpace α] → α → ℝ → Set α
-- Mathlib.Logic.Function.Conjugate
/-- Definition of `Function.Semiconj` in terms of functional equality.  -/
Function.semiconj_iff_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β}, Function.Semiconj f ga gb ↔ f ∘ ga = gb ∘ f
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_add_left : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Add β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i + f j) (f k) μ
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_mul_eq_union : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M} [inst_3 : DecidableEq M],
  a ≠ 0 →
    b ≠ 0 →
      UniqueFactorizationMonoid.primeFactors (a * b) =
        UniqueFactorizationMonoid.primeFactors a ∪ UniqueFactorizationMonoid.primeFactors b
-- Mathlib.LinearAlgebra.Dimension.Basic
Submodule.rank_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Submodule R M),
  Module.rank R ↥s ≤ Module.rank R M
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- If a set is disjoint from its translates by infinitely many bounded vectors, then it has measure
zero. This auxiliary lemma proves this assuming additionally that the set is bounded.  -/
MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E),
  Bornology.IsBounded s →
    Bornology.IsBounded (Set.range u) →
      Pairwise (Function.onFun Disjoint fun n => {u n} + s) → MeasurableSet s → μ s = 0
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.mem.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S] (i : n),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv))
      (AlgebraicGeometry.AffineSpace.coord S i) =
    (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).inv)
      (MvPolynomial.X i)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.nhds_basis_eball`. -/
EMetric.nhds_basis_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (Metric.eball x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.mk.injEq : ∀ (name : String) (kind : Lean.Lsp.SymbolKind) (tags : Array Lean.Lsp.SymbolTag) (location : Lean.Lsp.Location)
  (containerName? : Option String) (name_1 : String) (kind_1 : Lean.Lsp.SymbolKind) (tags_1 : Array Lean.Lsp.SymbolTag)
  (location_1 : Lean.Lsp.Location) (containerName?_1 : Option String),
  ({ name := name, kind := kind, tags := tags, location := location, containerName? := containerName? } =
      { name := name_1, kind := kind_1, tags := tags_1, location := location_1, containerName? := containerName?_1 }) =
    (name = name_1 ∧ kind = kind_1 ∧ tags = tags_1 ∧ location = location_1 ∧ containerName? = containerName?_1)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.toLinearIsometry_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G),
  (LinearIsometryEquiv.lTensor E f).toLinearIsometry = LinearIsometry.lTensor E f.toLinearIsometry
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `map_finsetProd`. -/
map_finset_prod : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {α : Type u_7} {F : Type u_8}
  [inst_2 : Fintype α] [inst_3 : EquivLike F M N] [MulEquivClass F M N] (f : F) (g : α → M), f (∏ i, g i) = ∏ i, f (g i)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.transvection_zero : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n), Matrix.transvection i j 0 = 1