mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.op_nonpos : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : α}, AddOpposite.op a ≤ 0 ↔ a ≤ 0
-- Mathlib.Algebra.Group.AddChar
AddChar.toAddMonoidHom_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (a : A),
  ψ.toAddMonoidHom a = Additive.ofMul (ψ a)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.toAddActionHom_injective : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  {f g : A →ₑ+[φ] B}, ↑f = ↑g → f = g
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'},
  Std.Internal.List.eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: Std.Internal.List.eraseKey k l
-- Std.Sync.Channel
/-- The central state structure for an unbounded channel. Maintains the following invariants:
1. `values = ∅ ∨ consumers = ∅`
2. `closed = true → consumers = ∅`
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State : Type → Type
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trPosNum_natEnd : ∀ (n : PosNum), ∀ x ∈ Turing.PartrecToTM2.trPosNum n, Turing.PartrecToTM2.natEnd x = false
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (t.alter k f).isEmpty = false →
    ∀ {fallback : α}, (t.alter k f).minKeyD fallback = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be an integral domain and `f : R[X]`. Let `s` be a finite index set.
Then a fraction of the form `f / ∏ i ∈ s, g i` evaluated in a field `K` containing `R[X]`
can be rewritten as `q + ∑ i ∈ s, r i / g i`, where
`degree (r i) < degree (g i)`, provided that the `g i` are monic and pairwise coprime.
See `quo_add_sum_rem_div_unique` for the uniqueness of this representation.  -/
Polynomial.div_prod_eq_quo_add_sum_rem_div : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Topology.Maps.Proper.Basic
/-- If `Y` is a compact topological space, then `Prod.fst : X × Y → X` is a closed map.  -/
isClosedMap_fst_of_compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y],
  IsClosedMap Prod.fst
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion : Lean.FileMap → String.Pos.Raw → Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- If `F` is an equivalence, then so is the functor `(S, F ⋙ G) ⥤ (S, G)`.  -/
CategoryTheory.StructuredArrow.isEquivalence_pre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [F.IsEquivalence], (CategoryTheory.StructuredArrow.pre S F G).IsEquivalence
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.fst_comp_inr : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P),
  (QuadraticMap.Isometry.fst M₂ Q₁).comp (QuadraticMap.Isometry.inr Q₁ 0) = 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.throwUnexpected : {α : Type} → Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.GoalM α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionResult.closed.sizeOf_spec : ∀ (seq : List Lean.Meta.Grind.TGrind), sizeOf (Lean.Meta.Grind.ActionResult.closed seq) = 1 + sizeOf seq
-- Init.Core
Std.LawfulLeftIdentity.mk : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → β} {o : outParam α} [toLeftIdentity : Std.LeftIdentity op o],
  (∀ (a : β), op o a = a) → Std.LawfulLeftIdentity op o
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.d.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι),
  HomologicalComplex.homotopyCofiber.d φ i j =
    if hij : c.Rel i j then
      (if hj : c.Rel j (c.next j) then
            -CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij)
                (CategoryTheory.CategoryStruct.comp (F.d j (c.next j))
                  (HomologicalComplex.homotopyCofiber.inlX φ (c.next j) j hj))
          else 0) +
          CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij)
            (CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j)) +
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i)
          (CategoryTheory.CategoryStruct.comp (G.d i j) (HomologicalComplex.homotopyCofiber.inrX φ j))
    else 0
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_zero_one : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  (b : α), toIcoMod ⋯ 0 b = Int.fract b
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.prod : ∀ {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Finset α},
  (∀ x ∈ s, f x ≡ g x [ZMOD n]) → ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [ZMOD n]
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
/-- A multivariate polynomial `f` whose support is nontrivial,
such that some variable `i` appears with exponent `1` in one nontrivial monomial,
whose monomials have disjoint supports, and which is primitive, is irreducible.  -/
MvPolynomial.irreducible_of_disjoint_support : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R] [IsDomain R] {f : MvPolynomial n R},
  f.support.Nontrivial →
    ∀ {d : n →₀ ℕ},
      d ∈ f.support →
        ∀ {i : n},
          d i = 1 →
            (↑f.support).PairwiseDisjoint Finsupp.support →
              (∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ MvPolynomial.coeff d f) → IsUnit r) → Irreducible f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_τ₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  (groupHomology.mapShortComplexH2 f φ).τ₂ = groupHomology.chainsMap₂ f φ
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftDual_rightDual : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : CategoryTheory.HasRightDual X], ᘁXᘁ = X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termG₁ : Lean.ParserDescr
-- Mathlib.Tactic.Simps.Basic
/-- Returns the projection information of a structure.  -/
Simps.projectionsInfo : List Simps.ProjectionData → String → Lean.Name → Lean.MessageData
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0_eq_mk0_inv_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R]
  {I J : ↥(nonZeroDivisors (Ideal R))}, ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChangeHomeomorph_coe : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ : Bundle.Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet)
  (h₂ : b ∈ e₂.baseSet), ⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpFullyFaithful.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddGrpFullyFaithful =
    {
      preimage := fun {G H} α =>
        CategoryTheory.AddGrp.homMk'
          (CategoryTheory.yonedaAddMonFullyFaithful.preimage
            (CategoryTheory.Functor.whiskerRight α (CategoryTheory.forget₂ AddGrpCat AddMonCat))),
      map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.pow_coe : ∀ {M : Type u_1} [inst : Monoid M] (n : M) (m : ℕ), ↑(Submonoid.pow n m) = n ^ m
-- Init.Data.Array.DecidableEq
Array.instDecidableEq_csimp : @Array.instDecidableEq = @Array.instDecidableEqImpl
-- Mathlib.Order.Preorder.Finite
OrderHom.range_eq_iff : ∀ {α : Type u_4} {β : Type u_5} [inst : LinearOrder α] [inst_1 : PartialOrder β] [Finite α] {f g : α →o β},
  Function.Injective ⇑f → Function.Injective ⇑g → (Set.range ⇑f = Set.range ⇑g ↔ f = g)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.some.inj : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Affine R} {x y : R} {h : W'.Nonsingular x y} {x_1 y_1 : R}
  {h_1 : W'.Nonsingular x_1 y_1},
  WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x_1 y_1 h_1 → x = x_1 ∧ y = y_1
-- Mathlib.SetTheory.ZFC.PSet
PSet.instEmptyCollection : EmptyCollection PSet.{u_1}
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.prodComonad_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {x x_1 : C} (g : x ⟶ x_1),
  (CategoryTheory.prodComonad X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] (k k' : α) (f : Option β → Option β) (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue? k' (Std.Internal.List.Const.alterKey k f l) =
      if (k == k') = true then f (Std.Internal.List.getValue? k l) else Std.Internal.List.getValue? k' l
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.continuousAt_Gamma : ∀ (s : ℂ), (∀ (m : ℕ), s ≠ -↑m) → ContinuousAt Complex.Gamma s
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaObjObjEquiv_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).obj Y),
  CategoryTheory.shrinkYonedaObjObjEquiv
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.obj X).map g)) f) =
    CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.shrinkYonedaObjObjEquiv f)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.match_1.eq_1 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match ByteArray.utf8DecodeChar?.FirstByte.invalid with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 ()
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 ()
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 ()
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 ()
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 ()) =
    h_1 ()
-- Lean.Widget.Diff
/-- A map from subexpr positions in `e₁` to 'diff points' which are tags
describing how the expression has changed relative to `before` at the given position. -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.changesAfter : Lean.Widget.ExprDiff✝ → Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.mid.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (hi : Order.IsPredPrelimit i) (hj : i < j),
  hi.mid hj = Classical.indefiniteDescription (Membership.mem (Set.Ioo i j)) ⋯
-- Mathlib.GroupTheory.Solvable
derivedSeries_succ : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), derivedSeries G (n + 1) = ⁅derivedSeries G n, derivedSeries G n⁆
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.trace R M = if H : ∃ s, Nonempty (Module.Basis (↥s) R M) then LinearMap.traceAux R ⋯.some else 0
-- Init.Data.Array.Subarray
/-- The ending index of the region of interest (exclusive).  -/
Subarray.stop : {α : Type u_1} → Subarray α → ℕ
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- The space of continuous alternating maps over an algebra over `R` is a module over `R`, for the
pointwise addition and scalar multiplication.  -/
ContinuousAlternatingMap.instModule : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_5} →
          [inst : Semiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : TopologicalSpace N] →
                      [inst_6 : ContinuousAdd N] →
                        [inst_7 : Module A M] →
                          [inst_8 : Module A N] →
                            [inst_9 : Module R N] →
                              [ContinuousConstSMul R N] → [SMulCommClass A R N] → Module R (M [⋀^ι]→L[A] N)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M},
  BddBelow s → BddBelow t → BddBelow (s * t)
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a monoid is commutative.  -/
Submonoid.center.commMonoid : {M : Type u_1} → [inst : Monoid M] → CommMonoid ↥(Submonoid.center M)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.ofNat.eq_2 : ∀ (n : ℕ), ↑n.succ = ONote.oadd 0 n.succPNat 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- A homothety with a nonzero scale factor preserves angles.  -/
EuclideanGeometry.oangle_homothety : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p p₁ p₂ p₃ : P) {r : ℝ},
  r ≠ 0 →
    EuclideanGeometry.oangle ((AffineMap.homothety p r) p₁) ((AffineMap.homothety p r) p₂)
        ((AffineMap.homothety p r) p₃) =
      EuclideanGeometry.oangle p₁ p₂ p₃
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).isEmpty =
        (((↑m).isEmpty || (↑m).size == 1 && m.contains k) && (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isNone)
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_one_right : ∀ {G : Type u_1} [inst : Group G] (g : G), ⁅g, 1⁆ = 1
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : SupSet α], sSupHom.instInhabited α = { default := sSupHom.id α }
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isUnit : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → k ≠ 0 → IsUnit ζ
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- If `g` is a ring automorphism of `L`, and `n : ℕ+`, then
`modularCyclotomicCharacter.toFun n g` is the `j : ZMod d` such that `g(ζ)=ζ^j` for all
`n`-th roots of unity. Here `d` is the number of `n`th roots of unity in `L`.  -/
modularCyclotomicCharacter.toFun : {L : Type u} → [inst : CommRing L] → [IsDomain L] → (n : ℕ) → [NeZero n] → L ≃+* L → ZMod (Nat.card ↥(rootsOfUnity n L))
-- Lean.Environment
Lean.ModuleData.constants : Lean.ModuleData → Array Lean.ConstantInfo
-- Mathlib.Data.Finset.Sort
Finset.sorted_zero_eq_min'_aux : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (h : 0 < (s.sort fun a b => a ≤ b).length) (H : s.Nonempty),
  (s.sort fun a b => a ≤ b).get ⟨0, h⟩ = s.min' H
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given `LawfulUpwardEnumerable`,
`LawfulUpwardEnumerableLT` and `LawfulUpwardEnumerableLeast?` instances.
 -/
Std.Rio.isEmpty : {α : Type u} →
  [inst : LT α] → [DecidableLT α] → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.Rio α → Bool
-- Init.Data.Iterators.Combinators.FlatMap
/-- Let `it` be an iterator and `f` a monadic function mapping `it`'s outputs to iterators.
Then `it.flatMapM f` is an iterator that goes over `it` and for each output, it applies `f` and
iterates over the resulting iterator. `it.flatMapM f` emits all values obtained from the inner
iterators -- first, all of the first inner iterator, then all of the second one, and so on.

**Marble diagram (without monadic effects):**

```text
it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMapM        ----a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` and the inner iterators are finite
* `Productive` instance: only if `it` is finite and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.

For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
Std.Iter.flatMapM : {α β α₂ γ : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : MonadAttach m] →
        [Std.Iterator α Id β] → [Std.Iterator α₂ m γ] → (f : β → m (Std.IterM m γ)) → Std.Iter β → Std.IterM m γ
-- Mathlib.Order.Closure
ClosureOperator.conjBy_trans : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α), c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f},
  (t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Computability.RE
/-- The computable functions are closed under if-then-else definitions
with computable predicates.  -/
ComputablePred.ite : ∀ {f₁ f₂ : ℕ → ℕ},
  Computable f₁ →
    Computable f₂ →
      ∀ {c : ℕ → Prop} [inst : DecidablePred c], ComputablePred c → Computable fun k => if c k then f₁ k else f₂ k
-- Mathlib.Topology.Algebra.Group.Basic
/-- Every weakly locally compact separable topological additive group is σ-compact.
Note: this is not true if we drop the topological group hypothesis.  -/
SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G], SigmaCompactSpace G
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.equalizer_eq_top : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {φ ψ : A →ₐ[R] B}, φ.equalizer ψ = ⊤ ↔ φ = ψ
-- Mathlib.Order.WithBot
WithBot.unbot_le_unbot_iff : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥), x.unbot hx ≤ y.unbot hy ↔ x ≤ y
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.trivial_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] (g : G) (v : V),
  ((ContRepresentation.trivial R G V) g) v = v
-- Mathlib.Data.PEquiv
PEquiv.single_apply : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a : α) (b : β),
  (PEquiv.single a b) a = some b
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The `n`th complete homogeneous symmetric `MvPolynomial σ R`.
It is the sum over all the degree n monomials in `MvPolynomial σ R`.  -/
MvPolynomial.hsymm : (σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → [DecidableEq σ] → ℕ → MvPolynomial σ R
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isNoImplicitLambda : Lean.Syntax → Bool
-- Init.Data.BitVec.Lemmas
BitVec.toInt_signExtend : ∀ {w v : ℕ} (x : BitVec w), (BitVec.signExtend v x).toInt = x.toInt.bmod (2 ^ min v w)
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `U`, the
logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic
derivatives.
 -/
MeromorphicOn.logDeriv_prod_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ i ∈ s, MeromorphicOn (F i) U) →
    (∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) →
      logDeriv (∏ i ∈ s, F i) =ᶠ[Filter.codiscreteWithin U] ∑ i ∈ s, logDeriv (F i)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsLeftUniformAddGroup.toIsTopologicalAddGroup : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : AddGroup G} [self : IsLeftUniformAddGroup G], IsTopologicalAddGroup G
-- Mathlib.Tactic.DefEqTransformations
/-- Check to see if there's an argument at some index `i`
such that it's the `i`th projection of a some expression.
Returns the expression.  -/
_private.Mathlib.Tactic.DefEqTransformations.0.Mathlib.Tactic.etaStruct?.findProj : Lean.ConstructorVal → Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM (Lean.LOption Lean.Expr)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_comp_C : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.constantCoeff.comp PowerSeries.C = RingHom.id R